The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables
L, k, k₁ range over natural numbers: the statement must hold for every choice. ((L k k₁ : ℕ))
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 Ω₁. Lean writes f x; papers write f(x). (Fintype Ω₁)
⟹Implies
If Ω₁, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω₁ → ℝ)
∀For all
The statement after the comma holds for every ω. (∀ ω, 0 ≤ w₁ ω)
∑Summation
Add up w₁(ω) for every ω. (∑ ω, w₁ ω)
=Equality
∑ ω, w₁(ω) and 1 are the same. (∑ ω, w₁ ω = 1)
<Less than
0 is strictly smaller than ε. (0 < ε)
·Multiplication
4 times σ2. (4 * σ2)
x : TVariables
pt, Q range over (Fin k → Fin k₁ → Ω₁) → ℕ → (Fin L → Bool) → ℝ: the statement must hold for every choice. ((pt Q : (Fin k → Fin k₁ → Ω₁) → ℕ → (Fi…)
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)
RReal numbers
The real numbers: every point on the number line. (ℝ)
≤At most
0 is less than or equal to w₁(ω). (0 ≤ w₁ ω)
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)
πPi
The ratio of a circle's circumference to its diameter, ≈ 3.14159. (π)
∃There exists
At least one t makes the statement after the comma true. (∃ t, k ≤ 2 * (Finset.univ.filter (fun j…)
aᵇPower
ε raised to the power 2. (ε ^ 2)
maxMaximum
The larger of 0 and min(1, phat(f, ℓ, b)). (max 0 (min 1 (phat f ℓ b)))
|s|Cardinality
The number of elements of filter(j ↦ |(∑ i, X(f(j, i), ℓ, b))/k₁ − (∑ i, X(f(t, i), …. ((Finset.univ.filter (fun j => |(∑ i, X …)
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)
minMinimum
The smaller of 1 and phat(f, ℓ, b). (min 1 (phat f ℓ b))
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)
∏Product
Multiply together w₁(f(i, j)) for every j. (∏ j, w₁ (f i j))
{ a if c; b otherwiseCases (if … then … else)
π(b') when ∀ i, i < ℓ → b'(i) = b(i), and 0 otherwise. (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b…)
x ↦ f(x)Function (λ-abstraction)
The function sending j to |(∑ i, X(f(j, i), ℓ, b))/k₁ − (∑ i, X(f(t, i), ℓ, b))/k₁| …. Lean writes fun x => …; papers write x ↦ …. (fun j => |(∑ i, X (f j i) ℓ b) / k₁ - (…)
|x|Absolute value
The size of (∑ i, X(f(j, i), ℓ, b))/k₁ − (∑ i, X(f(t, i), ℓ, b))/k₁ without its sign. (|(∑ i, X (f j i) ℓ b) / k₁ - (∑ i, X (f…)
(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 : ℕ))
-Subtraction
X(ω, ℓ, b) minus m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (X ω ℓ b - m (ℓ + 1) (Function.update b …)
a/bDivision
m(ℓ + 1, update(b, ⟨ℓ, h⟩, true)) divided by m(ℓ, b). In Lean, dividing by 0 gives 0. (m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ tru…)
+Addition
ℓ plus 1. (ℓ + 1)
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)
⟨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)
∧And
Both hold: k ≤ 2 · card(filter(j ↦ |(∑ i, X(f(j, i), ℓ, b))/k₁ − (∑ i…, and phat(f, ℓ, b) = (∑ i, X(f(t, i), ℓ, b))/k₁. (k ≤ 2 * (Finset.univ.filter (fun j => |…)
(x : T)As real numbers
L read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((L : ℝ))
theorem rc-unbiased-algorithm-to-proposal {L k k₁ : ℕ} {Ω₁ : Type} [Fintype Ω₁] (w₁ : Ω₁ → ℝ) (hw₁ : ∀ ω, 0 ≤ w₁ ω) (hsum₁ : ∑ ω, w₁ ω = 1) (π : (Fin L → Bool) → ℝ) (hπ : ∀ b, 0 ≤ π b) (hπs : ∑ b, π b = 1) (ε σ2 : ℝ) (hε : 0 < ε) (m : ℕ → (Fin L → Bool) → ℝ) (hm : ∀ ℓ b, m ℓ b = ∑ b' : Fin L → Bool, (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b i) then π b' else 0)) (X : Ω₁ → ℕ → (Fin L → Bool) → ℝ) (hk₁ : 0 < k₁) (hk₁σ : 4 * σ2 ≤ k₁ * ε ^ 2) (hmean : ∀ ℓ (h : ℓ < L) (b : Fin L → Bool), 0 < m ℓ b → ∑ ω, w₁ ω * X ω ℓ b = m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ true) / m ℓ b) (hvar : ∀ ℓ (h : ℓ < L) (b : Fin L → Bool), 0 < m ℓ b → ∑ ω, w₁ ω * (X ω ℓ b - m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ true) / m ℓ b) ^ 2 ≤ σ2) (phat : (Fin k → Fin k₁ → Ω₁) → ℕ → (Fin L → Bool) → ℝ) (hpreφ : ∀ f ℓ (b b' : Fin L → Bool), (∀ i : Fin L, (i : ℕ) < ℓ → b i = b' i) → phat f ℓ b = phat f ℓ b') (hcenter : ∀ f ℓ b, (∃ t, k ≤ 2 * (Finset.univ.filter (fun j => |(∑ i, X (f j i) ℓ b) / k₁ - (∑ i, X (f t i) ℓ b) / k₁| ≤ 2 * ε)).card) → ∃ t, k ≤ 2 * (Finset.univ.filter (fun j => |(∑ i, X (f j i) ℓ b) / k₁ - (∑ i, X (f t i) ℓ b) / k₁| ≤ 2 * ε)).card ∧ phat f ℓ b = (∑ i, X (f t i) ℓ b) / k₁) (pt Q : (Fin k → Fin k₁ → Ω₁) → ℕ → (Fin L → Bool) → ℝ) (hpt : ∀ f ℓ b, pt f ℓ b = (max 0 (min 1 (phat f ℓ b)) + 3 * ε) / (1 + 2 * (3 * ε))) (hQ : ∀ f ℓ b, Q f ℓ b = if h : ℓ < L then (if b ⟨ℓ, h⟩ then pt f ℓ b else 1 - pt f ℓ b) else 1) :
∑ f : Fin k → Fin k₁ → Ω₁, (∏ i, ∏ j, w₁ (f i j)) * ∑ b : Fin L → Bool, π b ^ 2 / ∏ ℓ ∈ Finset.range L, Q f ℓ b ≤ (1 + 2 * (3 * ε)) ^ L + ((L : ℝ) * 2 ^ L * (7 / 8 : ℝ) ^ k) * ((1 + 2 * (3 * ε)) / (3 * ε)) ^ L
The Randomized Conversion Theorem from its true premise, in one statement. Assume an algorithm whose output on each sub-instance (indicator values on a child block, i.e. the conditional mass) is an exactly unbiased estimate with variance at most σ² per run. Average k₁ runs per round (k₁ε² ≥ 4σ²), take a robust centre across k rounds per node, smooth by 3ε, and descend. Then the induced proposal over the 2^L keys satisfies E[Σ_b π_b²/r(b)] ≤ (1+6ε)^L + L·2^L·(7/8)^k·((1+6ε)/(3ε))^L over the product of all k·k₁ runs. Every step is inside the statement: Chebyshev for the average (rc-average-chebyshev) gives per-node success ≥ 3/4; majority amplification and the robust-centre lemma give per-node failure ≤ (7/8)^k; the union bound, the smoothing floor and the deterministic Conversion Theorem bound the expectation. With ε = 1/(6L) and k = O(L log(L+2)) the bound is a constant: any unbiased bounded-variance attention algorithm converts to a proposal of constant expected cost at polylog overhead.
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