Provedalphabaguettebaguette-zoptimizer
For Baguette's β₁ = 0.9, β₂ = 0.999: β₁² < β₂ and C² = 9990/189 < 53
What the notation means · or point at any symbol
- (x : T)As real numbers
- 9/10 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(9 / 10 : ℝ)) - aᵇPower
- 9/10 raised to the power 2. (
(9 / 10 : ℝ) ^ 2) - <Less than
- (9/10)^2 is strictly smaller than 999/1000. (
(9 / 10 : ℝ) ^ 2 < 999 / 1000) - a/bDivision
- 9 divided by 10. In Lean, dividing by 0 gives 0. (
9 / 10) - =Equality
- (1 − 9/10)^2/((1 − 999/1000) · (1 − (9/10)^2/(999/1000))) and 9990/189 are the same. (
(1 - 9 / 10 : ℝ) ^ 2 / ((1 - 999 / 1000…) - ∧And
- Both hold: (1 − 9/10)^2/((1 − 999/1000) · (1 − (9/10)^2/(999/1000))) …, and 9990/189 < 53. (
(1 - 9 / 10 : ℝ) ^ 2 / ((1 - 999 / 1000…) - -Subtraction
- 1 minus 9/10. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - 9 / 10) - ·Multiplication
- 1 − 999/1000 times 1 − (9/10)^2/(999/1000). (
(1 - 999 / 1000) * (1 - (9 / 10) ^ 2 / …)
theorem bz-baguette-adam-constant :
(9 / 10 : ℝ) ^ 2 < 999 / 1000 ∧ (1 - 9 / 10 : ℝ) ^ 2 / ((1 - 999 / 1000) * (1 - (9 / 10) ^ 2 / (999 / 1000))) = 9990 / 189 ∧ (9990 / 189 : ℝ) < 53Instantiates the Adam ratio constant for Baguette's learner (Learner.alpha), so C < 7.3 and the corrected step is at most lr·73. 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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.