Provedunbiased-attentionsampling-lower-boundadaptiveheadline-theorem

Adaptive-sampler lower bound: any sampler whose s probes depend adaptively on its coins and observed values obeys |o₁−o₂|(1 − s(k+1)/n) ≤ 2√(s(k+1)V/n) against a random plant

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=11}{g : \htmlData{mx=0}{\mathbb{N}} \mathrel{\htmlData{mx=10}{\to}} \htmlData{mx=1}{\Omega} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=4}{\htmlData{mx=2}{\operatorname{List}}\,\htmlData{mx=3}{\mathbb{R}}} \mathrel{\htmlData{mx=8}{\to}} \htmlData{mx=7}{\htmlData{mx=5}{\operatorname{Fin}}\,\htmlData{mx=6}{n}}}$ , $\htmlData{mx=7}{\mathit{out} : \htmlData{mx=0}{\Omega} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=3}{\htmlData{mx=1}{\operatorname{List}}\,\htmlData{mx=2}{\mathbb{R}}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ , $\htmlData{mx=13}{\mathit{hist} : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}) \mathrel{\htmlData{mx=12}{\to}} \htmlData{mx=5}{\Omega} \mathrel{\htmlData{mx=11}{\to}} \htmlData{mx=6}{\mathbb{N}} \mathrel{\htmlData{mx=10}{\to}} \htmlData{mx=9}{\htmlData{mx=7}{\operatorname{List}}\,\htmlData{mx=8}{\mathbb{R}}}}$ , $\htmlData{mx=5}{y_{1} : \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{n}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\mathbb{R}}}$ , $\htmlData{mx=11}{y_{2} : \htmlData{mx=4}{\htmlData{mx=0}{\operatorname{Finset}}\,\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{n}}} \mathrel{\htmlData{mx=10}{\to}} \htmlData{mx=7}{\htmlData{mx=5}{\operatorname{Fin}}\,\htmlData{mx=6}{n}} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=8}{\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=6}{\forall y, \omega,\ \htmlData{mx=3}{\htmlData{mx=0}{\mathit{hist}}(\htmlData{mx=1}{y}, \htmlData{mx=2}{\omega}, 0)} \mathrel{\htmlData{mx=5}{=}} \htmlData{mx=4}{\left[ \right]}}$ , $\htmlData{mx=26}{\forall y, \omega, t,\ \htmlData{mx=5}{\htmlData{mx=0}{\mathit{hist}}(\htmlData{mx=1}{y}, \htmlData{mx=2}{\omega}, \htmlData{mx=4}{\htmlData{mx=3}{t} + 1})} \mathrel{\htmlData{mx=25}{=}} \htmlData{mx=24}{\htmlData{mx=10}{\htmlData{mx=6}{\mathit{hist}}(\htmlData{mx=7}{y}, \htmlData{mx=8}{\omega}, \htmlData{mx=9}{t})} + \htmlData{mx=23}{\mathtt{+}(\htmlData{mx=22}{\left[ \htmlData{mx=21}{\htmlData{mx=11}{y}(\htmlData{mx=20}{\htmlData{mx=12}{g}(\htmlData{mx=13}{t}, \htmlData{mx=14}{\omega}, \htmlData{mx=19}{\htmlData{mx=15}{\mathit{hist}}(\htmlData{mx=16}{y}, \htmlData{mx=17}{\omega}, \htmlData{mx=18}{t})})})} \right]})}}}$ , $\htmlData{mx=12}{\forall S, j,\ \htmlData{mx=0}{j} \mathrel{\htmlData{mx=2}{\notin}} \htmlData{mx=1}{S} \mathrel{\htmlData{mx=11}{\implies}} \htmlData{mx=6}{\htmlData{mx=3}{y_{2}}(\htmlData{mx=4}{S}, \htmlData{mx=5}{j})} \mathrel{\htmlData{mx=10}{=}} \htmlData{mx=9}{\htmlData{mx=7}{y_{1}}(\htmlData{mx=8}{j})}}$ , $\htmlData{mx=12}{\sum_{\omega} \htmlData{mx=11}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=10}{\htmlData{mx=3}{\mathit{out}}(\htmlData{mx=4}{\omega}, \htmlData{mx=9}{\htmlData{mx=5}{\mathit{hist}}(\htmlData{mx=6}{y_{1}}, \htmlData{mx=7}{\omega}, \htmlData{mx=8}{s})})}}} \mathrel{\htmlData{mx=14}{=}} \htmlData{mx=13}{o_{1}}$ , $\htmlData{mx=15}{\sum_{\omega} \htmlData{mx=14}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=13}{(\htmlData{mx=12}{\htmlData{mx=10}{\htmlData{mx=3}{\mathit{out}}(\htmlData{mx=4}{\omega}, \htmlData{mx=9}{\htmlData{mx=5}{\mathit{hist}}(\htmlData{mx=6}{y_{1}}, \htmlData{mx=7}{\omega}, \htmlData{mx=8}{s})})} - \htmlData{mx=11}{o_{1}}})^{2}}}} \mathrel{\htmlData{mx=17}{\leq}} \htmlData{mx=16}{V}$ , $\htmlData{mx=23}{\forall S \in \htmlData{mx=22}{\htmlData{mx=17}{\operatorname{powersetCard}}(\htmlData{mx=19}{\htmlData{mx=18}{k} + 1}, \htmlData{mx=21}{\htmlData{mx=20}{\operatorname{univ}}})},\ \htmlData{mx=14}{\sum_{\omega} \htmlData{mx=13}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=12}{\htmlData{mx=3}{\mathit{out}}(\htmlData{mx=4}{\omega}, \htmlData{mx=11}{\htmlData{mx=5}{\mathit{hist}}(\htmlData{mx=8}{\htmlData{mx=6}{y_{2}}(\htmlData{mx=7}{S})}, \htmlData{mx=9}{\omega}, \htmlData{mx=10}{s})})}}} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{o_{2}}}$ , $\htmlData{mx=26}{\forall S \in \htmlData{mx=25}{\htmlData{mx=20}{\operatorname{powersetCard}}(\htmlData{mx=22}{\htmlData{mx=21}{k} + 1}, \htmlData{mx=24}{\htmlData{mx=23}{\operatorname{univ}}})},\ \htmlData{mx=17}{\sum_{\omega} \htmlData{mx=16}{\htmlData{mx=2}{\htmlData{mx=0}{w}(\htmlData{mx=1}{\omega})} \cdot \htmlData{mx=15}{(\htmlData{mx=14}{\htmlData{mx=12}{\htmlData{mx=3}{\mathit{out}}(\htmlData{mx=4}{\omega}, \htmlData{mx=11}{\htmlData{mx=5}{\mathit{hist}}(\htmlData{mx=8}{\htmlData{mx=6}{y_{2}}(\htmlData{mx=7}{S})}, \htmlData{mx=9}{\omega}, \htmlData{mx=10}{s})})} - \htmlData{mx=13}{o_{2}}})^{2}}}} \mathrel{\htmlData{mx=19}{\leq}} \htmlData{mx=18}{V}}$ 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)
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)
|x|Absolute value: The size of o₁ − o₂ without its sign. (|o₁ - o₂|)
RReal numbers: The real numbers: every point on the number line. (ℝ)
≤At most: 0 is less than or equal to w(ω). (0 ≤ w ω)
·Multiplication: w(ω) times out(ω, hist(y₁, ω, s)). (w ω * out ω (hist y₁ ω s))
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)
∉Not an element of: j is not a member of S. (j ∉ S)
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
aᵇPower: out(ω, hist(y₁, ω, s)) − o₁ raised to the power 2. ((out ω (hist y₁ ω s) - o₁) ^ 2)
-Subtraction: out(ω, hist(y₁, ω, s)) minus o₁. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (out ω (hist y₁ ω s) - o₁)
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)
(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)
+Addition: t plus 1. (t + 1)
[a, b]List: The list of , in order. ([])
(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-adaptive-sampler-lower-bound {n k s : ℕ} {Ω : Type} [Fintype Ω] (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (g : ℕ → Ω → List ℝ → Fin n) (out : Ω → List ℝ → ℝ) (hist : (Fin n → ℝ) → Ω → ℕ → List ℝ) (hhist0 : ∀ y ω, hist y ω 0 = []) (hhistS : ∀ y ω t, hist y ω (t + 1) = hist y ω t ++ [y (g t ω (hist y ω t))]) (y₁ : Fin n → ℝ) (y₂ : Finset (Fin n) → Fin n → ℝ) (hy : ∀ S j, j ∉ S → y₂ S j = y₁ j) (o₁ o₂ V : ℝ) (h1 : ∑ ω, w ω * out ω (hist y₁ ω s) = o₁) (hV1 : ∑ ω, w ω * (out ω (hist y₁ ω s) - o₁) ^ 2 ≤ V) (h2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * out ω (hist (y₂ S) ω s) = o₂) (hV2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * (out ω (hist (y₂ S) ω s) - o₂) ^ 2 ≤ V) (hk : k + 1 ≤ n) :
    |o₁ - o₂| * (1 - (s * (k + 1) : ℝ) / n) ≤ 2 * Real.sqrt ((s * (k + 1) : ℝ) / n * V)

Closes the modelling bridge raised in external review (codex, 2026-10-05) for the unconditional sampling threshold. The sampler is fully adaptive: the index of probe t is any function g(t, ω, history) of the coins ω and of all values observed so far, and the output is any function of the coins and the full history of s observations. The probe set of the UNPLANTED run is taken as the per-coin probe set, and a coupling lemma (proved by induction on the history) shows that whenever that set misses the plant S, the planted run makes exactly the same probes and returns the same output. The two-point random-plant bound (ua-end-to-end-unbiased-sampler, embedded) then applies verbatim. With the planted softmax instance of ua-sampling-threshold-two-sided this gives the Ω(min(n, e^R)) probe bound for every adaptive exactly unbiased sampler of constant variance.

How it was proved

Proved: 5 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: 237 lines of Lean

Adaptive-sampler lower bound: any sampler whose s probes depend adaptively on its coins and observed values obeys |o₁−o₂|(1 − s(k+1)/n) ≤ 2√(s(k+1)V/n) against a random plant

How it was proved

More proved statements