Provedalphabaguettebaguette-zv2

The projection part of RMSNorm's backward is a contraction: ‖v − z·mean(v⊙z)‖ ≤ ‖v‖

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=5}{v, z : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ and $\htmlData{mx=4}{\sum_{i} \htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{z}(\htmlData{mx=1}{i})}^{2}}} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{n}$ , then

\htmlData{mx=19}{\sum_{k} \htmlData{mx=18}{\left(\htmlData{mx=17}{\htmlData{mx=2}{\htmlData{mx=0}{v}(\htmlData{mx=1}{k})} - \htmlData{mx=16}{\htmlData{mx=5}{\htmlData{mx=3}{z}(\htmlData{mx=4}{k})} \cdot \left(\htmlData{mx=15}{\frac{\htmlData{mx=13}{\sum_{i} \htmlData{mx=12}{\htmlData{mx=8}{\htmlData{mx=6}{v}(\htmlData{mx=7}{i})} \cdot \htmlData{mx=11}{\htmlData{mx=9}{z}(\htmlData{mx=10}{i})}}}}{\htmlData{mx=14}{n}}}\right)}}\right)^{2}}} \mathrel{\htmlData{mx=25}{\leq}} \htmlData{mx=24}{\sum_{k} \htmlData{mx=23}{\htmlData{mx=22}{\htmlData{mx=20}{v}(\htmlData{mx=21}{k})}^{2}}}

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)
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: v, z range over Fin n → ℝ: the statement must hold for every choice. ((v z : Fin n → ℝ))
∑Summation: Add up z(i)^2 for every i. (∑ i, z i ^ 2)
≤At most: ∑ i, z(i)^2 is less than or equal to n. (∑ i, z i ^ 2 ≤ n)
aᵇPower: z(i) raised to the power 2. (z i ^ 2)
-Subtraction: v(k) minus z(k) · ((∑ i, v(i) · z(i))/n). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (v k - z k * ((∑ i, v i * z i) / n))
RReal numbers: The real numbers: every point on the number line. (ℝ)
a/bDivision: ∑ i, v(i) · z(i) divided by n. In Lean, dividing by 0 gives 0. ((∑ i, v i * z i) / n)
·Multiplication: v(i) times z(i). (v i * z i)

theorem bz2-rmsnorm-pullback-contraction {n : ℕ} (hn : 0 < n) (v z : Fin n → ℝ) (hz : ∑ i, z i ^ 2 ≤ n) :
    ∑ k, (v k - z k * ((∑ i, v i * z i) / n)) ^ 2 ≤ ∑ k, v k ^ 2

When ‖z‖² ≤ n (true for RMSNorm outputs), v ↦ v − z·(v·z)/n never increases the Euclidean norm. The only amplification in RMSNorm's input cotangent is the scalar r. 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: 24 lines of Lean

The projection part of RMSNorm's backward is a contraction: ‖v − z·mean(v⊙z)‖ ≤ ‖v‖

How it was proved

More proved statements