proofs
Provedrandomized-conversionconversion-theoremattention-compute-lawmedian-of-means

Run budget for boosting: k ≥ log(2n/δ)/log(8/7) rounds make the union-bound failure mass 2n (7/8)^k ≤ δ

For all n∈N\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}, δ∈R\htmlData{mx=1}{\delta \in \htmlData{mx=0}{\mathbb{R}}} and k∈N\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}, if 0<δ0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\delta}, 0<n0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n} and log⁡(2nδ)log⁡(87)≤k\htmlData{mx=7}{\frac{\htmlData{mx=4}{\log \left(\htmlData{mx=3}{\frac{\htmlData{mx=1}{2\htmlData{mx=0}{n}}}{\htmlData{mx=2}{\delta}}}\right)}}{\htmlData{mx=6}{\log \left(\htmlData{mx=5}{\frac{8}{7}}\right)}}} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{k}, then

2⋅n⋅78k≤δ\htmlData{mx=7}{\htmlData{mx=2}{2 \cdot \htmlData{mx=1}{\htmlData{mx=0}{n}}} \cdot \htmlData{mx=6}{\htmlData{mx=4}{\htmlData{mx=3}{\frac{7}{8}}}^{\htmlData{mx=5}{k}}}} \mathrel{\htmlData{mx=9}{\leq}} \htmlData{mx=8}{\delta}
What the notation means · or point at any symbol
NNatural numbers
The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
RReal numbers
The real numbers: every point on the number line. (ℝ)
<Less than
0 is strictly smaller than δ. (0 < δ)
logNatural logarithm
The logarithm of 2 · n/δ to base e: the power e must be raised to to give 2 · n/δ. (Real.log (2 * n / δ))
≤At most
log(2 · n/δ)/log(8/7) is less than or equal to k. (Real.log (2 * n / δ) / Real.log (8 / 7)…)
(x : T)As real numbers
n read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((n : ℝ))
·Multiplication
2 times n. (2 * n)
a/bDivision
2 · n divided by δ. In Lean, dividing by 0 gives 0. (2 * n / δ)
aᵇPower
7/8 raised to the power k. ((7 / 8 : ℝ) ^ k)

Combined with the majority-vote amplification (7/8)^k per node, this fixes the number of oracle runs per node at O(log(n/δ)) = O(log² n) for δ = n^{−log₂(L+2)}, so the randomized conversion costs only a polylog factor over the oracle. Part of the Randomized Conversion Theorem: the Conversion Theorem (counting ⇒ sampling descent) extended to every randomized bounded-variance attention algorithm via median-of-means boosting, a union bound over the 2n descent nodes, and ε-smoothing of each node; closes the residual scalability crux of the Attention Compute Law.

How it was proved

Proved
4 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
26 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements