Provedunbiased-attentionrandomized-algorithmssoftmaxaggregate

Per-row NO bound at precision n^{−θ}: β(1−s) ≥ log(8 N n^θ / m) ⇒ N e^{βs}/(m e^β) ≤ n^{−θ}/8

For all $\htmlData{mx=1}{N, m, n, \theta, \beta, s \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{m}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{n}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{N}$ , $0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{\beta}$ , $0 \mathrel{\htmlData{mx=8}{<}} \htmlData{mx=7}{\frac{\htmlData{mx=5}{\htmlData{mx=1}{8\htmlData{mx=0}{N}} \cdot \htmlData{mx=4}{\htmlData{mx=2}{n}^{\htmlData{mx=3}{\theta}}}}}{\htmlData{mx=6}{m}}}$ and $\htmlData{mx=8}{\log \left(\htmlData{mx=7}{\frac{\htmlData{mx=5}{\htmlData{mx=1}{8\htmlData{mx=0}{N}} \cdot \htmlData{mx=4}{\htmlData{mx=2}{n}^{\htmlData{mx=3}{\theta}}}}}{\htmlData{mx=6}{m}}}\right)} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{\htmlData{mx=9}{\beta} \cdot (\htmlData{mx=11}{1 - \htmlData{mx=10}{s}})}$ , then

\htmlData{mx=10}{\frac{\htmlData{mx=5}{\htmlData{mx=0}{N} \cdot \htmlData{mx=4}{e^{\htmlData{mx=3}{\htmlData{mx=1}{\beta} \cdot \htmlData{mx=2}{s}}}}}}{\htmlData{mx=9}{\htmlData{mx=6}{m} \cdot \htmlData{mx=8}{e^{\htmlData{mx=7}{\beta}}}}}} \mathrel{\htmlData{mx=16}{\leq}} \htmlData{mx=15}{\frac{\htmlData{mx=14}{\htmlData{mx=11}{n}^{\htmlData{mx=13}{-\htmlData{mx=12}{\theta}}}}}{8}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: N, m, n, θ, β, s range over real numbers: the statement must hold for every choice. ((N m n θ β s : ℝ))
<Less than: 0 is strictly smaller than m. (0 < m)
≤At most: 0 is less than or equal to N. (0 ≤ N)
logNatural logarithm: The logarithm of 8 · N · n^θ/m to base e: the power e must be raised to to give 8 · N · n^θ/m. (Real.log (8 * N * n ^ θ / m))
·Multiplication: 8 times N. (8 * N)
a/bDivision: 8 · N · n^θ divided by m. In Lean, dividing by 0 gives 0. (8 * N * n ^ θ / m)
eˣExponential function: e raised to the power β · s, where e ≈ 2.718. (Real.exp (β * s))
aᵇPower: n raised to the power θ. (n ^ θ)
-Subtraction: 1 minus s. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - s)
−xNegation: The negative of θ. (-θ)

theorem ua-row-bound-at-precision (N m n θ β s : ℝ) (hm : 0 < m) (hn : 0 < n) (hN : 0 ≤ N) (hβ : 0 ≤ β) (hpos : 0 < 8 * N * n ^ θ / m) (hgap : Real.log (8 * N * n ^ θ / m) ≤ β * (1 - s)) :
    N * Real.exp (β * s) / (m * Real.exp β) ≤ n ^ (-θ) / 8

With n^θ distinct queries copied n^{1−θ} times and n^φ distinct keys copied n^{1−φ} times (N = n keys, m = n^{1−φ} baseline copies), every NO row has output ≤ n^{−θ}/8 at score range ≈ (θ+φ) ln n, while a YES instance has n^{1−θ} rows ≥ 1/2. So constant-relative-error estimation of Σ_i o_i at range a ln n needs n^{a−o(1)} (unbalanced OV): relative-error aggregates of outputs are at least as hard as the partition-function aggregate. Part of 'Unbiased randomized attention: cost x variance thresholds', round 14 (aggregates of attention outputs).

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

Per-row NO bound at precision n^{−θ}: β(1−s) ≥ log(8 N n^θ / m) ⇒ N e^{βs}/(m e^β) ≤ n^{−θ}/8

How it was proved

More proved statements