Provedunbiased-attentionend-to-endsoftmaxhardness

END-TO-END REDUCTION: gadget rows at β = log(4n)/(1−s); per-row MSE ≤ 1/512, k runs, majority at 3/8 ⇒ NO (all x ≤ s) vs YES (some x = 1) decided except w.p. ≤ m(7/8)^k

For all $\htmlData{mx=1}{m, n \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=9}{x : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{m}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{Fin}}\,\htmlData{mx=4}{n}} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ , $\htmlData{mx=1}{s \in \htmlData{mx=0}{\mathbb{R}}}$ , $\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}}}$ and $\htmlData{mx=1}{k \in \htmlData{mx=0}{\mathbb{N}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ , $\htmlData{mx=0}{s} \mathrel{\htmlData{mx=1}{<}} 1$ , $\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=48}{\forall i,\ \htmlData{mx=45}{\sum_{\omega} \htmlData{mx=44}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=43}{\left(\htmlData{mx=42}{\htmlData{mx=6}{\htmlData{mx=3}{z}(\htmlData{mx=4}{i}, \htmlData{mx=5}{\omega})} - \htmlData{mx=41}{\frac{\htmlData{mx=19}{\sum_{j} \htmlData{mx=18}{e^{\htmlData{mx=17}{\htmlData{mx=12}{\frac{\htmlData{mx=9}{\log (\htmlData{mx=8}{4\htmlData{mx=7}{n}})}}{\htmlData{mx=11}{1 - \htmlData{mx=10}{s}}}} \cdot \htmlData{mx=16}{\htmlData{mx=13}{x}(\htmlData{mx=14}{i}, \htmlData{mx=15}{j})}}}}}}{\htmlData{mx=40}{\htmlData{mx=26}{e^{\htmlData{mx=25}{\frac{\htmlData{mx=22}{\log (\htmlData{mx=21}{4\htmlData{mx=20}{n}})}}{\htmlData{mx=24}{1 - \htmlData{mx=23}{s}}}}}} + \htmlData{mx=39}{\sum_{j} \htmlData{mx=38}{e^{\htmlData{mx=37}{\htmlData{mx=32}{\frac{\htmlData{mx=29}{\log (\htmlData{mx=28}{4\htmlData{mx=27}{n}})}}{\htmlData{mx=31}{1 - \htmlData{mx=30}{s}}}} \cdot \htmlData{mx=36}{\htmlData{mx=33}{x}(\htmlData{mx=34}{i}, \htmlData{mx=35}{j})}}}}}}}}}\right)^{2}}}} \mathrel{\htmlData{mx=47}{\leq}} \htmlData{mx=46}{\frac{1}{512}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ ), then

\htmlData{mx=86}{\sum_{f \in \htmlData{mx=79}{\htmlData{mx=0}{\operatorname{filter}}\left(\htmlData{mx=78}{f \mapsto \htmlData{mx=72}{\lnot \left(\left((\htmlData{mx=7}{\forall i, j,\ \htmlData{mx=4}{\htmlData{mx=1}{x}(\htmlData{mx=2}{i}, \htmlData{mx=3}{j})} \mathrel{\htmlData{mx=6}{\leq}} \htmlData{mx=5}{s}}) \mathrel{\htmlData{mx=36}{\implies}} \htmlData{mx=35}{\forall i,\ \htmlData{mx=34}{\lnot \htmlData{mx=8}{k} \mathrel{\htmlData{mx=33}{\leq}} \htmlData{mx=32}{2 \cdot \htmlData{mx=31}{\lvert \htmlData{mx=30}{\htmlData{mx=20}{\operatorname{filter}}\left(\htmlData{mx=29}{r \mapsto \htmlData{mx=21}{\frac{3}{8}} \mathrel{\htmlData{mx=28}{\leq}} \htmlData{mx=27}{\htmlData{mx=22}{z}(\htmlData{mx=23}{i}, \htmlData{mx=26}{\htmlData{mx=24}{f}(\htmlData{mx=25}{r})})}}\right)} \rvert}}}}\right) \mathbin{\htmlData{mx=71}{\land}} \left((\htmlData{mx=42}{\exists i, j,\ \htmlData{mx=40}{\htmlData{mx=37}{x}(\htmlData{mx=38}{i}, \htmlData{mx=39}{j})} \mathrel{\htmlData{mx=41}{=}} 1}) \mathrel{\htmlData{mx=70}{\implies}} \htmlData{mx=69}{\exists i,\ \htmlData{mx=43}{k} \mathrel{\htmlData{mx=68}{\leq}} \htmlData{mx=67}{2 \cdot \htmlData{mx=66}{\lvert \htmlData{mx=65}{\htmlData{mx=55}{\operatorname{filter}}\left(\htmlData{mx=64}{r \mapsto \htmlData{mx=56}{\frac{3}{8}} \mathrel{\htmlData{mx=63}{\leq}} \htmlData{mx=62}{\htmlData{mx=57}{z}(\htmlData{mx=58}{i}, \htmlData{mx=61}{\htmlData{mx=59}{f}(\htmlData{mx=60}{r})})}}\right)} \rvert}}}\right)\right)}}\right)}} \htmlData{mx=85}{\prod_{r} \htmlData{mx=84}{\htmlData{mx=80}{w}(\htmlData{mx=83}{\htmlData{mx=81}{f}(\htmlData{mx=82}{r})})}}} \mathrel{\htmlData{mx=93}{\leq}} \htmlData{mx=92}{\htmlData{mx=87}{m} \cdot \htmlData{mx=91}{\htmlData{mx=89}{\htmlData{mx=88}{\frac{7}{8}}}^{\htmlData{mx=90}{k}}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: m, n range over natural numbers: the statement must hold for every choice. ((m n : ℕ))
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 Ω)
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)
<Less than: 0 is strictly smaller than n. (0 < n)
∀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)
≤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)
⟹Implies: If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin n → ℝ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
aᵇPower: z(i, ω) − (∑ j, exp(log(4 · n)/(1 − s) · x(i, j)))/(exp(lo… raised to the power 2. ((z i ω - (∑ j, Real.exp (Real.log (4 * …)
eˣExponential function: e raised to the power log(4 · n)/(1 − s) · x(i, j), where e ≈ 2.718. (Real.exp (Real.log (4 * n) / (1 - s) * …)
logNatural logarithm: The logarithm of 4 · n to base e: the power e must be raised to to give 4 · n. (Real.log (4 * n))
a/bDivision: log(4 · n) divided by 1 − s. In Lean, dividing by 0 gives 0. (Real.log (4 * n) / (1 - s))
·Multiplication: 4 times n. (4 * n)
∧And: Both hold: (∀ i, j, x(i, j) ≤ s) → (∀ i, ¬(k ≤ 2 · card(filter(r ↦ 3/…, and (∃ i, j, x(i, j) = 1) → (∃ i, k ≤ 2 · card(filter(r ↦ 3/8 …. (((∀ i j, x i j ≤ s) → ∀ i, ¬ (k ≤ 2 * (…)
-Subtraction: 1 minus s. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - s)
¬Not: It is not the case that k ≤ 2 · card(filter(r ↦ 3/8 ≤ z(i, f(r)))). (¬ (k ≤ 2 * (Finset.univ.filter (fun r =…)
+Addition: exp(log(4 · n)/(1 − s)) plus ∑ j, exp(log(4 · n)/(1 − s) · x(i, j)). (Real.exp (Real.log (4 * n) / (1 - s)) +…)
|s|Cardinality: The number of elements of filter(r ↦ 3/8 ≤ z(i, f(r))). ((Finset.univ.filter (fun r => 3 / 8 ≤ z…)
x ↦ f(x)Function (λ-abstraction): The function sending r to 3/8 ≤ z(i, f(r)). Lean writes fun x => …; papers write x ↦ …. (fun r => 3 / 8 ≤ z i (f r))
∃There exists: At least one i, j makes the statement after the comma true. (∃ i j, x i j = 1)
∏Product: Multiply together w(f(r)) for every r. (∏ r, w (f r))
(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-reduction {m n : ℕ} {Ω : Type} [Fintype Ω] (x : Fin m → Fin n → ℝ) (s : ℝ) (hn : 0 < n) (hs : s < 1) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (z : Fin m → Ω → ℝ) (hmse : ∀ i, ∑ ω, w ω * (z i ω - (∑ j, Real.exp (Real.log (4 * n) / (1 - s) * x i j)) / (Real.exp (Real.log (4 * n) / (1 - s)) + ∑ j, Real.exp (Real.log (4 * n) / (1 - s) * x i j))) ^ 2 ≤ 1 / 512) (k : ℕ) :
    ∑ f ∈ Finset.univ.filter (fun f : Fin k → Ω => ¬ ( ((∀ i j, x i j ≤ s) → ∀ i, ¬ (k ≤ 2 * (Finset.univ.filter (fun r => 3 / 8 ≤ z i (f r))).card)) ∧ ((∃ i j, x i j = 1) → ∃ i, k ≤ 2 * (Finset.univ.filter (fun r => 3 / 8 ≤ z i (f r))).card))), ∏ r, w (f r) ≤ m * (7 / 8 : ℝ) ^ k

Fourth single-statement composition: the whole-instance gadget (ua-reduction-all-rows) composed with the hard-side decision/amplification/union bound (ua-end-to-end-hard-side), both inlined as universally quantified haves. Together with ua-tensor-power-inner-product (soundness amplification), ua-amplification-run-count (k = O(log m)) and ua-polylog-overhead-absorbed (time accounting), only SETH/OVC and Rubinstein's vector construction remain outside Lean in the sharp-threshold hardness argument. 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: 186 lines of Lean

END-TO-END REDUCTION: gadget rows at β = log(4n)/(1−s); per-row MSE ≤ 1/512, k runs, majority at 3/8 ⇒ NO (all x ≤ s) vs YES (some x = 1) decided except w.p. ≤ m(7/8)^k

How it was proved

More proved statements