Provedbalanced-conversionconversion-theoremattention-compute-lawlower-bound

Few-query lower bound (any sub-instance queries): a deterministic algorithm with transcript set T has family-average cost factor ≥ (1+4ε²)^L / |T|

For all $\htmlData{mx=1}{L \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=1}{\varepsilon \in \htmlData{mx=0}{\mathbb{R}}}$ , $\htmlData{mx=1}{T \in \htmlData{mx=0}{\operatorname{Type}}}$ , $\htmlData{mx=7}{\mathit{tr} : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{L}} \mathrel{\htmlData{mx=4}{\to}} \htmlData{mx=3}{\operatorname{Bool}}) \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=5}{T}}$ and $\htmlData{mx=9}{r : \htmlData{mx=0}{T} \mathrel{\htmlData{mx=8}{\to}} (\htmlData{mx=3}{\htmlData{mx=1}{\operatorname{Fin}}\,\htmlData{mx=2}{L}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\operatorname{Bool}}) \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=6}{\mathbb{R}}}$ , if $\htmlData{mx=5}{\forall t, b,\ 0 \mathrel{\htmlData{mx=4}{<}} \htmlData{mx=3}{\htmlData{mx=0}{r}(\htmlData{mx=1}{t}, \htmlData{mx=2}{b})}}$ and $\htmlData{mx=6}{\forall t,\ \htmlData{mx=4}{\sum_{b} \htmlData{mx=3}{\htmlData{mx=0}{r}(\htmlData{mx=1}{t}, \htmlData{mx=2}{b})}} \mathrel{\htmlData{mx=5}{=}} 1}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{T}}$ and $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Nonempty}}\,\htmlData{mx=1}{T}}$ ), then

\begin{aligned} & \htmlData{mx=11}{\frac{\htmlData{mx=6}{(\htmlData{mx=4}{1 + \htmlData{mx=3}{4 \cdot \htmlData{mx=2}{\htmlData{mx=1}{\varepsilon}^{2}}}})^{\htmlData{mx=5}{L}}}}{\htmlData{mx=10}{\htmlData{mx=9}{\htmlData{mx=7}{\operatorname{card}}(\htmlData{mx=8}{T})}}}} \\ & \quad \htmlData{mx=0}{\leq} \htmlData{mx=50}{\htmlData{mx=14}{\frac{1}{\htmlData{mx=13}{2^{\htmlData{mx=12}{L}}}}} \cdot \htmlData{mx=49}{\sum_{\sigma : \htmlData{mx=17}{\htmlData{mx=15}{\operatorname{Fin}}\,\htmlData{mx=16}{L}} \mathrel{\htmlData{mx=19}{\to}} \htmlData{mx=18}{\operatorname{Bool}}} \htmlData{mx=48}{\sum_{b : \htmlData{mx=22}{\htmlData{mx=20}{\operatorname{Fin}}\,\htmlData{mx=21}{L}} \mathrel{\htmlData{mx=24}{\to}} \htmlData{mx=23}{\operatorname{Bool}}} \htmlData{mx=47}{\frac{\htmlData{mx=40}{\left(\htmlData{mx=39}{\prod_{\ell} \left(\htmlData{mx=38}{\begin{cases} \htmlData{mx=27}{\htmlData{mx=25}{\frac{1}{2}} + \htmlData{mx=26}{\varepsilon}} & \text{if } \htmlData{mx=30}{\htmlData{mx=28}{\sigma}(\htmlData{mx=29}{\ell})} \mathrel{\htmlData{mx=34}{=}} \htmlData{mx=33}{\htmlData{mx=31}{b}(\htmlData{mx=32}{\ell})} \\ \htmlData{mx=37}{\htmlData{mx=35}{\frac{1}{2}} - \htmlData{mx=36}{\varepsilon}} & \text{otherwise} \end{cases}}\right)}\right)^{2}}}{\htmlData{mx=46}{\htmlData{mx=41}{r}(\htmlData{mx=44}{\htmlData{mx=42}{\mathit{tr}}(\htmlData{mx=43}{\sigma})}, \htmlData{mx=45}{b})}}}}}} \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. (ℕ)
RReal numbers: The real numbers: every point on the number line. (ℝ)
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 T. Lean writes f x; papers write f(x). (Fintype T)
Nonempty: Nonempty: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Nonempty)
∀For all: The statement after the comma holds for every t, b. (∀ t b, 0 < r t b)
a/bDivision: (1 + 4 · ε^2)^L divided by card(T). In Lean, dividing by 0 gives 0. ((1 + 4 * ε ^ 2) ^ L / (Fintype.card T :…)
≤At most: (1 + 4 · ε^2)^L/card(T) is less than or equal to 1/2^L · (∑ σ, ∑ b, (∏ ℓ, 1/2 + ε if σ(ℓ) = b(ℓ), else 1/2 …. ((1 + 4 * ε ^ 2) ^ L / (Fintype.card T :…)
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)
⟹Implies: If Fin(L), then Bool. (Between types, A → B is the type of functions from A to B.) (Fin L → Bool)
+Addition: 1 plus 4 · ε^2. (1 + 4 * ε ^ 2)
∑Summation: Add up r(t, b) for every b. (∑ b, r t b)
=Equality: ∑ b, r(t, b) and 1 are the same. (∑ b, r t b = 1)
·Multiplication: 4 times ε^2. (4 * ε ^ 2)
<Less than: 0 is strictly smaller than r(t, b). (0 < r t b)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
aᵇPower: ε raised to the power 2. (ε ^ 2)
(x : T)As real numbers: card(T) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((Fintype.card T : ℝ))
card: Fintype.card: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype.card)
∏Product: Multiply together 1/2 + ε if σ(ℓ) = b(ℓ), else 1/2 − ε for every ℓ. (∏ ℓ, (if σ ℓ = b ℓ then 1 / 2 + ε else …)
{ a if c; b otherwiseCases (if … then … else): 1/2 + ε when σ(ℓ) = b(ℓ), and 1/2 − ε otherwise. (if σ ℓ = b ℓ then 1 / 2 + ε else 1 / 2 …)
-Subtraction: 1/2 minus ε. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1 / 2 - ε)

theorem gq-few-query-lower-bound (L : ℕ) (ε : ℝ) {T : Type} [Fintype T] [Nonempty T] (tr : (Fin L → Bool) → T) (r : T → (Fin L → Bool) → ℝ) (hr : ∀ t b, 0 < r t b) (hrs : ∀ t, ∑ b, r t b = 1) :
    (1 + 4 * ε ^ 2) ^ L / (Fintype.card T : ℝ) ≤ (1 / 2 ^ L) * ∑ σ : Fin L → Bool, ∑ b : Fin L → Bool, (∏ ℓ, (if σ ℓ = b ℓ then 1 / 2 + ε else 1 / 2 - ε)) ^ 2 / r (tr σ) b

First rigorous lower bound in the programme that allows ARBITRARY sub-instance queries: with Q additive-ε queries (G grid answers each, |T| ≤ G^Q) and Q = o(ε² log n / log(1/ε)) no deterministic algorithm escapes the n^{Θ(ε²)} loss of converting to a proposal. Weaker than the node-query bound (which allows polylog queries); closing the gap is the open information-complexity question. Part of Balanced Conversion: the Conversion Theorem's two-way descent factor is exactly 1 + (p−q)²/(q(1−q)), so additive oracle error is second order at mass-balanced nodes; a mass-balanced descent converts any deterministic additive-ε oracle with loss n^{O(ε²)}, and the biased product family shows this is tight. Quantifies the last residual class of the Attention Compute Law.

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

Few-query lower bound (any sub-instance queries): a deterministic algorithm with transcript set T has family-average cost factor ≥ (1+4ε²)^L / |T|

How it was proved

More proved statements