Proof of `Fresh peeling after restrictions and deliberate extra pins` (1st statement)
groundedproofs/Lax342547Proofs/SecondPeeling.lean · lax-342547
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The ceiling of the new-rank allowance costs less than one extra dimension. For zeta at most one, the paper's final budget absorbs this and all old and deliberately added pins, with uniform slack.