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

Randomized Conversion constant: ε = 1/L and δ = (L+2)^{-L} give E[χ²] ≤ e² + 1

For all $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=1}{E \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{L}$ and $\htmlData{mx=0}{E} \mathrel{\htmlData{mx=21}{\leq}} \htmlData{mx=20}{\htmlData{mx=7}{\left(\htmlData{mx=5}{1 + \htmlData{mx=4}{2\left(\htmlData{mx=3}{\frac{1}{\htmlData{mx=2}{\htmlData{mx=1}{L}}}}\right)}}\right)^{\htmlData{mx=6}{L}}} + \htmlData{mx=19}{\htmlData{mx=13}{\frac{1}{\htmlData{mx=12}{(\htmlData{mx=10}{\htmlData{mx=9}{\htmlData{mx=8}{L}} + 2})^{\htmlData{mx=11}{L}}}}} \cdot \htmlData{mx=18}{(\htmlData{mx=16}{\htmlData{mx=15}{\htmlData{mx=14}{L}} + 2})^{\htmlData{mx=17}{L}}}}}$ , then

\htmlData{mx=0}{E} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=1}{e^{2}} + 1}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
<Less than: 0 is strictly smaller than L. (0 < L)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: E is less than or equal to (1 + 2 · (1/L))^L + 1/(L + 2)^L · (L + 2)^L. (E ≤ (1 + 2 * (1 / (L : ℝ))) ^ L + (1 / …)
aᵇPower: 1 + 2 · (1/L) raised to the power L. ((1 + 2 * (1 / (L : ℝ))) ^ L)
eˣExponential function: e raised to the power 2, where e ≈ 2.718. (Real.exp 2)
+Addition: 1 plus 2 · (1/L). (1 + 2 * (1 / (L : ℝ)))
·Multiplication: 2 times 1/L. (2 * (1 / (L : ℝ)))
a/bDivision: 1 divided by L. In Lean, dividing by 0 gives 0. (1 / (L : ℝ))
(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-randomized-conversion-constant (L : ℕ) (hL : 0 < L) (E : ℝ) (hE : E ≤ (1 + 2 * (1 / (L : ℝ))) ^ L + (1 / ((L : ℝ) + 2) ^ L) * ((L : ℝ) + 2) ^ L) :
    E ≤ Real.exp 2 + 1

With ε = 1/L and δ = (L+2)^{−L}, the expected chi-square of the synthesised proposal is at most e² + 1, a universal constant independent of n, the depth L = log₂ n, and the oracle's variance. The sampling-side cost of the Attention Compute Law therefore follows from any randomized bounded-variance estimator of attention normalisers, with no scalability assumption. 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: 24 lines of Lean

Randomized Conversion constant: ε = 1/L and δ = (L+2)^{-L} give E[χ²] ≤ e² + 1

How it was proved

More proved statements