Proof of `Polynomial order bound from the sampled width inequality`
groundedproofs/Lax263307Proofs/WidthGrowth.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
Cancel positive ell from the removed-edge bound. Combine it with the linear source width inequality to bound t by 12c times W. Raise this to the a-th power, substitute the class power bound and the host edge bound, then cancel the positive factor t^(a-1).