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

Smoothing floor: if every node proposal mixes in ε/(1+2ε) of mass, the L-level product is ≥ (ε/(1+2ε))^L

For all $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=9}{Q : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=8}{\to}} (\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{L}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\operatorname{Bool}}) \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ , $\htmlData{mx=1}{\varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ and $\htmlData{mx=5}{b : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{L}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\operatorname{Bool}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\varepsilon}$ , $\htmlData{mx=14}{\forall \ell,\ \htmlData{mx=0}{\ell} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{L} \mathrel{\htmlData{mx=13}{\implies}} \htmlData{mx=7}{\frac{\htmlData{mx=3}{\varepsilon}}{\htmlData{mx=6}{1 + \htmlData{mx=5}{2\htmlData{mx=4}{\varepsilon}}}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{\htmlData{mx=8}{Q}(\htmlData{mx=9}{\ell}, \htmlData{mx=10}{b})}}$ and $\htmlData{mx=9}{\forall \ell,\ \htmlData{mx=0}{\ell} \mathrel{\htmlData{mx=2}{<}} \htmlData{mx=1}{L} \mathrel{\htmlData{mx=8}{\implies}} 0 \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{\htmlData{mx=3}{Q}(\htmlData{mx=4}{\ell}, \htmlData{mx=5}{b})}}$ , then

\htmlData{mx=6}{\left(\htmlData{mx=4}{\frac{\htmlData{mx=0}{\varepsilon}}{\htmlData{mx=3}{1 + \htmlData{mx=2}{2\htmlData{mx=1}{\varepsilon}}}}}\right)^{\htmlData{mx=5}{L}}} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\prod_{\ell=0}^{\htmlData{mx=7}{L} - 1} \htmlData{mx=11}{\htmlData{mx=8}{Q}(\htmlData{mx=9}{\ell}, \htmlData{mx=10}{b})}}

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 ε. (0 < ε)
∀For all: The statement after the comma holds for every ℓ. (∀ ℓ, ℓ < L → ε / (1 + 2 * ε) ≤ Q ℓ b)
aᵇPower: ε/(1 + 2 · ε) raised to the power L. ((ε / (1 + 2 * ε)) ^ L)
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)
f(x)Function application: Fin applied to L. Lean writes f x; papers write f(x). (Fin L)
⟹Implies: If Fin(L), then Bool. (Between types, A → B is the type of functions from A to B.) (Fin L → Bool)
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)
a/bDivision: ε divided by 1 + 2 · ε. In Lean, dividing by 0 gives 0. (ε / (1 + 2 * ε))
≤At most: ε/(1 + 2 · ε) is less than or equal to Q(ℓ, b). (ε / (1 + 2 * ε) ≤ Q ℓ b)
+Addition: 1 plus 2 · ε. (1 + 2 * ε)
RReal numbers: The real numbers: every point on the number line. (ℝ)
·Multiplication: 2 times ε. (2 * ε)
∏Product: Multiply together Q(ℓ, b) for ℓ = 0, 1, …, L − 1. (∏ ℓ ∈ Finset.range L, Q ℓ b)

theorem rc-smoothing-floor {L : ℕ} (Q : ℕ → (Fin L → Bool) → ℝ) (ε : ℝ) (hε : 0 < ε) (b : Fin L → Bool) (hQ : ∀ ℓ, ℓ < L → ε / (1 + 2 * ε) ≤ Q ℓ b) (hQ1 : ∀ ℓ, ℓ < L → 0 ≤ Q ℓ b) :
    (ε / (1 + 2 * ε)) ^ L ≤ ∏ ℓ ∈ Finset.range L, Q ℓ b

Each level of the synthesised descent proposal is floored by the smoothing mass, so the proposal of every leaf is at least (ε/(1+2ε))^L. This bounds the chi-square on the bad event. 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: 15 lines of Lean

Smoothing floor: if every node proposal mixes in ε/(1+2ε) of mass, the L-level product is ≥ (ε/(1+2ε))^L

How it was proved

More proved statements