proofs
Provedvariance-share-lawtraining-energystochastic-attentionlaw

Variance-Share Law, lower bound: (σ² + A/b)(c₀ + b) ≥ (√(σ²c₀) + √A)² for every sampling budget b > 0

For all σ2,A,c0,b∈R\htmlData{mx=1}{\sigma_{2}, A, c_{0}, b \in \htmlData{mx=0}{\mathbb{R}}}, if 0≤σ20 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\sigma_{2}}, 0≤A0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{A}, 0<c00 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{c_{0}} and 0<b0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{b}, then

(σ2⋅c0+A)2≤(σ2+Ab)⋅(c0+b)\htmlData{mx=7}{\left(\htmlData{mx=6}{\htmlData{mx=3}{\sqrt{\htmlData{mx=2}{\htmlData{mx=0}{\sigma_{2}} \cdot \htmlData{mx=1}{c_{0}}}}} + \htmlData{mx=5}{\sqrt{\htmlData{mx=4}{A}}}}\right)^{2}} \mathrel{\htmlData{mx=17}{\leq}} \htmlData{mx=16}{\left(\htmlData{mx=12}{\htmlData{mx=8}{\sigma_{2}} + \htmlData{mx=11}{\frac{\htmlData{mx=9}{A}}{\htmlData{mx=10}{b}}}}\right) \cdot (\htmlData{mx=15}{\htmlData{mx=13}{c_{0}} + \htmlData{mx=14}{b}})}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
σ2, A, c0, b range over real numbers: the statement must hold for every choice. ((σ2 A c0 b : ℝ))
≤At most
0 is less than or equal to σ2. (0 ≤ σ2)
<Less than
0 is strictly smaller than c0. (0 < c0)
aᵇPower
√(σ2 · c0) + √(A) raised to the power 2. ((Real.sqrt (σ2 * c0) + Real.sqrt A) ^ 2)
√Square root
The non-negative number whose square is σ2 · c0. (Real.sqrt (σ2 * c0))
+Addition
√(σ2 · c0) plus √(A). (Real.sqrt (σ2 * c0) + Real.sqrt A)
·Multiplication
σ2 times c0. (σ2 * c0)
a/bDivision
A divided by b. In Lean, dividing by 0 gives 0. (A / b)

Energy-to-target for training with b-sample stochastic attention in the noise-dominated regime is ∝ (gradient variance) × (cost per step) = (σ² + A/b)(c₀ + b), where σ² is the intrinsic minibatch variance, A/b the attention-sampler variance and c₀ the non-attention cost. Outside the pure-noise regime replace σ² by σ²_eff = σ² + 1/κ (McCandlish et al.'s deterministic floor). Part of 'Variance-Share Law: compute-optimal sampling budgets for stochastic attention in training'.

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
32 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements