Provedbatch-sample-lawstochastic-attentionbatch-sizelaw
Effective batch: step variance (Σ² + A/b)/B equals exact-attention variance at B_eff = BΣ²/(Σ² + A/b)
For all , if , , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- S2, A, B, b range over real numbers: the statement must hold for every choice. (
(S2 A B b : ℝ)) - <Less than
- 0 is strictly smaller than S2. (
0 < S2) - ≤At most
- 0 is less than or equal to A. (
0 ≤ A) - =Equality
- (S2 + A/b)/B and S2/(B · S2/(S2 + A/b)) are the same. (
(S2 + A / b) / B = S2 / (B * S2 / (S2 +…) - +Addition
- S2 plus A/b. (
S2 + A / b) - a/bDivision
- A divided by b. In Lean, dividing by 0 gives 0. (
A / b) - ·Multiplication
- B times S2. (
B * S2)
theorem bs-effective-batch (S2 A B b : ℝ) (hS : 0 < S2) (hA : 0 ≤ A) (hB : 0 < B) (hb : 0 < b) :
(S2 + A / b) / B = S2 / (B * S2 / (S2 + A / b))Unbiased sampled attention with per-example independent sampling is optimization-equivalent to exact attention at the effective batch B_eff. Part of 'Batch–Sample Law: the optimal attention-sample budget shrinks as the batch grows'.
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
- 11 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.