Provedalphabaguettebaguette-zquantizer
The dyadic quantizer's error is below one grid step 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|Absolute value
- The size of x − ⌊x · 2^k⌋/2^k without its sign. (
|x - (⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k|) - <Less than
- |x − ⌊x · 2^k⌋/2^k| is strictly smaller than 1/2^k. (
|x - (⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k| < 1 / 2…) - -Subtraction
- x minus ⌊x · 2^k⌋/2^k. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
x - (⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k) - (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) - ⌊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)
theorem bz-dyadic-floor-error (k : ℕ) (x : ℝ) :
|x - (⌊x * 2 ^ k⌋ : ℝ) / 2 ^ k| < 1 / 2 ^ k|x − ⌊x·2ᵏ⌋/2ᵏ| < 2⁻ᵏ: storing a value on the grid costs less than one unit in the last place. 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
- 18 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.