Provedalphabaguettebaguette-zcapstone

Baguette's actual moment banks satisfy m(t)² ≤ C²·v(t) at every step

For all $\htmlData{mx=3}{g, m, v : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{\beta_{1}, \beta_{2} \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\beta_{2}}$ , $\htmlData{mx=0}{\beta_{2}} \mathrel{\htmlData{mx=1}{<}} 1$ , $\htmlData{mx=1}{\htmlData{mx=0}{\beta_{1}}^{2}} \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\beta_{2}}$ , $\htmlData{mx=1}{\htmlData{mx=0}{m}(0)} \mathrel{\htmlData{mx=2}{=}} 0$ , $\htmlData{mx=1}{\htmlData{mx=0}{v}(0)} \mathrel{\htmlData{mx=2}{=}} 0$ , $\htmlData{mx=17}{\forall t,\ \htmlData{mx=3}{\htmlData{mx=0}{m}(\htmlData{mx=2}{\htmlData{mx=1}{t} + 1})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=8}{\htmlData{mx=4}{\beta_{1}} \cdot \htmlData{mx=7}{\htmlData{mx=5}{m}(\htmlData{mx=6}{t})}} + \htmlData{mx=14}{(\htmlData{mx=10}{1 - \htmlData{mx=9}{\beta_{1}}}) \cdot \htmlData{mx=13}{\htmlData{mx=11}{g}(\htmlData{mx=12}{t})}}}}$ and $\htmlData{mx=18}{\forall t,\ \htmlData{mx=3}{\htmlData{mx=0}{v}(\htmlData{mx=2}{\htmlData{mx=1}{t} + 1})} \mathrel{\htmlData{mx=17}{=}} \htmlData{mx=16}{\htmlData{mx=8}{\htmlData{mx=4}{\beta_{2}} \cdot \htmlData{mx=7}{\htmlData{mx=5}{v}(\htmlData{mx=6}{t})}} + \htmlData{mx=15}{(\htmlData{mx=10}{1 - \htmlData{mx=9}{\beta_{2}}}) \cdot \htmlData{mx=14}{\htmlData{mx=13}{\htmlData{mx=11}{g}(\htmlData{mx=12}{t})}^{2}}}}}$ , then

\htmlData{mx=21}{\forall t,\ \htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{m}(\htmlData{mx=1}{t})}^{2}} \mathrel{\htmlData{mx=20}{\leq}} \htmlData{mx=19}{\htmlData{mx=15}{\frac{\htmlData{mx=6}{(\htmlData{mx=5}{1 - \htmlData{mx=4}{\beta_{1}}})^{2}}}{\htmlData{mx=14}{(\htmlData{mx=8}{1 - \htmlData{mx=7}{\beta_{2}}}) \cdot \left(\htmlData{mx=13}{1 - \htmlData{mx=12}{\frac{\htmlData{mx=10}{\htmlData{mx=9}{\beta_{1}}^{2}}}{\htmlData{mx=11}{\beta_{2}}}}}\right)}}} \cdot \htmlData{mx=18}{\htmlData{mx=16}{v}(\htmlData{mx=17}{t})}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
x : TVariables: g, m, v range over ℕ → ℝ: the statement must hold for every choice. ((g m v : ℕ → ℝ))
x ∈ TVariables: β₁, β₂ range over real numbers: the statement must hold for every choice. ((β₁ β₂ : ℝ))
<Less than: 0 is strictly smaller than β₂. (0 < β₂)
aᵇPower: β₁ raised to the power 2. (β₁ ^ 2)
f(x)Function application: m applied to 0. Lean writes f x; papers write f(x). (m 0)
=Equality: m(0) and 0 are the same. (m 0 = 0)
∀For all: The statement after the comma holds for every t. (∀ t, m (t + 1) = β₁ * m t + (1 - β₁) * …)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: m(t)^2 is less than or equal to (1 − β₁)^2/((1 − β₂) · (1 − β₁^2/β₂)) · v(t). (m t ^ 2 ≤ (1 - β₁) ^ 2 / ((1 - β₂) * (1…)
+Addition: t plus 1. (t + 1)
·Multiplication: β₁ times m(t). (β₁ * m t)
-Subtraction: 1 minus β₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - β₁)
a/bDivision: β₁^2 divided by β₂. In Lean, dividing by 0 gives 0. (β₁ ^ 2 / β₂)

theorem bz-closed-loop-moment-ratio (g m v : ℕ → ℝ) (β₁ β₂ : ℝ) (h2 : 0 < β₂) (h2' : β₂ < 1) (h12 : β₁ ^ 2 < β₂) (hm0 : m 0 = 0) (hv0 : v 0 = 0) (hm : ∀ t, m (t + 1) = β₁ * m t + (1 - β₁) * g t) (hv : ∀ t, v (t + 1) = β₂ * v t + (1 - β₂) * g t ^ 2) :
    ∀ t, m t ^ 2 ≤ (1 - β₁) ^ 2 / ((1 - β₂) * (1 - β₁ ^ 2 / β₂)) * v t

Composes the closed forms of both moments (zero-initialized recurrences, as in Baguette's step-zero checkpoint) with the weighted Cauchy–Schwarz ratio: for every step t, m(t)² ≤ C²·v(t) with C² = (1−β₁)²/((1−β₂)(1−β₁²/β₂)). No assumption on gradient magnitude is needed. 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: 87 lines of Lean

Baguette's actual moment banks satisfy m(t)² ≤ C²·v(t) at every step

How it was proved

More proved statements