Provedalphabaguettebaguette-zp2norm
Power-of-two normalization is exactly invariant to power-of-two input scaling
For all and , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- S, j range over natural numbers: the statement must hold for every choice. (
(S j : ℕ)) - ≠Not equal
- S and 0 are different. (
S ≠ 0) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - =Equality
- 2^j · x/2^(log(2, 4^j · S)/2) and x/2^(log(2, S)/2) are the same. (
(2 ^ j * x) / 2 ^ (Nat.log 2 (4 ^ j * S…) - aᵇPower
- 2 raised to the power j. (
2 ^ j) - ·Multiplication
- 2^j times x. (
2 ^ j * x) - log
- Nat.log: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Nat.log) - f(x)Function application
- Nat.log applied to 2, 4^j · S. Lean writes f x; papers write f(x). (
Nat.log 2 (4 ^ j * S)) - a/bDivision
- log(2, 4^j · S) divided by 2. In Lean, dividing by 0 gives 0. (
Nat.log 2 (4 ^ j * S) / 2)
theorem bz-power-of-two-input-invariance (S j : ℕ) (hS : S ≠ 0) (x : ℝ) :
(2 ^ j * x) / 2 ^ (Nat.log 2 (4 ^ j * S) / 2) = x / 2 ^ (Nat.log 2 S / 2)If the input row is scaled by 2ʲ (energy scaled by 4ʲ), the normalized value 2ʲx / 2^k(4ʲS) equals x / 2^k(S), with no error at all. RMSNorm only has this up to ε and rounding. 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
- 28 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.