Provedsampleabilitycertificateheadline-theoremsingle-statement
Sampleability Law, one statement: residual oscillation ≤ Δ ⇒ cost ≤ cosh²(Δ/2); samples certify the cost (failure ≤ (K²−1)/(Nδ²) under an envelope); features bound learned proposals
For all , , , , , , , and , if , , , , , , , , , , and (given , and ), then
What the notation means · or point at any symbol
- Type
- Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Type) - x ∈ TVariables
- J, I range over Type: the statement must hold for every choice. (
(J I : Type)) - Fintype
- Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fintype) - f(x)Function application
- Fintype applied to J. Lean writes f x; papers write f(x). (
Fintype J) - Nonempty
- Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Nonempty) - ⟹Implies
- If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (
J → ℝ) - x : TVariables
- s, st range over J → ℝ: the statement must hold for every choice. (
(s st : J → ℝ)) - ∀For all
- The statement after the comma holds for every i, j. (
∀ i j, (s i - st i) - (s j - st j) ≤ Δ) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - ∑Summation
- Add up r(j) for every j. (
∑ j, r j) - =Equality
- ∑ j, r(j) and 1 are the same. (
∑ j, r j = 1) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - <Less than
- 0 is strictly smaller than r(j). (
0 < r j) - ≤At most
- s(i) − st(i) − (s(j) − st(j)) is less than or equal to Δ. (
(s i - st i) - (s j - st j) ≤ Δ) - -Subtraction
- s(i) minus st(i). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
s i - st i) - eˣExponential function
- e raised to the power s(j), where e ≈ 2.718. (
Real.exp (s j)) - aᵇPower
- exp(s(j))/Z raised to the power 2. (
(Real.exp (s j) / Z) ^ 2) - a/bDivision
- exp(s(j)) divided by Z. In Lean, dividing by 0 gives 0. (
Real.exp (s j) / Z) - ·Multiplication
- K times r(j). (
K * r j) - coshHyperbolic cosine
- (eˣ + e⁻ˣ)/2 at Δ/2. (
Real.cosh (Δ / 2)) - filter
- Finset.univ.filter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Finset.univ.filter) - x ↦ f(x)Function (λ-abstraction)
- The function sending f to ¬((1 − δ) · C/(1 + δ)^2 < (∑ i, (exp(s(f(i)))/r(f(i)))^2)/…. Lean writes fun x => …; papers write x ↦ …. (
fun f : Fin N → J => ¬ ((1 - δ) * C / (…) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - ¬Not
- It is not the case that (1 − δ) · C/(1 + δ)^2 < (∑ i, (exp(s(f(i)))/r(f(i)))^2)/N/…. (
¬ ((1 - δ) * C / (1 + δ) ^ 2 < ((∑ i, (…) - ∧And
- Both hold: (1 − δ) · C/(1 + δ)^2 < (∑ i, (exp(s(f(i)))/r(f(i)))^2)/N/…, and (∑ i, (exp(s(f(i)))/r(f(i)))^2)/N/((∑ i, exp(s(f(i)))/r(f(…. (
(1 - δ) * C / (1 + δ) ^ 2 < ((∑ i, (Rea…) - +Addition
- 1 plus δ. (
1 + δ) - ∏Product
- Multiply together r(f(i)) for every i. (
∏ i, r (f i)) - √Square root
- The non-negative number whose square is ∑ i, lam(i) · π(i, j)^2. (
Real.sqrt (∑ i, lam i * π i j ^ 2)) - πPi
- The ratio of a circle's circumference to its diameter, ≈ 3.14159. (
π)
theorem sampleability-law-provable-form {J I : Type} [Fintype J] [Nonempty J] [Fintype I] (s st : J → ℝ) (Δ : ℝ) (hΔ : ∀ i j, (s i - st i) - (s j - st j) ≤ Δ) {N : ℕ} (r : J → ℝ) (Z C K δ : ℝ) (hr : ∀ j, 0 < r j) (hrs : ∑ j, r j = 1) (hZ : Z = ∑ j, Real.exp (s j)) (hC : C = ∑ j, (Real.exp (s j) / Z) ^ 2 / r j) (hK : ∀ j, Real.exp (s j) / Z ≤ K * r j) (hN : 0 < N) (hδ : 0 < δ) (hδ1 : δ < 1) (lam : I → ℝ) (π : I → J → ℝ) (rφ : J → ℝ) (hlam : ∀ i, 0 ≤ lam i) (hrφ : ∀ j, 0 < rφ j) (hrφs : ∑ j, rφ j = 1) :
(∑ j, (Real.exp (s j) / ∑ k, Real.exp (s k)) ^ 2 / (Real.exp (st j) / ∑ k, Real.exp (st k)) ≤ Real.cosh (Δ / 2) ^ 2) ∧ (1 ≤ C ∧ C ≤ K ∧ ∑ f ∈ Finset.univ.filter (fun f : Fin N → J => ¬ ((1 - δ) * C / (1 + δ) ^ 2 < ((∑ i, (Real.exp (s (f i)) / r (f i)) ^ 2) / N) / ((∑ i, Real.exp (s (f i)) / r (f i)) / N) ^ 2 ∧ ((∑ i, (Real.exp (s (f i)) / r (f i)) ^ 2) / N) / ((∑ i, Real.exp (s (f i)) / r (f i)) / N) ^ 2 < (1 + δ) * C / (1 - δ) ^ 2)), ∏ i, r (f i) ≤ (K ^ 2 - 1) / (N * δ ^ 2)) ∧ ((∑ j, Real.sqrt (∑ i, lam i * π i j ^ 2)) ^ 2 ≤ ∑ i, lam i * ∑ j, π i j ^ 2 / rφ j) ∧ ((∀ j, 0 < ∑ i, lam i * π i j ^ 2) → ∑ i, lam i * ∑ j, π i j ^ 2 / (Real.sqrt (∑ i, lam i * π i j ^ 2) / ∑ k, Real.sqrt (∑ i, lam i * π i k ^ 2)) = (∑ j, Real.sqrt (∑ i, lam i * π i j ^ 2)) ^ 2)The strongest provable single statement of the Sampleability Law. For a row with scores s: (i) any proposal softmax(s̃) whose score residual s − s̃ has oscillation ≤ Δ has cost factor Σπ²/r ≤ cosh²(Δ/2), so a head is cheaply sampleable as soon as some cheap score approximation is uniformly accurate up to a shift; (ii) with an envelope π ≤ K r, N draws from r give an empirical certificate mean(w²)/mean(w)² of the cost factor C within [(1−δ)C/(1+δ)², (1+δ)C/(1−δ)²] except with probability ≤ (K²−1)/(Nδ²), and 1 ≤ C ≤ K, so the same samples that compute attention certify the proposal; (iii) for a proposal built from features φ (a mixture over rows with weights λ, the posterior given φ), the expected cost is ≥ (Σ_j √E[π_j²|φ])² and r ∝ √E[π²|φ] attains it, which is the ceiling of any learned proposal on those features and the closed-form target for training one. The co-training dynamics (whether trained heads reach O(1) residual oscillation) remain a conjecture. Conjoins drift-oscillation-cosh-bound, sc-certificate-quadratic-failure and the variational cost law.
How it was proved
- Proved
- 5 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
- 349 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.