Provedalphabaguettebaguette-zv2
Baguette's RMSNorm amplification ceiling is 1/√ε = 100√10 ≈ 316 per normalization
What the notation means · or point at any symbol
- (x : T)As real numbers
- 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 : ℝ)) - =Equality
- 1/(1/100000) and 100000 are the same. (
(1 : ℝ) / (1 / 100000) = 100000) - a/bDivision
- 1 divided by 100000. In Lean, dividing by 0 gives 0. (
1 / 100000) - aᵇPower
- 316 raised to the power 2. (
(316 : ℝ) ^ 2) - <Less than
- 316^2 is strictly smaller than 100000. (
(316 : ℝ) ^ 2 < 100000) - ∧And
- Both hold: 316^2 < 100000, and 100000 < 317^2. (
(316 : ℝ) ^ 2 < 100000 ∧ (100000 : ℝ) <…)
theorem bz2-baguette-epsilon-ceiling :
(1 : ℝ) / (1 / 100000) = 100000 ∧ (316 : ℝ) ^ 2 < 100000 ∧ (100000 : ℝ) < 317 ^ 2Instantiates the gradient-amplification bound at Baguette's ε = 1e-5: 1/ε = 100000, and 316² < 100000 < 317², so the per-norm cotangent gain ceiling lies in (316, 317). With 160 normalizations on the residual path's branches, the worst case is a product of such factors, which is why certified gradient ranges are vacuous without data and why clipping remains necessary. Part of 'Baguette-Z v2' (revision after the hostile review).
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.