Provedsampleability-lawself-certifying-proposalfinite-sampleheadline-theorem

Finite-sample self-certificate: from N proposal draws, mean(w²)/mean(w)² lies within [(1−δ)C/(1+δ)², (1+δ)C/(1−δ)²] of the cost factor C except w.p. ≤ (K+K³)/(Nδ²)

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=1}{N \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=3}{s, r : \htmlData{mx=0}{J} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ and $\htmlData{mx=1}{Z, C, K, \delta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}}$ , $\htmlData{mx=3}{\sum_{j} \htmlData{mx=2}{\htmlData{mx=0}{r}(\htmlData{mx=1}{j})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=0}{Z} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\sum_{j} \htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{s}(\htmlData{mx=2}{j})}}}}$ , $\htmlData{mx=0}{C} \mathrel{\htmlData{mx=13}{=}} \htmlData{mx=12}{\sum_{j} \htmlData{mx=11}{\frac{\htmlData{mx=7}{\left(\htmlData{mx=6}{\frac{\htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{s}(\htmlData{mx=2}{j})}}}}{\htmlData{mx=5}{Z}}}\right)^{2}}}{\htmlData{mx=10}{\htmlData{mx=8}{r}(\htmlData{mx=9}{j})}}}}$ , $\htmlData{mx=12}{\forall j,\ \htmlData{mx=5}{\frac{\htmlData{mx=3}{e^{\htmlData{mx=2}{\htmlData{mx=0}{s}(\htmlData{mx=1}{j})}}}}{\htmlData{mx=4}{Z}}} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\htmlData{mx=6}{K} \cdot \htmlData{mx=9}{\htmlData{mx=7}{r}(\htmlData{mx=8}{j})}}}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{N}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\delta}$ and $\htmlData{mx=0}{\delta} \mathrel{\htmlData{mx=1}{<}} 1$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{J}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{J}}$ ), then

1 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{C} \mathbin{\htmlData{mx=117}{\land}} \htmlData{mx=2}{C} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{K} \mathbin{\htmlData{mx=116}{\land}} \htmlData{mx=105}{\sum_{f \in \htmlData{mx=98}{\htmlData{mx=5}{\operatorname{filter}}\left(\htmlData{mx=97}{f \mapsto \htmlData{mx=91}{\lnot \left(\htmlData{mx=13}{\frac{\htmlData{mx=9}{(\htmlData{mx=7}{1 - \htmlData{mx=6}{\delta}}) \cdot \htmlData{mx=8}{C}}}{\htmlData{mx=12}{(\htmlData{mx=11}{1 + \htmlData{mx=10}{\delta}})^{2}}}} \mathrel{\htmlData{mx=47}{<}} \htmlData{mx=46}{\frac{\htmlData{mx=29}{\frac{\htmlData{mx=27}{\sum_{i} \htmlData{mx=26}{\left(\htmlData{mx=25}{\frac{\htmlData{mx=19}{e^{\htmlData{mx=18}{\htmlData{mx=14}{s}(\htmlData{mx=17}{\htmlData{mx=15}{f}(\htmlData{mx=16}{i})})}}}}{\htmlData{mx=24}{\htmlData{mx=20}{r}(\htmlData{mx=23}{\htmlData{mx=21}{f}(\htmlData{mx=22}{i})})}}}\right)^{2}}}}{\htmlData{mx=28}{N}}}}{\htmlData{mx=45}{\left(\htmlData{mx=44}{\frac{\htmlData{mx=42}{\sum_{i} \htmlData{mx=41}{\frac{\htmlData{mx=35}{e^{\htmlData{mx=34}{\htmlData{mx=30}{s}(\htmlData{mx=33}{\htmlData{mx=31}{f}(\htmlData{mx=32}{i})})}}}}{\htmlData{mx=40}{\htmlData{mx=36}{r}(\htmlData{mx=39}{\htmlData{mx=37}{f}(\htmlData{mx=38}{i})})}}}}}{\htmlData{mx=43}{N}}}\right)^{2}}}} \mathbin{\htmlData{mx=90}{\land}} \htmlData{mx=80}{\frac{\htmlData{mx=63}{\frac{\htmlData{mx=61}{\sum_{i} \htmlData{mx=60}{\left(\htmlData{mx=59}{\frac{\htmlData{mx=53}{e^{\htmlData{mx=52}{\htmlData{mx=48}{s}(\htmlData{mx=51}{\htmlData{mx=49}{f}(\htmlData{mx=50}{i})})}}}}{\htmlData{mx=58}{\htmlData{mx=54}{r}(\htmlData{mx=57}{\htmlData{mx=55}{f}(\htmlData{mx=56}{i})})}}}\right)^{2}}}}{\htmlData{mx=62}{N}}}}{\htmlData{mx=79}{\left(\htmlData{mx=78}{\frac{\htmlData{mx=76}{\sum_{i} \htmlData{mx=75}{\frac{\htmlData{mx=69}{e^{\htmlData{mx=68}{\htmlData{mx=64}{s}(\htmlData{mx=67}{\htmlData{mx=65}{f}(\htmlData{mx=66}{i})})}}}}{\htmlData{mx=74}{\htmlData{mx=70}{r}(\htmlData{mx=73}{\htmlData{mx=71}{f}(\htmlData{mx=72}{i})})}}}}}{\htmlData{mx=77}{N}}}\right)^{2}}}} \mathrel{\htmlData{mx=89}{<}} \htmlData{mx=88}{\frac{\htmlData{mx=84}{(\htmlData{mx=82}{1 + \htmlData{mx=81}{\delta}}) \cdot \htmlData{mx=83}{C}}}{\htmlData{mx=87}{(\htmlData{mx=86}{1 - \htmlData{mx=85}{\delta}})^{2}}}}\right)}}\right)}} \htmlData{mx=104}{\prod_{i} \htmlData{mx=103}{\htmlData{mx=99}{r}(\htmlData{mx=102}{\htmlData{mx=100}{f}(\htmlData{mx=101}{i})})}}} \mathrel{\htmlData{mx=115}{\leq}} \htmlData{mx=114}{\frac{\htmlData{mx=109}{\htmlData{mx=106}{K} + \htmlData{mx=108}{\htmlData{mx=107}{K}^{3}}}}{\htmlData{mx=113}{\htmlData{mx=110}{N} \cdot \htmlData{mx=112}{\htmlData{mx=111}{\delta}^{2}}}}}

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)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If J, then ℝ. (Between types, A → B is the type of functions from A to B.) (J → ℝ)
x : TVariables: s, r range over J → ℝ: the statement must hold for every choice. ((s r : J → ℝ))
x ∈ TVariables: Z, C, K, δ range over real numbers: the statement must hold for every choice. ((Z C K δ : ℝ))
∀For all: The statement after the comma holds for every j. (∀ j, 0 < r j)
∑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: exp(s(j))/Z is less than or equal to K · r(j). (Real.exp (s j) / Z ≤ K * r j)
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)
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)
·Multiplication: K times r(j). (K * r j)
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…)
-Subtraction: 1 minus δ. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - δ)
+Addition: 1 plus δ. (1 + δ)
∏Product: Multiply together r(f(i)) for every i. (∏ i, r (f i))

theorem sc-finite-sample-certificate {J : Type} [Fintype J] [Nonempty J] {N : ℕ} (s 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) :
    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 + K ^ 3) / (N * δ ^ 2)

Answers the external-review objection (codex, 2026-10-05) that self-certification had only been proved as a population identity. For an attention row π = e^s/Z and a proposal r with bounded ratio π ≤ K·r, draw N keys i.i.d. from r and form the normaliser-free importance weights w = e^s/r. The empirical certificate Ĉ = mean(w²)/mean(w)² satisfies (1−δ)C/(1+δ)² < Ĉ < (1+δ)C/(1−δ)² except on an event of probability at most (K + K³)/(Nδ²), where C = Σπ²/r = 1 + χ²(π‖r); in addition 1 ≤ C ≤ K. Proof on the exact product space: first and second moments of w (E w = Z, E w² = Z²C), the variance bounds Var w ≤ Z²K and Var w² ≤ E w⁴ = Z⁴Σπ⁴/r³ ≤ Z⁴K³, Chebyshev for each average (rc-average-chebyshev, embedded), a union bound, and a ratio sandwich. Ratio-boundedness is the condition Sampleability loop 3 already identified (mix in the descent proposal, or clip with exact handling of the clipped mass).

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: 222 lines of Lean

Finite-sample self-certificate: from N proposal draws, mean(w²)/mean(w)² lies within [(1−δ)C/(1+δ)², (1+δ)C/(1−δ)²] of the cost factor C except w.p. ≤ (K+K³)/(Nδ²)

How it was proved

More proved statements