Kadin 1989: a sparse Turing-complete set for NP collapses PH to P^{NP[O(log n)]} #2062

Goal. Kadin's theorem: if NP has a sparse Turing-complete set, the polynomial hierarchy collapses to P^{NP[O(log n)]}.

Proposed by coordinator-claude-e6cf7b0d and selected by Samuel. Claimed by worker-claude-e6cf7b0d-kadin89 (Claude Code, Opus) on branch claude/kadin-1989.

Sources and statement

• Kadin, P^{NP[O(log n)]} and sparse Turing-complete sets for NP, JCSS 39(3):282–298, 1989. I could not access the full text, so I cite it without a locator. Its abstract states the stronger form, with hypothesis "sparse S ∈ NP with coNP ⊆ NP^S", and the Turing-complete case as a consequence. This is the 1989 JCSS paper. The erratum recorded in doc(BooleanHierarchy): record Kadin's erratum and the provenance of the deeper BH collapse #2015 concerns the 1988 SICOMP Boolean-hierarchy paper, not this one.
• The proof followed here is Hemaspaandra and Ogihara, The Complexity Theory Companion, Theorem 1.14 (p. 19, proof pp. 19–20), which attributes the theorem to Kadin [Kad89]. I checked this locator against the chapter PDF on the authors' companion site. The definition of P^{NP[O(log n)]} that I use, "allowed at most O(log n) queries to some NP oracle", is on p. 1 of the same chapter.

Target Lean statement (names provisional; M1 is #2065):

theorem PH_subset_PNPLog_of_sparse {S : Set (List Bool)} (hsparse : S ∈ SPARSE encBits)
    (hS : S ∈ NP encBits) (hSAT : SAT ∈ PWithOracle S encCNF) (enc : α ↪ List Bool) :
    PH enc ⊆ PNPLog enc

The hypotheses say that S is a sparse set in NP and that SAT ≤ᵀ S, which is Turing-completeness. NP ⊆ P^S then follows from Cook–Levin and PolyTimeReducible.mem_PWithOracle. The theorem also gives PH enc = SigmaP 2 enc along the way. The Companion concludes PH = Θ₂ᵖ. The reverse inclusion P^{NP[O(log n)]} ⊆ PH is not needed for Kadin's direction, so it is left as a follow-up.

Definitions (no bounded-query class exists on main)

In a new module Classes/Oracle/BoundedQuery.lean:

• ComputableInPolyTimeWithOracleQueries A r f input output: the same certificate as ComputableInPolyTimeWithOracle, plus a bound on the requests. Run against languageOracle A, the program makes at most r (input a).length requests, counted by OracleComp.queriesWith.
• PWithOracleQueries A r enc: the deciders of this kind.
• PNPLog enc := ⋃ A ∈ NP encBits, ⋃ c, PWithOracleQueries A (fun n => c * Nat.log 2 n + c) enc. This follows the shape of ENP in feat(Classes/Oracle): E relative to an oracle and E^NP (#1539 M1) #2055.

The requests are counted against the oracle A itself, which is the textbook convention. A clocked machine can always add a counter, so a bound uniform over all oracles would give the same class.

Proof plan

1. Finite-list oracle simulation (new, reusable). If f is polynomial time relative to S, there are a polynomial q and a polynomial-time F : α × List (List Bool) → β such that F (a, ℓ) = f a whenever ℓ agrees with S on all words of length at most q |enc a|. The proof builds the canonical oracle transcript one bit at a time with the existing replay API (replayConfig_pt, oracleReplies, replayOutput_oracleReplies), using plain ComputableInPolyTime.iterate*. Locality (interpret_languageOracle_congr) together with the clock bound on request lengths finishes the proof.
2. P^S ⊆ P/poly for sparse S (the Meyer direction of the ROADMAP item P/poly = P^SPARSE). The advice at length n is encList encBits applied to a listing of S^{≤ q n}. It has polynomial length because S is sparse. It is decoded with Decoder.bits.list and hardwired by PPoly.of_advice. Together with Karp–Lipton (NP_subset_PPolyOn_iff_SAT, PH_eq_SigmaP_two_of_SAT), this gives PH = Σ₂. That replaces the Companion's step "Θ₂ ⊆ Σ₂, and Θ₂ is closed under complement", which would need P^{NP} ⊆ Σ₂. The deviation is recorded in the docstring.
3. Census and recognition of S^{≤m}. Let L ∈ Σ₂. Write a ∈ L ↔ ∃ w, (a, w) ∉ B, where B ∈ NP ⊆ P^S, using exists_mem_PiP_of_mem_SigmaP_succ. Step 1 gives F and a polynomial m that bounds the oracle words relevant on inputs (a, w). Then define one NP language D on (a, k, b): some duplicate-free list ℓ of exactly k words has every word of length at most m |enc a| and in S, and if b = true, also ∃ w, F ((a, w), ℓ) = false. Membership in NP goes through mem_NP_of_witness with a decoder for the list of words, their S-certificates, and w. Duplicate-freeness is checked as (eraseDupsBy (· == ·) ℓ).length = ℓ.length.
   • D (a, k, false) says that the census ‖S^{≤m}‖ is at least k.
   • When k is the exact census, the guessed list is exactly S^{≤m}, so D (a, k, true) ↔ a ∈ L. This is where S ∈ NP and the exact census are used.
4. Binary search with O(log n) queries. The census lies in [0, N], where N = p_S(m |enc a|) is polynomial. The oracle program keeps an interval [lo, hi] that contains the census. While lo < hi, it asks D (a, ⌈(lo+hi)/2⌉, false) and halves the interval. It runs Nat.size N rounds, then asks D (a, lo, true). In total it makes at most Nat.size N + 1 ≤ c log n + c requests. The loop is certified with IsOraclePPTOn.iterateWith_spec', as in the SAT self-reduction of feat(Classes/Oracle): the SAT self-reduction relative to an oracle (#1539 M4a) #2059, with an extra lemma counting queriesWith through OracleComp.iterate. The oracle is encoded '' D ∈ NP encBits.
5. Collapse. Σ₂ ⊆ P^{NP[O(log n)]} by steps 3–4, and PH = Σ₂ by step 2. So PH ⊆ P^{NP[O(log n)]}.

Milestones

• M1: the bounded-query classes and their basic API: P ⊆, NP ∪ coNP ⊆ PNPLog, closure under complement, inclusion in P^A. Tests instantiate them non-vacuously.
• M2: the finite-list oracle simulation (step 1), P^S ⊆ P/poly for sparse S, and PH = Σ₂ under the hypotheses (step 2).
• M3: census, binary search, and Kadin's theorem (steps 3–5).