Provedalphabaguettealgorithm-ideac8

Power-of-two normalization: some scale 2ᵏ puts ‖x/2ᵏ‖² in [n/2, 2n)

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=5}{x : \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 $0 \mathrel{\htmlData{mx=5}{<}} \htmlData{mx=4}{\sum_{i} \htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{x}(\htmlData{mx=1}{i})}^{2}}}$ , then

\htmlData{mx=27}{\exists k \in \htmlData{mx=26}{\mathbb{Z}},\ \htmlData{mx=2}{\frac{\htmlData{mx=1}{\htmlData{mx=0}{n}}}{2}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\sum_{i} \htmlData{mx=10}{\left(\htmlData{mx=9}{\frac{\htmlData{mx=5}{\htmlData{mx=3}{x}(\htmlData{mx=4}{i})}}{\htmlData{mx=8}{\htmlData{mx=6}{2}^{\htmlData{mx=7}{k}}}}}\right)^{2}}} \mathbin{\htmlData{mx=25}{\land}} \htmlData{mx=21}{\sum_{i} \htmlData{mx=20}{\left(\htmlData{mx=19}{\frac{\htmlData{mx=15}{\htmlData{mx=13}{x}(\htmlData{mx=14}{i})}}{\htmlData{mx=18}{\htmlData{mx=16}{2}^{\htmlData{mx=17}{k}}}}}\right)^{2}}} \mathrel{\htmlData{mx=24}{<}} \htmlData{mx=23}{2\htmlData{mx=22}{n}}}

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 → ℝ)
∃There exists: At least one k makes the statement after the comma true. (∃ k : ℤ, (n : ℝ) / 2 ≤ ∑ i, (x i / (2:ℝ…)
∑Summation: Add up x(i)^2 for every i. (∑ i, x i ^ 2)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (ℤ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
aᵇPower: x(i) raised to the power 2. (x i ^ 2)
(x : T)As real numbers: n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((n : ℝ))
a/bDivision: n divided by 2. In Lean, dividing by 0 gives 0. ((n : ℝ) / 2)
≤At most: n/2 is less than or equal to ∑ i, (x(i)/2^k)^2. ((n : ℝ) / 2 ≤ ∑ i, (x i / (2:ℝ) ^ k) ^ 2)
∧And: Both hold: n/2 ≤ (∑ i, (x(i)/2^k)^2), and (∑ i, (x(i)/2^k)^2) < 2 · n. ((n : ℝ) / 2 ≤ ∑ i, (x i / (2:ℝ) ^ k) ^ …)
·Multiplication: 2 times n. (2 * n)

theorem p2n-energy-bracket (n : ℕ) (hn : 0 < n) (x : Fin n → ℝ) (hS : 0 < ∑ i, x i ^ 2) :
    ∃ k : ℤ, (n : ℝ) / 2 ≤ ∑ i, (x i / (2:ℝ) ^ k) ^ 2 ∧ ∑ i, (x i / (2:ℝ) ^ k) ^ 2 < 2 * n

Idea C8 (power-of-two RMSNorm). For any nonzero row x of width n there is an integer k such that dividing by 2ᵏ (an exponent-field change, exact in floating point barring under/overflow) gives n/2 ≤ ‖x/2ᵏ‖² < 2n. RMSNorm gives energy just below n; this keeps it within a factor 2 with no square root, division, or rounding in the scaling.

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: 35 lines of Lean

Power-of-two normalization: some scale 2ᵏ puts ‖x/2ᵏ‖² in [n/2, 2n)

How it was proved

More proved statements