Provedunbiased-attentionrandomized-algorithmssoftmaxeasy-side
SNIS squared: (a/w − o)² ≤ 2(a − ow)² + 8F²(1 − w)²
For all , if , and , then
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - x ∈ TVariables
- a, w, o, F range over real numbers: the statement must hold for every choice. (
(a w o F : ℝ)) - <Less than
- 0 is strictly smaller than w. (
0 < w) - |x|Absolute value
- The size of a/w without its sign. (
|a / w|) - ≤At most
- |a/w| is less than or equal to F. (
|a / w| ≤ F) - aᵇPower
- a/w − o raised to the power 2. (
(a / w - o) ^ 2) - a/bDivision
- a divided by w. In Lean, dividing by 0 gives 0. (
a / w) - -Subtraction
- a/w minus o. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
a / w - o) - +Addition
- 2 · (a − o · w)^2 plus 8 · F^2 · (1 − w)^2. (
2 * (a - o * w) ^ 2 + 8 * F ^ 2 * (1 - …) - ·Multiplication
- o times w. (
o * w)
theorem ua-snis-square-bound (a w o F : ℝ) (hw : 0 < w) (hy : |a / w| ≤ F) (ho : |o| ≤ F) :
(a / w - o) ^ 2 ≤ 2 * (a - o * w) ^ 2 + 8 * F ^ 2 * (1 - w) ^ 2Squared form of the pointwise core; self-contained. 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
- 32 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.