Provedunbiased-attentionheadline-theoremsampling-lower-boundattention-compute-law
Unconditional sampling threshold, two-sided, one statement: range-R rows cost ≤ e^R under the uniform proposal, and any unbiased sampler needs ≥ (n/m)·min(1/2, 1/64V) 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. (
ℝ) - 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₁ ω) - 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 : …) - 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) - (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 : ℝ)) - 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₁) - ∉Not an element of
- p is not a member of S. (
p ∉ S) - eˣExponential function
- e raised to the power R, where e ≈ 2.718. (
Real.exp R) - +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) - ∧And
- Both hold: a ≤ sc(j), and sc(j) ≤ a + R. (
a ≤ sc j ∧ sc j ≤ a + R) - { 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) - minMinimum
- The smaller of 1/2 and 1/(64 · V). (
min (1 / 2) (1 / (64 * V)))
theorem ua-sampling-threshold-two-sided {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 R : ℝ) (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) (hV : 0 < V) (hR : 0 ≤ R) (ho1 : o₁ = 0) (ho2 : o₂ = ((k + 1 : ℝ) * Real.exp R) / ((k + 1 : ℝ) * Real.exp R + ((n : ℝ) - (k + 1)))) (hplant : (n : ℝ) - (k + 1) ≤ (k + 1 : ℝ) * Real.exp R) :
(∀ (sc : Fin n → ℝ) (a : ℝ), (∀ j, a ≤ sc j ∧ sc j ≤ a + R) → (n : ℝ) * ∑ j, (Real.exp (sc j) / ∑ i, Real.exp (sc i)) ^ 2 ≤ Real.exp R) ∧ (∀ S ∈ Finset.powersetCard (k + 1) (Finset.univ : Finset (Fin n)), (∑ j, Real.exp (if j ∈ S then R else 0) * (if j ∈ S then (1 : ℝ) else 0)) / (∑ j, Real.exp (if j ∈ S then R else 0)) = ((k + 1 : ℝ) * Real.exp R) / ((k + 1 : ℝ) * Real.exp R + ((n : ℝ) - (k + 1)))) ∧ min (1 / 2) (1 / (64 * V)) ≤ (s * (k + 1) : ℝ) / nHeadline theorem of the Attention Compute Law's unconditional axis, end-to-end in one statement. (A) Upper: every attention row whose scores lie in an interval of width R has uniform-proposal cost factor n·Σπ² ≤ e^R. (B) Instance: the planted row (score R on a plant S of size m = k+1, 0 elsewhere, values 1 on the plant) has output m e^R/(m e^R + n − m), at least 1/2 when n − m ≤ m e^R. (C) Lower: any exactly unbiased sampler with variance ≤ V on the unplanted world (output 0) and on every planted world, reading at most s keys per run and agreeing between worlds when it misses the plant, satisfies s·m/n ≥ min(1/2, 1/(64V)); with m ≈ n e^{−R} this is s ≳ e^R. The verified ua-end-to-end-unbiased-sampler proof is inlined, so the statement is standalone. Adaptive probing beyond the stated agreement condition is covered by the coupling remark, not formalised.
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
- 289 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.