Provedrandomized-conversionconversion-theoremattention-compute-lawmedian-of-means
Floor exponent: with ε = 1/L the smoothing floor's reciprocal ((1+2ε)/ε)^L equals (L+2)^L
For all , if , then
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) - aᵇPower
- (1 + 2 · (1/L))/(1/L) raised to the power L. (
((1 + 2 * (1 / (L : ℝ))) / (1 / (L : ℝ)…) - =Equality
- ((1 + 2 · (1/L))/(1/L))^L and (L + 2)^L are the same. (
((1 + 2 * (1 / (L : ℝ))) / (1 / (L : ℝ)…) - +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-floor-exponent (L : ℕ) (hL : 0 < L) :
((1 + 2 * (1 / (L : ℝ))) / (1 / (L : ℝ))) ^ L = ((L : ℝ) + 2) ^ LFixing ε = 1/L, the worst-case chi-square on the bad event is (L+2)^L = n^{log₂(L+2)}, so a failure probability δ = n^{-log₂(L+2)} is enough. 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
- 11 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.