Provedunbiased-attentionrandomized-algorithmssoftmaxdebiasing

Explicit level law p_l ∝ 1/c_l: V_l ≤ A/c_l ⇒ cost × variance ≤ L²·A

For all $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{c, V : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{L}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ and $\htmlData{mx=1}{A \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall l,\ 0 \mathrel{\htmlData{mx=3}{<}} \htmlData{mx=2}{\htmlData{mx=0}{c}(\htmlData{mx=1}{l})}}$ and $\htmlData{mx=9}{\forall l,\ \htmlData{mx=2}{\htmlData{mx=0}{V}(\htmlData{mx=1}{l})} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\frac{\htmlData{mx=3}{A}}{\htmlData{mx=6}{\htmlData{mx=4}{c}(\htmlData{mx=5}{l})}}}}$ , then

\begin{aligned} & \htmlData{mx=31}{\left(\htmlData{mx=15}{\sum_{l} \htmlData{mx=14}{\htmlData{mx=10}{\frac{\htmlData{mx=4}{\frac{1}{\htmlData{mx=3}{\htmlData{mx=1}{c}(\htmlData{mx=2}{l})}}}}{\htmlData{mx=9}{\sum_{m} \htmlData{mx=8}{\frac{1}{\htmlData{mx=7}{\htmlData{mx=5}{c}(\htmlData{mx=6}{m})}}}}}} \cdot \htmlData{mx=13}{\htmlData{mx=11}{c}(\htmlData{mx=12}{l})}}}\right) \cdot \left(\htmlData{mx=30}{\sum_{l} \htmlData{mx=29}{\frac{\htmlData{mx=18}{\htmlData{mx=16}{V}(\htmlData{mx=17}{l})}}{\htmlData{mx=28}{\frac{\htmlData{mx=22}{\frac{1}{\htmlData{mx=21}{\htmlData{mx=19}{c}(\htmlData{mx=20}{l})}}}}{\htmlData{mx=27}{\sum_{m} \htmlData{mx=26}{\frac{1}{\htmlData{mx=25}{\htmlData{mx=23}{c}(\htmlData{mx=24}{m})}}}}}}}}}\right)} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=36}{\htmlData{mx=34}{\htmlData{mx=33}{\htmlData{mx=32}{L}}^{2}} \cdot \htmlData{mx=35}{A}} \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 L. Lean writes f x; papers write f(x). (Fin L)
⟹Implies: If Fin(L), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin L → ℝ)
x : TVariables: c, V range over Fin L → ℝ: the statement must hold for every choice. ((c V : Fin L → ℝ))
∀For all: The statement after the comma holds for every l. (∀ l, 0 < c l)
<Less than: 0 is strictly smaller than c(l). (0 < c l)
≤At most: V(l) is less than or equal to A/c(l). (V l ≤ A / c l)
·Multiplication: 1/c(l)/(∑ m, 1/c(m)) times c(l). (((1 / c l) / ∑ m, 1 / c m) * c l)
RReal numbers: The real numbers: every point on the number line. (ℝ)
a/bDivision: A divided by c(l). In Lean, dividing by 0 gives 0. (A / c l)
∑Summation: Add up 1/c(m) for every m. (∑ m, 1 / c m)
(x : T)As real numbers: L read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((L : ℝ))
aᵇPower: L raised to the power 2. ((L : ℝ) ^ 2)

theorem ua-mlmc-inverse-cost-allocation {L : ℕ} (c V : Fin L → ℝ) (A : ℝ) (hc : ∀ l, 0 < c l) (hV : ∀ l, V l ≤ A / c l) :
    (∑ l, ((1 / c l) / ∑ m, 1 / c m) * c l) * (∑ l, V l / ((1 / c l) / ∑ m, 1 / c m)) ≤ (L : ℝ) ^ 2 * A

Composes the debiasing side: with level costs c_l and level variances V_l ≤ A/c_l (which the SNIS bound gives with A = O(F²(1+χ²))), the inverse-cost level law achieves expected cost × variance ≤ L²A. 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: 29 lines of Lean

Explicit level law p_l ∝ 1/c_l: V_l ≤ A/c_l ⇒ cost × variance ≤ L²·A

How it was proved

More proved statements