Proof of `Cumulative separator cost over disjoint discarded shores`
groundedproofs/Lax263307Proofs/RepeatedCutAccounting.lean · lax-263307
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 cost of a union is at most the sum of nonnegative individual costs. Use the per-cut estimate and the original order bound on each left shore. Pairwise disjoint discarded shores have total size at most n; summing and factoring gives the claimed global cost bound.