Provedunbiased-attentionend-to-endsoftmaxlower-bound

END-TO-END unbiased-sampler bound: ≤ s probes per run, unbiased in unplanted and every planted world (var ≤ V), agreement when probes miss ⇒ |o₁−o₂|(1−s(k+1)/n) ≤ 2√(s(k+1)V/n)

For all $\htmlData{mx=1}{n, k, s \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{\Omega \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=3}{w : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=7}{\mathit{Pr} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=5}{\htmlData{mx=1}{\operatorname{Finset}}\,\htmlData{mx=4}{\htmlData{mx=2}{\operatorname{Fin}}\,\htmlData{mx=3}{n}}}}$ , $\htmlData{mx=3}{z_{1} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=9}{z_{2} : \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{n}}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=5}{\Omega} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ and $\htmlData{mx=1}{o_{1}, o_{2}, V \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=4}{\forall \omega,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}}$ , $\htmlData{mx=3}{\sum_{\omega} \htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})}} \mathrel{\htmlData{mx=4}{=}} 1$ , $\htmlData{mx=9}{\forall \omega,\ \htmlData{mx=6}{\lvert \htmlData{mx=5}{\htmlData{mx=3}{\mathit{Pr}}(\htmlData{mx=4}{\omega})} \rvert} \mathrel{\htmlData{mx=8}{\leq}} \htmlData{mx=7}{s}}$ , $\htmlData{mx=7}{\sum_{\omega} \htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{z_{1}}(\htmlData{mx=4}{\omega})}}} \mathrel{\htmlData{mx=9}{=}} \htmlData{mx=8}{o_{1}}$ , $\htmlData{mx=10}{\sum_{\omega} \htmlData{mx=9}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=8}{(\htmlData{mx=7}{\htmlData{mx=5}{\htmlData{mx=3}{z_{1}}(\htmlData{mx=4}{\omega})} - \htmlData{mx=6}{o_{1}}})^{2}}}} \mathrel{\htmlData{mx=12}{\leq}} \htmlData{mx=11}{V}$ , $\htmlData{mx=17}{\forall S \in \htmlData{mx=16}{\htmlData{mx=11}{\operatorname{powersetCard}}(\htmlData{mx=13}{\htmlData{mx=12}{k} + 1}, \htmlData{mx=15}{\htmlData{mx=14}{\operatorname{univ}}})},\ \htmlData{mx=8}{\sum_{\omega} \htmlData{mx=7}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=6}{\htmlData{mx=3}{z_{2}}(\htmlData{mx=4}{S}, \htmlData{mx=5}{\omega})}}} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{o_{2}}}$ , $\htmlData{mx=20}{\forall S \in \htmlData{mx=19}{\htmlData{mx=14}{\operatorname{powersetCard}}(\htmlData{mx=16}{\htmlData{mx=15}{k} + 1}, \htmlData{mx=18}{\htmlData{mx=17}{\operatorname{univ}}})},\ \htmlData{mx=11}{\sum_{\omega} \htmlData{mx=10}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=9}{(\htmlData{mx=8}{\htmlData{mx=6}{\htmlData{mx=3}{z_{2}}(\htmlData{mx=4}{S}, \htmlData{mx=5}{\omega})} - \htmlData{mx=7}{o_{2}}})^{2}}}} \mathrel{\htmlData{mx=13}{\leq}} \htmlData{mx=12}{V}}$ , $\htmlData{mx=16}{\forall S, \omega,\ (\htmlData{mx=6}{\forall p \in \htmlData{mx=5}{\htmlData{mx=3}{\mathit{Pr}}(\htmlData{mx=4}{\omega})},\ \htmlData{mx=0}{p} \mathrel{\htmlData{mx=2}{\notin}} \htmlData{mx=1}{S}}) \mathrel{\htmlData{mx=15}{\implies}} \htmlData{mx=10}{\htmlData{mx=7}{z_{2}}(\htmlData{mx=8}{S}, \htmlData{mx=9}{\omega})} \mathrel{\htmlData{mx=14}{=}} \htmlData{mx=13}{\htmlData{mx=11}{z_{1}}(\htmlData{mx=12}{\omega})}}$ and $\htmlData{mx=1}{\htmlData{mx=0}{k} + 1} \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{n}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\Omega}}$ ), then

\htmlData{mx=12}{\htmlData{mx=3}{\left\lvert \htmlData{mx=2}{\htmlData{mx=0}{o_{1}} - \htmlData{mx=1}{o_{2}}} \right\rvert} \cdot \left(\htmlData{mx=11}{1 - \htmlData{mx=10}{\frac{\htmlData{mx=8}{\htmlData{mx=7}{\htmlData{mx=4}{s} \cdot (\htmlData{mx=6}{\htmlData{mx=5}{k} + 1})}}}{\htmlData{mx=9}{n}}}}\right)} \mathrel{\htmlData{mx=24}{\leq}} \htmlData{mx=23}{2\htmlData{mx=22}{\sqrt{\htmlData{mx=21}{\htmlData{mx=19}{\frac{\htmlData{mx=17}{\htmlData{mx=16}{\htmlData{mx=13}{s} \cdot (\htmlData{mx=15}{\htmlData{mx=14}{k} + 1})}}}{\htmlData{mx=18}{n}}} \cdot \htmlData{mx=20}{V}}}}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: n, k, s range over natural numbers: the statement must hold for every choice. ((n k s : ℕ))
Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to Ω. Lean writes f x; papers write f(x). (Fintype Ω)
⟹Implies: If Ω, then ℝ. (Between types, A → B is the type of functions from A to B.) (Ω → ℝ)
∀For all: The statement after the comma holds for every ω. (∀ ω, 0 ≤ w ω)
∑Summation: Add up w(ω) for every ω. (∑ ω, w ω)
=Equality: ∑ ω, w(ω) and 1 are the same. (∑ ω, w ω = 1)
|x|Absolute value: The size of o₁ − o₂ without its sign. (|o₁ - o₂|)
RReal numbers: The real numbers: every point on the number line. (ℝ)
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)
≤At most: 0 is less than or equal to w(ω). (0 ≤ w ω)
|s|Cardinality: The number of elements of Pr(ω). ((Pr ω).card)
·Multiplication: w(ω) times z₁(ω). (w ω * z₁ ω)
powersetCard: Finset.powersetCard: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.powersetCard)
aᵇPower: z₁(ω) − o₁ raised to the power 2. ((z₁ ω - o₁) ^ 2)
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)
-Subtraction: z₁(ω) minus o₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (z₁ ω - o₁)
(x : T)As real numbers: s · (k + 1) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((s * (k + 1) : ℝ))
a/bDivision: s · (k + 1) divided by n. In Lean, dividing by 0 gives 0. ((s * (k + 1) : ℝ) / n)
∉Not an element of: p is not a member of S. (p ∉ S)
+Addition: k plus 1. (k + 1)
(x : T)Type ascription: univ read as a Finset(Fin(n)). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Finset.univ : Finset (Fin n)))
univ: Finset.univ: 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)
√Square root: The non-negative number whose square is s · (k + 1)/n · V. (Real.sqrt ((s * (k + 1) : ℝ) / n * V))

theorem ua-end-to-end-unbiased-sampler {n k s : ℕ} {Ω : Type} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (Pr : Ω → Finset (Fin n)) (hPr : ∀ ω, (Pr ω).card ≤ s) (z₁ : Ω → ℝ) (z₂ : Finset (Fin n) → Ω → ℝ) (o₁ o₂ V : ℝ) (h1 : ∑ ω, w ω * z₁ ω = o₁) (hV1 : ∑ ω, w ω * (z₁ ω - o₁) ^ 2 ≤ V) (h2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * z₂ S ω = o₂) (hV2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * (z₂ S ω - o₂) ^ 2 ≤ V) (hsame : ∀ S ω, (∀ p ∈ Pr ω, p ∉ S) → z₂ S ω = z₁ ω) (hk : k + 1 ≤ n) :
    |o₁ - o₂| * (1 - (s * (k + 1) : ℝ) / n) ≤ 2 * Real.sqrt ((s * (k + 1) : ℝ) / n * V)

Fifth single-statement composition and the unconditional half of the sharp threshold: the two-point lemma applied on the product type Finset(Fin n) × Ω (plant uniform on (k+1)-subsets, W(S,ω) = 1{S ∈ pc}/C · w(ω)) with the random-plant hitting bound applied per run. With a plant of size n e^{−R} that moves the output by ≥ 1/2 (ua-planted-output) and V constant, an exactly unbiased sampler needs s ≥ Ω(min(n, e^R)) probes per row. Adaptive probing is covered by the standard coupling remark (probes coincide with the unplanted world until the first hit), not formalised. Part of 'Unbiased randomized attention: cost x variance thresholds' (end-to-end composition round).

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

END-TO-END unbiased-sampler bound: ≤ s probes per run, unbiased in unplanted and every planted world (var ≤ V), agreement when probes miss ⇒ |o₁−o₂|(1−s(k+1)/n) ≤ 2√(s(k+1)V/n)

How it was proved

More proved statements