Provedalphabaguettebaguette-zrange

Baguette-Z widths: 80 blocks with gains ≤ 2¹⁰ fit int64 with 44 fractional bits, int32 with 13

For all $\htmlData{mx=1}{G, x_{0} \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=0}{G} \mathrel{\htmlData{mx=2}{\leq}} \htmlData{mx=1}{2^{10}}$ and $\htmlData{mx=1}{\left\lvert \htmlData{mx=0}{x_{0}} \right\rvert} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{2^{10}}$ , then

\begin{aligned} & \htmlData{mx=8}{(\htmlData{mx=6}{\htmlData{mx=2}{\left\lvert \htmlData{mx=1}{x_{0}} \right\rvert} + \htmlData{mx=5}{80(\htmlData{mx=4}{2\htmlData{mx=3}{G}})}}) \cdot \htmlData{mx=7}{2^{44}}} \mathrel{\htmlData{mx=10}{<}} \htmlData{mx=9}{2^{63}} \\ & \htmlData{mx=0}{\land} \htmlData{mx=18}{(\htmlData{mx=16}{\htmlData{mx=12}{\left\lvert \htmlData{mx=11}{x_{0}} \right\rvert} + \htmlData{mx=15}{80(\htmlData{mx=14}{2\htmlData{mx=13}{G}})}}) \cdot \htmlData{mx=17}{2^{13}}} \mathrel{\htmlData{mx=20}{<}} \htmlData{mx=19}{2^{31}} \end{aligned}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: G, x0 range over real numbers: the statement must hold for every choice. ((G x0 : ℝ))
≤At most: G is less than or equal to 2^10. (G ≤ 2 ^ 10)
|x|Absolute value: The size of x0 without its sign. (|x0|)
<Less than: (|x0| + 80 · (2 · G)) · 2^44 is strictly smaller than 2^63. ((|x0| + 80 * (2 * G)) * 2 ^ 44 < 2 ^ 63)
∧And: Both hold: (|x0| + 80 · (2 · G)) · 2^44 < 2^63, and (|x0| + 80 · (2 · G)) · 2^13 < 2^31. ((|x0| + 80 * (2 * G)) * 2 ^ 44 < 2 ^ 63…)
+Addition: |x0| plus 80 · (2 · G). (|x0| + 80 * (2 * G))
aᵇPower: 2 raised to the power 10. (2 ^ 10)
·Multiplication: 2 times G. (2 * G)

theorem bz-baguette-width-certificate (G x0 : ℝ) (hG : G ≤ 2 ^ 10) (hx0 : |x0| ≤ 2 ^ 10) :
    (|x0| + 80 * (2 * G)) * 2 ^ 44 < 2 ^ 63 ∧ (|x0| + 80 * (2 * G)) * 2 ^ 13 < 2 ^ 31

With embedding coordinates ≤ 2¹⁰ and per-layer increments ≤ 2·2¹⁰ (gained normalized outputs, gains in the AdamW box ≤ 730 < 2¹⁰), the residual stays below 161·2¹⁰ < 2¹⁸. That fits int64 at 2⁻⁴⁴ resolution and int32 at 2⁻¹³. 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: 19 lines of Lean

Baguette-Z widths: 80 blocks with gains ≤ 2¹⁰ fit int64 with 44 fractional bits, int32 with 13

How it was proved

More proved statements