Provedunbiased-attentionrandomized-algorithmssoftmaxfull-exponent

Exponent bookkeeping: n·n^α = n^{1+α}

For all $\htmlData{mx=1}{n, \alpha \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ , then

\htmlData{mx=4}{\htmlData{mx=0}{n} \cdot \htmlData{mx=3}{\htmlData{mx=1}{n}^{\htmlData{mx=2}{\alpha}}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{\htmlData{mx=5}{n}^{\htmlData{mx=7}{1 + \htmlData{mx=6}{\alpha}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: n, α range over real numbers: the statement must hold for every choice. ((n α : ℝ))
<Less than: 0 is strictly smaller than n. (0 < n)
·Multiplication: n times n^α. (n * n ^ α)
=Equality: n · n^α and n^(1 + α) are the same. (n * n ^ α = n ^ (1 + α))
aᵇPower: n raised to the power α. (n ^ α)
+Addition: 1 plus α. (1 + α)

theorem ua-exponent-one-plus-alpha (n α : ℝ) (hn : 0 < n) :
    n * n ^ α = n ^ (1 + α)

Uniform sampling costs n rows × e^R = n^α samples = n^{1+α}; the multiplicity gadget inherits the n^{1+α−o(1)} unbalanced-OV lower bound. Together: the exponent of constant-MSE attention at score range α ln n is exactly min(1+α, 2) (SETH, polylog dimension; candidate). Part of 'Unbiased randomized attention: cost x variance thresholds', round 12 (full exponent: multiplicity gadget for α < 1).

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

Exponent bookkeeping: n·n^α = n^{1+α}

How it was proved

More proved statements