Provedalphabaguettebaguette-zv2

Fixed: at a 2⁻⁴⁰ residual grid, P2N's Σx² fits int128 and the residual fits int64

For all $\htmlData{mx=4}{q : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Fin}}\,576} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{Z}}}$ , if $\htmlData{mx=7}{\forall i,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{q}(\htmlData{mx=1}{i})} \right\rvert} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{161 \cdot \htmlData{mx=4}{2^{50}}}}$ , then

\htmlData{mx=4}{\sum_{i} \htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{q}(\htmlData{mx=1}{i})}^{2}}} \mathrel{\htmlData{mx=6}{<}} \htmlData{mx=5}{2^{127}} \mathbin{\htmlData{mx=12}{\land}} \htmlData{mx=9}{\htmlData{mx=7}{161} \cdot \htmlData{mx=8}{2^{50}}} \mathrel{\htmlData{mx=11}{<}} \htmlData{mx=10}{2^{63}}

What the notation means · or point at any symbol

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 576. Lean writes f x; papers write f(x). (Fin 576)
⟹Implies: If Fin(576), then ℤ. (Between types, A → B is the type of functions from A to B.) (Fin 576 → ℤ)
∀For all: The statement after the comma holds for every i. (∀ i, |q i| ≤ 161 * 2 ^ 50)
∑Summation: Add up q(i)^2 for every i. (∑ i, q i ^ 2)
<Less than: ∑ i, q(i)^2 is strictly smaller than 2^127. (∑ i, q i ^ 2 < 2 ^ 127)
∧And: Both hold: (∑ i, q(i)^2) < 2^127, and 161 · 2^50 < 2^63. (∑ i, q i ^ 2 < 2 ^ 127 ∧ (161 : ℤ) * 2 …)
|x|Absolute value: The size of q(i) without its sign. (|q i|)
≤At most: |q(i)| is less than or equal to 161 · 2^50. (|q i| ≤ 161 * 2 ^ 50)
ZIntegers: The integers …, −2, −1, 0, 1, 2, …. (ℤ)
·Multiplication: 161 times 2^50. (161 * 2 ^ 50)
aᵇPower: 2 raised to the power 50. (2 ^ 50)
(x : T)As integers: 161 read as an element of integers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((161 : ℤ))

theorem bz2-p2n-accumulator-headroom (q : Fin 576 → ℤ) (hq : ∀ i, |q i| ≤ 161 * 2 ^ 50) :
    ∑ i, q i ^ 2 < 2 ^ 127 ∧ (161 : ℤ) * 2 ^ 50 < 2 ^ 63

Repairs the arithmetic error found in review (M5). With the certified residual bound |x| ≤ 161·2¹⁰, codes at a 2⁻⁴⁰ grid are ≤ 161·2⁵⁰. Their 576-term sum of squares is < 2¹²⁷ (fits int128), and the codes themselves are < 2⁶³ (fit int64). Resolution 2⁻⁴⁰ ≈ 9·10⁻¹³ remains far below BF16 noise. 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: 20 lines of Lean

Fixed: at a 2⁻⁴⁰ residual grid, P2N's Σx² fits int128 and the residual fits int64

How it was proved

More proved statements