Proof of `Geometric contraction with an additive rounding error`
groundedproofs/Lax235315Proofs/Contraction.lean · lax-235315
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 additive rounding error remains bounded by twice its per-round value after any number of halvings.
Proof strategy
Induct on the number of rounds. Monotonicity of natural division propagates the inductive bound through the next halving; the exact quotient identity for adding a multiple of two absorbs the new error term.
Attribution
The induction and quotient calculation adapt the arithmetic argument in , specialized to the single-sequence statement here.