Provedsampleability-lawheadline-theoremself-certifying-proposal
Self-certification theorem (Sampleability Law, strongest provable form): the attention samples certify, bound, identify and train their own proposal cost
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) - 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, r, f range over J → ℝ: the statement must hold for every choice. (
(s r f : J → ℝ)) - x ∈ TVariables
- θ₀, θ, φ, F, ε range over real numbers: the statement must hold for every choice. (
(θ₀ θ φ F ε : ℝ)) - NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - ∀For all
- The statement after the comma holds for every j. (
∀ j, π j = Real.exp (s j) / ∑ k, Real.e…) - ≤At most
- 0 is less than or equal to F. (
0 ≤ F) - ·Multiplication
- ∑ j, π(j)^2/r(j) times F^2. (
(∑ j, π j ^ 2 / r j) * F ^ 2) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - πPi
- The ratio of a circle's circumference to its diameter, ≈ 3.14159. (
π) - =Equality
- π(j) and exp(s(j))/(∑ k, exp(s(k))) are the same. (
π j = Real.exp (s j) / ∑ k, Real.exp (s…) - <Less than
- 0 is strictly smaller than r(j). (
0 < r j) - HasDerivAt
- HasDerivAt: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
HasDerivAt) - aᵇPower
- π(j) raised to the power 2. (
π j ^ 2) - eˣExponential function
- e raised to the power s(j), where e ≈ 2.718. (
Real.exp (s j)) - a/bDivision
- exp(s(j)) divided by ∑ k, exp(s(k)). In Lean, dividing by 0 gives 0. (
Real.exp (s j) / ∑ k, Real.exp (s k)) - x ↦ f(x)Function (λ-abstraction)
- The function sending t to rr(j, t). Lean writes fun x => …; papers write x ↦ …. (
fun t => rr j t) - ∑Summation
- Add up exp(s(k)) for every k. (
∑ k, Real.exp (s k)) - −xNegation
- The negative of ∑ j, rr(j, θ₀) · (π(j)/rr(j, θ₀))^2 · (r'(j, θ₀)/rr(j, θ₀)). (
-∑ j, rr j θ₀ * (π j / rr j θ₀) ^ 2 * (…) - ∧And
- Both hold: ∀ a, (∀ j, 0 < a(j)) → log(∑ j, a(j) · exp((θ + φ)/2 · f(j…, and (∑ j, π(j)^2/r(j)) · F^2/N ≤ ε^2. (
(∀ a : J → ℝ, (∀ j, 0 < a j) → Real.log…) - logNatural logarithm
- The logarithm of ∑ j, a(j) · exp((θ + φ)/2 · f(j)) to base e: the power e must be raised to to give ∑ j, a(j) · exp((θ + φ)/2 · f(j)). (
Real.log (∑ j, a j * Real.exp ((θ + φ) …) - +Addition
- θ plus φ. (
θ + φ)
theorem sc-self-certification-theorem {J : Type} [Fintype J] [Nonempty J] (s r f : J → ℝ) (π : J → ℝ) (rr r' : J → ℝ → ℝ) (θ₀ θ φ F ε : ℝ) (N : ℕ) (hπ : ∀ j, π j = Real.exp (s j) / ∑ k, Real.exp (s k)) (hr : ∀ j, 0 < r j) (hrs : ∑ j, r j = 1) (hrr : ∀ j, 0 < rr j θ₀) (hd : ∀ j, HasDerivAt (fun t => rr j t) (r' j θ₀) θ₀) (hF : 0 ≤ F) (hε : 0 < ε) (hNpos : 0 < N) (hN : (∑ j, π j ^ 2 / r j) * F ^ 2 / ε ^ 2 ≤ N) :
(∑ j, r j * (π j / r j) ^ 2 = ∑ j, π j ^ 2 / r j) ∧ (∑ j, r j * (Real.exp (s j) / r j) ^ 2 = (∑ j, Real.exp (s j)) ^ 2 * ∑ j, π j ^ 2 / r j) ∧ (1 ≤ ∑ j, π j ^ 2 / r j) ∧ (∑ j, π j ^ 2 / r j = 1 → ∀ j, π j = r j) ∧ HasDerivAt (fun t => ∑ j, π j ^ 2 / rr j t) (-∑ j, rr j θ₀ * (π j / rr j θ₀) ^ 2 * (r' j θ₀ / rr j θ₀)) θ₀ ∧ (∀ a : J → ℝ, (∀ j, 0 < a j) → Real.log (∑ j, a j * Real.exp ((θ + φ) / 2 * f j)) ≤ (Real.log (∑ j, a j * Real.exp (θ * f j)) + Real.log (∑ j, a j * Real.exp (φ * f j))) / 2) ∧ ((∑ j, π j ^ 2 / r j) * F ^ 2 / N ≤ ε ^ 2)One statement combining the provable core of the Sampleability Law. For an attention row π = softmax(s) and any positive proposal r: (1) the certificate E_r[(π/r)²] equals the cost factor Σπ²/r = 1 + χ²; (2) it is computable from unnormalised weights, E_r[(e^s/r)²] = Z²·Σπ²/r; (3) it is at least 1; (4) it equals 1 only for the exact proposal r = π; (5) its gradient in a proposal parameter is an expectation of the same importance ratio (HasDerivAt); (6) for score-shaped proposals each log-sum-exp term of the log cost is midpoint-convex; and (7) N ≥ (Σπ²/r)F²/ε² samples give variance ≤ ε². The Law's full claim, that co-training drives every predictable head to O(1) cost, is a statement about neural training dynamics and is not provable in Lean; this is the strongest formal form, and the empirical claim stays a conjecture.
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
- 103 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.