Provedalphabaguettebaguette-zquantizer
Dyadic floor quantizer brackets its input: q/2ᵏ ≤ x < (q+1)/2ᵏ
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. (
ℝ) - (x : T)As real numbers
- ⌊x · 2^k⌋ read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(⌊x * 2 ^ k⌋ : ℝ)) - a/bDivision
- ⌊x · 2^k⌋ divided by 2^k. In Lean, dividing by 0 gives 0. (
(⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k) - ≤At most
- ⌊x · 2^k⌋/2^k is less than or equal to x. (
(⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k ≤ x) - ∧And
- Both hold: ⌊x · 2^k⌋/2^k ≤ x, and x < (⌊x · 2^k⌋ + 1)/2^k. (
(⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k ≤ x ∧ x < ((⌊…) - ⌊x⌋Floor
- The largest integer not above x · 2^k. (
⌊x * 2 ^ k⌋) - ·Multiplication
- x times 2^k. (
x * 2 ^ k) - aᵇPower
- 2 raised to the power k. (
2 ^ k) - <Less than
- x is strictly smaller than (⌊x · 2^k⌋ + 1)/2^k. (
x < ((⌊x * 2 ^ k⌋ : ℝ) + 1) / 2 ^ k) - +Addition
- ⌊x · 2^k⌋ plus 1. (
(⌊x * 2 ^ k⌋ : ℝ) + 1)
theorem bz-dyadic-floor-bracket (k : ℕ) (x : ℝ) :
(⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k ≤ x ∧ x < ((⌊x * 2 ^ k⌋ : ℝ) + 1) / 2 ^ kQ(x) = ⌊x·2ᵏ⌋ is the integer code of x on the grid 2⁻ᵏ. Every Baguette-Z integer state (residual stream, master weights, moments) is stored this way. 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
- 17 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.