Provedsecond-order-bias-lawstochastic-attentiondepthcounterexample
Counterexample: ReLU at its kink with ±s noise has bias s/2 = √V/2 (first order)
For all , if , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to s. (
0 ≤ s) - ·Multiplication
- 1/2 times max(s, 0). (
(1 / 2) * max s 0) - +Addition
- 1/2 · max(s, 0) plus 1/2 · max(−s, 0). (
(1 / 2) * max s 0 + (1 / 2) * max (-s) 0) - -Subtraction
- 1/2 · max(s, 0) + 1/2 · max(−s, 0) minus max(0, 0). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
(1 / 2) * max s 0 + (1 / 2) * max (-s) …) - =Equality
- 1/2 · max(s, 0) + 1/2 · max(−s, 0) − max(0, 0) and s/2 are the same. (
(1 / 2) * max s 0 + (1 / 2) * max (-s) …) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 2) - maxMaximum
- The larger of s and 0. (
max s 0) - −xNegation
- The negative of s. (
-s)
theorem sob-relu-first-order-bias (s : ℝ) (hs : 0 ≤ s) :
(1 / 2) * max s 0 + (1 / 2) * max (-s) 0 - max 0 0 = s / 2The Second-Order Bias Law fails for non-smooth activations; Baguette (SiLU/SwiGLU, softmax, RMSNorm) is in the smooth regime. 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
- 10 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.