Provedbatch-sample-lawstochastic-attentionbatch-sizelaw
Compute-to-target (B + B_noise + B_noise·A/(bΣ²))(c₀ + b) ≥ (√((B+B_noise)c₀) + √(B_noise A/Σ²))² for every budget b > 0
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
- B, Bn, A, S2, c0, b range over real numbers: the statement must hold for every choice. (
(B Bn A S2 c0 b : ℝ)) - ≤At most
- 0 is less than or equal to B. (
0 ≤ B) - <Less than
- 0 is strictly smaller than S2. (
0 < S2) - aᵇPower
- √((B + Bn) · c0) + √(Bn · A/S2) raised to the power 2. (
(Real.sqrt ((B + Bn) * c0) + Real.sqrt …) - √Square root
- The non-negative number whose square is (B + Bn) · c0. (
Real.sqrt ((B + Bn) * c0)) - ·Multiplication
- B + Bn times c0. (
(B + Bn) * c0) - +Addition
- B plus Bn. (
B + Bn) - a/bDivision
- Bn · A divided by S2. In Lean, dividing by 0 gives 0. (
Bn * A / S2)
theorem bs-compute-lower-bound (B Bn A S2 c0 b : ℝ) (hB : 0 ≤ B) (hBn : 0 ≤ Bn) (hA : 0 ≤ A) (hS : 0 < S2) (hc : 0 < c0) (hb : 0 < b) :
(Real.sqrt ((B + Bn) * c0) + Real.sqrt (Bn * A / S2)) ^ 2 ≤ (B + Bn + Bn * A / (b * S2)) * (c0 + b)AM–GM on the steps-to-target × cost-per-step product under the large-batch model S = S_min(1 + B_noise/B_eff); equality at b*²(B+B_noise) = B_noise A c₀/Σ². 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
- 37 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.