Provedalphabaguettebaguette-zv2
Grid moments keep relative precision 1/M once v ≥ M·2⁻ᵏ
For all and , if and , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- v, M range over real numbers: the statement must hold for every choice. (
(v M : ℝ)) - <Less than
- 0 is strictly smaller than M. (
0 < M) - a/bDivision
- M divided by 2^k. In Lean, dividing by 0 gives 0. (
M / 2 ^ k) - ≤At most
- M/2^k is less than or equal to v. (
M / 2 ^ k ≤ v) - |x|Absolute value
- The size of v − ⌊v · 2^k⌋/2^k without its sign. (
|v - (⌊v * 2 ^ k⌋ : ℝ) / 2 ^ k|) - -Subtraction
- v minus ⌊v · 2^k⌋/2^k. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
v - (⌊v * 2 ^ k⌋ : ℝ) / 2 ^ k) - aᵇPower
- 2 raised to the power k. (
2 ^ k) - (x : T)As real numbers
- ⌊v · 2^k⌋ read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(⌊v * 2 ^ k⌋ : ℝ)) - ⌊x⌋Floor
- The largest integer not above v · 2^k. (
⌊v * 2 ^ k⌋) - ·Multiplication
- v times 2^k. (
v * 2 ^ k)
theorem bz2-moment-resolution (k : ℕ) (v M : ℝ) (hM : 0 < M) (hv : M / 2 ^ k ≤ v) :
|v - (⌊v * 2 ^ k⌋ : ℝ) / 2 ^ k| ≤ v / MThe real hazard of integer optimizer state is underflow, not overflow (review S6): a moment v stored on grid 2⁻ᵏ has relative error ≤ 1/M whenever v ≥ M·2⁻ᵏ. Typical second moments ~10⁻¹² need k ≈ 60 for M ≈ 10⁶. Part of 'Baguette-Z v2' (revision after the hostile review).
How it was proved
- Proved
- 3 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 24 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.