Provedalphabaguettebaguette-zp2norm

After the shift, every coordinate has magnitude below 2 (|xᵢ| < 2^(k+1))

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

\htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{x}(\htmlData{mx=1}{i})} \right\rvert} \mathrel{\htmlData{mx=7}{<}} \htmlData{mx=6}{2^{\htmlData{mx=5}{\htmlData{mx=4}{k} + 1}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
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 → ℤ)
∑Summation: Add up x(i)^2 for every i. (∑ i, x i ^ 2)
<Less than: ∑ i, x(i)^2 is strictly smaller than 4^(k + 1). (∑ i, x i ^ 2 < 4 ^ (k + 1))
|x|Absolute value: The size of x(i) without its sign. (|x i|)
aᵇPower: x(i) raised to the power 2. (x i ^ 2)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (ℤ)
+Addition: k plus 1. (k + 1)

theorem bz-shifted-coordinate-bound {n : ℕ} (x : Fin n → ℤ) (k : ℕ) (hk : ∑ i, x i ^ 2 < 4 ^ (k + 1)) (i : Fin n) :
    |x i| < 2 ^ (k + 1)

If Σ xⱼ² < 4^(k+1) then each |xᵢ| < 2^(k+1), i.e. |xᵢ/2ᵏ| < 2. Normalized sublayer inputs and outputs live in (−2, 2) coordinatewise: a fixed, tiny range for the BF16 operands. 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: 16 lines of Lean

After the shift, every coordinate has magnitude below 2 (|xᵢ| < 2^(k+1))

How it was proved

More proved statements