Provedalphabaguettebaguette-zv2

Backward through depth: if each layer amplifies by at most 1 + A(l), the cotangent at the input is ≤ Π(1 + A(l)) × output

For all $\htmlData{mx=3}{d, A : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=4}{\forall l,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{A}(\htmlData{mx=1}{l})}}$ and $\htmlData{mx=17}{\forall l,\ \htmlData{mx=0}{l} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{L} \mathrel{\htmlData{mx=16}{\implies}} \htmlData{mx=5}{\htmlData{mx=3}{d}(\htmlData{mx=4}{l})} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{(\htmlData{mx=9}{1 + \htmlData{mx=8}{\htmlData{mx=6}{A}(\htmlData{mx=7}{l})}}) \cdot \htmlData{mx=13}{\htmlData{mx=10}{d}(\htmlData{mx=12}{\htmlData{mx=11}{l} + 1})}}}$ , then

\htmlData{mx=1}{\htmlData{mx=0}{d}(0)} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\left(\htmlData{mx=7}{\prod_{l=0}^{\htmlData{mx=2}{L} - 1} (\htmlData{mx=6}{1 + \htmlData{mx=5}{\htmlData{mx=3}{A}(\htmlData{mx=4}{l})}})}\right) \cdot \htmlData{mx=10}{\htmlData{mx=8}{d}(\htmlData{mx=9}{L})}}

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: d, A range over ℕ → ℝ: the statement must hold for every choice. ((d A : ℕ → ℝ))
∀For all: The statement after the comma holds for every l. (∀ l, 0 ≤ A l)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to A(l). (0 ≤ A l)
<Less than: l is strictly smaller than L. (l < L)
∏Product: Multiply together 1 + A(l) for l = 0, 1, …, L − 1. (∏ l ∈ Finset.range L, (1 + A l))
f(x)Function application: A applied to l. Lean writes f x; papers write f(x). (A l)
·Multiplication: 1 + A(l) times d(l + 1). ((1 + A l) * d (l + 1))
+Addition: 1 plus A(l). (1 + A l)

theorem bz2-backward-depth-product-bound (d A : ℕ → ℝ) (L : ℕ) (hA : ∀ l, 0 ≤ A l) (h : ∀ l, l < L → d l ≤ (1 + A l) * d (l + 1)) :
    d 0 ≤ (∏ l ∈ Finset.range L, (1 + A l)) * d L

For residual stacks, d(l) ≤ (1 + A(l))·d(l+1) per layer gives d(0) ≤ Π_{l<L}(1 + A(l))·d(L). Combined with the per-norm 1/√ε ceiling, this shows the worst-case gradient bound grows geometrically with depth (80 layers), which is why Baguette-Z v2 certifies state, not gradients, and keeps the refuse-nonfinite policy. Part of 'Baguette-Z v2' (revision after the hostile review).

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: 26 lines of Lean

Backward through depth: if each layer amplifies by at most 1 + A(l), the cotangent at the input is ≤ Π(1 + A(l)) × output

How it was proved

More proved statements