Provedsampleability-lawself-certifying-proposalimportance-samplingattention-compute-law
Certified sample budget: N ≥ C F²/ε² samples give importance-sampling variance C F²/N ≤ ε²
For all and , 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
- C, F, ε range over real numbers: the statement must hold for every choice. (
(C F ε : ℝ)) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - ≤At most
- 0 is less than or equal to C. (
0 ≤ C) - <Less than
- 0 is strictly smaller than ε. (
0 < ε) - ·Multiplication
- C times F^2. (
C * F ^ 2) - a/bDivision
- C · F^2 divided by ε^2. In Lean, dividing by 0 gives 0. (
C * F ^ 2 / ε ^ 2) - aᵇPower
- F raised to the power 2. (
F ^ 2)
theorem sc-certified-budget (C F ε : ℝ) (N : ℕ) (hC : 0 ≤ C) (hF : 0 ≤ F) (hε : 0 < ε) (hN : C * F ^ 2 / ε ^ 2 ≤ N) (hNpos : 0 < N) :
C * F ^ 2 / N ≤ ε ^ 2The certified cost factor C sets the sample count that guarantees the target variance; the budget is self-set from the certificate. Part of 'The Sampleability Law: a transformer can be trained to make its own attention cheap to sample, and the samples certify the saving' (self-certifying learned proposals inside the Attention Compute Law).
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
- 13 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.