Provedalphabaguettebaguette-zschedule
Grid accumulation of on-grid values reproduces the exact real sum
For all , and :
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - f(x)Function application
- Fin applied to n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℤ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℤ) - =Equality
- (∑ i, ⌊m(i)/2^k · 2^k⌋)/2^k and ∑ i, m(i)/2^k are the same. (
(∑ i, (⌊((m i : ℝ) / 2 ^ k) * 2 ^ k⌋ : …) - ∑Summation
- Add up ⌊m(i)/2^k · 2^k⌋ for every i. (
∑ i, (⌊((m i : ℝ) / 2 ^ k) * 2 ^ k⌋ : ℝ)) - ⌊x⌋Floor
- The largest integer not above m(i)/2^k · 2^k. (
⌊((m i : ℝ) / 2 ^ k) * 2 ^ k⌋) - ZIntegers
- The integers …, −2, −1, 0, 1, 2, …. (
ℤ) - ·Multiplication
- m(i)/2^k times 2^k. (
((m i : ℝ) / 2 ^ k) * 2 ^ k) - (x : T)As real numbers
- m(i) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(m i : ℝ)) - a/bDivision
- m(i) divided by 2^k. In Lean, dividing by 0 gives 0. (
(m i : ℝ) / 2 ^ k) - aᵇPower
- 2 raised to the power k. (
2 ^ k)
theorem bz-on-grid-sum-exact (k : ℕ) {n : ℕ} (m : Fin n → ℤ) :
(∑ i, (⌊((m i : ℝ) / 2 ^ k) * 2 ^ k⌋ : ℝ)) / 2 ^ k = ∑ i, (m i : ℝ) / 2 ^ kIf every term is already a grid value m/2ᵏ, quantize-and-add has zero error. Part of the plan 'Baguette-Z: closed-loop certified integer-state training'.
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
- 14 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.