Provedunbiased-attentionrandomized-algorithmssoftmaxfull-exponent
Multiplicity gadget YES: value-1 mass ≥ baseline mass m·e^β ⇒ output ≥ 1/2
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
- S, m, β range over real numbers: the statement must hold for every choice. (
(S m β : ℝ)) - <Less than
- 0 is strictly smaller than m. (
0 < m) - ·Multiplication
- m times exp(β). (
m * Real.exp β) - ≤At most
- m · exp(β) is less than or equal to S. (
m * Real.exp β ≤ S) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 2) - eˣExponential function
- e raised to the power β, where e ≈ 2.718. (
Real.exp β) - +Addition
- m · exp(β) plus S. (
m * Real.exp β + S)
theorem ua-multiplicity-gap-yes (S m β : ℝ) (hm : 0 < m) (hS : m * Real.exp β ≤ S) :
1 / 2 ≤ S / (m * Real.exp β + S)For α < 1: start from unbalanced OV (n queries, n^α distinct keys), copy each key m = n^{1−α} times and add m value-0 baseline keys at the top score β. A query with an orthogonal partner has m partner copies at score β, so its output is ≥ 1/2. Part of 'Unbiased randomized attention: cost x variance thresholds', round 12 (full exponent: multiplicity gadget for α < 1).
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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.