Provedunbiased-attentionrandomized-algorithmssoftmaxgradient-hardness

Exactly one of t independent Bernoulli(p) coins is heads with probability t·p·(1−p)^{t−1}

For all $\htmlData{mx=1}{t \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=1}{p \in \htmlData{mx=0}{\mathbb{R}}}$ :

\begin{aligned} & \htmlData{mx=37}{\sum_{f \in \htmlData{mx=26}{\htmlData{mx=1}{\operatorname{filter}}(\htmlData{mx=25}{f \mapsto \htmlData{mx=18}{\lvert \htmlData{mx=17}{\htmlData{mx=10}{\operatorname{filter}}(\htmlData{mx=16}{i \mapsto \htmlData{mx=13}{\htmlData{mx=11}{f}(\htmlData{mx=12}{i})} \mathrel{\htmlData{mx=15}{=}} \htmlData{mx=14}{\operatorname{true}}})} \rvert} \mathrel{\htmlData{mx=19}{=}} 1})}} \htmlData{mx=36}{\prod_{i} \left(\htmlData{mx=35}{\begin{cases} \htmlData{mx=27}{p} & \text{if } \htmlData{mx=30}{\htmlData{mx=28}{f}(\htmlData{mx=29}{i})} \mathrel{\htmlData{mx=32}{=}} \htmlData{mx=31}{\operatorname{true}} \\ \htmlData{mx=34}{1 - \htmlData{mx=33}{p}} & \text{otherwise} \end{cases}}\right)}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=46}{\htmlData{mx=40}{\htmlData{mx=38}{t} \cdot \htmlData{mx=39}{p}} \cdot \htmlData{mx=45}{(\htmlData{mx=42}{1 - \htmlData{mx=41}{p}})^{\htmlData{mx=44}{\htmlData{mx=43}{t} - 1}}}} \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. (ℕ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
∑Summation: Add up ∏ i, p if f(i) = true, else 1 − p for each f in filter(f ↦ card(filter(i ↦ f(i) = true)) = 1). (∑ f ∈ Finset.univ.filter (fun f : Fin t…)
filter: Finset.univ.filter: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ.filter)
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)
⟹Implies: If Fin(t), then Bool. (Between types, A → B is the type of functions from A to B.) (Fin t → Bool)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
|s|Cardinality: The number of elements of filter(i ↦ f(i) = true). ((Finset.univ.filter (fun i => f i = tru…)
x ↦ f(x)Function (λ-abstraction): The function sending i to f(i) = true. Lean writes fun x => …; papers write x ↦ …. (fun i => f i = true)
f(x)Function application: f applied to i. Lean writes f x; papers write f(x). (f i)
=Equality: f(i) and true are the same. (f i = true)
true: true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (true)
∏Product: Multiply together p if f(i) = true, else 1 − p for every i. (∏ i, (if f i = true then p else 1 - p))
{ a if c; b otherwiseCases (if … then … else): p when f(i) = true, and 1 − p otherwise. (if f i = true then p else 1 - p)
-Subtraction: 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 - p)
·Multiplication: t times p. (t * p)
aᵇPower: 1 − p raised to the power t − 1. ((1 - p) ^ (t - 1))

theorem ua-exactly-one-probability (t : ℕ) (p : ℝ) :
    ∑ f ∈ Finset.univ.filter (fun f : Fin t → Bool => (Finset.univ.filter (fun i => f i = true)).card = 1), ∏ i, (if f i = true then p else 1 - p) = t * p * (1 - p) ^ (t - 1)

Proven exactly on the product space {0,1}^t: the exactly-one outcomes are the t indicator vectors, each of weight p(1−p)^{t−1}. Removes the last textbook ingredient of the isolation step; the gradient-hardness reduction now rests only on SETH/OVC and Rubinstein's protocol outside Lean. Part of 'Unbiased randomized attention: cost x variance thresholds', round 8 (isolation probability made exact).

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

Exactly one of t independent Bernoulli(p) coins is heads with probability t·p·(1−p)^{t−1}

How it was proved

More proved statements