Provedalphabaguettermsnormbackward
Alpha's RMSNorm input pullback r·(v − z·mean(v⊙z)) is the exact derivative of v·RMSNorm_ε
For all , and , if and , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - <Less than
- 0 is strictly smaller than n. (
0 < n) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - f(x)Function application
- Fin applied to n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℝ) - x : TVariables
- x, h, v range over Fin n → ℝ: the statement must hold for every choice. (
(x h v : Fin n → ℝ)) - HasDerivAt
- HasDerivAt: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
HasDerivAt) - x ↦ f(x)Function (λ-abstraction)
- The function sending t to ∑ i, v(i) · ((x(i) + t · h(i))/√((∑ j, (x(j) + t · h(j))^2…. Lean writes fun x => …; papers write x ↦ …. (
fun t : ℝ => ∑ i, v i * ((x i + t * h i…) - +Addition
- x(i) plus t · h(i). (
x i + t * h i) - ·Multiplication
- t times h(i). (
t * h i) - √Square root
- The non-negative number whose square is (∑ j, (x(j) + t · h(j))^2)/n + ε. (
Real.sqrt ((∑ j, (x j + t * h j) ^ 2) /…) - a/bDivision
- ∑ j, (x(j) + t · h(j))^2 divided by n. In Lean, dividing by 0 gives 0. (
(∑ j, (x j + t * h j) ^ 2) / n) - ∑Summation
- Add up (x(j) + t · h(j))^2 for every j. (
∑ j, (x j + t * h j) ^ 2) - aᵇPower
- x(j) + t · h(j) raised to the power 2. (
(x j + t * h j) ^ 2) - -Subtraction
- v(k) minus x(k)/√((∑ j, x(j)^2)/n + ε) · ((∑ i, v(i) · (x(i)/√((∑ j, …. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
v k - x k / Real.sqrt ((∑ j, x j ^ 2) /…)
theorem rmsnorm-pullback-is-derivative (n : ℕ) (hn : 0 < n) (ε : ℝ) (hε : 0 < ε) (x h v : Fin n → ℝ) :
HasDerivAt (fun t : ℝ => ∑ i, v i * ((x i + t * h i) / Real.sqrt ((∑ j, (x j + t * h j) ^ 2) / n + ε))) (∑ k, h k * (1 / Real.sqrt ((∑ j, x j ^ 2) / n + ε) * (v k - x k / Real.sqrt ((∑ j, x j ^ 2) / n + ε) * ((∑ i, v i * (x i / Real.sqrt ((∑ j, x j ^ 2) / n + ε))) / n)))) 0Component.MeanSquareNormalization.propagateMeanSquareInputWith computes, for z = r·x, r = (Σx²/n + ε)^(-1/2) and v = dy ⊙ gain, the input cotangent dx = r·(v − z·mean(v⊙z)). Its comment says this is "the real analytic VJP". This theorem proves it over ℝ: along any direction h, the derivative at 0 of t ↦ ⟨v, RMSNorm_ε(x + t·h)⟩ equals ⟨h, dx⟩. ε stays in r, as the source requires; an ε-free shortcut would change the derivative.
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
- 66 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.