Boosted Randomized Conversion, end-to-end: k robust-centred runs of a base ε-oracle (each right w.p. ≥ 3/4 per node) induce a proposal with E[Σπ²/r] ≤ (1+6ε)^L + L2^L(7/8)^k((1+6ε)/3ε)^L
For all L,k∈N, Ω0∈Type, w0:Ω0→R, π:(FinL→Bool)→R, ε∈R, m:N→(FinL→Bool)→R, p0:Ω0→N→(FinL→Bool)→R, phat:(Fink→Ω0)→N→(FinL→Bool)→R, pt,Q:(Fink→Ω0)→N→(FinL→Bool)→R and hQ∈∀f,ℓ,b,Q(f,ℓ,b)=⎩⎨⎧:(ℓ)<Lthen({pt(f,ℓ,b)1−pt(f,ℓ,b)if b(⟨ℓ,h⟩)otherwise)if hotherwiseelse1, if ∀ω,0≤w0(ω), ∑ωw0(ω)=1, ∀b,0≤π(b), ∑bπ(b)=1, 0<ε, ∀ℓ,b,m(ℓ,b)=∑b′:FinL→Bool({π(b′)0if (∀i:FinL,i<ℓ⟹b′(i)=b(i))otherwise), ∀ℓ,h:ℓ<L,b:FinL→Bool,∑ω∈filter(ω↦0<m(ℓ,b)∧ε<∣p0(ω,ℓ,b)−m(ℓ,b)m(ℓ+1,update(b,⟨ℓ,h⟩,true))∣)w0(ω)≤41, ∀f,ℓ,b,b′:FinL→Bool,(∀i:FinL,i<ℓ⟹b(i)=b′(i))⟹phat(f,ℓ,b)=phat(f,ℓ,b′), ∀f,ℓ,b,(∃t,k≤2⋅∣filter(j↦∣p0(f(j),ℓ,b)−p0(f(t),ℓ,b)∣≤2ε)∣)⟹∃t,k≤2⋅∣filter(j↦∣p0(f(j),ℓ,b)−p0(f(t),ℓ,b)∣≤2ε)∣∧phat(f,ℓ,b)=p0(f(t),ℓ,b) and ∀f,ℓ,b,pt(f,ℓ,b)=1+2(3ε)max(0,min(1,phat(f,ℓ,b)))+3ε (given FintypeΩ0), then
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables
L, k range over natural numbers: the statement must hold for every choice. ((L 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 < ε)
x : TVariables
pt, Q range over (Fin k → Ω₀) → ℕ → (Fin L → Bool) → ℝ: the statement must hold for every choice. ((pt Q : (Fin k → Ω₀) → ℕ → (Fin L → Boo…)
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…)
∏Product
Multiply together w₀(f(i)) for every i. (∏ i, w₀ (f i))
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 ↦ |p0(f(j), ℓ, b) − p0(f(t), ℓ, b)| ≤ 2 · ε). ((Finset.univ.filter (fun j => |p0 (f j)…)
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)
{ 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…)
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 : 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 : ℕ))
aᵇPower
π(b) raised to the power 2. (π b ^ 2)
x ↦ f(x)Function (λ-abstraction)
The function sending ω to 0 < m(ℓ, b) ∧ ε < |p0(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩…. Lean writes fun x => …; papers write x ↦ …. (fun ω => 0 < m ℓ b ∧ ε < |p0 ω ℓ b - m …)
∧And
Both hold: 0 < m(ℓ, b), and ε < |p0(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, …. (0 < m ℓ b ∧ ε < |p0 ω ℓ b - m (ℓ + 1) (…)
·Multiplication
2 times ε. (2 * ε)
|x|Absolute value
The size of p0(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b) without its sign. (|p0 ω ℓ b - m (ℓ + 1) (Function.update …)
-Subtraction
p0(ω, ℓ, b) minus m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (p0 ω ℓ 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)
(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 : ℝ))
⟨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)
theorem rc-boosted-conversion-end-to-end {L k : ℕ} {Ω₀ : Type} [Fintype Ω₀] (w₀ : Ω₀ → ℝ) (hw₀ : ∀ ω, 0 ≤ w₀ ω) (hsum₀ : ∑ ω, w₀ ω = 1) (π : (Fin L → Bool) → ℝ) (hπ : ∀ b, 0 ≤ π b) (hπs : ∑ b, π b = 1) (ε : ℝ) (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)) (p0 : Ω₀ → ℕ → (Fin L → Bool) → ℝ) (hbase : ∀ ℓ (h : ℓ < L) (b : Fin L → Bool), ∑ ω ∈ Finset.univ.filter (fun ω => 0 < m ℓ b ∧ ε < |p0 ω ℓ b - m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ true) / m ℓ b|), w₀ ω ≤ 1 / 4) (phat : (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 => |p0 (f j) ℓ b - p0 (f t) ℓ b| ≤ 2 * ε)).card) → ∃ t, k ≤ 2 * (Finset.univ.filter (fun j => |p0 (f j) ℓ b - p0 (f t) ℓ b| ≤ 2 * ε)).card ∧ phat f ℓ b = p0 (f t) ℓ b) (pt Q : (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 → Ω₀, (∏ i, w₀ (f i)) * ∑ 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 Attention Compute Law's crux for randomized algorithms, fully composed in one statement. A batched base algorithm answers every node of the key tree in one run; at each node it is ε-accurate except with probability 1/4. Run it k times independently (product weights on Fin k → Ω₀) and let the node estimate be any robust centre of the k answers (one with at least half the answers within 2ε of it), chosen from the answers only (prefix-dependent). Then the smoothed descent proposal satisfies E[Σ_b π_b²/r(b)] ≤ (1+6ε)^L + L·2^L·(7/8)^k·((1+6ε)/(3ε))^L. Proof inside: each node's failure event is contained in 'at least half the runs were bad' (robust-centre lemma), whose product mass is ≤ (7/8)^k (majority-vote amplification); then the end-to-end Randomized Conversion Theorem applies with ε' = 3ε, q = (7/8)^k. The 3/4 base guarantee follows for any unbiased variance-σ² algorithm by averaging 4σ²/ε² runs (rc-average-chebyshev).
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