proofs
Provedalphabaguettebaguette-zcapstone

Closed loop: AdamW-updated output gains keep the residual inside a linear, time-uniform certificate

For all g,u:N→N→R\htmlData{mx=5}{g, u : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=1}{\mathbb{N}} \mathrel{\htmlData{mx=3}{\to}} \htmlData{mx=2}{\mathbb{R}}}, a,η,K∈R\htmlData{mx=1}{a, \eta, K \in \htmlData{mx=0}{\mathbb{R}}}, t∈N\htmlData{mx=1}{t \in \htmlData{mx=0}{\mathbb{N}}} and x,z:N→R\htmlData{mx=3}{x, z : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}, if 0<a0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{a}, a≤1\htmlData{mx=0}{a} \mathrel{\htmlData{mx=1}{\leq}} 1, 0≤η0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\eta}, ∀l,t, ∣u(l,t)∣≤K\htmlData{mx=7}{\forall l, t,\ \htmlData{mx=4}{\left\lvert \htmlData{mx=3}{\htmlData{mx=0}{u}(\htmlData{mx=1}{l}, \htmlData{mx=2}{t})} \right\rvert} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{K}}, ∀l, ∣g(l,0)∣≤1\htmlData{mx=5}{\forall l,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{g}(\htmlData{mx=1}{l}, 0)} \right\rvert} \mathrel{\htmlData{mx=4}{\leq}} 1}, ∀l,t, g(l,t+1)=(1−a)⋅g(l,t)−η⋅u(l,t)\htmlData{mx=20}{\forall l, t,\ \htmlData{mx=4}{\htmlData{mx=0}{g}(\htmlData{mx=1}{l}, \htmlData{mx=3}{\htmlData{mx=2}{t} + 1})} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{\htmlData{mx=11}{(\htmlData{mx=6}{1 - \htmlData{mx=5}{a}}) \cdot \htmlData{mx=10}{\htmlData{mx=7}{g}(\htmlData{mx=8}{l}, \htmlData{mx=9}{t})}} - \htmlData{mx=17}{\htmlData{mx=12}{\eta} \cdot \htmlData{mx=16}{\htmlData{mx=13}{u}(\htmlData{mx=14}{l}, \htmlData{mx=15}{t})}}}}, ∀l, ∣z(l)∣<2\htmlData{mx=5}{\forall l,\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{z}(\htmlData{mx=1}{l})} \right\rvert} \mathrel{\htmlData{mx=4}{<}} 2} and ∀l, x(l+1)=x(l)+g(l,t)⋅z(l)\htmlData{mx=17}{\forall l,\ \htmlData{mx=3}{\htmlData{mx=0}{x}(\htmlData{mx=2}{\htmlData{mx=1}{l} + 1})} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=6}{\htmlData{mx=4}{x}(\htmlData{mx=5}{l})} + \htmlData{mx=14}{\htmlData{mx=10}{\htmlData{mx=7}{g}(\htmlData{mx=8}{l}, \htmlData{mx=9}{t})} \cdot \htmlData{mx=13}{\htmlData{mx=11}{z}(\htmlData{mx=12}{l})}}}}, then

∀L∈N, ∣x(L)∣≤∣x(0)∣+L⋅(2max⁡(1,η⋅Ka))\htmlData{mx=19}{\forall L \in \htmlData{mx=18}{\mathbb{N}},\ \htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{x}(\htmlData{mx=1}{L})} \right\rvert} \mathrel{\htmlData{mx=17}{\leq}} \htmlData{mx=16}{\htmlData{mx=6}{\left\lvert \htmlData{mx=5}{\htmlData{mx=4}{x}(0)} \right\rvert} + \htmlData{mx=15}{\htmlData{mx=7}{L} \cdot \left(\htmlData{mx=14}{2\htmlData{mx=13}{\max(1, \htmlData{mx=12}{\frac{\htmlData{mx=10}{\htmlData{mx=8}{\eta} \cdot \htmlData{mx=9}{K}}}{\htmlData{mx=11}{a}}})}}\right)}}}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x : TVariables
g, u range over ℕ → ℕ → ℝ: the statement must hold for every choice. ((g u : ℕ → ℕ → ℝ))
x ∈ TVariables
a, η, K range over real numbers: the statement must hold for every choice. ((a η K : ℝ))
<Less than
0 is strictly smaller than a. (0 < a)
≤At most
a is less than or equal to 1. (a ≤ 1)
∀For all
The statement after the comma holds for every l, t. (∀ l t, |u l t| ≤ K)
⟹Implies
If ℕ, then ℝ. (Between types, A → B is the type of functions from A to B.) (ℕ → ℝ)
|x|Absolute value
The size of u(l, t) without its sign. (|u l t|)
=Equality
g(l, t + 1) and (1 − a) · g(l, t) − η · u(l, t) are the same. (g l (t + 1) = (1 - a) * g l t - η * u l…)
RReal numbers
The real numbers: every point on the number line. (ℝ)
f(x)Function application
u applied to l, t. Lean writes f x; papers write f(x). (u l t)
+Addition
t plus 1. (t + 1)
·Multiplication
1 − a times g(l, t). ((1 - a) * g l t)
-Subtraction
1 minus a. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - a)
maxMaximum
The larger of 1 and η · K/a. (max 1 (η * K / a))
a/bDivision
η · K divided by a. In Lean, dividing by 0 gives 0. (η * K / a)

Output gains start at |g(l,0)| ≤ 1 and evolve by AdamW with decay (any directions |u| ≤ K). Sublayer outputs are power-of-two normalized (|z| < 2). Then at EVERY training step t and depth L, the residual satisfies |x(L)| ≤ |x(0)| + L·2·max(1, ηK/a). The integer width of the residual stream is fixed at compile time for an unbounded training run. 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
39 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements