Provedunbiased-attentionrandomized-algorithmssoftmaxhardness

Augmented embedding: q·k_c − q·k_base = −(β/d)(dist(a,c) − θ)

For all $\htmlData{mx=1}{d \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{a, c : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{d}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{\beta, \theta \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=1}{\htmlData{mx=0}{d}} \mathrel{\htmlData{mx=2}{\neq}} 0$ , then

\begin{aligned} & \htmlData{mx=61}{\htmlData{mx=33}{\htmlData{mx=23}{\htmlData{mx=13}{\sum_{i} \htmlData{mx=12}{\htmlData{mx=8}{\htmlData{mx=4}{\frac{\htmlData{mx=2}{2\htmlData{mx=1}{\beta}}}{\htmlData{mx=3}{d}}} \cdot \htmlData{mx=7}{\htmlData{mx=5}{a}(\htmlData{mx=6}{i})}} \cdot \htmlData{mx=11}{\htmlData{mx=9}{c}(\htmlData{mx=10}{i})}}} + \htmlData{mx=22}{\htmlData{mx=16}{\frac{\htmlData{mx=14}{\beta}}{\htmlData{mx=15}{d}}} \cdot \htmlData{mx=21}{-\left(\htmlData{mx=20}{\sum_{i} \htmlData{mx=19}{\htmlData{mx=17}{c}(\htmlData{mx=18}{i})}}\right)}}} + \htmlData{mx=32}{\htmlData{mx=31}{\frac{\htmlData{mx=29}{\htmlData{mx=24}{\beta} \cdot \left(\htmlData{mx=28}{\sum_{i} \htmlData{mx=27}{\htmlData{mx=25}{a}(\htmlData{mx=26}{i})}}\right)}}{\htmlData{mx=30}{d}}} \cdot 0}} - \left(\htmlData{mx=60}{\htmlData{mx=50}{\left(\htmlData{mx=43}{\sum_{i} \htmlData{mx=42}{\htmlData{mx=41}{\htmlData{mx=37}{\frac{\htmlData{mx=35}{2\htmlData{mx=34}{\beta}}}{\htmlData{mx=36}{d}}} \cdot \htmlData{mx=40}{\htmlData{mx=38}{a}(\htmlData{mx=39}{i})}} \cdot 0}}\right) + \htmlData{mx=49}{\htmlData{mx=46}{\frac{\htmlData{mx=44}{\beta}}{\htmlData{mx=45}{d}}} \cdot \htmlData{mx=48}{-\htmlData{mx=47}{\theta}}}} + \htmlData{mx=59}{\htmlData{mx=58}{\frac{\htmlData{mx=56}{\htmlData{mx=51}{\beta} \cdot \left(\htmlData{mx=55}{\sum_{i} \htmlData{mx=54}{\htmlData{mx=52}{a}(\htmlData{mx=53}{i})}}\right)}}{\htmlData{mx=57}{d}}} \cdot 1}}\right)} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=87}{\htmlData{mx=65}{-\htmlData{mx=64}{\frac{\htmlData{mx=62}{\beta}}{\htmlData{mx=63}{d}}}} \cdot \left(\htmlData{mx=86}{\htmlData{mx=84}{\htmlData{mx=74}{\htmlData{mx=69}{\sum_{i} \htmlData{mx=68}{\htmlData{mx=66}{a}(\htmlData{mx=67}{i})}} + \htmlData{mx=73}{\sum_{i} \htmlData{mx=72}{\htmlData{mx=70}{c}(\htmlData{mx=71}{i})}}} - \htmlData{mx=83}{2 \cdot \htmlData{mx=82}{\sum_{i} \htmlData{mx=81}{\htmlData{mx=77}{\htmlData{mx=75}{a}(\htmlData{mx=76}{i})} \cdot \htmlData{mx=80}{\htmlData{mx=78}{c}(\htmlData{mx=79}{i})}}}}} - \htmlData{mx=85}{\theta}}\right)} \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
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)
f(x)Function application: Fin applied to d. Lean writes f x; papers write f(x). (Fin d)
⟹Implies: If Fin(d), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin d → ℝ)
x : TVariables: a, c range over Fin d → ℝ: the statement must hold for every choice. ((a c : Fin d → ℝ))
x ∈ TVariables: β, θ range over real numbers: the statement must hold for every choice. ((β θ : ℝ))
(x : T)As real numbers: d read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((d : ℝ))
≠Not equal: d and 0 are different. ((d : ℝ) ≠ 0)
-Subtraction: (∑ i, 2 · β/d · a(i) · c(i)) + β/d · −(∑ i, c(i)) + β · (∑… minus (∑ i, 2 · β/d · a(i) · 0) + β/d · −θ + β · (∑ i, a(i))/d · 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. ((∑ i, (2 * β / d * a i) * c i + (β / d)…)
=Equality: (∑ i, 2 · β/d · a(i) · c(i)) + β/d · −(∑ i, c(i)) + β · (∑… and −(β/d) · ((∑ i, a(i)) + (∑ i, c(i)) − 2 · (∑ i, a(i) · c(i… are the same. ((∑ i, (2 * β / d * a i) * c i + (β / d)…)
∑Summation: Add up 2 · β/d · a(i) · c(i) for every i. (∑ i, (2 * β / d * a i) * c i)
+Addition: ∑ i, 2 · β/d · a(i) · c(i) plus β/d · −(∑ i, c(i)). (∑ i, (2 * β / d * a i) * c i + (β / d) …)
·Multiplication: 2 times β. (2 * β)
a/bDivision: 2 · β divided by d. In Lean, dividing by 0 gives 0. (2 * β / d)
RReal numbers: The real numbers: every point on the number line. (ℝ)
−xNegation: The negative of ∑ i, c(i). (-(∑ i, c i))

theorem ua-augmented-scores {d : ℕ} (a c : Fin d → ℝ) (β θ : ℝ) (hd : (d : ℝ) ≠ 0) :
    (∑ i, (2 * β / d * a i) * c i + (β / d) * (-(∑ i, c i)) + (β * (∑ i, a i) / d) * 0) - ((∑ i, (2 * β / d * a i) * 0) + (β / d) * (-θ) + (β * (∑ i, a i) / d) * 1) = -(β / d) * ((∑ i, a i + ∑ i, c i - 2 * ∑ i, a i * c i) - θ)

With q = (2β/d·a, β/d, β|a|/d), k_c = (c, −|c|, 0), k_base = (0, −θ, 1), the score of key c relative to the shared baseline key is exactly −(β/d)(Hamming(a,c) − θ). Feeding a (1+ε)-gap Hamming closest-pair instance (Rubinstein 2018) with θ = (1+ε/2)t and β ε t/(2d) ≥ ln(4n) into the range-aware gap lemmas gives score range ≤ β = O(log n / (ε·t/d)). Part of 'Unbiased randomized attention: cost x variance thresholds' (open theory problem), round 2.

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

Augmented embedding: q·k_c − q·k_base = −(β/d)(dist(a,c) − θ)

How it was proved

More proved statements