Provedunbiased-attentionrandomized-algorithmssoftmaxaggregate
Aggregate gadget: M close copy-pairs at score β vs ≤ P pairs at score ≤ βs; β(1−s) ≥ log(4P/M) ⇒ YES total ≥ 4 × NO total
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
- P, M, β, s range over real numbers: the statement must hold for every choice. (
(P M β s : ℝ)) - <Less than
- 0 is strictly smaller than M. (
0 < M) - ≤At most
- M is less than or equal to 4 · P. (
M ≤ 4 * P) - logNatural logarithm
- The logarithm of 4 · P/M to base e: the power e must be raised to to give 4 · P/M. (
Real.log (4 * P / M)) - ·Multiplication
- 4 times P. (
4 * P) - eˣExponential function
- e raised to the power β · s, where e ≈ 2.718. (
Real.exp (β * s)) - a/bDivision
- 4 · P divided by M. In Lean, dividing by 0 gives 0. (
4 * P / M) - -Subtraction
- 1 minus s. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - s)
theorem ua-aggregate-gap (P M β s : ℝ) (hM : 0 < M) (hPM : M ≤ 4 * P) (hβ : 0 ≤ β) (hgap : Real.log (4 * P / M) ≤ β * (1 - s)) :
4 * (P * Real.exp (β * s)) ≤ M * Real.exp βFor the batch partition function Σ_{i,j} e^{s_ij} (the aggregate quantity of Charikar–Siminelakis 2019, Thm 1.2): unbalanced gap-MaxIP with n^θ × n^φ distinct vectors, both sides copied up to n, gives M = n^{2−α'} close copy-pairs (α' = θ + φ) against P = n² pairs. Part of 'Unbiased randomized attention: cost x variance thresholds', round 13 (aggregate / batch partition function).
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
- 22 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.