Provedalphabaguettebaguette-zcapstone

Every step's Adam direction is bounded: |m(t)/(√v(t) + ε)| ≤ C

For all $\htmlData{mx=3}{g, m, v : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=1}{\beta_{1}, \beta_{2} \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=1}{\varepsilon \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})}}}}$ , $\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}}}}}$ and $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}$ , then

\begin{aligned} & \htmlData{mx=0}{\forall} t, \\ & \quad \htmlData{mx=12}{\left\lvert \htmlData{mx=11}{\frac{\htmlData{mx=4}{\htmlData{mx=2}{m}(\htmlData{mx=3}{t})}}{\htmlData{mx=10}{\htmlData{mx=8}{\sqrt{\htmlData{mx=7}{\htmlData{mx=5}{v}(\htmlData{mx=6}{t})}}} + \htmlData{mx=9}{\varepsilon}}}} \right\rvert} \\ & \quad \quad \htmlData{mx=1}{\leq} \htmlData{mx=25}{\sqrt{\htmlData{mx=24}{\frac{\htmlData{mx=15}{(\htmlData{mx=14}{1 - \htmlData{mx=13}{\beta_{1}}})^{2}}}{\htmlData{mx=23}{(\htmlData{mx=17}{1 - \htmlData{mx=16}{\beta_{2}}}) \cdot \left(\htmlData{mx=22}{1 - \htmlData{mx=21}{\frac{\htmlData{mx=19}{\htmlData{mx=18}{\beta_{1}}^{2}}}{\htmlData{mx=20}{\beta_{2}}}}}\right)}}}}} \end{aligned}

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. (ℝ)
|x|Absolute value: The size of m(t)/(√(v(t)) + ε) without its sign. (|m t / (Real.sqrt (v t) + ε)|)
≤At most: |m(t)/(√(v(t)) + ε)| is less than or equal to √((1 − β₁)^2/((1 − β₂) · (1 − β₁^2/β₂))). (|m t / (Real.sqrt (v t) + ε)| ≤ Real.sq…)
a/bDivision: m(t) divided by √(v(t)) + ε. In Lean, dividing by 0 gives 0. (m t / (Real.sqrt (v t) + ε))
+Addition: t plus 1. (t + 1)
√Square root: The non-negative number whose square is v(t). (Real.sqrt (v t))
·Multiplication: β₁ times m(t). (β₁ * m t)
-Subtraction: 1 minus β₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - β₁)

theorem bz-closed-loop-step-direction (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) (ε : ℝ) (hε : 0 < ε) :
    ∀ t, |m t / (Real.sqrt (v t) + ε)| ≤ Real.sqrt ((1 - β₁) ^ 2 / ((1 - β₂) * (1 - β₁ ^ 2 / β₂)))

Composes the moment-ratio capstone with the update bound: from the raw recurrences alone, every coordinate's Adam direction is at most C = √((1−β₁)²/((1−β₂)(1−β₁²/β₂))) at every step. For Baguette C < 7.3. 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: 105 lines of Lean

Every step's Adam direction is bounded: |m(t)/(√v(t) + ε)| ≤ C

How it was proved

More proved statements