Provedalphabaguettebaguette-zoptimizer
Baguette's master weights stay within max(|θ₀|, 730) for an unbounded run
For all , if and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to C. (
0 ≤ C) - aᵇPower
- C raised to the power 2. (
C ^ 2) - <Less than
- C^2 is strictly smaller than 53. (
C ^ 2 < 53) - ∧And
- Both hold: C/(1 − 9/10)/(1/10) < 730, and 730 < 2^10. (
C / (1 - 9 / 10) / (1 / 10) < 730 ∧ (73…) - -Subtraction
- 1 minus 9/10. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - 9 / 10) - a/bDivision
- 9 divided by 10. In Lean, dividing by 0 gives 0. (
9 / 10) - (x : T)As real numbers
- 730 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(730 : ℝ))
theorem bz-baguette-weight-box (C : ℝ) (hC0 : 0 ≤ C) (hC : C ^ 2 < 53) :
C / (1 - 9 / 10) / (1 / 10) < 730 ∧ (730 : ℝ) < 2 ^ 10With per-step direction ≤ C/(1−β₁) < 73 (C < 7.3) and decay a = lr·0.1, the uniform box radius ηK/a = K/0.1 is below 730. Every master weight, gain and embedding coordinate of Baguette-Z fits in 10 integer bits for all time. 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
- 16 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.