Provedalphabaguettebaguette-zp2norm
After the power-of-two shift the energy lies in [1, 4)
For all , 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. (
ℕ) - ≠Not equal
- S and 0 are different. (
S ≠ 0) - (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:ℝ)) - ≤At most
- 1 is less than or equal to S/4^(log(2, S)/2). (
(1:ℝ) ≤ S / 4 ^ (Nat.log 2 S / 2)) - ∧And
- Both hold: 1 ≤ S/4^(log(2, S)/2), and S/4^(log(2, S)/2) < 4. (
(1:ℝ) ≤ S / 4 ^ (Nat.log 2 S / 2) ∧ (S:…) - aᵇPower
- 4 raised to the power log(2, S)/2. (
4 ^ (Nat.log 2 S / 2)) - 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, S. Lean writes f x; papers write f(x). (
Nat.log 2 S) - a/bDivision
- log(2, S) divided by 2. In Lean, dividing by 0 gives 0. (
Nat.log 2 S / 2) - <Less than
- S/4^(log(2, S)/2) is strictly smaller than 4. (
(S:ℝ) / 4 ^ (Nat.log 2 S / 2) < 4)
theorem bz-shifted-energy-bracket (S : ℕ) (hS : S ≠ 0) :
(1:ℝ) ≤ S / 4 ^ (Nat.log 2 S / 2) ∧ (S:ℝ) / 4 ^ (Nat.log 2 S / 2) < 4Real-valued form: 1 ≤ S/4ᵏ < 4 for k = ⌊log₂S/2⌋. RMSNorm's ideal energy is fixed; here it varies only within a factor 4, absorbed by the learned gain. 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
- 30 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.