Provedalphabaguettebaguette-zrange

A gained, power-of-two-normalized increment is bounded by 2|gain|

For all $\htmlData{mx=1}{g, z \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=1}{\left\lvert \htmlData{mx=0}{z} \right\rvert} \mathrel{\htmlData{mx=2}{<}} 2$ , then

\htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{g} \cdot \htmlData{mx=1}{z}} \right\rvert} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{2 \cdot \htmlData{mx=5}{\left\lvert \htmlData{mx=4}{g} \right\rvert}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: g, z range over real numbers: the statement must hold for every choice. ((g z : ℝ))
|x|Absolute value: The size of z without its sign. (|z|)
<Less than: |z| is strictly smaller than 2. (|z| < 2)
≤At most: |g · z| is less than or equal to 2 · |g|. (|g * z| ≤ 2 * |g|)
·Multiplication: g times z. (g * z)

theorem bz-gained-increment-bound (g z : ℝ) (hz : |z| < 2) :
    |g * z| ≤ 2 * |g|

If |z| < 2 (power-of-two normalization of the sublayer output) then |g·z| ≤ 2|g|. The residual increment per layer is bounded by twice the output gain. 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: 13 lines of Lean

A gained, power-of-two-normalized increment is bounded by 2|gain|

How it was proved

More proved statements