Provedconversion-theorembalanced-conversionlower-boundnode-query
Node-query lower bound (formal): every randomized algorithm mapping ε-accurate node answers to a proposal has a product-family member with expected cost ≥ (1+4ε²)^L
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. (
ℕ) - 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 Ω) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ≤At most
- 0 is less than or equal to ε. (
0 ≤ ε) - <Less than
- ε is strictly smaller than 1/2. (
ε < 1 / 2) - ⟹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) - a/bDivision
- 1 divided by 2. In Lean, dividing by 0 gives 0. (
1 / 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) - 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) - x ↦ f(x)Function (λ-abstraction)
- The function sending _, _ to 1/2. Lean writes fun x => …; papers write x ↦ …. (
fun _ _ => 1 / 2) - ∧And
- Both hold: 0 < (∑ b', ∏ i, 1/2 + ε if σ(i) = b'(i), else 1/2 − ε if ∀…, and |1/2 − (∑ b', ∏ i, 1/2 + ε if σ(i) = b'(i), else 1/2 − ε i…. (
0 < (∑ b' : Fin L → Bool, (if (∀ i : Fi…) - (x : T)As natural numbers
- i read as an element of natural numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(i : ℕ)) - ∏Product
- Multiply together 1/2 + ε if σ(i) = b'(i), else 1/2 − ε for every i. (
∏ i, (if σ i = b' i then 1 / 2 + ε else…) - { a if c; b otherwiseCases (if … then … else)
- 1/2 + ε when σ(i) = b'(i), and 1/2 − ε otherwise. (
if σ i = b' i then 1 / 2 + ε else 1 / 2…) - +Addition
- 1/2 plus ε. (
1 / 2 + ε) - -Subtraction
- 1/2 minus ε. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 / 2 - ε) - |x|Absolute value
- The size of 1/2 − (∑ b', ∏ i, 1/2 + ε if σ(i) = b'(i), else 1/2 − ε if… without its sign. (
|(1 : ℝ) / 2 - (∑ b' : Fin L → Bool, (i…) - (x : T)As real numbers
- 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 : ℝ)) - update
- Function.update: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Function.update) - ⟨a, b⟩Anonymous constructor
- Builds a structure (a pair, a subtype element, …) from ℓ, h. (
⟨ℓ, h⟩) - true
- true: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
true) - ∃There exists
- At least one σ makes the statement after the comma true. (
∃ σ : Fin L → Bool, (1 + 4 * ε ^ 2) ^ L…) - ·Multiplication
- 4 times ε^2. (
4 * ε ^ 2) - aᵇPower
- ε raised to the power 2. (
ε ^ 2)
theorem nq-node-query-lower-bound {L : ℕ} {Ω : Type} [Fintype Ω] (ε : ℝ) (hε0 : 0 ≤ ε) (hε : ε < 1 / 2) (w : Ω → ℝ) (hw : ∀ ω, 0 ≤ w ω) (hsum : ∑ ω, w ω = 1) (alg : Ω → (ℕ → (Fin L → Bool) → ℝ) → ((Fin L → Bool) → ℝ)) (halg : ∀ ω b, 0 < alg ω (fun _ _ => 1 / 2) b) (halgs : ∀ ω, ∑ b, alg ω (fun _ _ => 1 / 2) b = 1) :
(∀ (σ : Fin L → Bool) (ℓ : ℕ) (h : ℓ < L) (b : Fin L → Bool), 0 < (∑ b' : Fin L → Bool, (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b i) then ∏ i, (if σ i = b' i then 1 / 2 + ε else 1 / 2 - ε) else 0)) ∧ |(1 : ℝ) / 2 - (∑ b' : Fin L → Bool, (if (∀ i : Fin L, (i : ℕ) < (ℓ + 1) → b' i = (Function.update b ⟨ℓ, h⟩ true) i) then ∏ i, (if σ i = b' i then 1 / 2 + ε else 1 / 2 - ε) else 0)) / (∑ b' : Fin L → Bool, (if (∀ i : Fin L, (i : ℕ) < ℓ → b' i = b i) then ∏ i, (if σ i = b' i then 1 / 2 + ε else 1 / 2 - ε) else 0))| ≤ ε) ∧ ∃ σ : Fin L → Bool, (1 + 4 * ε ^ 2) ^ L ≤ ∑ ω, w ω * ∑ b : Fin L → Bool, (∏ i, (if σ i = b i then 1 / 2 + ε else 1 / 2 - ε)) ^ 2 / alg ω (fun _ _ => 1 / 2) bAnswers review round 2 (codex), which noted bc2-family-lower-bound had no query model. Family: per-level product measures π_σ(b) = Π_i (1/2 ± ε) over σ ∈ {0,1}^L, with ε < 1/2. (1) Validity: for every member and every node, the prefix mass factorises coordinate-wise and the node's conditional mass is exactly 1/2 ± ε, so the all-1/2 answer table is ε-accurate for every member simultaneously. (2) Fooling: any algorithm alg(ω, answers) that outputs a proposal (randomised by coins ω, adaptive or not, since its input is the whole answer table) produces the same proposal distribution for every member when fed that table, and averaging the family bound over members gives a member σ with E_ω[Σ_b π_σ(b)²/r_ω(b)] ≥ (1+4ε²)^L = n^{log₂(1+4ε²)}. This is the n^{Θ(ε²)} lower bound for node-query conversions, matching the balanced-descent upper bound in the exponent. It does not cover algorithms that query arbitrary sub-instances (see gq-few-query-lower-bound for the few-query general case).
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
- 127 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.