Provedunbiased-attentionsampling-lower-boundadaptiveheadline-theorem
Explicit e^R threshold: with the plant size m = ⌈n/(1+e^R)⌉ (which exists when 1+e^R ≤ n), every adaptive exactly unbiased sampler needs s ≥ min(1/2, 1/64V)·(1+e^R)/2 probes
For all , , , , , and , if , , , , , , , , , , , and (given ), then
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) - <Less than
- 0 is strictly smaller than V. (
0 < V) - 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(_ ↦ 0, ω, s)). (
w ω * out ω (hist (fun _ => 0) ω 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) - 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(_ ↦ 0, ω, s)) − 0 raised to the power 2. (
(out ω (hist (fun _ => 0) ω s) - 0) ^ 2) - -Subtraction
- out(ω, hist(_ ↦ 0, ω, s)) minus 0. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
out ω (hist (fun _ => 0) ω s) - 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) - +Addition
- t plus 1. (
t + 1) - [a, b]List
- The list of , in order. (
[]) - x ↦ f(x)Function (λ-abstraction)
- The function sending _ to 0. Lean writes fun x => …; papers write x ↦ …. (
fun _ => 0) - (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) - ∃There exists
- At least one m makes the statement after the comma true. (
∃ m : ℕ, 1 ≤ m ∧ m ≤ N ∧ (N : ℝ) - m ≤ …) - ∧And
- Both hold: N − m ≤ m · exp(R'), and m · (1 + exp(R')) ≤ 2 · N. (
(N : ℝ) - m ≤ m * Real.exp R' ∧ (m : ℝ)…) - { a if c; b otherwiseCases (if … then … else)
- R when j ∈ S, and 0 otherwise. (
if j ∈ S then R else 0) - ∈Element of
- j is a member of S. (
j ∈ S) - a/bDivision
- (k + 1) · exp(R) divided by (k + 1) · exp(R) + (n − (k + 1)). In Lean, dividing by 0 gives 0. (
((k + 1 : ℝ) * Real.exp R) / ((k + 1 : …) - (x : T)As real numbers
- k + 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(k + 1 : ℝ)) - minMinimum
- The smaller of 1/2 and 1/(64 · V). (
min (1 / 2) (1 / (64 * V))) - eˣExponential function
- e raised to the power R, where e ≈ 2.718. (
Real.exp R)
theorem ua-adaptive-sampling-threshold-explicit {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))]) (R V : ℝ) (h1 : ∑ ω, w ω * out ω (hist (fun _ => 0) ω s) = 0) (hV1 : ∑ ω, w ω * (out ω (hist (fun _ => 0) ω s) - 0) ^ 2 ≤ V) (h2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * out ω (hist (fun j => if j ∈ S then R else 0) ω s) = ((k + 1 : ℝ) * Real.exp R) / ((k + 1 : ℝ) * Real.exp R + ((n : ℝ) - (k + 1)))) (hV2 : ∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), ∑ ω, w ω * (out ω (hist (fun j => if j ∈ S then R else 0) ω s) - ((k + 1 : ℝ) * Real.exp R) / ((k + 1 : ℝ) * Real.exp R + ((n : ℝ) - (k + 1)))) ^ 2 ≤ V) (hk : k + 1 ≤ n) (hV : 0 < V) (hR : 0 ≤ R) (hplant : (n : ℝ) - (k + 1) ≤ (k + 1 : ℝ) * Real.exp R) (hsmall : (k + 1 : ℝ) * (1 + Real.exp R) ≤ 2 * n) :
(∀ (N : ℕ) (R' : ℝ), 1 + Real.exp R' ≤ N → ∃ m : ℕ, 1 ≤ m ∧ m ≤ N ∧ (N : ℝ) - m ≤ m * Real.exp R' ∧ (m : ℝ) * (1 + Real.exp R') ≤ 2 * N) ∧ min (1 / 2) (1 / (64 * V)) * ((1 + Real.exp R) / 2) ≤ sAnswers review round 3 (codex), which correctly noted that ua-adaptive-sampling-threshold proves s(k+1)/n ≥ min(1/2, 1/(64V)) but that its plant condition only bounds n/(k+1) from above, so the e^R threshold did not follow. This statement adds the missing parameter link: (1) for every N and R' with 1 + e^{R'} ≤ N there is a plant size m (namely ⌈N/(1+e^{R'})⌉) with 1 ≤ m ≤ N, constant planted mass N − m ≤ m e^{R'}, and small plant m(1+e^{R'}) ≤ 2N; (2) with such a plant (hypothesis (k+1)(1+e^R) ≤ 2n), every fully adaptive sampler that is exactly unbiased with variance ≤ V on the planted softmax family needs s ≥ min(1/2, 1/(64V))·(1+e^R)/2 probes per run. Embeds ua-adaptive-sampling-threshold (coupling lemma, softmax instance, two-point bound). Scope as stated by the reviewer: coordinate-value queries, common finite randomness, no preprocessing.
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
- 351 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.