Provedunbiased-attentionrandomized-algorithmssoftmaxgradient-hardness
Isolation: keeping each of t ≥ 1 partners w.p. p ∈ [1/(4t), 1/(2t)] leaves exactly one w.p. t p (1−p)^{t−1} ≥ 1/8
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. (
ℕ) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 1 is less than or equal to t. (
1 ≤ t) - a/bDivision
- 1 divided by 4 · t. In Lean, dividing by 0 gives 0. (
1 / (4 * t)) - ·Multiplication
- 4 times t. (
4 * t) - aᵇPower
- 1 − p raised to the power t − 1. (
(1 - p) ^ (t - 1)) - -Subtraction
- 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - p)
theorem ua-isolation-probability (t : ℕ) (p : ℝ) (ht : 1 ≤ t) (hp1 : 1 / (4 * t) ≤ p) (hp2 : p ≤ 1 / (2 * t)) :
1 / 8 ≤ t * p * (1 - p) ^ (t - 1)Bernoulli's inequality. Subsampling keys at rate 2^{−j} for the right j isolates a single partner in some YES row with constant probability (Valiant–Vazirani style), which removes the o → 1 obstruction of the gradient gadget. Part of 'Unbiased randomized attention: cost x variance thresholds', round 7 (gradient hardness via isolation).
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.