Provedsecond-order-bias-lawstochastic-attentiondepthlaw

Bias accumulation through depth: b_{ℓ+1} ≤ λ b_ℓ + c, b_0 = 0 ⇒ b_L ≤ c Σ_{k<L} λ^k

For all $\htmlData{mx=3}{b : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=1}{\mathit{lam}, c \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\mathit{lam}}$ , $\htmlData{mx=1}{\htmlData{mx=0}{b}(0)} \mathrel{\htmlData{mx=2}{=}} 0$ and $\htmlData{mx=12}{\forall l,\ \htmlData{mx=3}{\htmlData{mx=0}{b}(\htmlData{mx=2}{\htmlData{mx=1}{l} + 1})} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\htmlData{mx=8}{\htmlData{mx=4}{\mathit{lam}} \cdot \htmlData{mx=7}{\htmlData{mx=5}{b}(\htmlData{mx=6}{l})}} + \htmlData{mx=9}{c}}}$ , then

\htmlData{mx=2}{\htmlData{mx=0}{b}(\htmlData{mx=1}{L})} \mathrel{\htmlData{mx=10}{\leq}} \htmlData{mx=9}{\htmlData{mx=3}{c} \cdot \htmlData{mx=8}{\sum_{k=0}^{\htmlData{mx=4}{L} - 1} \htmlData{mx=7}{\htmlData{mx=5}{\mathit{lam}}^{\htmlData{mx=6}{k}}}}}

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: lam, c range over real numbers: the statement must hold for every choice. ((lam c : ℝ))
≤At most: 0 is less than or equal to lam. (0 ≤ lam)
f(x)Function application: b applied to 0. Lean writes f x; papers write f(x). (b 0)
=Equality: b(0) and 0 are the same. (b 0 = 0)
∀For all: The statement after the comma holds for every l. (∀ l, b (l + 1) ≤ lam * b l + c)
RReal numbers: The real numbers: every point on the number line. (ℝ)
+Addition: l plus 1. (l + 1)
∑Summation: Add up lam^k for k = 0, 1, …, L − 1. (∑ k ∈ Finset.range L, lam ^ k)
·Multiplication: lam times b(l). (lam * b l)
aᵇPower: lam raised to the power k. (lam ^ k)

theorem sob-bias-accumulation (b : ℕ → ℝ) (lam c : ℝ) (hlam : 0 ≤ lam) (h0 : b 0 = 0) (hstep : ∀ l, b (l + 1) ≤ lam * b l + c) (L : ℕ) :
    b L ≤ c * ∑ k ∈ Finset.range L, lam ^ k

Bias stays O(L·V) for λ ≈ 1 residual blocks; geometric blow-up only if blocks amplify (λ > 1). Part of 'Second-Order Bias Law: unbiased stochastic attention stays (almost) unbiased through smooth depth'.

How it was proved

Proved: 4 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: 18 lines of Lean

Bias accumulation through depth: b_{ℓ+1} ≤ λ b_ℓ + c, b_0 = 0 ⇒ b_L ≤ c Σ_{k<L} λ^k

How it was proved

More proved statements