Provedunbiased-attentionrandomized-algorithmssoftmaxdebiasing

Level differences: (Y₁ − Y₀)² ≤ 2(Y₁ − o)² + 2(Y₀ − o)²

For all $\htmlData{mx=1}{y_{1}, y_{0}, o \in \htmlData{mx=0}{\mathbb{R}}}$ :

\htmlData{mx=3}{(\htmlData{mx=2}{\htmlData{mx=0}{y_{1}} - \htmlData{mx=1}{y_{0}}})^{2}} \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{\htmlData{mx=8}{2 \cdot \htmlData{mx=7}{(\htmlData{mx=6}{\htmlData{mx=4}{y_{1}} - \htmlData{mx=5}{o}})^{2}}} + \htmlData{mx=13}{2 \cdot \htmlData{mx=12}{(\htmlData{mx=11}{\htmlData{mx=9}{y_{0}} - \htmlData{mx=10}{o}})^{2}}}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: y1, y0, o range over real numbers: the statement must hold for every choice. ((y1 y0 o : ℝ))
aᵇPower: y1 − y0 raised to the power 2. ((y1 - y0) ^ 2)
≤At most: (y1 − y0)^2 is less than or equal to 2 · (y1 − o)^2 + 2 · (y0 − o)^2. ((y1 - y0) ^ 2 ≤ 2 * (y1 - o) ^ 2 + 2 * …)
-Subtraction: y1 minus y0. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (y1 - y0)
·Multiplication: 2 times (y1 − o)^2. (2 * (y1 - o) ^ 2)
+Addition: 2 · (y1 − o)^2 plus 2 · (y0 − o)^2. (2 * (y1 - o) ^ 2 + 2 * (y0 - o) ^ 2)

theorem ua-level-difference-bound (y1 y0 o : ℝ) :
    (y1 - y0) ^ 2 ≤ 2 * (y1 - o) ^ 2 + 2 * (y0 - o) ^ 2

So V_l ≤ 2(MSE_{l+1} + MSE_l): level variances inherit the SNIS 1/N rate. 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: 10 lines of Lean

Level differences: (Y₁ − Y₀)² ≤ 2(Y₁ − o)² + 2(Y₀ − o)²

How it was proved

More proved statements