Provedalphabaguettebaguette-zquantizer
Quantizing commutes with adding grid values: Q(x + m/2ᵏ) = Q(x) + m
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. (
ℕ) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ZIntegers
- The integers …, −2, −1, 0, 1, 2, …. (
ℤ) - ⌊x⌋Floor
- The largest integer not above (x + m/2^k) · 2^k. (
⌊(x + (m : ℝ) / 2 ^ k) * 2 ^ k⌋) - =Equality
- ⌊(x + m/2^k) · 2^k⌋ and ⌊x · 2^k⌋ + m are the same. (
⌊(x + (m : ℝ) / 2 ^ k) * 2 ^ k⌋ = ⌊x * …) - ·Multiplication
- x + m/2^k times 2^k. (
(x + (m : ℝ) / 2 ^ k) * 2 ^ k) - +Addition
- x plus m/2^k. (
x + (m : ℝ) / 2 ^ k) - (x : T)As real numbers
- m read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(m : ℝ)) - a/bDivision
- m divided by 2^k. In Lean, dividing by 0 gives 0. (
(m : ℝ) / 2 ^ k) - aᵇPower
- 2 raised to the power k. (
2 ^ k)
theorem bz-dyadic-shift-equivariant (k : ℕ) (x : ℝ) (m : ℤ) :
⌊(x + (m : ℝ) / 2 ^ k) * 2 ^ k⌋ = ⌊x * 2 ^ k⌋ + mAdding an exact grid value before or after quantization gives the same code. This is why integer residual adds of already-quantized increments never round. 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
- 13 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.