Proof of `Rounding loses at most one weight unit per vertex` (2nd statement)
groundedproofs/Lax263307Proofs/RoundingBounds.lean · lax-263307
What this proof establishes
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 total weight lost by rounding a set is at most one scaling unit per selected vertex.
Proof strategy
Sum the pointwise lower bounds and collect the constant scaling units.
Attribution
Bonnet–Chang, proof of Theorem 2 in Section 6.