proofs
Provedalphabaguettebaguette-zv2

The original 2⁻⁴⁴ grid really overflowed: a certified-range row's Σx² reaches ≥ 2¹²⁷

2127≤∑_i:Fin⁡ 576(161⋅254)2\htmlData{mx=1}{\htmlData{mx=0}{2}^{127}} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\sum_{\mathit{\_i} : \htmlData{mx=3}{\htmlData{mx=2}{\operatorname{Fin}}\,576}} \htmlData{mx=7}{(\htmlData{mx=6}{\htmlData{mx=4}{161} \cdot \htmlData{mx=5}{2^{54}}})^{2}}}
What the notation means · or point at any symbol
(x : T)As integers
2 read as an element of integers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((2:ℤ))
aᵇPower
2 raised to the power 127. ((2:ℤ) ^ 127)
≤At most
2^127 is less than or equal to ∑ _i, (161 · 2^54)^2. ((2:ℤ) ^ 127 ≤ ∑ _i : Fin 576, ((161:ℤ) …)
∑Summation
Add up (161 · 2^54)^2 for every _i in Fin(576). (∑ _i : Fin 576, ((161:ℤ) * 2 ^ 54) ^ 2)
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)
·Multiplication
161 times 2^54. ((161:ℤ) * 2 ^ 54)

Formal record of the review's M5 finding: at the original grid, a row whose 576 codes all sit at the certified maximum 161·2⁵⁴ has Σx² ≥ 2¹²⁷, overflowing int128. The v2 spec uses 2⁻⁴⁰ (see bz2-p2n-accumulator-headroom). 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
13 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements