Provedunbiased-attentionrandomized-algorithmssoftmaxaggregate
A factor-2 estimate separates totals that differ by a factor 4
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
- Z, zhat, T range over real numbers: the statement must hold for every choice. (
(Z zhat T : ℝ)) - <Less than
- 0 is strictly smaller than T. (
0 < T) - a/bDivision
- Z divided by 2. In Lean, dividing by 0 gives 0. (
Z / 2) - ≤At most
- Z/2 is less than or equal to zhat. (
Z / 2 ≤ zhat) - ∧And
- Both hold: Z/2 ≤ zhat, and zhat ≤ 2 · Z. (
Z / 2 ≤ zhat ∧ zhat ≤ 2 * Z) - ⟹Implies
- If 4 · T ≤ Z, then 2 · T ≤ zhat. (Between types, A → B is the type of functions from A to B.) (
4 * T ≤ Z → 2 * T ≤ zhat) - ·Multiplication
- 2 times Z. (
2 * Z)
theorem ua-factor-two-separates (Z zhat T : ℝ) (hT : 0 < T) (hz : Z / 2 ≤ zhat ∧ zhat ≤ 2 * Z) :
(4 * T ≤ Z → 2 * T ≤ zhat) ∧ (Z ≤ T → zhat ≤ 2 * T)Z/2 ≤ ẑ ≤ 2Z: YES (Z ≥ 4T) gives ẑ ≥ 2T, NO (Z ≤ T) gives ẑ ≤ 2T, with the threshold T computable from n, β, s. 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
- 12 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.