Provedconversion-theoremrandomized-conversionheadline-theoremattention-compute-law
Randomized Conversion Theorem, end-to-end: a coin-dependent ε-oracle failing w.p. ≤ q per node induces a proposal with E[Σπ²/r] ≤ (1+2ε)^L + L·2^L·q·((1+2ε)/ε)^L
For all , , , , , , , and , if , , , , , , , and (given ), then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - 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) - x ∈ TVariables
- ε, q range over real numbers: the statement must hold for every choice. (
(ε q : ℝ)) - <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) - 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. (
π) - 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)) - aᵇPower
- π(b) raised to the power 2. (
π b ^ 2) - 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…) - ∏Product
- Multiply together Q(ω, ℓ, b) for ℓ = 0, 1, …, L − 1. (
∏ ℓ ∈ Finset.range L, Q ω ℓ 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 : ℕ)) - ·Multiplication
- 2 times ε. (
2 * ε) - x ↦ f(x)Function (λ-abstraction)
- The function sending ω to 0 < m(ℓ, b) ∧ ε < |phat(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, …. Lean writes fun x => …; papers write x ↦ …. (
fun ω => 0 < m ℓ b ∧ ε < |phat ω ℓ b - …) - ∧And
- Both hold: 0 < m(ℓ, b), and ε < |phat(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ…. (
0 < m ℓ b ∧ ε < |phat ω ℓ b - m (ℓ + 1)…) - |x|Absolute value
- The size of phat(ω, ℓ, b) − m(ℓ + 1, update(b, ⟨ℓ, h⟩, true))/m(ℓ, b) without its sign. (
|phat ω ℓ b - m (ℓ + 1) (Function.updat…) - -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…) - (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/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)
theorem rc-randomized-conversion-end-to-end {L : ℕ} {Ω : Type} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (π : (Fin L → Bool) → ℝ) (hπ : ∀ b, 0 ≤ π b) (hπs : ∑ b, π b = 1) (ε q : ℝ) (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)) (phat : Ω → ℕ → (Fin L → Bool) → ℝ) (hpre : ∀ ω ℓ (b b' : Fin L → Bool), (∀ i : Fin L, (i : ℕ) < ℓ → b i = b' i) → phat ω ℓ b = phat ω ℓ b') (hfail : ∀ ℓ (h : ℓ < L) (b : Fin L → Bool), ∑ ω ∈ Finset.univ.filter (fun ω => 0 < m ℓ b ∧ ε < |phat ω ℓ b - m (ℓ + 1) (Function.update b ⟨ℓ, h⟩ true) / m ℓ b|), w ω ≤ q) (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) :
∑ ω, w ω * ∑ b : Fin L → Bool, π b ^ 2 / ∏ ℓ ∈ Finset.range L, Q ω ℓ b ≤ (1 + 2 * ε) ^ L + ((L : ℝ) * 2 ^ L * q) * ((1 + 2 * ε) / ε) ^ LEnd-to-end form of the Attention Compute Law's crux for randomized algorithms, in one statement. Coins ω carry weights w; the oracle estimate phat(ω, ℓ, b) depends only on the node (prefix) and, for each node, differs from the true conditional mass by more than ε with probability at most q. The smoothed descent proposal r_ω(b) = Π_ℓ Q_ω(ℓ, b) then satisfies E_ω[Σ_b π_b²/r_ω(b)] ≤ (1+2ε)^L + L·2^L·q·((1+2ε)/ε)^L. Inside the proof: the deterministic Conversion Theorem (cv-conversion-theorem, embedded) bounds the good event; the smoothing floor (every factor ≥ ε/(1+2ε)) bounds every outcome; and a union bound over the L·2^L (level, leaf) indices bounds the bad mass. With q ≤ (7/8)^k from median-of-means boosting (rc-average-chebyshev, ua-majority-vote-amplification), k = O(L log(L+2)) runs per node make the second term O(1); composing the boosting layer into this statement is the remaining step.
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
- 347 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.