Proof of `Rounding loses at most one weight unit per vertex` (1st statement)
groundedproofs/Lax263307Proofs/RoundingBounds.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
Floor rounding bounds each original vertex weight between its rounded weight and one further scaling unit.
Proof strategy
Apply the lower and upper floor inequalities to and multiply by the positive scaling unit.
Attribution
Bonnet–Chang, proof of Theorem 2 in Section 6.