Provedunbiased-attentiongradient-hardnesssampler-lower-bound

Planted gradient gap: with u = k = 1_P and plant mass p, the query-gradient covariance Σπ u k − (Σπu)(Σπk) equals p(1 − p)

For all $\htmlData{mx=1}{n \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=5}{\pi : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ , $\htmlData{mx=5}{P \in \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{n}}}}$ and $\htmlData{mx=1}{p \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\sum_{j \in \htmlData{mx=0}{P}} \htmlData{mx=3}{\htmlData{mx=1}{\pi}(\htmlData{mx=2}{j})}} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{p}$ , then

\begin{aligned} & \htmlData{mx=38}{\htmlData{mx=16}{\sum_{j} \htmlData{mx=15}{\htmlData{mx=3}{\htmlData{mx=1}{\pi}(\htmlData{mx=2}{j})} \cdot \left(\htmlData{mx=14}{\left(\htmlData{mx=8}{\begin{cases} \htmlData{mx=4}{1} & \text{if } \htmlData{mx=5}{j} \mathrel{\htmlData{mx=7}{\in}} \htmlData{mx=6}{P} \\ 0 & \text{otherwise} \end{cases}}\right) \cdot \left(\htmlData{mx=13}{\begin{cases} \htmlData{mx=9}{1} & \text{if } \htmlData{mx=10}{j} \mathrel{\htmlData{mx=12}{\in}} \htmlData{mx=11}{P} \\ 0 & \text{otherwise} \end{cases}}\right)}\right)}} - \htmlData{mx=37}{\left(\htmlData{mx=26}{\sum_{j} \htmlData{mx=25}{\htmlData{mx=19}{\htmlData{mx=17}{\pi}(\htmlData{mx=18}{j})} \cdot \left(\htmlData{mx=24}{\begin{cases} \htmlData{mx=20}{1} & \text{if } \htmlData{mx=21}{j} \mathrel{\htmlData{mx=23}{\in}} \htmlData{mx=22}{P} \\ 0 & \text{otherwise} \end{cases}}\right)}}\right) \cdot \left(\htmlData{mx=36}{\sum_{j} \htmlData{mx=35}{\htmlData{mx=29}{\htmlData{mx=27}{\pi}(\htmlData{mx=28}{j})} \cdot \left(\htmlData{mx=34}{\begin{cases} \htmlData{mx=30}{1} & \text{if } \htmlData{mx=31}{j} \mathrel{\htmlData{mx=33}{\in}} \htmlData{mx=32}{P} \\ 0 & \text{otherwise} \end{cases}}\right)}}\right)}} \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=42}{\htmlData{mx=39}{p} \cdot (\htmlData{mx=41}{1 - \htmlData{mx=40}{p}})} \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. (ℕ)
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 n. Lean writes f x; papers write f(x). (Fin n)
⟹Implies: If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (Fin n → ℝ)
Finset: Finset: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset)
∑Summation: Add up π(j) for each j in P. (∑ j ∈ P, π j)
=Equality: ∑ j, π(j) and p are the same. (∑ j ∈ P, π j = p)
-Subtraction: ∑ j, π(j) · (1 if j ∈ P, else 0 · 1 if j ∈ P, else 0) minus (∑ j, π(j) · 1 if j ∈ P, else 0) · (∑ j, π(j) · 1 if j ∈ P…. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (∑ j, π j * ((if j ∈ P then (1 : ℝ) else…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
πPi: The ratio of a circle's circumference to its diameter, ≈ 3.14159. (π)
·Multiplication: 1 if j ∈ P, else 0 times 1 if j ∈ P, else 0. ((if j ∈ P then (1 : ℝ) else 0) * (if j …)
{ a if c; b otherwiseCases (if … then … else): 1 when j ∈ P, and 0 otherwise. (if j ∈ P then (1 : ℝ) else 0)
∈Element of: j is a member of P. (j ∈ P)
(x : T)As real numbers: 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1 : ℝ))

theorem ug-planted-gradient-gap {n : ℕ} (π : Fin n → ℝ) (P : Finset (Fin n)) (p : ℝ) (hp : ∑ j ∈ P, π j = p) :
    ∑ j, π j * ((if j ∈ P then (1 : ℝ) else 0) * (if j ∈ P then (1 : ℝ) else 0)) - (∑ j, π j * (if j ∈ P then (1 : ℝ) else 0)) * (∑ j, π j * (if j ∈ P then (1 : ℝ) else 0)) = p * (1 - p)

In the planted world the gradient coordinate is the covariance p(1−p); in the unplanted world (u ≡ 0) it is 0. The planted/unplanted gap of the GRADIENT functional is therefore p(1−p), and ua-end-to-end-unbiased-sampler applies verbatim: an exactly unbiased gradient sampler needs Ω(min(n, e^R)) probes per row. Part of 'Unbiased randomized attention: cost x variance thresholds', gradient-hardness round: the unconditional sampler lower bound transferred to the query gradient.

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

Planted gradient gap: with u = k = 1_P and plant mass p, the query-gradient covariance Σπ u k − (Σπu)(Σπk) equals p(1 − p)

How it was proved

More proved statements