Provedunbiased-attentionrandomized-algorithmssoftmaxhardness

Time accounting: for every δ > 0, k and C > 0, eventually C·(log n)^k·n^{2−δ} ≤ n^{2−δ/2}

For all $\htmlData{mx=1}{\delta, k, C \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\delta}$ and $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{C}$ , then

\htmlData{mx=18}{\forall^{\mathsf{f}} x \text{ in } \htmlData{mx=17}{\operatorname{atTop}},\ \htmlData{mx=10}{\htmlData{mx=5}{\htmlData{mx=0}{C} \cdot \htmlData{mx=4}{\htmlData{mx=2}{\log \htmlData{mx=1}{x}}^{\htmlData{mx=3}{k}}}} \cdot \htmlData{mx=9}{\htmlData{mx=6}{x}^{\htmlData{mx=8}{2 - \htmlData{mx=7}{\delta}}}}} \mathrel{\htmlData{mx=16}{\leq}} \htmlData{mx=15}{\htmlData{mx=11}{x}^{\htmlData{mx=14}{2 - \htmlData{mx=13}{\frac{\htmlData{mx=12}{\delta}}{2}}}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: δ, k, C range over real numbers: the statement must hold for every choice. ((δ k C : ℝ))
<Less than: 0 is strictly smaller than δ. (0 < δ)
∀ᶠEventually: The statement after the comma holds for all x far enough along atTop (for Filter.atTop: for all large enough x). (∀ᶠ x in Filter.atTop, C * Real.log x ^ …)
atTop: Filter.atTop: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Filter.atTop)
·Multiplication: C times log(x)^k. (C * Real.log x ^ k)
≤At most: C · log(x)^k · x^(2 − δ) is less than or equal to x^(2 − δ/2). (C * Real.log x ^ k * x ^ (2 - δ) ≤ x ^ …)
logNatural logarithm: The logarithm of x to base e: the power e must be raised to to give x. (Real.log x)
aᵇPower: log(x) raised to the power k. (Real.log x ^ k)
-Subtraction: 2 minus δ. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (2 - δ)
a/bDivision: δ divided by 2. In Lean, dividing by 0 gives 0. (δ / 2)

theorem ua-polylog-overhead-absorbed (δ k C : ℝ) (hδ : 0 < δ) (hC : 0 < C) :
    ∀ᶠ x in Filter.atTop, C * Real.log x ^ k * x ^ (2 - δ) ≤ x ^ (2 - δ / 2)

The arithmetic core of the reductions' time accounting: running an n^{2−δ} estimator O(log^k n) times (isolation levels × majority-vote amplification) is still n^{2−δ/2}, truly subquadratic, so it would refute SETH/OVC. Proven from Mathlib's (log x)^r = o(x^s). Part of 'Unbiased randomized attention: cost x variance thresholds', round 11 (time accounting).

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

Time accounting: for every δ > 0, k and C > 0, eventually C·(log n)^k·n^{2−δ} ≤ n^{2−δ/2}

How it was proved

More proved statements