feat(Classes/Sparse): Kadin's theorem, PH ⊆ P^{NP[O(log n)]} under a sparse Turing-complete set for NP (#2062 M3)

Complexity.lean

@@ -1360,6 +1360,7 @@ public import Complexity.Computability.Complexity.Classes.Sparse.BoundedTruthTab
 public import Complexity.Computability.Complexity.Classes.Sparse.Conjunctive
 public import Complexity.Computability.Complexity.Classes.Sparse.Fortune
 public import Complexity.Computability.Complexity.Classes.Sparse.Hausdorff
+public import Complexity.Computability.Complexity.Classes.Sparse.Kadin
 public import Complexity.Computability.Complexity.Classes.Sparse.Mahaney
 public import Complexity.Computability.Complexity.Classes.Sparse.OneQuery
 public import Complexity.Computability.Complexity.Classes.Sparse.Prune

Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Classes.Oracle.QueryBit
 public import Complexity.Computability.Complexity.Problems.SAT
+public import Complexity.Languages.Probabilistic.Iteration
 import Complexity.Computability.Complexity.Classes.NP.Image
 import Complexity.Computability.Complexity.CookLevin.Completeness
 import Complexity.Computability.Probabilistic.Oracle.Composition
@@ -41,6 +42,8 @@ is closed under complement.
 
 ## Main results
 
+* `Cslib.OracleComp.length_queriesWith_iterate_le`: a bounded loop of rounds with boundedly many
+  requests makes boundedly many requests.
 * `Cslib.Complexity.ComputableInPolyTimeWithOracleQueries.computableInPolyTimeWithOracle`,
   `.mono`, `.map`: forgetting and weakening the bound, and postprocessing.
 * `Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithOracleQueries`: polynomial time
@@ -62,7 +65,21 @@ is closed under complement.
 
 @[expose] public section
 
-namespace Cslib.Complexity
+namespace Cslib
+
+/-- **A bounded loop makes a bounded number of requests**: if every round makes at most `r`
+requests, `n` rounds make at most `n * r`. -/
+theorem OracleComp.length_queriesWith_iterate_le {ι State : Type} {spec : OracleSpec.{0, 0} ι}
+    (answer : (q : ι) → spec q) {step : State → OracleComp spec State} {r : ℕ}
+    (h : ∀ st, (queriesWith answer (step st)).length ≤ r) (n : ℕ) (st : State) :
+    (queriesWith answer (iterate n step st)).length ≤ n * r := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [iterate_succ, queriesWith_bind, List.length_append, Nat.succ_mul]
+    exact Nat.add_le_add ih (h _)
+
+namespace Complexity
 
 open Probability Turing.MultiTapeTM Cslib.Logic.PL
 
@@ -232,4 +249,6 @@ theorem PNPLog_subset_PWithOracle (enc : α ↪ List Bool) :
 
 end
 
-end Cslib.Complexity
+end Complexity
+
+end Cslib

Complexity/Foundations/Data/BitString/ShortMembers.lean

@@ -23,7 +23,11 @@ public import Complexity.Foundations.Data.BitString.ShortWords
 ## Main results
 
 * `Cslib.BitString.mem_shortMembers`: its members.
+* `Cslib.BitString.nodup_shortMembers`: it has no repetition.
 * `Cslib.BitString.length_shortMembers`: its length is the number of short members.
+* `Cslib.BitString.length_le_length_shortMembers`,
+  `Cslib.BitString.mem_iff_of_length_eq_length_shortMembers`: the census bounds the duplicate-free
+  lists of short members, and a list attaining it lists them all.
 -/
 
 @[expose] public section
@@ -42,10 +46,38 @@ variable {S : Set (List Bool)} {n : ℕ}
 theorem mem_shortMembers {w : List Bool} : w ∈ shortMembers S n ↔ w ∈ S ∧ w.length ≤ n := by
   simp [shortMembers, and_comm]
 
+theorem nodup_shortMembers (S : Set (List Bool)) (n : ℕ) : (shortMembers S n).Nodup :=
+  Finset.nodup_toList _
+
 open Classical in
 /-- The listing has one entry for each member of `S` of length at most `n`. -/
 theorem length_shortMembers (S : Set (List Bool)) (n : ℕ) :
     (shortMembers S n).length = ((shortWords n).filter (· ∈ S)).card := by
   rw [shortMembers, Finset.length_toList]
 
+/-- **The census bounds the lists of distinct short members.** -/
+theorem length_le_length_shortMembers {ℓ : List (List Bool)} (hnd : ℓ.Nodup)
+    (h : ∀ s ∈ ℓ, s ∈ S ∧ s.length ≤ n) : ℓ.length ≤ (shortMembers S n).length := by
+  rw [← List.toFinset_card_of_nodup hnd, ← List.toFinset_card_of_nodup (nodup_shortMembers S n)]
+  exact Finset.card_le_card fun s hs => by
+    rw [List.mem_toFinset] at hs ⊢
+    exact mem_shortMembers.mpr (h s hs)
+
+/-- **A list attaining the census lists all short members.** A duplicate-free list of short
+members of `S` with as many entries as there are short members agrees with `S` on every short
+word. -/
+theorem mem_iff_of_length_eq_length_shortMembers {ℓ : List (List Bool)} (hnd : ℓ.Nodup)
+    (h : ∀ s ∈ ℓ, s ∈ S ∧ s.length ≤ n) (hlen : ℓ.length = (shortMembers S n).length)
+    {s : List Bool} (hs : s.length ≤ n) : s ∈ ℓ ↔ s ∈ S := by
+  have hsub : ℓ.toFinset ⊆ (shortMembers S n).toFinset := fun t ht => by
+    rw [List.mem_toFinset] at ht ⊢
+    exact mem_shortMembers.mpr (h t ht)
+  have heq := Finset.eq_of_subset_of_card_le hsub (by
+    rw [List.toFinset_card_of_nodup hnd, List.toFinset_card_of_nodup (nodup_shortMembers S n),
+      hlen])
+  refine ⟨fun hsℓ => (h s hsℓ).1, fun hsS => ?_⟩
+  have hmem : s ∈ (shortMembers S n).toFinset :=
+    List.mem_toFinset.mpr (mem_shortMembers.mpr ⟨hsS, hs⟩)
+  rwa [← heq, List.mem_toFinset] at hmem
+
 end Cslib.BitString

Complexity/Foundations/Data/List/Counting.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Init
 public import Mathlib.Data.List.Basic
+import Mathlib.Data.List.Nodup
 
 /-!
 # List counts and scan bounds
@@ -17,6 +18,7 @@ public import Mathlib.Data.List.Basic
 
 * `List.length_flatMap_le`: blocks of bounded length have bounded total length.
 * `List.decide_mem_eq_any`: membership as a scan of the list.
+* `List.not_any_one_lt_countP_iff_nodup`: duplicate-freeness as a scan of the list.
 * `List.countP_and_not_add_countP_and`: members satisfying one predicate split by whether
   they satisfy another.
 * `List.existsUnique_fin_of_countP_eq_one`, `List.existsUnique_mem_of_countP_eq_one`: a Boolean
@@ -44,6 +46,21 @@ theorem List.decide_mem_eq_any {α : Type*} [DecidableEq α] (a : α) (l : List
   rw [Bool.eq_iff_iff, decide_eq_true_eq, List.any_eq_true]
   simp
 
+/-- Duplicate-freeness as a scan of the list: no member occurs more than once, counted with
+`countP`. This is the form in which polynomial-time tests for repetitions are certified. -/
+theorem List.not_any_one_lt_countP_iff_nodup {α : Type*} [DecidableEq α] (l : List α) :
+    (!(l.any fun a => decide (1 < l.countP fun b => decide (b = a)))) = true ↔ l.Nodup := by
+  have hc (a : α) : (l.countP fun b => decide (b = a)) = l.count a := by
+    rw [List.count_eq_countP]
+    congr 1
+  simp only [Bool.not_eq_true', List.any_eq_false, decide_eq_true_eq, Nat.not_lt, hc]
+  rw [List.nodup_iff_count_le_one]
+  refine ⟨fun h a => ?_, fun h a _ => h a⟩
+  by_cases ha : a ∈ l
+  · exact h a ha
+  · rw [List.count_eq_zero_of_not_mem ha]
+    omega
+
 /-- Partitioning the elements of a list satisfying `p` by whether they satisfy `q`. -/
 theorem List.countP_and_not_add_countP_and {α : Type*} (p q : α → Prop) [DecidablePred p]
     [DecidablePred q] (l : List α) :

ComplexityTests/SparseKadin.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+import Complexity.Computability.Complexity.Classes.Oracle.Closure
+import Complexity.Computability.Complexity.Classes.Sparse.Kadin
+
+/-! # Kadin's theorem: census, binary search and the collapse -/
+
+namespace ComplexityTests.SparseKadin
+
+open Cslib Cslib.BitString Cslib.Complexity Turing.MultiTapeTM
+
+/-- The words consisting only of `true`s, a sparse language. -/
+private def unary : Set (List Bool) := {w | ∀ b ∈ w, b = true}
+
+-- A list attaining the census of the short members lists them all: the three all-`true` words of
+-- length at most `2`, in any order, agree with `unary` on every word of length at most `2`.
+example : [false] ∉ [[true, true], [], [true]] := by
+  have := mem_iff_of_length_eq_length_shortMembers (S := unary) (n := 2)
+    (ℓ := [[true, true], [], [true]]) (by decide)
+    (fun s hs => by
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hs
+      rcases hs with rfl | rfl | rfl <;> simp [unary])
+    (by
+      have hset : ∀ w : List Bool, w ∈ shortMembers unary 2 ↔
+          w ∈ ({[], [true], [true, true]} : Finset (List Bool)) := by
+        intro w
+        simp only [mem_shortMembers, unary, Set.mem_ofPred_eq, Finset.mem_insert,
+          Finset.mem_singleton]
+        constructor
+        · rintro ⟨hw, hlen⟩
+          match w, hlen with
+          | [], _ => simp
+          | [a], _ => simp [hw a (by simp)]
+          | [a, b], _ => simp [hw a (by simp), hw b (by simp)]
+        · rintro (rfl | rfl | rfl) <;> simp
+      rw [← List.toFinset_card_of_nodup (nodup_shortMembers unary 2),
+        show (shortMembers unary 2).toFinset = {[], [true], [true, true]} from
+          Finset.ext fun w => by rw [List.mem_toFinset, hset]]
+      rfl) (s := [false]) (by simp)
+  simp only [this, unary, Set.mem_ofPred_eq, List.mem_singleton, forall_eq]
+  decide
+
+-- Binary search finds the threshold `5` of `k ≤ 5` in `[0, 10]` with four rounds.
+example : ((KadinCensus.searchStep fun k => decide (k ≤ 5))^[4] (0, 10)).1 = 5 :=
+  KadinCensus.fst_iterate_searchStep (by norm_num) (by norm_num)
+
+example : (KadinCensus.searchStep fun k => decide (k ≤ 5))^[4] (0, 10) = (5, 5) := by
+  decide
+
+-- The algorithm, run against the oracle of the words of length at most `3` with requests
+-- `true ^ k`, finds the threshold `3` and accepts; it makes at most five requests.
+open Classical in
+example : OracleComp.interpret (m := Id) (languageOracle {w : List Bool | w.length ≤ 3})
+    (KadinCensus.program (fun x : Unit × ℕ => List.replicate x.2 true)
+      (fun x => List.replicate x.2 true) (fun _ => 10) (fun _ => 4) ()) = true := by
+  have key : ((KadinCensus.searchStep fun k => decide (k ≤ 3))^[4] (0, 10)).1 = 3 :=
+    KadinCensus.fst_iterate_searchStep (by norm_num) (by norm_num)
+  rw [KadinCensus.interpret_program]
+  simp only [Set.mem_ofPred_eq, List.length_replicate]
+  convert key.le using 4
+  exact decide_eq_true_iff
+
+example (answer : Unit × List Bool → List Bool) :
+    (OracleComp.queriesWith answer
+      (KadinCensus.program (fun x : Unit × ℕ => List.replicate x.2 true)
+        (fun x => List.replicate x.2 true) (fun _ => 10) (fun _ => 4) ())).length ≤ 5 :=
+  KadinCensus.length_queriesWith_program_le answer _ _ _ _ ()
+
+-- With the empty sparse set, the census is `0`: the request `(a, 0, false)` holds and
+-- `(a, 1, false)` does not.
+private theorem empty_mem_NP : (∅ : Set (List Bool)) ∈ NP encBits :=
+  P_subset_NP ⟨fun _ => false, ComputableInPolyTime.const false, fun _ => by simp⟩
+
+example (G : (List Bool × List Bool) × List (List Bool) → Bool) (a : List Bool) :
+    (a, 0, false) ∈ KadinCensus.language ∅ encBits 1 1 G ∧
+      (a, 1, false) ∉ KadinCensus.language ∅ encBits 1 1 G := by
+  rw [KadinCensus.mem_language_false_iff, KadinCensus.mem_language_false_iff]
+  have h0 : KadinCensus.census (∅ : Set (List Bool)) encBits 1 a = 0 := by
+    simp [KadinCensus.census, List.length_eq_zero_iff, List.eq_nil_iff_forall_not_mem]
+  omega
+
+-- The requests are in `NP`, for the sparse `NP` set `∅` and any polynomial-time `G`.
+example : KadinCensus.language ∅ encBits 1 1
+    (fun _ : (List Bool × List Bool) × List (List Bool) => false) ∈
+      NP (encPair encBits (encPair encUnary encBool)) :=
+  KadinCensus.language_mem_NP empty_mem_NP Set.finite_empty.mem_SPARSE
+    (ComputableInPolyTime.const false)
+
+-- The hypotheses of Kadin's theorem hold if `SAT ∈ P`, with the empty sparse set.
+example (h : SAT ∈ P encCNF) : PH encBits ⊆ PNPLog encBits :=
+  PH_subset_PNPLog_of_sparse Set.finite_empty.mem_SPARSE empty_mem_NP
+    (P_subset_PWithOracle ∅ encCNF h) encBits
+
+end ComplexityTests.SparseKadin

ROADMAP.md

@@ -210,8 +210,10 @@ index links to canonical definitions rather than keeping a second set.
   not charged to the space bound, and their transitivity; the rest of the inclusion hierarchy of
   Ladner, Lynch and Selman, and its separations.
 - **Sparse and tally sets:** `P/poly ⊆ P^SPARSE` (Meyer), the converse of
-  `PWithOracle_subset_PPolyOn` in `Classes/Sparse/Turing.lean`; Kadin's collapse of `PH` to
-  `P^{NP[O(log n)]}` under a sparse Turing-complete set for `NP` ([#2062]).
+  `PWithOracle_subset_PPolyOn` in `Classes/Sparse/Turing.lean`. After Kadin's
+  `PH ⊆ P^{NP[O(log n)]}` (`Classes/Sparse/Kadin.lean`, [#2062]): `P^{NP[O(log n)]} ⊆ Σ₂ᴾ ∩ Π₂ᴾ`,
+  hence `PH = Θ₂ᴾ` under his hypothesis; his stronger form with a sparse `S ∈ NP` and
+  `coNP ⊆ NP^S`; and `P^{NP[O(log n)]} = P^NP_tt` (Hemachandra).
 - **Berman–Hartmanis:** p-isomorphism and paddability; paddable NP-complete sets are p-isomorphic,
   so the standard NP-complete problems are all p-isomorphic to SAT; the isomorphism conjecture as a
   hypothesis; every many-one complete set for EXP is complete under one-one, length-increasing