Provedsampleability-lawself-certifying-proposalfinite-sampleconversion-theorem
Certificate for the descent proposal: with an ε-accurate node oracle, N draws certify the cost factor within (1±δ) factors except w.p. ≤ ((1+2ε)^L + (1+2ε)^{3L})/(Nδ²)
For all , , , , , and , if , , , , , , , and , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - x ∈ TVariables
- L, N range over natural numbers: the statement must hold for every choice. (
(L N : ℕ)) - =Equality
- Z and ∑ b, exp(s(b)) are the same. (
Z = ∑ b, Real.exp (s b)) - <Less than
- 0 is strictly smaller than ε. (
0 < ε) - x : TVariables
- pt, Q range over ℕ → (Fin L → Bool) → ℝ: the statement must hold for every choice. (
(pt Q : ℕ → (Fin L → Bool) → ℝ)) - 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) - f(x)Function application
- Fin applied to L. Lean writes f x; papers write f(x). (
Fin L) - ⟹Implies
- If Fin(L), then Bool. (Between types, A → B is the type of functions from A to B.) (
Fin L → Bool) - ∑Summation
- Add up exp(s(b)) for every b. (
∑ b, Real.exp (s b)) - 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) - Bool
- Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Bool) - eˣExponential function
- e raised to the power s(b), where e ≈ 2.718. (
Real.exp (s b)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - maxMaximum
- The larger of 0 and min(1, phat(ℓ, b)). (
max 0 (min 1 (phat ℓ b))) - minMinimum
- The smaller of 1 and phat(ℓ, b). (
min 1 (phat ℓ b)) - x ↦ f(x)Function (λ-abstraction)
- The function sending f to ¬((1 − δ) · (∑ b, (exp(s(b))/Z)^2/(∏ ℓ, Q(ℓ, b)))/(1 + δ)^…. Lean writes fun x => …; papers write x ↦ …. (
fun f : Fin N → (Fin L → Bool) => ¬ ((1…) - then
- then: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
then) - |x|Absolute value
- The size of phat(ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b) without its sign. (
|phat ℓ b - m (ℓ + 1) (Function.update …) - ≤At most
- |phat(ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b)| is less than or equal to ε. (
|phat ℓ b - m (ℓ + 1) (Function.update …) - -Subtraction
- phat(ℓ, b) minus m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
phat ℓ b - m (ℓ + 1) (Function.update b…) - { a if c; b otherwiseCases (if … then … else)
- exp(s(b'))/Z when ∀ i, i < ℓ → b'(i) = b(i), and 0 otherwise. (
if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b…) - ∀For all
- The statement after the comma holds for every i. (
∀ i : Fin L, (i : ℕ) < ℓ → b' i = b i) - +Addition
- ℓ plus 1. (
ℓ + 1) - (x : T)As natural numbers
- i read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(i : ℕ)) - update
- Function.update: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Function.update) - ·Multiplication
- 2 times ε. (
2 * ε) - ¬Not
- It is not the case that (1 − δ) · (∑ b, (exp(s(b))/Z)^2/(∏ ℓ, Q(ℓ, b)))/(1 + δ)^2 …. (
¬ ((1 - δ) * (∑ b, (Real.exp (s b) / Z)…) - ∧And
- Both hold: (1 − δ) · (∑ b, (exp(s(b))/Z)^2/(∏ ℓ, Q(ℓ, b)))/(1 + δ)^2 …, and (∑ i, (exp(s(f(i)))/(∏ ℓ, Q(ℓ, f(i))))^2)/N/((∑ i, exp(s(f…. (
(1 - δ) * (∑ b, (Real.exp (s b) / Z) ^ …) - ⟨a, b⟩Anonymous constructor
- Builds a structure (a pair, a subtype element, …) from ℓ, h. (
⟨ℓ, h⟩) - true
- true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
true) - aᵇPower
- exp(s(b))/Z raised to the power 2. (
(Real.exp (s b) / Z) ^ 2) - a/bDivision
- exp(s(b')) divided by Z. In Lean, dividing by 0 gives 0. (
Real.exp (s b') / Z) - ∏Product
- Multiply together Q(ℓ, b) for ℓ = 0, 1, …, L − 1. (
∏ ℓ ∈ Finset.range L, Q ℓ b)
theorem sc-certificate-for-descent-proposal {L N : ℕ} (s : (Fin L → Bool) → ℝ) (Z ε δ : ℝ) (hZ : Z = ∑ b, Real.exp (s b)) (hε : 0 < ε) (m : ℕ → (Fin L → Bool) → ℝ) (hm : ∀ ℓ b, m ℓ b = ∑ b' : Fin L → Bool, (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b i) then Real.exp (s b') / Z else 0)) (phat : ℕ → (Fin L → Bool) → ℝ) (hpre : ∀ ℓ (b b' : Fin L → Bool), (∀ i : Fin L, (i : ℕ) < ℓ → b i = b' i) → phat ℓ b = phat ℓ b') (hacc : ∀ ℓ (h : ℓ < L) b, 0 < m ℓ b → |phat ℓ b - m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ true) / m ℓ b| ≤ ε) (pt Q : ℕ → (Fin L → Bool) → ℝ) (hpt : ∀ ℓ b, pt ℓ b = (max 0 (min 1 (phat ℓ b)) + ε) / (1 + 2 * ε)) (hQ : ∀ ℓ b, Q ℓ b = if h : ℓ < L then (if b ⟨ℓ, h⟩ then pt ℓ b else 1 - pt ℓ b) else 1) (hN : 0 < N) (hδ : 0 < δ) (hδ1 : δ < 1) :
∑ f ∈ Finset.univ.filter (fun f : Fin N → (Fin L → Bool) => ¬ ((1 - δ) * (∑ b, (Real.exp (s b) / Z) ^ 2 / ∏ ℓ ∈ Finset.range L, Q ℓ b) / (1 + δ) ^ 2 < ((∑ i, (Real.exp (s (f i)) / (∏ ℓ ∈ Finset.range L, Q ℓ (f i))) ^ 2) / N) / ((∑ i, Real.exp (s (f i)) / (∏ ℓ ∈ Finset.range L, Q ℓ (f i))) / N) ^ 2 ∧ ((∑ i, (Real.exp (s (f i)) / (∏ ℓ ∈ Finset.range L, Q ℓ (f i))) ^ 2) / N) / ((∑ i, Real.exp (s (f i)) / (∏ ℓ ∈ Finset.range L, Q ℓ (f i))) / N) ^ 2 < (1 + δ) * (∑ b, (Real.exp (s b) / Z) ^ 2 / ∏ ℓ ∈ Finset.range L, Q ℓ b) / (1 - δ) ^ 2)), ∏ i, (∏ ℓ ∈ Finset.range L, Q ℓ (f i)) ≤ ((1 + 2 * ε) ^ L + ((1 + 2 * ε) ^ L) ^ 3) / (N * δ ^ 2)Answers review round 2 (codex): the finite-sample certificate's ratio bound K is derived, not assumed. For attention scores s over 2^L keys and the smoothed descent proposal r = Π_ℓ Q_ℓ built from any prefix-dependent ε-accurate node oracle, the Conversion Theorem (cv-conversion-theorem, embedded) gives r a distribution with π ≤ (1+2ε)^L·r; the finite-sample certificate (sc-finite-sample-certificate, embedded) then applies with K = (1+2ε)^L. So N i.i.d. draws from the proposal yield the normaliser-free statistic mean(w²)/mean(w)² within [(1−δ)C/(1+δ)², (1+δ)C/(1−δ)²] of the true cost factor C except with probability ≤ (K + K³)/(Nδ²). At ε = 1/L, K ≤ e², so a constant number of draws per δ² certifies the cost. One statement, no assumed K.
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
- 476 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.