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

Robust centre (median-free median-of-means): a strict majority of estimates within ε of p yields a selectable estimate within 3ε of p

For all $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{a : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{k}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{p, \varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\varepsilon}$ and $\htmlData{mx=0}{k} \mathrel{\htmlData{mx=25}{<}} \htmlData{mx=24}{2 \cdot \htmlData{mx=23}{\lvert \htmlData{mx=22}{\htmlData{mx=12}{\operatorname{filter}}(\htmlData{mx=21}{i \mapsto \htmlData{mx=18}{\left\lvert \htmlData{mx=17}{\htmlData{mx=15}{\htmlData{mx=13}{a}(\htmlData{mx=14}{i})} - \htmlData{mx=16}{p}} \right\rvert} \mathrel{\htmlData{mx=20}{\leq}} \htmlData{mx=19}{\varepsilon}})} \rvert}}$ , then

\begin{aligned} & (\htmlData{mx=33}{\exists t,\ \htmlData{mx=1}{k} \mathrel{\htmlData{mx=32}{\leq}} \htmlData{mx=31}{2 \cdot \htmlData{mx=30}{\lvert \htmlData{mx=29}{\htmlData{mx=16}{\operatorname{filter}}(\htmlData{mx=28}{j \mapsto \htmlData{mx=24}{\left\lvert \htmlData{mx=23}{\htmlData{mx=19}{\htmlData{mx=17}{a}(\htmlData{mx=18}{j})} - \htmlData{mx=22}{\htmlData{mx=20}{a}(\htmlData{mx=21}{t})}} \right\rvert} \mathrel{\htmlData{mx=27}{\leq}} \htmlData{mx=26}{2\htmlData{mx=25}{\varepsilon}}})} \rvert}}}) \\ & \htmlData{mx=0}{\land} \left(\right. \htmlData{mx=34}{\forall} t, \\ & \quad \htmlData{mx=36}{k} \mathrel{\htmlData{mx=67}{\leq}} \htmlData{mx=66}{2 \cdot \htmlData{mx=65}{\lvert \htmlData{mx=64}{\htmlData{mx=51}{\operatorname{filter}}(\htmlData{mx=63}{j \mapsto \htmlData{mx=59}{\left\lvert \htmlData{mx=58}{\htmlData{mx=54}{\htmlData{mx=52}{a}(\htmlData{mx=53}{j})} - \htmlData{mx=57}{\htmlData{mx=55}{a}(\htmlData{mx=56}{t})}} \right\rvert} \mathrel{\htmlData{mx=62}{\leq}} \htmlData{mx=61}{2\htmlData{mx=60}{\varepsilon}}})} \rvert}} \\ & \quad \htmlData{mx=35}{\implies} \htmlData{mx=73}{\left\lvert \htmlData{mx=72}{\htmlData{mx=70}{\htmlData{mx=68}{a}(\htmlData{mx=69}{t})} - \htmlData{mx=71}{p}} \right\rvert} \mathrel{\htmlData{mx=76}{\leq}} \htmlData{mx=75}{3\htmlData{mx=74}{\varepsilon}} \left.\right) \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
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 k. Lean writes f x; papers write f(x). (Fin k)
⟹Implies: If Fin(k), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin k → ℝ)
x ∈ TVariables: p, ε range over real numbers: the statement must hold for every choice. ((p ε : ℝ))
≤At most: 0 is less than or equal to ε. (0 ≤ ε)
<Less than: k is strictly smaller than 2 · card(filter(i ↦ |a(i) − p| ≤ ε)). (k < 2 * (Finset.univ.filter (fun i => |…)
∧And: Both hold: ∃ t, k ≤ 2 · card(filter(j ↦ |a(j) − a(t)| ≤ 2 · ε)), and ∀ t, k ≤ 2 · card(filter(j ↦ |a(j) − a(t)| ≤ 2 · ε)) → |a(…. ((∃ t, k ≤ 2 * (Finset.univ.filter (fun …)
∃There exists: At least one t makes the statement after the comma true. (∃ t, k ≤ 2 * (Finset.univ.filter (fun j…)
·Multiplication: 2 times card(filter(i ↦ |a(i) − p| ≤ ε)). (2 * (Finset.univ.filter (fun i => |a i …)
RReal numbers: The real numbers: every point on the number line. (ℝ)
|s|Cardinality: The number of elements of filter(i ↦ |a(i) − p| ≤ ε). ((Finset.univ.filter (fun i => |a i - p|…)
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 ↦ f(x)Function (λ-abstraction): The function sending i to |a(i) − p| ≤ ε. Lean writes fun x => …; papers write x ↦ …. (fun i => |a i - p| ≤ ε)
|x|Absolute value: The size of a(i) − p without its sign. (|a i - p|)
-Subtraction: a(i) minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (a i - p)
∀For all: The statement after the comma holds for every t. (∀ t, k ≤ 2 * (Finset.univ.filter (fun j…)

theorem rc-robust-center {k : ℕ} (a : Fin k → ℝ) (p ε : ℝ) (hε : 0 ≤ ε) (hmaj : k < 2 * (Finset.univ.filter (fun i => |a i - p| ≤ ε)).card) :
    (∃ t, k ≤ 2 * (Finset.univ.filter (fun j => |a j - a t| ≤ 2 * ε)).card) ∧ (∀ t, k ≤ 2 * (Finset.univ.filter (fun j => |a j - a t| ≤ 2 * ε)).card → |a t - p| ≤ 3 * ε)

A comparison-only rule: pick any estimate that has at least half of the estimates within 2ε of it; such an estimate exists, and every such estimate is within 3ε of the truth whenever a strict majority of estimates are ε-accurate. This replaces the median in the boosting step and needs no ordering argument. 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: 42 lines of Lean

Robust centre (median-free median-of-means): a strict majority of estimates within ε of p yields a selectable estimate within 3ε of p

How it was proved

More proved statements