Provedalphabaguettebaguette-zv2

P2N = c·(x/‖x‖) with a PER-TOKEN factor c ∈ [1, 2): the jitter cannot be absorbed by a per-channel gain

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{R}}}$ and $\htmlData{mx=1}{S \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=0}{S} \mathrel{\htmlData{mx=1}{\neq}} 0$ , then

\begin{aligned} & \htmlData{mx=0}{\exists} c \in \htmlData{mx=1}{\mathbb{R}}, \\ & \quad 1 \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{c} \\ & \quad \htmlData{mx=2}{\land} \htmlData{mx=5}{c} \mathrel{\htmlData{mx=6}{<}} 2 \\ & \quad \htmlData{mx=2}{\land} \htmlData{mx=25}{\forall i,\ \htmlData{mx=15}{\frac{\htmlData{mx=9}{\htmlData{mx=7}{x}(\htmlData{mx=8}{i})}}{\htmlData{mx=14}{2^{\htmlData{mx=13}{\frac{\htmlData{mx=12}{\htmlData{mx=10}{\operatorname{log}}(2, \htmlData{mx=11}{S})}}{2}}}}}} \mathrel{\htmlData{mx=24}{=}} \htmlData{mx=23}{\htmlData{mx=16}{c} \cdot \left(\htmlData{mx=22}{\frac{\htmlData{mx=19}{\htmlData{mx=17}{x}(\htmlData{mx=18}{i})}}{\htmlData{mx=21}{\sqrt{\htmlData{mx=20}{S}}}}}\right)}} \end{aligned}

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 → ℝ)
≠Not equal: S and 0 are different. (S ≠ 0)
∃There exists: At least one c makes the statement after the comma true. (∃ c : ℝ, 1 ≤ c ∧ c < 2 ∧ ∀ i, x i / 2 ^…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 1 is less than or equal to c. (1 ≤ c)
<Less than: c is strictly smaller than 2. (c < 2)
∧And: Both hold: c < 2, and ∀ i, x(i)/2^(log(2, S)/2) = c · (x(i)/√(S)). (c < 2 ∧ ∀ i, x i / 2 ^ (Nat.log 2 S / 2…)
∀For all: The statement after the comma holds for every i. (∀ i, x i / 2 ^ (Nat.log 2 S / 2) = c * …)
=Equality: x(i)/2^(log(2, S)/2) and c · (x(i)/√(S)) are the same. (x i / 2 ^ (Nat.log 2 S / 2) = c * (x i …)
aᵇPower: 2 raised to the power log(2, S)/2. (2 ^ (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)
a/bDivision: log(2, S) divided by 2. In Lean, dividing by 0 gives 0. (Nat.log 2 S / 2)
·Multiplication: c times x(i)/√(S). (c * (x i / Real.sqrt S))
√Square root: The non-negative number whose square is S. (Real.sqrt S)

theorem bz2-p2n-is-jittered-unit-normalization {n : ℕ} (x : Fin n → ℝ) (S : ℕ) (hS0 : S ≠ 0) :
    ∃ c : ℝ, 1 ≤ c ∧ c < 2 ∧ ∀ i, x i / 2 ^ (Nat.log 2 S / 2) = c * (x i / Real.sqrt S)

Corrects the false claim that the learned gain absorbs P2N's slack. For a row whose energy is S = Σxᵢ² (any S ≠ 0; the identity is per row), P2N divides by 2ᵏ (k = ⌊log₂S/2⌋), which equals c·xᵢ/√S with c = √S/2ᵏ ∈ [1, 2). c depends on the row (token), so P2N is unit normalization times a token-dependent factor of up to 2×, which a per-channel gain cannot cancel. 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: 56 lines of Lean

P2N = c·(x/‖x‖) with a PER-TOKEN factor c ∈ [1, 2): the jitter cannot be absorbed by a per-channel gain

How it was proved

More proved statements