Provedunbiased-attentionrandomized-algorithmssoftmaxgradient-hardness

Random grid level: success ≥ 1/8 at one of J+1 equally likely levels gives overall success ≥ 1/(8(J+1))

For all $\htmlData{mx=1}{J \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=6}{q : \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=2}{\htmlData{mx=1}{J} + 1}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ and $\htmlData{mx=4}{j_{0} \in \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=2}{\htmlData{mx=1}{J} + 1}}}$ , if $\htmlData{mx=4}{\forall j,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{q}(\htmlData{mx=1}{j})}}$ and $\htmlData{mx=0}{\frac{1}{8}} \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\htmlData{mx=1}{q}(\htmlData{mx=2}{j_{0}})}$ , then

\htmlData{mx=4}{\frac{1}{\htmlData{mx=3}{8(\htmlData{mx=2}{\htmlData{mx=1}{\htmlData{mx=0}{J}} + 1})}}} \mathrel{\htmlData{mx=14}{\leq}} \htmlData{mx=13}{\sum_{j} \htmlData{mx=12}{\htmlData{mx=8}{\frac{1}{\htmlData{mx=7}{\htmlData{mx=6}{\htmlData{mx=5}{J}} + 1}}} \cdot \htmlData{mx=11}{\htmlData{mx=9}{q}(\htmlData{mx=10}{j})}}}

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 J + 1. Lean writes f x; papers write f(x). (Fin (J + 1))
⟹Implies: If Fin(J + 1), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin (J + 1) → ℝ)
∀For all: The statement after the comma holds for every j. (∀ j, 0 ≤ q j)
a/bDivision: 1 divided by 8. In Lean, dividing by 0 gives 0. (1 / 8)
+Addition: J plus 1. (J + 1)
≤At most: 0 is less than or equal to q(j). (0 ≤ q j)
·Multiplication: 8 times J + 1. (8 * ((J : ℝ) + 1))
(x : T)As real numbers: J read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((J : ℝ))
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up 1/(J + 1) · q(j) for every j. (∑ j, (1 / ((J : ℝ) + 1)) * q j)

theorem ua-random-level-success {J : ℕ} (q : Fin (J + 1) → ℝ) (hq : ∀ j, 0 ≤ q j) (j0 : Fin (J + 1)) (hj0 : 1 / 8 ≤ q j0) :
    1 / (8 * ((J : ℝ) + 1)) ≤ ∑ j, (1 / ((J : ℝ) + 1)) * q j

With J = O(log n), isolation succeeds with probability Ω(1/log n) per trial; O(log n) independent trials (majority-vote amplification) make it a constant, all within polylog overhead. Part of 'Unbiased randomized attention: cost x variance thresholds', round 10 (isolation grid and Boolean tensor powers).

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: 14 lines of Lean

Random grid level: success ≥ 1/8 at one of J+1 equally likely levels gives overall success ≥ 1/(8(J+1))

How it was proved

More proved statements