Provedunbiased-attentionend-to-endsoftmaxhardness

END-TO-END hard side: per-row MSE ≤ 1/512 on a finite space ⇒ over k independent runs, P(some row's majority vote at threshold 1/8 is wrong) ≤ m·(7/8)^k

For all $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{w : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=7}{z : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{m}} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=3}{\Omega} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ , $\htmlData{mx=5}{o : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{m}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ , if $\htmlData{mx=4}{\forall \omega,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}}$ , $\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1$ and $\htmlData{mx=16}{\forall i,\ \htmlData{mx=13}{\sum_{\omega} \htmlData{mx=12}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=11}{(\htmlData{mx=10}{\htmlData{mx=6}{\htmlData{mx=3}{z}(\htmlData{mx=4}{i}, \htmlData{mx=5}{\omega})} - \htmlData{mx=9}{\htmlData{mx=7}{o}(\htmlData{mx=8}{i})}})^{2}}}} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{\frac{1}{512}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ ), then

\htmlData{mx=51}{\sum_{f \in \htmlData{mx=44}{\htmlData{mx=0}{\operatorname{filter}}\left(\htmlData{mx=43}{f \mapsto \htmlData{mx=37}{\exists i,\ \htmlData{mx=1}{k} \mathrel{\htmlData{mx=36}{\leq}} \htmlData{mx=35}{2 \cdot \htmlData{mx=34}{\lvert \htmlData{mx=33}{\htmlData{mx=18}{\operatorname{filter}}\left(\htmlData{mx=32}{j \mapsto \htmlData{mx=19}{\frac{1}{8}} \mathrel{\htmlData{mx=31}{\leq}} \htmlData{mx=30}{\left\lvert \htmlData{mx=29}{\htmlData{mx=25}{\htmlData{mx=20}{z}(\htmlData{mx=21}{i}, \htmlData{mx=24}{\htmlData{mx=22}{f}(\htmlData{mx=23}{j})})} - \htmlData{mx=28}{\htmlData{mx=26}{o}(\htmlData{mx=27}{i})}} \right\rvert}}\right)} \rvert}}}}\right)}} \htmlData{mx=50}{\prod_{j} \htmlData{mx=49}{\htmlData{mx=45}{w}(\htmlData{mx=48}{\htmlData{mx=46}{f}(\htmlData{mx=47}{j})})}}} \mathrel{\htmlData{mx=58}{\leq}} \htmlData{mx=57}{\htmlData{mx=52}{m} \cdot \htmlData{mx=56}{\htmlData{mx=54}{\htmlData{mx=53}{\frac{7}{8}}}^{\htmlData{mx=55}{k}}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to Ω. Lean writes f x; papers write f(x). (Fintype Ω)
⟹Implies: If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω → ℝ)
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)
∀For all: The statement after the comma holds for every ω. (∀ ω, 0 ≤ w ω)
∑Summation: Add up w(ω) for every ω. (∑ ω, w ω)
=Equality: ∑ ω, w(ω) and 1 are the same. (∑ ω, w ω = 1)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w(ω). (0 ≤ w ω)
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)
·Multiplication: w(ω) times (z(i, ω) − o(i))^2. (w ω * (z i ω - o i) ^ 2)
aᵇPower: z(i, ω) − o(i) raised to the power 2. ((z i ω - o i) ^ 2)
-Subtraction: z(i, ω) minus o(i). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (z i ω - o i)
a/bDivision: 1 divided by 512. In Lean, dividing by 0 gives 0. (1 / 512)
∃There exists: At least one i makes the statement after the comma true. (∃ i, k ≤ 2 * (Finset.univ.filter (fun j…)
|s|Cardinality: The number of elements of filter(j ↦ 1/8 ≤ |z(i, f(j)) − o(i)|). ((Finset.univ.filter (fun j => 1 / 8 ≤ |…)
x ↦ f(x)Function (λ-abstraction): The function sending j to 1/8 ≤ |z(i, f(j)) − o(i)|. Lean writes fun x => …; papers write x ↦ …. (fun j => 1 / 8 ≤ |z i (f j) - o i|)
|x|Absolute value: The size of z(i, f(j)) − o(i) without its sign. (|z i (f j) - o i|)
∏Product: Multiply together w(f(j)) for every j. (∏ j, w (f j))
(x : T)As real numbers: 7/8 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((7 / 8 : ℝ))

theorem ua-end-to-end-hard-side {m : ℕ} {Ω : Type} [Fintype Ω] (w : Ω → ℝ) (z : Fin m → Ω → ℝ) (o : Fin m → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (hmse : ∀ i, ∑ ω, w ω * (z i ω - o i) ^ 2 ≤ 1 / 512) (k : ℕ) :
    ∑ f ∈ Finset.univ.filter (fun f : Fin k → Ω => ∃ i, k ≤ 2 * (Finset.univ.filter (fun j => 1 / 8 ≤ |z i (f j) - o i|)).card), ∏ j, w (f j) ≤ m * (7 / 8 : ℝ) ^ k

Third single-statement composition (external review asked for end-to-end claims): Chebyshev per row (MSE ≤ 1/512 ⇒ failure ≤ 1/8, leaving Markov-truncation slack as the reviewer requested), exponential-moment majority-vote amplification (inlined), and the union bound over m rows via indicators, all on the exact k-fold product space. With k ≥ log(3m)/log(8/7) every row of the OV/MaxIP gadget is decided correctly with probability ≥ 2/3, which is what the SETH reduction consumes. Part of 'Unbiased randomized attention: cost x variance thresholds' (end-to-end composition round).

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: 105 lines of Lean

END-TO-END hard side: per-row MSE ≤ 1/512 on a finite space ⇒ over k independent runs, P(some row's majority vote at threshold 1/8 is wrong) ≤ m·(7/8)^k

How it was proved

More proved statements