Provedalphabaguettebaguette-zquantizer

Values already on the grid are stored exactly: Q(m/2ᵏ) = m

For all $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{Z}}}$ :

\htmlData{mx=8}{\left\lfloor \htmlData{mx=7}{\htmlData{mx=4}{\frac{\htmlData{mx=1}{\htmlData{mx=0}{m}}}{\htmlData{mx=3}{2^{\htmlData{mx=2}{k}}}}} \cdot \htmlData{mx=6}{2^{\htmlData{mx=5}{k}}}} \right\rfloor} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{m}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (ℤ)
⌊x⌋Floor: The largest integer not above m/2^k · 2^k. (⌊((m : ℝ) / 2 ^ k) * 2 ^ k⌋)
=Equality: ⌊m/2^k · 2^k⌋ and m are the same. (⌊((m : ℝ) / 2 ^ k) * 2 ^ k⌋ = m)
·Multiplication: m/2^k times 2^k. (((m : ℝ) / 2 ^ k) * 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-grid-fixed-point (k : ℕ) (m : ℤ) :
    ⌊((m : ℝ) / 2 ^ k) * 2 ^ k⌋ = m

Re-quantizing a grid value is the identity, so integer state round-trips through the real-valued view without loss. 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

Values already on the grid are stored exactly: Q(m/2ᵏ) = m

How it was proved

More proved statements