Provedunbiased-attentionrandomized-algorithmssoftmaxfull-exponent
Multiplicity gadget NO: N keys with x ≤ s, baseline mass m·e^β, β = log(4N/m)/(1−s) ⇒ output ≤ 1/4
For all , and , if , , , and , then
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 N. Lean writes f x; papers write f(x). (
Fin N) - ⟹Implies
- If Fin(N), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin N → ℝ) - x ∈ TVariables
- m, s range over real numbers: the statement must hold for every choice. (
(m s : ℝ)) - <Less than
- 0 is strictly smaller than m. (
0 < m) - ≤At most
- 0 is less than or equal to s. (
0 ≤ s) - ∀For all
- The statement after the comma holds for every k. (
∀ k, x k ≤ s) - ∑Summation
- Add up exp(log(4 · N/m)/(1 − s) · x(k)) for every k. (
∑ k, Real.exp (Real.log (4 * N / m) / (…) - ·Multiplication
- 4 times N. (
4 * N) - eˣExponential function
- e raised to the power log(4 · N/m)/(1 − s) · x(k), where e ≈ 2.718. (
Real.exp (Real.log (4 * N / m) / (1 - s…) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - logNatural logarithm
- The logarithm of 4 · N/m to base e: the power e must be raised to to give 4 · N/m. (
Real.log (4 * N / m)) - a/bDivision
- 4 · N divided by m. In Lean, dividing by 0 gives 0. (
4 * N / m) - -Subtraction
- 1 minus s. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - s) - +Addition
- m · exp(log(4 · N/m)/(1 − s)) plus ∑ k, exp(log(4 · N/m)/(1 − s) · x(k)). (
m * Real.exp (Real.log (4 * N / m) / (1…)
theorem ua-multiplicity-gap-no {N : ℕ} (x : Fin N → ℝ) (m s : ℝ) (hm : 0 < m) (hs0 : 0 ≤ s) (hs : s < 1) (hNm : m ≤ 4 * N) (hx : ∀ k, x k ≤ s) :
(∑ k, Real.exp (Real.log (4 * N / m) / (1 - s) * x k)) / (m * Real.exp (Real.log (4 * N / m) / (1 - s)) + ∑ k, Real.exp (Real.log (4 * N / m) / (1 - s) * x k)) ≤ 1 / 4All N = n value-1 keys weigh ≤ e^{βs} each, and 4N e^{βs} = m e^β exactly at this β. 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
- 32 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.