Provedunbiased-attentionrandomized-algorithmssoftmaxgradient-hardness

Dyadic grid hits the isolation window: for t ≥ 1, j = ⌊log₂ t⌋ + 2 has 1/(4t) ≤ 2^{−j} ≤ 1/(2t)

For all $\htmlData{mx=1}{t \in \htmlData{mx=0}{\mathbb{N}}}$ , if $1 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{t}$ , then

\begin{aligned} & \htmlData{mx=0}{\exists} j \in \htmlData{mx=1}{\mathbb{N}}, \\ & \quad \htmlData{mx=3}{j} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{\htmlData{mx=6}{\htmlData{mx=4}{\operatorname{log}}(2, \htmlData{mx=5}{t})} + 2} \\ & \quad \htmlData{mx=2}{\land} \htmlData{mx=12}{\frac{1}{\htmlData{mx=11}{4 \cdot \htmlData{mx=10}{\htmlData{mx=9}{t}}}}} \mathrel{\htmlData{mx=17}{\leq}} \htmlData{mx=16}{\htmlData{mx=14}{\htmlData{mx=13}{\frac{1}{2}}}^{\htmlData{mx=15}{j}}} \\ & \quad \htmlData{mx=2}{\land} \htmlData{mx=21}{\htmlData{mx=19}{\htmlData{mx=18}{\frac{1}{2}}}^{\htmlData{mx=20}{j}}} \mathrel{\htmlData{mx=25}{\leq}} \htmlData{mx=24}{\frac{1}{\htmlData{mx=23}{2\htmlData{mx=22}{t}}}} \end{aligned}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
≤At most: 1 is less than or equal to t. (1 ≤ t)
∃There exists: At least one j makes the statement after the comma true. (∃ j : ℕ, j ≤ Nat.log 2 t + 2 ∧ 1 / (4 *…)
log: Nat.log: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nat.log)
f(x)Function application: Nat.log applied to 2, t. Lean writes f x; papers write f(x). (Nat.log 2 t)
+Addition: log(2, t) plus 2. (Nat.log 2 t + 2)
a/bDivision: 1 divided by 4 · t. In Lean, dividing by 0 gives 0. (1 / (4 * (t : ℝ)))
∧And: Both hold: 1/(4 · t) ≤ (1/2)^j, and (1/2)^j ≤ 1/(2 · t). (1 / (4 * (t : ℝ)) ≤ (1 / 2 : ℝ) ^ j ∧ (…)
·Multiplication: 4 times t. (4 * (t : ℝ))
(x : T)As real numbers: t read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((t : ℝ))
aᵇPower: 1/2 raised to the power j. ((1 / 2 : ℝ) ^ j)

theorem ua-dyadic-rate-exists (t : ℕ) (ht : 1 ≤ t) :
    ∃ j : ℕ, j ≤ Nat.log 2 t + 2 ∧ 1 / (4 * (t : ℝ)) ≤ (1 / 2 : ℝ) ^ j ∧ (1 / 2 : ℝ) ^ j ≤ 1 / (2 * t)

So trying the O(log n) subsampling rates 2^{−j}, j ≤ log₂ n + 2, always includes one in the window where isolation succeeds with probability ≥ 1/8. 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: 20 lines of Lean

Dyadic grid hits the isolation window: for t ≥ 1, j = ⌊log₂ t⌋ + 2 has 1/(4t) ≤ 2^{−j} ≤ 1/(2t)

How it was proved

More proved statements