From 59b5ade0d6df0ca33df3c367d5861dd500a7fcba Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:30:59 -0400 Subject: [PATCH 01/12] feat(Classes/Oracle): bounded-query oracle classes and P^{NP[O(log n)]} (#2062 M1) Define ComputableInPolyTimeWithOracleQueries, PWithOracleQueries and PNPLog, with the basic API: P, NP and coNP inside PNPLog (one request to SAT through Cook-Levin), closure under complement, and inclusion in P^NP. Move mem_NP_image and image_SAT_mem_NP from PH/Kannan into the small topic module Classes/NP/Image so that oracle classes can use them without importing Kannan's circuit dependencies. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/NP/Image.lean | 62 +++++ .../Classes/Oracle/BoundedQuery.lean | 244 ++++++++++++++++++ .../Complexity/Classes/PH/Kannan.lean | 31 +-- ComplexityTests/OracleBoundedQuery.lean | 55 ++++ references.bib | 21 ++ 6 files changed, 385 insertions(+), 30 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/NP/Image.lean create mode 100644 Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean create mode 100644 ComplexityTests/OracleBoundedQuery.lean diff --git a/Complexity.lean b/Complexity.lean index 5830f638a9..97ffc768ce 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1232,6 +1232,7 @@ public import Complexity.Computability.Complexity.Classes.ModP.GapP public import Complexity.Computability.Complexity.Classes.NP public import Complexity.Computability.Complexity.Classes.NP.Closure public import Complexity.Computability.Complexity.Classes.NP.GuessVerify +public import Complexity.Computability.Complexity.Classes.NP.Image public import Complexity.Computability.Complexity.Classes.NP.Nondeterministic public import Complexity.Computability.Complexity.Classes.NP.SelfReduction public import Complexity.Computability.Complexity.Classes.NP.TruthTable @@ -1239,6 +1240,7 @@ public import Complexity.Computability.Complexity.Classes.NP.Witness public import Complexity.Computability.Complexity.Classes.Operators public import Complexity.Computability.Complexity.Classes.Oracle public import Complexity.Computability.Complexity.Classes.Oracle.BakerGillSolovay +public import Complexity.Computability.Complexity.Classes.Oracle.BoundedQuery public import Complexity.Computability.Complexity.Classes.Oracle.Closure public import Complexity.Computability.Complexity.Classes.Oracle.Collapse public import Complexity.Computability.Complexity.Classes.Oracle.Counting diff --git a/Complexity/Computability/Complexity/Classes/NP/Image.lean b/Complexity/Computability/Complexity/Classes/NP/Image.lean new file mode 100644 index 0000000000..15efd0c503 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/NP/Image.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Problems.SAT +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder +import Complexity.Computability.Complexity.Problems.SAT.PolyTime +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List + +/-! +# Images of problems in `NP` + +The encodings of the members of a problem in `NP` form a problem in `NP` on words, when the +encoding has a decoder (`Cslib.Complexity.mem_NP_image`): the verifier decodes the word, checks +that it encodes what was decoded, and runs the verifier of the problem. In particular the +encodings of the satisfiable formulas form a problem in `NP` on words +(`Cslib.Complexity.image_SAT_mem_NP`), an oracle language that answers, through the Cook–Levin +reduction, every problem in `NP`. + +## Main results + +* `Cslib.Complexity.mem_NP_image`: images of problems in `NP` under encodings with decoders. +* `Cslib.Complexity.image_SAT_mem_NP`: the encodings of the satisfiable formulas. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +/-- **Images of problems in `NP`.** The encodings of the members of a problem in `NP` form a +problem in `NP` on words, when the encoding has a decoder: the verifier decodes the word, checks +that it encodes what was decoded, and runs the verifier of the problem. -/ +theorem mem_NP_image {β : Type} {encB : β ↪ List Bool} (D : Decoder encB) {B : Set β} + (hB : B ∈ NP encB) : encB '' B ∈ NP encBits := by + obtain ⟨p, V, hV, hBV⟩ := mem_NP.mp hB + have hdec : ComputableInPolyTime (fun x : List Bool × List Bool => D.decode x.1) + (encPair encBits encBits) encB := D.computableInPolyTime.comp (.fst _ _) + have henc : ComputableInPolyTime (fun b => encB b) encB encBits := .of_eq fun _ => rfl + refine mem_NP.mpr + ⟨p, fun x => decide (encB (D.decode x.1) = x.1) && V (D.decode x.1, x.2), by fun_prop, + fun w => ?_⟩ + simp only [encBits_apply, Bool.and_eq_true, decide_eq_true_eq] + constructor + · rintro ⟨b, hb, rfl⟩ + obtain ⟨c, hc, hVc⟩ := (hBV b).1 hb + exact ⟨c, hc, by rw [D.decode_enc], by rw [D.decode_enc]; exact hVc⟩ + · rintro ⟨c, hc, hw, hVc⟩ + exact ⟨D.decode w, (hBV _).2 ⟨c, by rw [hw]; exact hc, hVc⟩, hw⟩ + +/-- The encodings of the satisfiable formulas form a problem in `NP` on words. -/ +theorem image_SAT_mem_NP : encCNF '' SAT ∈ NP encBits := + mem_NP_image (.list (.list (.pair .nat .bool))) SAT.mem_NP + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean new file mode 100644 index 0000000000..0c45e21b91 --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean @@ -0,0 +1,244 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Oracle +public import Complexity.Computability.Complexity.Problems.SAT +import Complexity.Computability.Complexity.Classes.NP.Image +import Complexity.Computability.Complexity.CookLevin.Completeness +import Complexity.Computability.Probabilistic.Oracle.Composition + +/-! +# Bounded-query oracle classes and `P^{NP[O(log n)]}` + +`f` is computable in polynomial time relative to `A` with `r` requests +(`Cslib.Complexity.ComputableInPolyTimeWithOracleQueries`) when it has the certificate of +`Cslib.Complexity.ComputableInPolyTimeWithOracle` and the program, run against the oracle +language `A`, makes at most `r n` requests on instances of encoded length `n` +(`Cslib.OracleComp.queriesWith`). The requests are counted against `A` itself, as in the usual +definition of a machine with oracle `A` making a bounded number of queries; the certificate's +clock bounds the requests against every oracle in any case +(`Cslib.Probability.IsOraclePPTOn.query_bounds`). + +`P^{NP[O(log n)]}` (`Cslib.Complexity.PNPLog`) is the class of problems decided in polynomial time +with at most `c log₂ n + c` requests to some oracle language in `NP`, for a constant `c` +[Hemaspaandra and Ogihara, Section 1.2][HemaspaandraOgihara2002] [Kadin][Kadin1989]. It contains +`NP` and `coNP` with one request to the encodings of the satisfiable formulas +(`Cslib.Complexity.NP_subset_PWithOracleQueries_image_SAT`), through the Cook–Levin reduction, and +is closed under complement. + +## Main definitions + +* `Cslib.Complexity.ComputableInPolyTimeWithOracleQueries`: polynomial time relative to an oracle + with a bounded number of requests. +* `Cslib.Complexity.PWithOracleQueries`: the problems so decided. +* `Cslib.Complexity.PNPLog`: `P^{NP[O(log n)]}`. + +## Main results + +* `Cslib.Complexity.ComputableInPolyTimeWithOracleQueries.computableInPolyTimeWithOracle`, + `.mono`, `.map`: forgetting and weakening the bound, and postprocessing. +* `Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithOracleQueries`: polynomial time + makes no request. +* `Cslib.Complexity.computableInPolyTimeWithOracleQueries_query`: one request decides membership + of a polynomial-time request word. +* `Cslib.Complexity.compl_mem_PWithOracleQueries`, `Cslib.Complexity.compl_mem_PNPLog`: closure + under complement. +* `Cslib.Complexity.NP_subset_PWithOracleQueries_image_SAT`: one request to `SAT` decides a + problem in `NP`. +* `Cslib.Complexity.P_subset_PNPLog`, `Cslib.Complexity.NP_subset_PNPLog`, + `Cslib.Complexity.coNP_subset_PNPLog`, `Cslib.Complexity.PNPLog_subset_PWithOracle`. + +## References + +* [L. A. Hemaspaandra, M. Ogihara, *The Complexity Theory Companion*][HemaspaandraOgihara2002] +* [J. Kadin, *P^{NP[O(log n)]} and sparse Turing-complete sets for NP*][Kadin1989] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Probability Turing.MultiTapeTM Cslib.Logic.PL + +variable {α β γ : Type} + +/-- `f` is computable in polynomial time relative to the oracle language `A` with at most `r n` +requests on instances of encoded length `n`: one deterministic word-query program has the +certificate of `ComputableInPolyTimeWithOracle`, computes `f` against `A`, and makes at most +`r (input a).length` requests on `a` against `A`. -/ +def ComputableInPolyTimeWithOracleQueries (A : Set (List Bool)) (r : ℕ → ℕ) (f : α → β) + (input : α ↪ List Bool) (output : β ↪ List Bool) : Prop := + ∃ program : α → WordQueryComp Unit β, + IsOraclePPTOn input output (fun a => OracleComp.interpret ProbOracleComp.query (program a)) ∧ + ∀ a, OracleComp.interpret (m := Id) (languageOracle A) (program a) = f a ∧ + (OracleComp.queriesWith (languageOracle A) (program a)).length ≤ r (input a).length + +namespace ComputableInPolyTimeWithOracleQueries + +variable {A : Set (List Bool)} {r r' : ℕ → ℕ} {input : α ↪ List Bool} {middle : β ↪ List Bool} + {output : γ ↪ List Bool} + +/-- A bounded number of requests is in particular polynomial time relative to the oracle. -/ +theorem computableInPolyTimeWithOracle {f : α → β} + (h : ComputableInPolyTimeWithOracleQueries A r f input middle) : + ComputableInPolyTimeWithOracle A f input middle := + let ⟨program, hprogram, heq⟩ := h + ⟨program, hprogram, fun a => (heq a).1⟩ + +/-- Weakening the bound on the requests. -/ +theorem mono {f : α → β} (h : ComputableInPolyTimeWithOracleQueries A r f input middle) + (hr : ∀ n, r n ≤ r' n) : ComputableInPolyTimeWithOracleQueries A r' f input middle := + let ⟨program, hprogram, heq⟩ := h + ⟨program, hprogram, fun a => ⟨(heq a).1, (heq a).2.trans (hr _)⟩⟩ + +/-- Polynomial-time postprocessing of the result makes no further request. -/ +theorem map {f : α → β} {g : β → γ} (h : ComputableInPolyTimeWithOracleQueries A r f input middle) + (hg : ComputableInPolyTime g middle output) : + ComputableInPolyTimeWithOracleQueries A r (fun a => g (f a)) input output := by + obtain ⟨program, hprogram, heq⟩ := h + refine ⟨fun a => g <$> program a, ?_, fun a => ⟨?_, ?_⟩⟩ + · simpa only [OracleComp.interpret_map] using hprogram.map' hg + · rw [OracleComp.interpret_map, (heq a).1] + rfl + · rw [OracleComp.queriesWith_map] + exact (heq a).2 + +end ComputableInPolyTimeWithOracleQueries + +/-- A polynomial-time computation makes no request. -/ +theorem _root_.Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithOracleQueries + {f : α → β} {input : α ↪ List Bool} {output : β ↪ List Bool} + (h : ComputableInPolyTime f input output) (A : Set (List Bool)) (r : ℕ → ℕ) : + ComputableInPolyTimeWithOracleQueries A r f input output := + ⟨fun a => pure (f a), h.isOraclePPTOn, fun _ => ⟨rfl, by simp⟩⟩ + +open Classical in +/-- **One request.** The polynomial-time request `req a` is submitted and the first bit of the +reply is read: this decides whether `req a ∈ A` with one request. -/ +theorem computableInPolyTimeWithOracleQueries_query {req : α → List Bool} + {input : α ↪ List Bool} (hreq : ComputableInPolyTime req input encBits) + (A : Set (List Bool)) : + ComputableInPolyTimeWithOracleQueries A (fun _ => 1) (fun a => decide (req a ∈ A)) input + encBool := by + refine ⟨fun a => (fun reply => decide (reply = [true])) <$> + (List.take 1 <$> OracleComp.query ((), req a)), ?_, fun a => ⟨?_, ?_⟩⟩ + · simp only [OracleComp.interpret_map, OracleComp.interpret_query] + exact (IsOraclePPTOn.query_take' () hreq (limit := fun _ => 1) + (ComputableInPolyTime.const 1)).map' + (ComputableInPolyTime.id'.decide_eq' (ComputableInPolyTime.const [true])) + · change decide (List.take 1 (languageOracle A ((), req a)) = [true]) = decide (req a ∈ A) + rw [languageOracle_apply] + cases decide (req a ∈ A) <;> rfl + · simp + +/-- The problems decided in polynomial time relative to the oracle language `A` with at most +`r n` requests on instances of encoded length `n`. -/ +def PWithOracleQueries (A : Set (List Bool)) (r : ℕ → ℕ) (enc : α ↪ List Bool) : Set (Set α) := + {L | ∃ f : α → Bool, ComputableInPolyTimeWithOracleQueries A r f enc encBool ∧ + ∀ a, a ∈ L ↔ f a = true} + +theorem mem_PWithOracleQueries {A : Set (List Bool)} {r : ℕ → ℕ} {enc : α ↪ List Bool} + {L : Set α} : + L ∈ PWithOracleQueries A r enc ↔ ∃ f : α → Bool, + ComputableInPolyTimeWithOracleQueries A r f enc encBool ∧ ∀ a, a ∈ L ↔ f a = true := + Iff.rfl + +/-- **`P^{NP[O(log n)]}`**: the problems decided in polynomial time with at most `c log₂ n + c` +requests, on instances of encoded length `n`, to some oracle language in `NP` +[Hemaspaandra and Ogihara, Section 1.2][HemaspaandraOgihara2002] [Kadin][Kadin1989]. -/ +def PNPLog (enc : α ↪ List Bool) : Set (Set α) := + ⋃ A ∈ NP encBits, ⋃ c : ℕ, PWithOracleQueries A (fun n => c * Nat.log 2 n + c) enc + +theorem mem_PNPLog {enc : α ↪ List Bool} {L : Set α} : + L ∈ PNPLog enc ↔ ∃ A ∈ NP encBits, ∃ c : ℕ, + L ∈ PWithOracleQueries A (fun n => c * Nat.log 2 n + c) enc := by + simp only [PNPLog, Set.mem_iUnion, exists_prop] + +section + +variable {A : Set (List Bool)} {r r' : ℕ → ℕ} {enc : α ↪ List Bool} {L : Set α} + +theorem PWithOracleQueries_subset_PWithOracle : + PWithOracleQueries A r enc ⊆ PWithOracle A enc := fun _ ⟨f, hf, hL⟩ => + ⟨f, hf.computableInPolyTimeWithOracle, hL⟩ + +theorem PWithOracleQueries_mono (hr : ∀ n, r n ≤ r' n) : + PWithOracleQueries A r enc ⊆ PWithOracleQueries A r' enc := fun _ ⟨f, hf, hL⟩ => + ⟨f, hf.mono hr, hL⟩ + +/-- A problem in `P` is decided with no request. -/ +theorem P_subset_PWithOracleQueries (A : Set (List Bool)) (r : ℕ → ℕ) (enc : α ↪ List Bool) : + P enc ⊆ PWithOracleQueries A r enc := fun _ ⟨f, hf, hL⟩ => + ⟨f, hf.computableInPolyTimeWithOracleQueries A r, hL⟩ + +/-- **Closure under complement**: negate the decider, with the same requests. -/ +theorem compl_mem_PWithOracleQueries (hL : L ∈ PWithOracleQueries A r enc) : + Lᶜ ∈ PWithOracleQueries A r enc := by + obtain ⟨f, hf, hL⟩ := hL + refine ⟨fun a => !f a, hf.map (by fun_prop), fun a => ?_⟩ + rw [Set.mem_compl_iff, hL a] + simp + +open Classical in +/-- A problem that reduces in polynomial time to the oracle language is decided with one +request. -/ +theorem mem_PWithOracleQueries_of_reduction {req : α → List Bool} + (hreq : ComputableInPolyTime req enc encBits) (h : ∀ a, a ∈ L ↔ req a ∈ A) : + L ∈ PWithOracleQueries A (fun _ => 1) enc := + ⟨_, computableInPolyTimeWithOracleQueries_query hreq A, fun a => by + rw [h a, decide_eq_true_iff]⟩ + +/-- **One request to `SAT` decides a problem in `NP`**: the request is the encoding of the +Cook–Levin reduction of the instance. -/ +theorem NP_subset_PWithOracleQueries_image_SAT (enc : α ↪ List Bool) : + NP enc ⊆ PWithOracleQueries (encCNF '' SAT) (fun _ => 1) enc := by + intro L hL + obtain ⟨f, hf, hfL⟩ := CookLevin.SAT_npHard enc L hL + have henc : ComputableInPolyTime (fun φ : CNF ℕ => encCNF φ) encCNF encBits := + .of_eq fun _ => rfl + refine mem_PWithOracleQueries_of_reduction (req := fun a => encCNF (f a)) (henc.comp hf) + fun a => ?_ + rw [hfL a] + exact ⟨fun h => ⟨f a, h, rfl⟩, fun ⟨_, h, he⟩ => encCNF.injective he ▸ h⟩ + +/-- A problem decided with `c log₂ n + c` requests to an oracle language in `NP` is in +`P^{NP[O(log n)]}`. -/ +theorem mem_PNPLog_of_mem_PWithOracleQueries (hA : A ∈ NP encBits) {c : ℕ} + (hL : L ∈ PWithOracleQueries A (fun n => c * Nat.log 2 n + c) enc) : L ∈ PNPLog enc := + mem_PNPLog.mpr ⟨A, hA, c, hL⟩ + +/-- **`P^{NP[O(log n)]}` is closed under complement.** -/ +theorem compl_mem_PNPLog (hL : L ∈ PNPLog enc) : Lᶜ ∈ PNPLog enc := by + obtain ⟨A, hA, c, hL⟩ := mem_PNPLog.mp hL + exact mem_PNPLog_of_mem_PWithOracleQueries hA (compl_mem_PWithOracleQueries hL) + +/-- `P ⊆ P^{NP[O(log n)]}`. -/ +theorem P_subset_PNPLog (enc : α ↪ List Bool) : P enc ⊆ PNPLog enc := fun _ hL => + mem_PNPLog_of_mem_PWithOracleQueries image_SAT_mem_NP + (P_subset_PWithOracleQueries _ (fun n => 0 * Nat.log 2 n + 0) enc hL) + +/-- **`NP ⊆ P^{NP[O(log n)]}`**, with one request to `SAT`. -/ +theorem NP_subset_PNPLog (enc : α ↪ List Bool) : NP enc ⊆ PNPLog enc := fun _ hL => + mem_PNPLog_of_mem_PWithOracleQueries (c := 1) image_SAT_mem_NP + (PWithOracleQueries_mono (fun n => by omega) (NP_subset_PWithOracleQueries_image_SAT enc hL)) + +/-- **`coNP ⊆ P^{NP[O(log n)]}`**. -/ +theorem coNP_subset_PNPLog (enc : α ↪ List Bool) : coNP enc ⊆ PNPLog enc := fun _ hL => by + simpa only [compl_compl] using compl_mem_PNPLog (NP_subset_PNPLog enc hL) + +/-- `P^{NP[O(log n)]} ⊆ P^{NP}`. -/ +theorem PNPLog_subset_PWithOracle (enc : α ↪ List Bool) : + PNPLog enc ⊆ ⋃ A ∈ NP encBits, PWithOracle A enc := by + intro L hL + obtain ⟨A, hA, c, hL⟩ := mem_PNPLog.mp hL + exact Set.mem_biUnion hA (PWithOracleQueries_subset_PWithOracle hL) + +end + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/PH/Kannan.lean b/Complexity/Computability/Complexity/Classes/PH/Kannan.lean index c85c3142bd..ca03474d3f 100644 --- a/Complexity/Computability/Complexity/Classes/PH/Kannan.lean +++ b/Complexity/Computability/Complexity/Classes/PH/Kannan.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Circuit.Boolean.PPoly public import Complexity.Computability.Circuit.Boolean.Substitution +public import Complexity.Computability.Complexity.Classes.NP.Image public import Complexity.Computability.Complexity.Classes.PH public import Complexity.Computability.Complexity.Problems.SAT public import Complexity.Computability.MCSP.NP @@ -62,10 +63,6 @@ not say which of the two languages witnesses the theorem. ## Main results -* `Cslib.Complexity.mem_NP_image`: the encodings of the members of a problem in `NP` form a - problem in `NP` on words, when the encoding has a decoder. -* `Cslib.Complexity.image_SAT_mem_NP`: the encodings of the satisfiable formulas form a problem in - `NP` on words. * `Cslib.Complexity.Kannan.language_notMem_SIZE`: Kannan's language has no circuits of size `O(n ^ k)`. * `Cslib.Complexity.Kannan.language_mem_SigmaP_three`: Kannan's language is in `Σ₃`. @@ -87,32 +84,6 @@ namespace Cslib.Complexity open Circuits Circuits.Boolean Turing.MultiTapeTM Filter -/-! ### Images of problems in `NP` -/ - -/-- **Images of problems in `NP`.** The encodings of the members of a problem in `NP` form a -problem in `NP` on words, when the encoding has a decoder: the verifier decodes the word, checks -that it encodes what was decoded, and runs the verifier of the problem. -/ -theorem mem_NP_image {β : Type} {encB : β ↪ List Bool} (D : Decoder encB) {B : Set β} - (hB : B ∈ NP encB) : encB '' B ∈ NP encBits := by - obtain ⟨p, V, hV, hBV⟩ := mem_NP.mp hB - have hdec : ComputableInPolyTime (fun x : List Bool × List Bool => D.decode x.1) - (encPair encBits encBits) encB := D.computableInPolyTime.comp (.fst _ _) - have henc : ComputableInPolyTime (fun b => encB b) encB encBits := .of_eq fun _ => rfl - refine mem_NP.mpr - ⟨p, fun x => decide (encB (D.decode x.1) = x.1) && V (D.decode x.1, x.2), by fun_prop, - fun w => ?_⟩ - simp only [encBits_apply, Bool.and_eq_true, decide_eq_true_eq] - constructor - · rintro ⟨b, hb, rfl⟩ - obtain ⟨c, hc, hVc⟩ := (hBV b).1 hb - exact ⟨c, hc, by rw [D.decode_enc], by rw [D.decode_enc]; exact hVc⟩ - · rintro ⟨c, hc, hw, hVc⟩ - exact ⟨D.decode w, (hBV _).2 ⟨c, by rw [hw]; exact hc, hVc⟩, hw⟩ - -/-- The encodings of the satisfiable formulas form a problem in `NP` on words. -/ -theorem image_SAT_mem_NP : encCNF '' SAT ∈ NP encBits := - mem_NP_image (.list (.list (.pair .nat .bool))) SAT.mem_NP - namespace Kannan /-! ### Parameters -/ diff --git a/ComplexityTests/OracleBoundedQuery.lean b/ComplexityTests/OracleBoundedQuery.lean new file mode 100644 index 0000000000..7374d42c03 --- /dev/null +++ b/ComplexityTests/OracleBoundedQuery.lean @@ -0,0 +1,55 @@ +/- +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.NP.Image +import Complexity.Computability.Complexity.Classes.Oracle.BoundedQuery +import Complexity.Computability.Complexity.Problems.SAT.PolyTime + +/-! # Bounded-query oracle classes and `P^{NP[O(log n)]}` -/ + +namespace ComplexityTests.OracleBoundedQuery + +open Cslib Cslib.Complexity Cslib.Logic.PL Turing.MultiTapeTM + +-- One request decides the oracle language itself, with the bound `1` at every length. +open Classical in +example (A : Set (List Bool)) : + ComputableInPolyTimeWithOracleQueries A (fun _ => 1) (fun w => decide (w ∈ A)) encBits + encBool := + computableInPolyTimeWithOracleQueries_query ComputableInPolyTime.id' A + +-- The single-request program asks exactly the word it decides: one request, answered by `A`. +open Classical in +example (A : Set (List Bool)) (w : List Bool) : + OracleComp.queriesWith (languageOracle A) + ((fun reply => decide (reply = [true])) <$> + (List.take 1 <$> OracleComp.query (spec := fun _ : Unit × List Bool => List Bool) + ((), w))) = [((), w)] := by + simp + +-- `SAT` and its complement are in `P^{NP[O(log n)]}`. +example : SAT ∈ PNPLog encCNF := NP_subset_PNPLog encCNF SAT.mem_NP + +example : SATᶜ ∈ PNPLog encCNF := compl_mem_PNPLog (NP_subset_PNPLog encCNF SAT.mem_NP) + +-- `SAT` is decided by one request to the encodings of the satisfiable formulas, and so lies in +-- `P` relative to that oracle. +example : SAT ∈ PWithOracleQueries (encCNF '' SAT) (fun _ => 1) encCNF := + NP_subset_PWithOracleQueries_image_SAT encCNF SAT.mem_NP + +example : SAT ∈ PWithOracle (encCNF '' SAT) encCNF := + PWithOracleQueries_subset_PWithOracle (NP_subset_PWithOracleQueries_image_SAT encCNF SAT.mem_NP) + +-- The classes grow with the bound on the requests. +example : PWithOracleQueries (encCNF '' SAT) (fun _ => 1) encCNF ⊆ + PWithOracleQueries (encCNF '' SAT) (fun n => Nat.log 2 n + 1) encCNF := + PWithOracleQueries_mono fun _ => by omega + +-- A polynomial-time problem needs no request at all: the bound `0` suffices. +example : (Set.univ : Set (List Bool)) ∈ PWithOracleQueries ∅ (fun _ => 0) encBits := + P_subset_PWithOracleQueries ∅ _ encBits ⟨fun _ => true, ComputableInPolyTime.const true, + fun _ => by simp⟩ + +end ComplexityTests.OracleBoundedQuery diff --git a/references.bib b/references.bib index a11861ab4d..3707d4aff6 100644 --- a/references.bib +++ b/references.bib @@ -2362,6 +2362,16 @@ @misc{HemaspaandraHemaspaandraHempel1999 abstract in SIGACT News 29, 10--22, 1998} } +@book{HemaspaandraOgihara2002, + author = {Hemaspaandra, Lane A. and Ogihara, Mitsunori}, + title = {The Complexity Theory Companion}, + series = {Texts in Theoretical Computer Science. An EATCS Series}, + publisher = {Springer}, + address = {Berlin, Heidelberg}, + year = {2002}, + doi = {10.1007/978-3-662-04880-1} +} + @article{ Hennessy1985, author = {Matthew Hennessy and Robin Milner}, @@ -2762,6 +2772,17 @@ @article{Kadin1988 doi = {10.1137/0217080} } +@article{Kadin1989, + author = {Kadin, Jim}, + title = {{$P^{NP[O(\log n)]}$} and Sparse {Turing}-Complete Sets for {NP}}, + journal = {Journal of Computer and System Sciences}, + volume = {39}, + number = {3}, + pages = {282--298}, + year = {1989}, + doi = {10.1016/0022-0000(89)90024-X} +} + @article{Kadin1991, author = {Kadin, Jim}, title = {Erratum: The Polynomial Time Hierarchy Collapses if the {Boolean} Hierarchy Collapses}, From c1eda7513c7fc81d66ddbce0565f9c8d41259315 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:38:53 -0400 Subject: [PATCH 02/12] doc(Classes/Oracle): cite the page that defines P^{NP[O(log n)]} Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Computability/Complexity/Classes/Oracle/BoundedQuery.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean index 0c45e21b91..e04576572b 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean @@ -27,7 +27,7 @@ clock bounds the requests against every oracle in any case `P^{NP[O(log n)]}` (`Cslib.Complexity.PNPLog`) is the class of problems decided in polynomial time with at most `c log₂ n + c` requests to some oracle language in `NP`, for a constant `c` -[Hemaspaandra and Ogihara, Section 1.2][HemaspaandraOgihara2002] [Kadin][Kadin1989]. It contains +[Hemaspaandra and Ogihara, p. 1][HemaspaandraOgihara2002] [Kadin][Kadin1989]. It contains `NP` and `coNP` with one request to the encodings of the satisfiable formulas (`Cslib.Complexity.NP_subset_PWithOracleQueries_image_SAT`), through the Cook–Levin reduction, and is closed under complement. @@ -151,7 +151,7 @@ theorem mem_PWithOracleQueries {A : Set (List Bool)} {r : ℕ → ℕ} {enc : α /-- **`P^{NP[O(log n)]}`**: the problems decided in polynomial time with at most `c log₂ n + c` requests, on instances of encoded length `n`, to some oracle language in `NP` -[Hemaspaandra and Ogihara, Section 1.2][HemaspaandraOgihara2002] [Kadin][Kadin1989]. -/ +[Hemaspaandra and Ogihara, p. 1][HemaspaandraOgihara2002] [Kadin][Kadin1989]. -/ def PNPLog (enc : α ↪ List Bool) : Set (Set α) := ⋃ A ∈ NP encBits, ⋃ c : ℕ, PWithOracleQueries A (fun n => c * Nat.log 2 n + c) enc From a615f875c96e0ae1170c112663981b265700b49c Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:40:16 -0400 Subject: [PATCH 03/12] =?UTF-8?q?feat(Classes/Sparse):=20finite-list=20ora?= =?UTF-8?q?cles,=20P^SPARSE=20=E2=8A=86=20P/poly,=20and=20PH=20=3D=20?= =?UTF-8?q?=CE=A3=E2=82=82=20under=20a=20sparse=20Turing-hard=20set=20(#20?= =?UTF-8?q?62=20M2)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A computation in polynomial time relative to S runs in polynomial time against any finite list of words that agrees with S on words no longer than its clock (ComputableInPolyTimeWithOracle.exists_listOracle): the canonical oracle transcript is built bit by bit with the replay API. With the list of short members of a sparse S as advice, P^S ⊆ P/poly (PWithOracle_subset_PPolyOn), and Karp–Lipton gives PH = Σ₂ when SAT is Turing reducible to a sparse set. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Oracle/ListOracle.lean | 258 ++++++++++++++++++ .../Complexity/Classes/Sparse/Turing.lean | 135 +++++++++ ComplexityTests/SparseTuring.lean | 55 ++++ ROADMAP.md | 6 +- 5 files changed, 454 insertions(+), 2 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean create mode 100644 Complexity/Computability/Complexity/Classes/Sparse/Turing.lean create mode 100644 ComplexityTests/SparseTuring.lean diff --git a/Complexity.lean b/Complexity.lean index 97ffc768ce..1ba97f7042 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1247,6 +1247,7 @@ public import Complexity.Computability.Complexity.Classes.Oracle.Counting public import Complexity.Computability.Complexity.Classes.Oracle.CountingEquivalence public import Complexity.Computability.Complexity.Classes.Oracle.Deterministic public import Complexity.Computability.Complexity.Classes.Oracle.Diagonal +public import Complexity.Computability.Complexity.Classes.Oracle.ListOracle public import Complexity.Computability.Complexity.Classes.Oracle.Lowness public import Complexity.Computability.Complexity.Classes.Oracle.Monotone public import Complexity.Computability.Complexity.Classes.Oracle.PP @@ -1333,6 +1334,7 @@ public import Complexity.Computability.Complexity.Classes.Sparse.Hausdorff public import Complexity.Computability.Complexity.Classes.Sparse.Mahaney public import Complexity.Computability.Complexity.Classes.Sparse.OneQuery public import Complexity.Computability.Complexity.Classes.Sparse.Prune +public import Complexity.Computability.Complexity.Classes.Sparse.Turing public import Complexity.Computability.Complexity.Classes.TFNP public import Complexity.Computability.Complexity.Classes.TFNP.SearchToDecision public import Complexity.Computability.Complexity.Classes.TFNP.Subclasses diff --git a/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean b/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean new file mode 100644 index 0000000000..acecabc80b --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean @@ -0,0 +1,258 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Oracle +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Oracle +import Complexity.Computability.Complexity.Classes.Oracle.Deterministic +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat + +/-! +# Oracles given as finite lists + +A computation in polynomial time relative to an oracle language `S` asks only words no longer +than its clock, a polynomial `q` in the encoded input length. So any finite list `ℓ` of words +that agrees with `S` on the words of length at most `q n` can replace the oracle, and the run +against `ℓ` is polynomial-time in the input and `ℓ` together +(`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle`). This is how a sparse oracle +is replaced by advice, or by a guessed list of its short members. + +The proof replays the coin-fixed run of a machine certifying the computation +(`Cslib.Probability.IsOraclePPTOn.exists_fin_run_pure_false`) from its instruction-indexed +transcript of oracle replies (`Turing.MultiTapePTM.oracleReplies`). The transcript against the +list is built one bit at a time (`Turing.MultiTapePTM.listReplyStep`): each step replays the +transcript so far, and if the next instruction makes a query, looks its request up in the list. +The pending request of the instruction at index `i` has at most `i` symbols +(`Turing.MultiTapePTM.length_pendingRequest_replayPrefix_le`), so oracles that agree on the words +no longer than the clock give the same transcript +(`Turing.MultiTapePTM.oracleReplies_congr`). + +## Main definitions + +* `Turing.MultiTapePTM.listReplyStep`: extend a transcript by the reply of a list oracle. + +## Main results + +* `Turing.MultiTapePTM.oracleReplies_congr`: transcripts depend only on the replies to words no + longer than the clock. +* `Turing.MultiTapePTM.iterate_listReplyStep`: iterating the step builds the transcript. +* `Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle`, + `Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`: polynomial time + relative to `S` is polynomial time with a list that agrees with `S` on short words. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09], Section 3.4. +-/ + +@[expose] public section + +namespace Turing.MultiTapePTM + +open Cslib MultiTapeMachine MultiTapeTM + +variable {k : ℕ} {Control Operation : Type} [DecidableEq Operation] + (machine : MultiTapePTM k Bool Control Operation) + +/-- **Transcripts depend only on short replies.** Oracles that agree on every word of length less +than the clock give the same transcript: the request pending before instruction `i` has at most +`i` symbols. -/ +theorem oracleReplies_congr {g g' : List Bool → Bool} {fuel : ℕ} (input : List Bool) + (h : ∀ w : List Bool, w.length < fuel → g w = g' w) : + machine.oracleReplies g fuel input = machine.oracleReplies g' fuel input := by + set t := machine.oracleReplies g fuel input + set t' := machine.oracleReplies g' fuel input + have hlen : t.length = fuel := machine.length_oracleReplies g fuel input + have hlen' : t'.length = fuel := machine.length_oracleReplies g' fuel input + have htake : ∀ i ≤ fuel, t.take i = t'.take i := by + intro i hi + induction i with + | zero => rfl + | succ i ih => + have hlt : i < fuel := hi + have ih := ih hlt.le + have hcfg : machine.replayPrefix input t i = machine.replayPrefix input t' i := by + simp only [replayPrefix, ih] + have hreq : (machine.pendingRequest (machine.replayPrefix input t i)).length < fuel := + lt_of_le_of_lt ((machine.length_pendingRequest_replayPrefix_le input t i).trans + (Nat.min_le_left _ _)) hlt + have hbit : t[i]'(by omega) = t'[i]'(by omega) := by + rw [← List.getD_eq_getElem t false, ← List.getD_eq_getElem t' false, + machine.getD_oracleReplies g fuel input i hlt, + machine.getD_oracleReplies g' fuel input i hlt] + dsimp only + rw [← hcfg, h _ hreq] + rw [List.take_succ_eq_append_getElem (by omega), List.take_succ_eq_append_getElem (by omega), + ih, hbit] + simpa only [List.take_of_length_le hlen.le, List.take_of_length_le hlen'.le] using + htake fuel le_rfl + +/-- Extend the transcript `answers` by one bit: replay it, and if the next instruction makes a +query, reply whether its request is in the list `ℓ`; otherwise pad with `false`. -/ +def listReplyStep (p : List Bool × List (List Bool)) (answers : List Bool) : List Bool := + let cfg := machine.replayConfig p.1 answers + answers ++ [if (machine.pendingQuery cfg).isSome then decide (machine.pendingRequest cfg ∈ p.2) + else false] + +/-- A canonical transcript one instruction longer extends the shorter one by the reply at its +last instruction. -/ +theorem oracleReplies_succ (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : + machine.oracleReplies g (fuel + 1) input = machine.oracleReplies g fuel input ++ + [let cfg := machine.replayConfig input (machine.oracleReplies g fuel input) + if (machine.pendingQuery cfg).isSome then g (machine.pendingRequest cfg) else false] := by + have hlen := machine.length_oracleReplies g (fuel + 1) input + have htake : (machine.oracleReplies g (fuel + 1) input).take fuel = + machine.oracleReplies g fuel input := by + unfold oracleReplies + rw [take_oracleRepliesFrom, Nat.min_eq_left (Nat.le_succ fuel)] + have hbit := machine.getD_oracleReplies g (fuel + 1) input fuel (Nat.lt_succ_self fuel) + rw [List.getD_eq_getElem _ _ (by omega)] at hbit + have hcfg : machine.replayPrefix input (machine.oracleReplies g (fuel + 1) input) fuel = + machine.replayConfig input (machine.oracleReplies g fuel input) := by + rw [replayPrefix, htake] + rw [hcfg] at hbit + calc machine.oracleReplies g (fuel + 1) input + = (machine.oracleReplies g (fuel + 1) input).take fuel ++ + [(machine.oracleReplies g (fuel + 1) input)[fuel]'(by omega)] := by + rw [← List.take_succ_eq_append_getElem (by omega), List.take_of_length_le (by omega)] + _ = _ := by rw [htake, hbit] + +/-- **Iterating the step builds the transcript** of the list oracle. -/ +theorem iterate_listReplyStep (input : List Bool) (ℓ : List (List Bool)) (fuel : ℕ) : + (machine.listReplyStep (input, ℓ))^[fuel] [] = + machine.oracleReplies (fun w => decide (w ∈ ℓ)) fuel input := by + induction fuel with + | zero => rfl + | succ fuel ih => + rw [Function.iterate_succ_apply', ih, oracleReplies_succ] + rfl + +section PolyTime + +variable [Finite Control] [Finite Operation] + +/-- The step is polynomial-time, jointly in the input, the list and the transcript. -/ +theorem computableInPolyTime_listReplyStep : + ComputableInPolyTime (fun x : (List Bool × List (List Bool)) × List Bool => + machine.listReplyStep x.1 x.2) (encPair (encPair encBits (encList encBits)) encBits) + encBits := by + let _ := Fintype.ofFinite Operation + have hpair : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => (x.1.1, x.2)) + (encPair (encPair encBits (encList encBits)) encBits) (encPair encBits encBits) := + (ComputableInPolyTime.fst _ _).fst'.prod (.snd _ _) + have hcfg : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => machine.replayConfig x.1.1 x.2) + (encPair (encPair encBits (encList encBits)) encBits) encFiniteConfig := + machine.replayConfig_pt.comp + (g := fun x : (List Bool × List (List Bool)) × List Bool => (x.1.1, x.2)) hpair + have hquery : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => + (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome) + (encPair (encPair encBits (encList encBits)) encBits) encBool := + (ComputableInPolyTime.of_finite Option.isSome).comp + (machine.pendingQuery_pt.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => + machine.replayConfig x.1.1 x.2) hcfg) + have hmem : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => + decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2)) + (encPair (encPair encBits (encList encBits)) encBits) encBool := + ComputableInPolyTime.decide_mem (ComputableInPolyTime.fst _ _).snd' + (machine.pendingRequest_pt.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => + machine.replayConfig x.1.1 x.2) hcfg) + have hbit : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => + if (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome then + decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2) else false) + (encPair (encPair encBits (encList encBits)) encBits) encBool := + ComputableInPolyTime.ite' hquery hmem (ComputableInPolyTime.const false) + have hsingle : ComputableInPolyTime (fun b : Bool => [b]) encBool encBits := + .of_eq fun _ => rfl + exact ComputableInPolyTime.bitsAppend (ComputableInPolyTime.snd _ _) + (hsingle.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => + if (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome then + decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2) else false) hbit) + +end PolyTime + +end Turing.MultiTapePTM + +namespace Cslib.Complexity + +open Probability Turing.MultiTapeTM + +variable {α β : Type} {S : Set (List Bool)} {input : α ↪ List Bool} + +open Classical in +/-- **A finite list can replace the oracle.** If `f` is computable in polynomial time relative to +`S`, there are a polynomial `q` and a function `F`, polynomial-time in an instance and a list of +words together, such that `F (a, ℓ)` is the encoded result `output (f a)` whenever `ℓ` agrees with +`S` on every word of length at most `q (input a).length`. -/ +theorem ComputableInPolyTimeWithOracle.exists_listOracle {f : α → β} {output : β ↪ List Bool} + (hf : ComputableInPolyTimeWithOracle S f input output) : + ∃ (F : α × List (List Bool) → List Bool) (q : Polynomial ℕ), + ComputableInPolyTime F (encPair input (encList encBits)) encBits ∧ + ∀ a ℓ, (∀ w : List Bool, w.length ≤ q.eval (input a).length → (w ∈ ℓ ↔ w ∈ S)) → + F (a, ℓ) = output (f a) := by + obtain ⟨program, hcert, hprogram⟩ := hf + obtain ⟨k, m, machine, c, d, hrun⟩ := hcert.exists_fin_run_pure_false + let T : α → ℕ := fun a => c * ((input a).length + 1) ^ d + have hTa : ComputableInPolyTime T input encUnary := + ((ComputableInPolyTime.unary_eval (Polynomial.C c * (Polynomial.X + 1) ^ d)).comp + (ComputableInPolyTime.encoding_length input)).of_enc_eq fun a => by simp [T] + have hT : ComputableInPolyTime (fun x : α × List (List Bool) => T x.1) + (encPair input (encList encBits)) encUnary := + hTa.comp (ComputableInPolyTime.fst _ _) + have hinput : ComputableInPolyTime (fun a : α => input a) input encBits := .of_eq fun _ => rfl + have hinput' : ComputableInPolyTime (fun x : α × List (List Bool) => input x.1) + (encPair input (encList encBits)) encBits := + hinput.comp (g := fun x : α × List (List Bool) => x.1) (.fst _ _) + have hpar : ComputableInPolyTime (fun x : α × List (List Bool) => (input x.1, x.2)) + (encPair input (encList encBits)) (encPair encBits (encList encBits)) := + hinput'.prod (.snd _ _) + have hiter : ComputableInPolyTime + (fun x : α × List (List Bool) => (machine.listReplyStep (input x.1, x.2))^[T x.1] []) + (encPair input (encList encBits)) encBits := + ComputableInPolyTime.iterateWith_of_bounded_growth hpar hT (ComputableInPolyTime.const []) + machine.computableInPolyTime_listReplyStep (.const 1) fun x answers => by + simp [Turing.MultiTapePTM.listReplyStep] + have hout : ComputableInPolyTime + (fun x : α × List (List Bool) => + machine.replayOutput (input x.1) ((machine.listReplyStep (input x.1, x.2))^[T x.1] [])) + (encPair input (encList encBits)) encBits := + machine.computableInPolyTime_replayOutput.comp (g := fun x : α × List (List Bool) => + (input x.1, (machine.listReplyStep (input x.1, x.2))^[T x.1] [])) (hinput'.prod hiter) + refine ⟨_, Polynomial.C c * (Polynomial.X + 1) ^ d, hout, fun a ℓ hℓ => ?_⟩ + dsimp only + rw [machine.iterate_listReplyStep, machine.oracleReplies_congr (g' := fun w => decide (w ∈ S)) + _ fun w hw => ?_, machine.replayOutput_oracleReplies, ← hprogram a, ← hrun a] + · rfl + · refine decide_eq_decide.mpr (hℓ w ?_) + simp only [Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_add, + Polynomial.eval_X, Polynomial.eval_one] + exact hw.le + +/-- **A finite list can replace the oracle of a decision**: the Boolean form of +`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle`. -/ +theorem ComputableInPolyTimeWithOracle.exists_listOracle_bool {f : α → Bool} + (hf : ComputableInPolyTimeWithOracle S f input encBool) : + ∃ (F : α × List (List Bool) → Bool) (q : Polynomial ℕ), + ComputableInPolyTime F (encPair input (encList encBits)) encBool ∧ + ∀ a ℓ, (∀ w : List Bool, w.length ≤ q.eval (input a).length → (w ∈ ℓ ↔ w ∈ S)) → + F (a, ℓ) = f a := by + obtain ⟨F, q, hF, hFS⟩ := hf.exists_listOracle + refine ⟨fun x => decide (F x = [true]), q, + ComputableInPolyTime.decide_eq' hF (ComputableInPolyTime.const [true]), fun a ℓ hℓ => ?_⟩ + change decide (F (a, ℓ) = [true]) = f a + rw [hFS a ℓ hℓ, encBool_apply] + cases f a <;> rfl + +end Cslib.Complexity diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean b/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean new file mode 100644 index 0000000000..bf3ee4a31a --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean @@ -0,0 +1,135 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Circuit.Boolean.PPoly +public import Complexity.Computability.Complexity.Classes.Oracle +public import Complexity.Computability.Complexity.Classes.PH +public import Complexity.Computability.Complexity.Classes.Sparse +public import Complexity.Computability.Complexity.Problems.SAT +public import Mathlib.Data.Set.Finite.List +import Complexity.Computability.Circuit.Boolean.Advice +import Complexity.Computability.Circuit.Boolean.PolynomialTime +import Complexity.Computability.Complexity.Classes.Oracle.ListOracle +import Complexity.Computability.Complexity.Classes.PH.KarpLipton +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length + +/-! +# Sparse Turing-hard sets + +Polynomial time relative to a sparse oracle language `S` is in `P/poly` +(`Cslib.Complexity.PWithOracle_subset_PPolyOn`): on inputs of length `n` the oracle is asked only +words of length at most `q n` for a polynomial `q`, and the list of the members of `S` of length +at most `q n` (`Cslib.Complexity.shortMembers`) has polynomial length because `S` is sparse. That +list is the advice; a finite list replaces the oracle in polynomial time +(`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`), and hardwiring the +advice (`Cslib.Circuits.Boolean.PPoly.of_advice`) gives circuits of polynomial size. This is one +half of `P/poly = P^SPARSE`, which [Hemaspaandra and Ogihara, p. 22][HemaspaandraOgihara2002] cite +as well known, and whose bibliographic notes (p. 27) attribute it, through Berman and Hartmanis, +to Meyer. + +Consequently, if `SAT` is polynomial-time Turing reducible to a sparse set, then `SAT` has circuits +of polynomial size and the Karp–Lipton theorem collapses the polynomial hierarchy to `Σ₂` +(`Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`): if `NP` has a sparse +polynomial-time Turing-hard set, then `PH = NP^NP` +[Hemaspaandra and Ogihara, Theorem 1.16][HemaspaandraOgihara2002] [Karp and Lipton][KarpLipton1980]. +The sparse set need not lie in `NP`. + +## Main definitions + +* `Cslib.Complexity.shortMembers`: a list of the members of a language of length at most `n`. + +## Main results + +* `Cslib.Complexity.mem_shortMembers`: its members. +* `Cslib.Complexity.exists_length_encList_shortMembers_le`: for a sparse language, the encoded list + has polynomial length. +* `Cslib.Complexity.PWithOracle_subset_PPolyOn`: `P^S ⊆ P/poly` for sparse `S`. +* `Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`: a sparse Turing-hard set for `NP` + collapses `PH` to `Σ₂`. + +## References + +* [L. A. Hemaspaandra, M. Ogihara, *The Complexity Theory Companion*][HemaspaandraOgihara2002] +* [R. M. Karp, R. J. Lipton, *Some connections between nonuniform and uniform complexity + classes*][KarpLipton1980] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Circuits Circuits.Boolean Turing.MultiTapeTM Cslib.Logic.PL + +variable {α : Type} {S : Set (List Bool)} + +/-- The members of `S` of length at most `n`, listed in some order without repetition. -/ +noncomputable def shortMembers (S : Set (List Bool)) (n : ℕ) : List (List Bool) := + ((List.finite_length_le Bool n).subset + (fun _ hw => hw.2 : {w | w ∈ S ∧ w.length ≤ n} ⊆ {w | w.length ≤ n})).toFinset.toList + +@[simp] +theorem mem_shortMembers {n : ℕ} {w : List Bool} : w ∈ shortMembers S n ↔ w ∈ S ∧ w.length ≤ n := by + simp [shortMembers] + +/-- **Short members of a sparse language have a short listing**: the encoded list of the members +of length at most `n` has length at most `c (n + 1) ^ d`. -/ +theorem exists_length_encList_shortMembers_le (hS : S ∈ SPARSE encBits) : + ∃ c d : ℕ, ∀ n, (encList encBits (shortMembers S n)).length ≤ c * (n + 1) ^ d := by + obtain ⟨c, d, hcard⟩ := exists_card_le_of_mem_SPARSE hS + refine ⟨2 * c, d + 1, fun n => ?_⟩ + have hlen : (shortMembers S n).length ≤ c * (n + 1) ^ d := by + unfold shortMembers + rw [Finset.length_toList] + exact hcard n _ fun w hw => by simpa using hw + have hsum : ((shortMembers S n).map fun w => 2 * (encBits w).length + 1).sum ≤ + (shortMembers S n).length * (2 * n + 1) := by + have h := List.sum_le_length_nsmul ((shortMembers S n).map fun w => 2 * (encBits w).length + 1) + (2 * n + 1) fun x hx => by + obtain ⟨w, hw, rfl⟩ := List.mem_map.mp hx + have := (mem_shortMembers.mp hw).2 + simp only [encBits_apply] + omega + simpa only [List.length_map, smul_eq_mul] using h + rw [length_encList] + calc _ ≤ (shortMembers S n).length * (2 * n + 1) := hsum + _ ≤ c * (n + 1) ^ d * (2 * (n + 1)) := Nat.mul_le_mul hlen (by omega) + _ = 2 * c * (n + 1) ^ (d + 1) := by ring + +/-- **Polynomial time relative to a sparse oracle is in `P/poly`.** The advice at length `n` lists +the members of `S` no longer than the oracle words the computation may ask. -/ +theorem PWithOracle_subset_PPolyOn (hS : S ∈ SPARSE encBits) (enc : α ↪ List Bool) : + PWithOracle S enc ⊆ PPolyOn enc := by + rintro L ⟨f, hf, hL⟩ + obtain ⟨F, q, hF, hFS⟩ := hf.exists_listOracle_bool + have hF' : ComputableInPolyTime (fun x : List (List Bool) × α => F (x.2, x.1)) + (encPair (encList encBits) enc) encBool := + hF.comp (g := fun x : List (List Bool) × α => (x.2, x.1)) + ((ComputableInPolyTime.snd _ _).prod (.fst _ _)) + obtain ⟨M, hM, hFM⟩ := PPoly.exists_of_polyTime hF' + obtain ⟨c, d, hadv⟩ := exists_length_encList_shortMembers_le hS + let adv : ℕ → List Bool := fun n => encList encBits (shortMembers S (q.eval n)) + have hadvPoly : PolynomiallyBounded fun n => (adv n).length := by + refine PolynomiallyBounded.mono_of_le (g := fun n => c * (q.eval n + 1) ^ d) (by fun_prop) + fun n => hadv _ + let L' : Language Bool := {x : List Bool | frame (adv x.length) ++ x ∈ M} + refine ⟨L', PPoly.of_advice hM adv hadvPoly (fun _ => Iff.rfl), fun a => ?_⟩ + change a ∈ L ↔ frame (adv (enc a).length) ++ enc a ∈ M + have hFM' := hFM (shortMembers S (q.eval (enc a).length), a) + rw [encPair_apply] at hFM' + rw [hL a, ← hFM', hFS a _ fun w hw => by simp only [mem_shortMembers, hw, and_true]] + +/-- **A sparse Turing-hard set for `NP` collapses `PH` to `Σ₂`**: if `SAT` is decided in +polynomial time relative to a sparse oracle language, then `SAT` has circuits of polynomial size, +and the Karp–Lipton theorem applies [Hemaspaandra and Ogihara, Theorem 1.16] +[HemaspaandraOgihara2002]. -/ +theorem PH_eq_SigmaP_two_of_SAT_mem_PWithOracle (hS : S ∈ SPARSE encBits) + (hSAT : SAT ∈ PWithOracle S encCNF) (enc : α ↪ List Bool) : PH enc = SigmaP 2 enc := + PH_eq_SigmaP_two_of_SAT (PWithOracle_subset_PPolyOn hS encCNF hSAT) + +end Cslib.Complexity diff --git a/ComplexityTests/SparseTuring.lean b/ComplexityTests/SparseTuring.lean new file mode 100644 index 0000000000..43c1822e8c --- /dev/null +++ b/ComplexityTests/SparseTuring.lean @@ -0,0 +1,55 @@ +/- +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.Oracle.ListOracle +import Complexity.Computability.Complexity.Classes.Sparse.Turing + +/-! # Finite-list oracles and sparse Turing-hard sets -/ + +namespace ComplexityTests.SparseTuring + +open Cslib Cslib.Complexity Cslib.Circuits.Boolean Cslib.Logic.PL Turing.MultiTapeTM + +/-- The words consisting only of `true`s, a sparse language. -/ +private def unary : Set (List Bool) := {w | ∀ b ∈ w, b = true} + +private theorem unary_mem_SPARSE : unary ∈ SPARSE encBits := mem_SPARSE_of_unary fun _ h => h + +-- The short members of `unary` are exactly the all-`true` words of bounded length. +example : [true, true] ∈ shortMembers unary 2 := by + simp [unary] + +example : [true, true] ∉ shortMembers unary 1 := by + simp + +example : [true, false] ∉ shortMembers unary 5 := by + simp [unary] + +-- Their encoded listing has polynomial length. +example : ∃ c d : ℕ, ∀ n, (encList encBits (shortMembers unary n)).length ≤ c * (n + 1) ^ d := + exists_length_encList_shortMembers_le unary_mem_SPARSE + +-- A finite list replaces the oracle of the one-request decider of `unary`: a list agreeing with +-- `unary` on short words gives the right answer on every input. +open Classical in +example : ∃ (F : List Bool × List (List Bool) → Bool) (q : Polynomial ℕ), + ComputableInPolyTime F (encPair encBits (encList encBits)) encBool ∧ + ∀ w, F (w, shortMembers unary (q.eval w.length)) = decide (w ∈ unary) := by + obtain ⟨F, q, hF, hFS⟩ := (computableInPolyTimeWithOracle_mem unary).exists_listOracle_bool + refine ⟨F, q, hF, fun w => hFS w _ fun v hv => ?_⟩ + rw [encBits_apply] at hv + simp [hv] + +-- `P` relative to the sparse oracle `unary` is in `P/poly`; in particular `unary` itself is. +example : unary ∈ PPolyOn encBits := + PWithOracle_subset_PPolyOn unary_mem_SPARSE encBits (mem_PWithOracle_self unary) + +-- The collapse applies to every sparse oracle to which `SAT` is Turing reducible. +example (hSAT : SAT ∈ PWithOracle unary encCNF) : + PH encBits = SigmaP 2 encBits := + PH_eq_SigmaP_two_of_SAT_mem_PWithOracle unary_mem_SPARSE hSAT encBits + +end ComplexityTests.SparseTuring diff --git a/ROADMAP.md b/ROADMAP.md index b5fe735041..ec346a7149 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -209,8 +209,9 @@ index links to canonical definitions rather than keeping a second set. - **Reducibilities** ([#1351]): logspace Turing reductions, in an oracle model whose query tape is 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), extending - `PPoly.of_sparse` in `Circuit/Boolean/Sparse.lean`. +- **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]). - **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 @@ -875,3 +876,4 @@ not planned, not as proved. [#1817]: https://github.com/cslib-community/complexitylib/issues/1817 [#1824]: https://github.com/cslib-community/complexitylib/issues/1824 [#2019]: https://github.com/cslib-community/complexitylib/issues/2019 +[#2062]: https://github.com/cslib-community/complexitylib/issues/2062 From 4c59e2fca4e0f9649e1bfbcc2b1a7cddf0dea40e Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:47:16 -0400 Subject: [PATCH 04/12] wip(Classes/Sparse): Kadin census requests and their NP membership (#2062 M3) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/Sparse/Kadin.lean | 309 ++++++++++++++++++ 1 file changed, 309 insertions(+) create mode 100644 Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean new file mode 100644 index 0000000000..b90605c4fd --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean @@ -0,0 +1,309 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Oracle.BoundedQuery +public import Complexity.Computability.Complexity.Classes.PH +public import Complexity.Computability.Complexity.Classes.Sparse.Turing +import Complexity.Computability.Complexity.Classes.NP.Witness +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Cslib.Foundations.Data.Polynomial.Monotone + +/-! +# Kadin's theorem: sparse Turing-complete sets for `NP` + +If `NP` has a sparse polynomial-time Turing-complete set, that is a sparse `S ∈ NP` to which +`SAT` is polynomial-time Turing reducible, then the polynomial hierarchy collapses to +`P^{NP[O(log n)]}` [Kadin][Kadin1989] [Hemaspaandra and Ogihara, Theorem 1.14][HemaspaandraOgihara2002]. + +The proof follows the census argument of [Hemaspaandra and Ogihara, Theorem 1.14] +[HemaspaandraOgihara2002]. The census of `S` up to length `m` is the number of members of `S` of +length at most `m`; it is polynomial in `m` because `S` is sparse. + +* With `S ∈ NP`, "the census is at least `k`" is a problem in `NP`: guess `k` distinct members, + each with its certificate. Binary search finds the exact census with `O(log n)` such requests. +* Given the exact census `k`, a list of `k` distinct short members of `S` lists them all + (`Cslib.Complexity.mem_iff_of_length_eq_length_shortMembers`), so it can replace the oracle `S` + (`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`). Hence one more + request in `NP`, which guesses the list and a first certificate, decides a problem in `Σ₂`. + +So `Σ₂ ⊆ P^{NP[O(log n)]}`. The Companion completes the proof by `Θ₂ ⊆ Σ₂ ∩ Π₂` and closure of +`Θ₂` under complement; here `PH = Σ₂` comes instead from the sparse form of the Karp–Lipton +theorem (`Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`). + +## Main definitions + +* `Cslib.Complexity.KadinCensus.language`: the `NP` problem asked by the algorithm, on triples + `(a, k, b)`: `k` distinct short members of `S` exist, and if `b`, they also witness the first + quantifier of a `Σ₂` problem. + +## Main results + +* `Cslib.Complexity.length_le_length_shortMembers`, + `Cslib.Complexity.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. +* `Cslib.Complexity.KadinCensus.mem_language_false_iff`, + `Cslib.Complexity.KadinCensus.mem_language_census_true_iff`: the meaning of the requests. +* `Cslib.Complexity.KadinCensus.language_mem_NP`: the requests form a problem in `NP`. + +## References + +* [J. Kadin, *P^{NP[O(log n)]} and sparse Turing-complete sets for NP*][Kadin1989] +* [L. A. Hemaspaandra, M. Ogihara, *The Complexity Theory Companion*][HemaspaandraOgihara2002] +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Turing.MultiTapeTM + +variable {α : Type} {S : Set (List Bool)} + +/-! ### The census -/ + +theorem nodup_shortMembers (S : Set (List Bool)) (n : ℕ) : (shortMembers S n).Nodup := + Finset.nodup_toList _ + +/-- **The census bounds the lists of distinct short members.** -/ +theorem length_le_length_shortMembers {ℓ : List (List Bool)} {n : ℕ} (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)} {n : ℕ} (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 + +/-- The census of a sparse language is polynomially bounded. -/ +theorem exists_length_shortMembers_le (hS : S ∈ SPARSE encBits) : + ∃ c d : ℕ, ∀ n, (shortMembers S n).length ≤ c * (n + 1) ^ d := by + obtain ⟨c, d, hcard⟩ := exists_card_le_of_mem_SPARSE hS + refine ⟨c, d, fun n => ?_⟩ + unfold shortMembers + rw [Finset.length_toList] + exact hcard n _ fun w hw => by simpa using hw + +/-! ### The requests -/ + +namespace KadinCensus + +variable (S) (enc : α ↪ List Bool) (m p : Polynomial ℕ) + (G : (α × List Bool) × List (List Bool) → Bool) + +/-- A guess for the request `(a, k, b)`: `ℓ` lists `k` distinct members of `S` of length at most +`m |enc a|`, and if `b`, some word `w` of length `p |enc a|` has `G ((a, w), ℓ) = false`. -/ +def Guess (x : α × ℕ × Bool) (ℓ : List (List Bool)) : Prop := + ℓ.Nodup ∧ ℓ.length = x.2.1 ∧ (∀ s ∈ ℓ, s ∈ S ∧ s.length ≤ m.eval (enc x.1).length) ∧ + (x.2.2 = true → ∃ w : List Bool, w.length = p.eval (enc x.1).length ∧ G ((x.1, w), ℓ) = false) + +/-- The requests that have a guess. -/ +def language : Set (α × ℕ × Bool) := {x | ∃ ℓ, Guess S enc m p G x ℓ} + +/-- The census of `S` up to the length `m |enc a|`. -/ +noncomputable def census (a : α) : ℕ := (shortMembers S (m.eval (enc a).length)).length + +variable {S enc m p G} + +/-- **A request with `b = false` asks whether the census is at least `k`.** -/ +theorem mem_language_false_iff {a : α} {k : ℕ} : + (a, k, false) ∈ language S enc m p G ↔ k ≤ census S enc m a := by + constructor + · rintro ⟨ℓ, hnd, hlen, hmem, -⟩ + have hle := length_le_length_shortMembers hnd hmem + rw [hlen] at hle + exact hle + · intro hk + refine ⟨(shortMembers S (m.eval (enc a).length)).take k, + (nodup_shortMembers _ _).sublist (List.take_sublist _ _), + by rw [List.length_take]; exact Nat.min_eq_left hk, fun s hs => ?_, + fun h => absurd h Bool.false_ne_true⟩ + exact mem_shortMembers.mp (List.mem_of_mem_take hs) + +/-- **At the exact census, a request with `b = true` asks for the first quantifier.** If `G` +computes `g` whenever its list agrees with `S` on the words of length at most `m |enc a|`, the +request `(a, census, true)` asks whether some `w` of length `p |enc a|` has `g (a, w) = false`. -/ +theorem mem_language_census_true_iff {a : α} {g : α × List Bool → Bool} + (hG : ∀ w ℓ, w.length = p.eval (enc a).length → + (∀ s : List Bool, s.length ≤ m.eval (enc a).length → (s ∈ ℓ ↔ s ∈ S)) → + G ((a, w), ℓ) = g (a, w)) : + (a, census S enc m a, true) ∈ language S enc m p G ↔ + ∃ w : List Bool, w.length = p.eval (enc a).length ∧ g (a, w) = false := by + constructor + · rintro ⟨ℓ, hnd, hlen, hmem, hw⟩ + obtain ⟨w, hwlen, hGw⟩ := hw rfl + exact ⟨w, hwlen, (hG w ℓ hwlen fun s hs => + mem_iff_of_length_eq_length_shortMembers hnd hmem hlen hs) ▸ hGw⟩ + · rintro ⟨w, hwlen, hgw⟩ + refine ⟨shortMembers S (m.eval (enc a).length), nodup_shortMembers _ _, rfl, + fun s hs => mem_shortMembers.mp hs, fun _ => ⟨w, hwlen, ?_⟩⟩ + rw [hG w _ hwlen fun s hs => by simp only [mem_shortMembers, hs, and_true]] + exact hgw + +/-! ### The requests are in `NP` -/ + +/-- A duplicate-free list is one in which no entry occurs twice, tested by counting. -/ +theorem not_any_one_lt_countP_iff_nodup (l : List (List Bool)) : + (!(l.any fun s => decide (1 < l.countP fun t => decide (t = s)))) = true ↔ l.Nodup := by + have hc (s : List Bool) : (l.countP fun t => decide (t = s)) = l.count s := by + rw [List.count_eq_countP] + congr 1 + funext t + rw [Bool.eq_iff_iff] + simp + simp only [Bool.not_eq_true', List.any_eq_false, decide_eq_true_eq, 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 + +variable (enc m p G) in +/-- The check of a witness `(pairs, w)` for the request `(a, k, b)`: the first components of +`pairs` are `k` distinct words of length at most `m |enc a|`, each with an accepted certificate of +the verifier `VS` of `S`, and if `b`, `w` has length `p |enc a|` and `G ((a, w), ℓ) = false`. -/ +def check (VS : List Bool × List Bool → Bool) (pS : Polynomial ℕ) + (z : (α × ℕ × Bool) × (List (List Bool × List Bool) × List Bool)) : Bool := + !((z.2.1.map Prod.fst).any fun s => + decide (1 < (z.2.1.map Prod.fst).countP fun t => decide (t = s))) && + decide ((z.2.1.map Prod.fst).length = z.1.2.1) && + !(z.2.1.any fun sc => !(decide (sc.1.length ≤ m.eval (enc z.1.1).length) && + decide (sc.2.length = pS.eval sc.1.length) && VS sc)) && + (!z.1.2.2 || (decide (z.2.2.length = p.eval (enc z.1.1).length) && + !G ((z.1.1, z.2.2), z.2.1.map Prod.fst))) + +theorem check_eq_true_iff {VS : List Bool × List Bool → Bool} {pS : Polynomial ℕ} + {x : α × ℕ × Bool} {y : List (List Bool × List Bool) × List Bool} : + check enc m p G VS pS (x, y) = true ↔ + (y.1.map Prod.fst).Nodup ∧ (y.1.map Prod.fst).length = x.2.1 ∧ + (∀ sc ∈ y.1, sc.1.length ≤ m.eval (enc x.1).length ∧ + sc.2.length = pS.eval sc.1.length ∧ VS sc = true) ∧ + (x.2.2 = true → y.2.length = p.eval (enc x.1).length ∧ + G ((x.1, y.2), y.1.map Prod.fst) = false) := by + unfold check + rw [Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true, not_any_one_lt_countP_iff_nodup, + and_assoc, and_assoc] + refine and_congr Iff.rfl (and_congr decide_eq_true_iff (and_congr ?_ ?_)) + · simp [List.any_eq_false, and_assoc] + · cases x.2.2 <;> simp + +/-- The witnesses: the certificates of `S` are read by its verifier `VS`. -/ +theorem language_eq_setOf_check {VS : List Bool × List Bool → Bool} {pS : Polynomial ℕ} + (hSV : IsVerifier encBits pS VS S) : + language S enc m p G = {x | ∃ y, check enc m p G VS pS (x, y) = true} := by + classical + ext x + simp only [Set.mem_ofPred_eq, check_eq_true_iff] + constructor + · rintro ⟨ℓ, hnd, hlen, hmem, hw⟩ + have hcert (s : List Bool) (hs : s ∈ S) : + ∃ c, c.length = pS.eval s.length ∧ VS (s, c) = true := (hSV s).1 hs + let cert : List Bool → List Bool := fun s => if hs : s ∈ S then (hcert s hs).choose else [] + have hmap : (ℓ.map fun s => (s, cert s)).map Prod.fst = ℓ := by + rw [List.map_map] + exact List.map_id' ℓ + refine ⟨(ℓ.map fun s => (s, cert s), + if h : x.2.2 = true then (hw h).choose else []), by rw [hmap]; exact hnd, + by rw [hmap]; exact hlen, fun sc hsc => ?_, fun h => ?_⟩ + · obtain ⟨s, hs, rfl⟩ := List.mem_map.mp hsc + have hsS := (hmem s hs).1 + simp only [cert, hsS, ↓reduceDIte] + exact ⟨(hmem s hs).2, (hcert s hsS).choose_spec.1, (hcert s hsS).choose_spec.2⟩ + · simp only [h, ↓reduceDIte, hmap] + exact (hw h).choose_spec + · rintro ⟨⟨pairs, w⟩, hnd, hlen, hpairs, hw⟩ + refine ⟨pairs.map Prod.fst, hnd, hlen, fun s hs => ?_, fun h => ⟨w, hw h⟩⟩ + obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hs + obtain ⟨hlenS, hc, hV⟩ := hpairs sc hsc + exact ⟨(hSV sc.1).2 ⟨sc.2, hc, hV⟩, hlenS⟩ + +/-- The check of a witness is polynomial-time. -/ +theorem computableInPolyTime_check {VS : List Bool × List Bool → Bool} {pS : Polynomial ℕ} + (hVS : ComputableInPolyTime VS (encPair encBits encBits) encBool) + (hG : ComputableInPolyTime G (encPair (encPair enc encBits) (encList encBits)) encBool) : + ComputableInPolyTime (check enc m p G VS pS) + (encPair (encPair enc (encPair encUnary encBool)) + (encPair (encList (encPair encBits encBits)) encBits)) encBool := by + unfold check + fun_prop + +/-- **The requests form a problem in `NP`** when `S` is a sparse problem in `NP` and `G` is +polynomial-time: a witness lists the guessed members with their certificates, and the word `w`. +Its length is polynomial because the census of `S` is. -/ +theorem language_mem_NP (hS : S ∈ NP encBits) (hsparse : S ∈ SPARSE encBits) + (hG : ComputableInPolyTime G (encPair (encPair enc encBits) (encList encBits)) encBool) : + language S enc m p G ∈ NP (encPair enc (encPair encUnary encBool)) := by + obtain ⟨pS, VS, hVS, hSV⟩ := mem_NP.mp hS + obtain ⟨c, d, hcensus⟩ := exists_length_shortMembers_le hsparse + rw [language_eq_setOf_check hSV] + refine mem_NP_of_witness + (p := 2 * (Polynomial.C c * (m + 1) ^ d * (4 * m + 2 * pS.comp m + 3)) + 1 + p) + (Decoder.pair (Decoder.list (Decoder.pair .bits .bits)) .bits) + (computableInPolyTime_check hVS hG) (fun _ _ => Iff.rfl) fun x y hy => ?_ + obtain ⟨hnd, hlen, hpairs, hw⟩ := check_eq_true_iff.mp hy + set n := (enc x.1).length + refine ⟨(y.1, if x.2.2 = true then y.2 else []), check_eq_true_iff.mpr + ⟨hnd, hlen, hpairs, fun h => by simpa only [h, ↓reduceIte] using hw h⟩, ?_⟩ + -- the guessed words are distinct short members of `S`, so there are at most census many + have hcount : y.1.length ≤ c * (m.eval n + 1) ^ d := by + have hle := length_le_length_shortMembers (S := S) (n := m.eval n) hnd fun s hs => by + obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hs + obtain ⟨hlenS, hc, hV⟩ := hpairs sc hsc + exact ⟨(hSV sc.1).2 ⟨sc.2, by rw [encBits_apply]; exact hc, hV⟩, hlenS⟩ + rw [List.length_map] at hle + exact hle.trans (hcensus _) + have hpair (sc : List Bool × List Bool) (hsc : sc ∈ y.1) : + 2 * (encPair encBits encBits sc).length + 1 ≤ + 4 * m.eval n + 2 * pS.eval (m.eval n) + 3 := by + obtain ⟨hlenS, hc, -⟩ := hpairs sc hsc + have hpS : pS.eval sc.1.length ≤ pS.eval (m.eval n) := pS.eval_mono hlenS + rw [length_encPair, encBits_apply, encBits_apply, hc] + omega + have hlist : (encList (encPair encBits encBits) y.1).length ≤ + c * (m.eval n + 1) ^ d * (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) := by + rw [length_encList] + have h := List.sum_le_length_nsmul (y.1.map fun sc => 2 * (encPair encBits encBits sc).length + 1) + (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) fun z hz => by + obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hz + exact hpair sc hsc + rw [List.length_map, smul_eq_mul] at h + exact h.trans (Nat.mul_le_mul_right _ hcount) + have hword : (if x.2.2 = true then y.2 else []).length ≤ p.eval n := by + split_ifs with h + · exact (hw h).1.le + · exact Nat.zero_le _ + have hn : n ≤ (encPair enc (encPair encUnary encBool) x).length := length_le_encPair_left _ _ _ + refine le_trans ?_ (Polynomial.eval_mono _ hn) + rw [length_encPair, encBits_apply] + simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_C, + Polynomial.eval_one, Polynomial.eval_comp, Polynomial.eval_ofNat] + omega + +end KadinCensus + +end Cslib.Complexity From 453f4c5817eb6c9a7aed979753378c1212261c4f Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:48:09 -0400 Subject: [PATCH 05/12] feat(Classes/Oracle): name the one-request program queryBit Expose the single-request program with its interpretation, request list and oracle PPT certificate, so that oracle programs with several requests can count them. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Classes/Oracle/BoundedQuery.lean | 47 ++++++++++++++----- ComplexityTests/OracleBoundedQuery.lean | 11 +++-- 2 files changed, 40 insertions(+), 18 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean index e04576572b..76b7a32aba 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean @@ -34,6 +34,7 @@ is closed under complement. ## Main definitions +* `Cslib.Complexity.queryBit`: one request, reading one bit of the reply. * `Cslib.Complexity.ComputableInPolyTimeWithOracleQueries`: polynomial time relative to an oracle with a bounded number of requests. * `Cslib.Complexity.PWithOracleQueries`: the problems so decided. @@ -118,24 +119,44 @@ theorem _root_.Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithO ComputableInPolyTimeWithOracleQueries A r f input output := ⟨fun a => pure (f a), h.isOraclePPTOn, fun _ => ⟨rfl, by simp⟩⟩ +/-- **One request**: submit the word `w` and read the first bit of the reply. -/ +def queryBit (w : List Bool) : WordQueryComp Unit Bool := + (fun reply => decide (reply = [true])) <$> (List.take 1 <$> OracleComp.query ((), w)) + +open Classical in +/-- Against an oracle language, one request answers membership of its word. -/ +theorem interpret_queryBit (A : Set (List Bool)) (w : List Bool) : + OracleComp.interpret (m := Id) (languageOracle A) (queryBit w) = decide (w ∈ A) := by + change decide (List.take 1 (languageOracle A ((), w)) = [true]) = decide (w ∈ A) + rw [languageOracle_apply] + cases decide (w ∈ A) <;> rfl + +/-- One request makes one request. -/ +@[simp] +theorem queriesWith_queryBit (answer : Unit × List Bool → List Bool) (w : List Bool) : + OracleComp.queriesWith answer (queryBit w) = [((), w)] := by + simp [queryBit] + +/-- One request for a polynomial-time word is strict oracle PPT: the word is written on the query +buffer and one bit of the reply is read. -/ +theorem isOraclePPTOn_queryBit {req : α → List Bool} {input : α ↪ List Bool} + (hreq : ComputableInPolyTime req input encBits) : + IsOraclePPTOn input encBool + (fun a => OracleComp.interpret ProbOracleComp.query (queryBit (req a))) := by + simp only [queryBit, OracleComp.interpret_map, OracleComp.interpret_query] + exact (IsOraclePPTOn.query_take' () hreq (limit := fun _ => 1) + (ComputableInPolyTime.const 1)).map' + (ComputableInPolyTime.id'.decide_eq' (ComputableInPolyTime.const [true])) + open Classical in -/-- **One request.** The polynomial-time request `req a` is submitted and the first bit of the -reply is read: this decides whether `req a ∈ A` with one request. -/ +/-- **One request** to `A` for the polynomial-time word `req a` decides whether `req a ∈ A`. -/ theorem computableInPolyTimeWithOracleQueries_query {req : α → List Bool} {input : α ↪ List Bool} (hreq : ComputableInPolyTime req input encBits) (A : Set (List Bool)) : ComputableInPolyTimeWithOracleQueries A (fun _ => 1) (fun a => decide (req a ∈ A)) input - encBool := by - refine ⟨fun a => (fun reply => decide (reply = [true])) <$> - (List.take 1 <$> OracleComp.query ((), req a)), ?_, fun a => ⟨?_, ?_⟩⟩ - · simp only [OracleComp.interpret_map, OracleComp.interpret_query] - exact (IsOraclePPTOn.query_take' () hreq (limit := fun _ => 1) - (ComputableInPolyTime.const 1)).map' - (ComputableInPolyTime.id'.decide_eq' (ComputableInPolyTime.const [true])) - · change decide (List.take 1 (languageOracle A ((), req a)) = [true]) = decide (req a ∈ A) - rw [languageOracle_apply] - cases decide (req a ∈ A) <;> rfl - · simp + encBool := + ⟨fun a => queryBit (req a), isOraclePPTOn_queryBit hreq, + fun a => ⟨interpret_queryBit A (req a), by simp⟩⟩ /-- The problems decided in polynomial time relative to the oracle language `A` with at most `r n` requests on instances of encoded length `n`. -/ diff --git a/ComplexityTests/OracleBoundedQuery.lean b/ComplexityTests/OracleBoundedQuery.lean index 7374d42c03..3e4fd93776 100644 --- a/ComplexityTests/OracleBoundedQuery.lean +++ b/ComplexityTests/OracleBoundedQuery.lean @@ -21,12 +21,13 @@ example (A : Set (List Bool)) : computableInPolyTimeWithOracleQueries_query ComputableInPolyTime.id' A -- The single-request program asks exactly the word it decides: one request, answered by `A`. -open Classical in example (A : Set (List Bool)) (w : List Bool) : - OracleComp.queriesWith (languageOracle A) - ((fun reply => decide (reply = [true])) <$> - (List.take 1 <$> OracleComp.query (spec := fun _ : Unit × List Bool => List Bool) - ((), w))) = [((), w)] := by + OracleComp.queriesWith (languageOracle A) (queryBit w) = [((), w)] := by + simp + +open Classical in +example : OracleComp.interpret (m := Id) (languageOracle {[true]}) (queryBit [true]) = true := by + rw [interpret_queryBit] simp -- `SAT` and its complement are in `P^{NP[O(log n)]}`. From 51bcabf98d40f8185e2ca92cdc73ab6655603fb1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:51:53 -0400 Subject: [PATCH 06/12] wip(Classes/Sparse): binary-search oracle program for the census (#2062 M3) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/Sparse/Kadin.lean | 193 ++++++++++++++++++ 1 file changed, 193 insertions(+) diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean index b90605c4fd..c62ce4a7c4 100644 --- a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean @@ -10,11 +10,15 @@ module public import Complexity.Computability.Complexity.Classes.Oracle.BoundedQuery public import Complexity.Computability.Complexity.Classes.PH public import Complexity.Computability.Complexity.Classes.Sparse.Turing +public import Complexity.Languages.Probabilistic.Iteration import Complexity.Computability.Complexity.Classes.NP.Witness +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation +import Complexity.Computability.Probabilistic.Oracle.Composition import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length import Cslib.Foundations.Data.Polynomial.Monotone @@ -304,6 +308,195 @@ theorem language_mem_NP (hS : S ∈ NP encBits) (hsparse : S ∈ SPARSE encBits) Polynomial.eval_one, Polynomial.eval_comp, Polynomial.eval_ofNat] omega +/-! ### Binary search with one request per round -/ + +/-- One round of binary search on the interval `(lo, hi)`: if `lo < hi`, test the midpoint +`mid = ⌈(lo + hi) / 2⌉` with `P` and keep `(mid, hi)` or `(lo, mid - 1)`. -/ +def searchStep (P : ℕ → Bool) (st : ℕ × ℕ) : ℕ × ℕ := + if st.1 < st.2 then + if P ((st.1 + st.2 + 1) / 2) then ((st.1 + st.2 + 1) / 2, st.2) + else (st.1, (st.1 + st.2 + 1) / 2 - 1) + else st + +/-- A round keeps the threshold `C` of `P k = (k ≤ C)` inside the interval and halves it. -/ +theorem searchStep_spec {C : ℕ} {st : ℕ × ℕ} (h₁ : st.1 ≤ C) (h₂ : C ≤ st.2) : + (searchStep (fun k => decide (k ≤ C)) st).1 ≤ C ∧ C ≤ (searchStep (fun k => decide (k ≤ C)) st).2 ∧ + (searchStep (fun k => decide (k ≤ C)) st).2 - (searchStep (fun k => decide (k ≤ C)) st).1 ≤ + (st.2 - st.1) / 2 := by + unfold searchStep + by_cases h : st.1 < st.2 + · by_cases h' : (st.1 + st.2 + 1) / 2 ≤ C + · simp only [h, h', decide_true, ↓reduceIte] + refine ⟨trivial, ?_, ?_⟩ <;> omega + · simp only [h, h', decide_false, ↓reduceIte, Bool.false_eq_true] + refine ⟨?_, ?_, ?_⟩ <;> omega + · simp only [h, ↓reduceIte] + refine ⟨?_, ?_, ?_⟩ <;> omega + +/-- After `i` rounds from `(0, N)` the interval contains `C` and has length at most `N / 2 ^ i`. -/ +theorem iterate_searchStep_spec {C N : ℕ} (hC : C ≤ N) (i : ℕ) : + ((searchStep (fun k => decide (k ≤ C)))^[i] (0, N)).1 ≤ C ∧ + C ≤ ((searchStep (fun k => decide (k ≤ C)))^[i] (0, N)).2 ∧ + ((searchStep (fun k => decide (k ≤ C)))^[i] (0, N)).2 - + ((searchStep (fun k => decide (k ≤ C)))^[i] (0, N)).1 ≤ N / 2 ^ i := by + induction i with + | zero => exact ⟨Nat.zero_le _, hC, by simp⟩ + | succ i ih => + obtain ⟨h₁, h₂, h₃⟩ := ih + obtain ⟨h₁', h₂', h₃'⟩ := searchStep_spec h₁ h₂ + rw [Function.iterate_succ_apply'] + refine ⟨h₁', h₂', h₃'.trans ?_⟩ + rw [pow_succ, ← Nat.div_div_eq_div_mul] + exact Nat.div_le_div_right h₃ + +/-- **Binary search finds the threshold** after `count` rounds when `N < 2 ^ count`. -/ +theorem fst_iterate_searchStep {C N count : ℕ} (hC : C ≤ N) (hcount : N < 2 ^ count) : + ((searchStep (fun k => decide (k ≤ C)))^[count] (0, N)).1 = C := by + obtain ⟨h₁, h₂, h₃⟩ := iterate_searchStep_spec hC count + rw [Nat.div_eq_of_lt hcount] at h₃ + omega + +/-- One round against an oracle: the midpoint `k` is tested by one request for `req (a, k)`. -/ +def searchStepProgram (req : α × ℕ → List Bool) (a : α) (st : ℕ × ℕ) : + WordQueryComp Unit (ℕ × ℕ) := + if st.1 < st.2 then + (fun b => if b then ((st.1 + st.2 + 1) / 2, st.2) else (st.1, (st.1 + st.2 + 1) / 2 - 1)) <$> + queryBit (req (a, (st.1 + st.2 + 1) / 2)) + else pure st + +open Classical in +theorem interpret_searchStepProgram (A : Set (List Bool)) (req : α × ℕ → List Bool) (a : α) + (st : ℕ × ℕ) : + OracleComp.interpret (m := Id) (languageOracle A) (searchStepProgram req a st) = + searchStep (fun k => decide (req (a, k) ∈ A)) st := by + unfold searchStepProgram searchStep + by_cases h : st.1 < st.2 + · simp only [h, ↓reduceIte, OracleComp.interpret_map, interpret_queryBit] + rfl + · simp only [h, ↓reduceIte] + rfl + +/-- A round makes at most one request. -/ +theorem length_queriesWith_searchStepProgram_le (answer : Unit × List Bool → List Bool) + (req : α × ℕ → List Bool) (a : α) (st : ℕ × ℕ) : + (OracleComp.queriesWith answer (searchStepProgram req a st)).length ≤ 1 := by + unfold searchStepProgram + split_ifs <;> simp + +/-- A loop whose rounds make at most one request each makes at most one request per round. -/ +theorem length_queriesWith_iterate_le {State : Type} (answer : Unit × List Bool → List Bool) + {step : State → WordQueryComp Unit State} + (h : ∀ st, (OracleComp.queriesWith answer (step st)).length ≤ 1) (n : ℕ) (st : State) : + (OracleComp.queriesWith answer (OracleComp.iterate n step st)).length ≤ n := by + induction n with + | zero => simp + | succ n ih => + rw [OracleComp.iterate_succ, OracleComp.queriesWith_bind, List.length_append] + exact Nat.add_le_add ih (h _) + +/-- The algorithm: `count a` rounds of binary search from `(0, N a)` with the requests `req`, +then one request `fin (a, lo)` at the threshold found. -/ +def program (req fin : α × ℕ → List Bool) (N count : α → ℕ) (a : α) : WordQueryComp Unit Bool := + OracleComp.iterate (count a) (searchStepProgram req a) (0, N a) >>= fun st => + queryBit (fin (a, st.1)) + +open Classical in +theorem interpret_program (A : Set (List Bool)) (req fin : α × ℕ → List Bool) (N count : α → ℕ) + (a : α) : + OracleComp.interpret (m := Id) (languageOracle A) (program req fin N count a) = + decide (fin (a, ((searchStep fun k => decide (req (a, k) ∈ A))^[count a] (0, N a)).1) ∈ A) := by + rw [program, OracleComp.interpret_bind, OracleComp.interpret_id_iterate] + simp only [interpret_searchStepProgram] + exact interpret_queryBit A _ + +/-- The algorithm makes at most `count a + 1` requests. -/ +theorem length_queriesWith_program_le (answer : Unit × List Bool → List Bool) + (req fin : α × ℕ → List Bool) (N count : α → ℕ) (a : α) : + (OracleComp.queriesWith answer (program req fin N count a)).length ≤ count a + 1 := by + rw [program, OracleComp.queriesWith_bind, List.length_append, queriesWith_queryBit, + List.length_singleton] + exact Nat.add_le_add_right + (length_queriesWith_iterate_le answer (length_queriesWith_searchStepProgram_le answer req a) _ _) 1 + +open Probability in +/-- **The algorithm is strict oracle PPT** when the requests, the bound `N` and the count are +polynomial-time. Every reachable interval lies within `[0, N a]`. -/ +theorem isOraclePPTOn_program {enc : α ↪ List Bool} {req fin : α × ℕ → List Bool} + {N count : α → ℕ} (hreq : ComputableInPolyTime req (encPair enc encUnary) encBits) + (hfin : ComputableInPolyTime fin (encPair enc encUnary) encBits) + (hN : ComputableInPolyTime N enc encUnary) (hcount : ComputableInPolyTime count enc encUnary) : + IsOraclePPTOn enc encBool + (fun a => OracleComp.interpret ProbOracleComp.query (program req fin N count a)) := by + have hmid : ComputableInPolyTime (fun pair : α × ℕ × ℕ => (pair.2.1 + pair.2.2 + 1) / 2) + (encPair enc (encPair encUnary encUnary)) encUnary := + (ComputableInPolyTime.unary_div_const 2).comp + (g := fun pair : α × ℕ × ℕ => pair.2.1 + pair.2.2 + 1) (by fun_prop) + have hq : IsOraclePPTOn (encPair enc (encPair encUnary encUnary)) encBool + (fun pair : α × ℕ × ℕ => OracleComp.interpret ProbOracleComp.query + (queryBit (req (pair.1, (pair.2.1 + pair.2.2 + 1) / 2)))) := + isOraclePPTOn_queryBit (input := encPair enc (encPair encUnary encUnary)) + (req := fun pair : α × ℕ × ℕ => req (pair.1, (pair.2.1 + pair.2.2 + 1) / 2)) + (hreq.comp (g := fun pair : α × ℕ × ℕ => (pair.1, (pair.2.1 + pair.2.2 + 1) / 2)) + ((ComputableInPolyTime.fst _ _).prod hmid)) + have hpost : ComputableInPolyTime (fun x : (α × ℕ × ℕ) × Bool => + if x.2 then ((x.1.2.1 + x.1.2.2 + 1) / 2, x.1.2.2) + else (x.1.2.1, (x.1.2.1 + x.1.2.2 + 1) / 2 - 1)) + (encPair (encPair enc (encPair encUnary encUnary)) encBool) (encPair encUnary encUnary) := by + have hmid' : ComputableInPolyTime (fun x : (α × ℕ × ℕ) × Bool => (x.1.2.1 + x.1.2.2 + 1) / 2) + (encPair (encPair enc (encPair encUnary encUnary)) encBool) encUnary := + hmid.comp (g := fun x : (α × ℕ × ℕ) × Bool => x.1) (.fst _ _) + have hlo : ComputableInPolyTime (fun x : (α × ℕ × ℕ) × Bool => x.1.2.1) + (encPair (encPair enc (encPair encUnary encUnary)) encBool) encUnary := by fun_prop + have hhi : ComputableInPolyTime (fun x : (α × ℕ × ℕ) × Bool => x.1.2.2) + (encPair (encPair enc (encPair encUnary encUnary)) encBool) encUnary := by fun_prop + exact ComputableInPolyTime.ite' (ComputableInPolyTime.snd _ _) (hmid'.prod hhi) + (hlo.prod (ComputableInPolyTime.unary_sub' hmid' (ComputableInPolyTime.const 1))) + have hyes := hq.map_with' (f := fun pair b => if b then ((pair.2.1 + pair.2.2 + 1) / 2, pair.2.2) + else (pair.2.1, (pair.2.1 + pair.2.2 + 1) / 2 - 1)) hpost + have hno : IsOraclePPTOn (Operation := Unit) (encPair enc (encPair encUnary encUnary)) + (encPair encUnary encUnary) (fun pair : α × ℕ × ℕ => pure pair.2) := + (ComputableInPolyTime.snd _ _).isOraclePPTOn + have hcond : ComputableInPolyTime (fun pair : α × ℕ × ℕ => decide (pair.2.1 < pair.2.2)) + (encPair enc (encPair encUnary encUnary)) encBool := by fun_prop + have hstep : IsOraclePPTOn (encPair enc (encPair encUnary encUnary)) (encPair encUnary encUnary) + (fun pair : α × ℕ × ℕ => OracleComp.interpret ProbOracleComp.query + (searchStepProgram req pair.1 pair.2)) := by + refine (IsOraclePPTOn.ite' (condition := fun pair : α × ℕ × ℕ => pair.2.1 < pair.2.2) hcond + hyes hno).congr fun pair State oracle s => ?_ + unfold searchStepProgram + split_ifs <;> simp only [OracleComp.interpret_map, OracleComp.interpret_pure] + have hinit : ComputableInPolyTime (fun a => ((0 : ℕ), N a)) enc (encPair encUnary encUnary) := + (ComputableInPolyTime.const 0).prod hN + have hsize : PolyBounded (fun a => (enc a).length) (fun a => 3 * N a + 1) := + ((PolyBounded.const 3).mul hN.polyBounded).add (.const 1) + have hit := IsOraclePPTOn.iterateWith_spec' (input := enc) + (stateEncoding := encPair encUnary encUnary) (count := count) + (initial := fun a => ((0 : ℕ), N a)) + (step := fun a st => OracleComp.interpret ProbOracleComp.query (searchStepProgram req a st)) + hcount hinit hstep (fun a _ st => st.1 ≤ st.2 ∧ st.2 ≤ N a) + (fun a => ⟨Nat.zero_le _, le_rfl⟩) (fun a i st _ hinv next hnext => by + unfold searchStepProgram at hnext + by_cases h : st.1 < st.2 + · rw [ite_eq_left_iff.mpr (fun h' => absurd h h'), OracleComp.interpret_map] at hnext + obtain ⟨b, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hnext + cases b <;> simp only [Bool.false_eq_true, ↓reduceIte] <;> omega + · rw [ite_eq_right_iff.mpr (fun h' => absurd h' h), OracleComp.interpret_pure] at hnext + rw [OracleComp.eq_of_mem_supportWith_pure hnext] + exact hinv) + hsize (fun a i st _ hinv => by + simp only [length_encPair, encUnary_apply, List.length_replicate] + omega) + have hfinal : IsOraclePPTOn (encPair enc (encPair encUnary encUnary)) encBool + (fun pair : α × ℕ × ℕ => OracleComp.interpret ProbOracleComp.query + (queryBit (fin (pair.1, pair.2.1)))) := + isOraclePPTOn_queryBit (input := encPair enc (encPair encUnary encUnary)) + (req := fun pair : α × ℕ × ℕ => fin (pair.1, pair.2.1)) + (hfin.comp (g := fun pair : α × ℕ × ℕ => (pair.1, pair.2.1)) + ((ComputableInPolyTime.fst _ _).prod (ComputableInPolyTime.snd _ _).fst')) + have hbind := hit.1.bind_with (second := fun a st => OracleComp.interpret ProbOracleComp.query + (queryBit (fin (a, st.1)))) hfinal + simpa only [program, OracleComp.interpret_bind, OracleComp.interpret_iterate] using hbind + end KadinCensus end Cslib.Complexity From 21d1dd4b1aa7f22732fe9c98cad1dde15eb271db Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:53:44 -0400 Subject: [PATCH 07/12] wip(Classes/Sparse): Kadin's theorem assembled (#2062 M3) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Complexity/Classes/Sparse/Kadin.lean | 106 ++++++++++++++++++ 1 file changed, 106 insertions(+) diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean index c62ce4a7c4..89692ae1ba 100644 --- a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean @@ -11,7 +11,13 @@ public import Complexity.Computability.Complexity.Classes.Oracle.BoundedQuery public import Complexity.Computability.Complexity.Classes.PH public import Complexity.Computability.Complexity.Classes.Sparse.Turing public import Complexity.Languages.Probabilistic.Iteration +import Complexity.Computability.Complexity.Classes.NP.Image import Complexity.Computability.Complexity.Classes.NP.Witness +import Complexity.Computability.Complexity.Classes.Oracle.Closure +import Complexity.Computability.Complexity.Classes.Oracle.ListOracle +import Complexity.Computability.Complexity.Classes.PH.Projection +import Complexity.Computability.Complexity.CookLevin.Completeness +import Complexity.Computability.Complexity.Problems.SAT.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation import Complexity.Computability.Probabilistic.Oracle.Composition import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic @@ -19,6 +25,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length import Cslib.Foundations.Data.Polynomial.Monotone @@ -499,4 +506,103 @@ theorem isOraclePPTOn_program {enc : α ↪ List Bool} {req fin : α × ℕ → end KadinCensus + +/-! ### Kadin's theorem -/ + +/-- A polynomially bounded quantity has a logarithmic number of bits: `⌈log₂ N n⌉ ≤ K log₂ n + K`. +-/ +theorem exists_clog_le_of_polynomiallyBounded {N : ℕ → ℕ} (hN : PolynomiallyBounded N) : + ∃ K : ℕ, ∀ n, Nat.clog 2 (N n) ≤ K * Nat.log 2 n + K := by + obtain ⟨e, f, h⟩ := polynomiallyBounded_iff_le.mp hN + refine ⟨f + e, fun n => Nat.clog_le_of_le_pow ?_⟩ + have hn : n + 1 ≤ 2 ^ (Nat.log 2 n + 1) := Nat.lt_pow_succ_log_self (by norm_num) n + have he : e ≤ 2 ^ e := (Nat.lt_two_pow_self).le + calc N n ≤ e * (n + 1) ^ f := h n + _ ≤ 2 ^ e * (2 ^ (Nat.log 2 n + 1)) ^ f := + Nat.mul_le_mul he (Nat.pow_le_pow_left hn f) + _ = 2 ^ (f * Nat.log 2 n + f + e) := by rw [← pow_mul, ← pow_add]; ring_nf + _ ≤ 2 ^ ((f + e) * Nat.log 2 n + (f + e)) := + Nat.pow_le_pow_right (by norm_num) (by nlinarith [Nat.zero_le (Nat.log 2 n)]) + +open Classical in +/-- **`Σ₂ ⊆ P^{NP[O(log n)]}` under a sparse Turing-complete set for `NP`.** Binary search with +requests to `SAT` finds the census of `S` up to the length of the oracle words, and one more +request, at the exact census, guesses the short members of `S` together with the first certificate +of the `Σ₂` problem [Hemaspaandra and Ogihara, Theorem 1.14][HemaspaandraOgihara2002]. -/ +theorem SigmaP_two_subset_PNPLog_of_sparse (hsparse : S ∈ SPARSE encBits) (hS : S ∈ NP encBits) + (hSAT : SAT ∈ PWithOracle S encCNF) (enc : α ↪ List Bool) : + SigmaP 2 enc ⊆ PNPLog enc := by + intro L hL + -- `a ∈ L ↔ ∃ w, (a, w) ∈ B` with `B ∈ coNP`, and `Bᶜ ∈ NP ⊆ P^S` + obtain ⟨p, B, hB, hLB⟩ := exists_mem_PiP_of_mem_SigmaP_succ (k := 1) hL + rw [PiP_one_eq_coNP] at hB + obtain ⟨g, hg, hgB⟩ := (CookLevin.SAT_npHard _ _ hB).mem_PWithOracle hSAT + obtain ⟨G, q, hG, hGg⟩ := hg.exists_listOracle_bool + -- the oracle words asked on `(a, w)` with `|w| = p |enc a|` have length at most `m |enc a|` + let m : Polynomial ℕ := q.comp (2 * Polynomial.X + 1 + p) + have hD := KadinCensus.language_mem_NP (m := m) (p := p) hS hsparse hG + obtain ⟨red, hred, hDred⟩ := CookLevin.SAT_npHard _ _ hD + have henc : ComputableInPolyTime (fun φ : Cslib.Logic.PL.CNF ℕ => encCNF φ) encCNF encBits := + .of_eq fun _ => rfl + have hreqb (b : Bool) : ComputableInPolyTime (fun x : α × ℕ => encCNF (red (x.1, x.2, b))) + (encPair enc encUnary) encBits := + henc.comp (hred.comp (g := fun x : α × ℕ => (x.1, x.2, b)) + ((ComputableInPolyTime.fst _ _).prod ((ComputableInPolyTime.snd _ _).prod + (ComputableInPolyTime.const b)))) + have hmemA (x : α × ℕ × Bool) : + encCNF (red x) ∈ encCNF '' SAT ↔ x ∈ KadinCensus.language S enc m p G := by + rw [hDred x] + exact ⟨fun ⟨_, h, he⟩ => encCNF.injective he ▸ h, fun h => ⟨_, h, rfl⟩⟩ + -- the census bound and the number of rounds + obtain ⟨c, d, hcensus⟩ := exists_length_shortMembers_le hsparse + let N : α → ℕ := fun a => c * (m.eval (enc a).length + 1) ^ d + let count : α → ℕ := fun a => Nat.clog 2 (N a + 1) + have hN : ComputableInPolyTime N enc encUnary := + ((ComputableInPolyTime.unary_eval (Polynomial.C c * (m + 1) ^ d)).comp + (ComputableInPolyTime.encoding_length enc)).of_enc_eq fun a => by simp [N] + have hcount : ComputableInPolyTime count enc encUnary := + (ComputableInPolyTime.unary_clog_const 2).comp + (ComputableInPolyTime.unary_add' hN (ComputableInPolyTime.const 1)) + obtain ⟨K, hK⟩ := exists_clog_le_of_polynomiallyBounded + (N := fun n => c * (m.eval n + 1) ^ d + 1) (by fun_prop) + let prog := KadinCensus.program (fun x => encCNF (red (x.1, x.2, false))) + (fun x => encCNF (red (x.1, x.2, true))) N count + refine mem_PNPLog_of_mem_PWithOracleQueries (c := K + 1) image_SAT_mem_NP + ⟨fun a => OracleComp.interpret (m := Id) (languageOracle (encCNF '' SAT)) (prog a), + ⟨prog, KadinCensus.isOraclePPTOn_program (hreqb false) (hreqb true) hN hcount, + fun a => ⟨rfl, ?_⟩⟩, fun a => ?_⟩ + · refine (KadinCensus.length_queriesWith_program_le _ _ _ _ _ a).trans ?_ + have := hK (enc a).length + simp only [N, count] at this ⊢ + nlinarith [Nat.zero_le (Nat.log 2 (enc a).length)] + -- correctness: binary search finds the census, and the last request decides `L` + have hP : (fun k => decide (encCNF (red (a, k, false)) ∈ encCNF '' SAT)) = + fun k => decide (k ≤ KadinCensus.census S enc m a) := by + funext k + rw [Bool.eq_iff_iff, decide_eq_true_iff, decide_eq_true_iff, hmemA, + KadinCensus.mem_language_false_iff] + have hcen : KadinCensus.census S enc m a ≤ N a := hcensus _ + have hlt : N a < 2 ^ count a := Nat.lt_of_succ_le (Nat.le_pow_clog (by norm_num) _) + have hlast := KadinCensus.mem_language_census_true_iff (S := S) (enc := enc) (m := m) (p := p) + (G := G) (a := a) (g := g) fun w ℓ hw hℓ => hGg (a, w) ℓ fun s hs => + hℓ s (by simpa [m, length_encPair, hw] using hs) + change a ∈ L ↔ OracleComp.interpret (m := Id) (languageOracle (encCNF '' SAT)) + (KadinCensus.program (fun x => encCNF (red (x.1, x.2, false))) + (fun x => encCNF (red (x.1, x.2, true))) N count a) = true + rw [KadinCensus.interpret_program, decide_eq_true_iff] + dsimp only + rw [hmemA, hP, KadinCensus.fst_iterate_searchStep hcen hlt, hlast, hLB a] + refine exists_congr fun w => and_congr_right fun _ => ?_ + rw [← Bool.not_eq_true, ← hgB, Set.mem_compl_iff, not_not] + +/-- **Kadin's theorem** [Kadin][Kadin1989] [Hemaspaandra and Ogihara, Theorem 1.14] +[HemaspaandraOgihara2002]: if `NP` has a sparse polynomial-time Turing-complete set, that is a +sparse `S ∈ NP` with `SAT` decided in polynomial time relative to `S`, then the polynomial +hierarchy is contained in `P^{NP[O(log n)]}`. -/ +theorem PH_subset_PNPLog_of_sparse (hsparse : S ∈ SPARSE encBits) (hS : S ∈ NP encBits) + (hSAT : SAT ∈ PWithOracle S encCNF) (enc : α ↪ List Bool) : + PH enc ⊆ PNPLog enc := by + rw [PH_eq_SigmaP_two_of_SAT_mem_PWithOracle hsparse hSAT enc] + exact SigmaP_two_subset_PNPLog_of_sparse hsparse hS hSAT enc + end Cslib.Complexity From 7861f3512374965cf3b6957f9994c811644fb472 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:57:04 -0400 Subject: [PATCH 08/12] =?UTF-8?q?feat(Classes/Sparse):=20Kadin's=20theorem?= =?UTF-8?q?,=20PH=20=E2=8A=86=20P^{NP[O(log=20n)]}=20under=20a=20sparse=20?= =?UTF-8?q?Turing-complete=20set=20for=20NP=20(#2062=20M3)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Census requests in NP, binary search with one request per round, the final request at the exact census, and the collapse via the sparse form of Karp-Lipton. Tests instantiate the census, the search and the hypotheses. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Complexity/Classes/Sparse/Kadin.lean | 54 ++++++++--- ComplexityTests/SparseKadin.lean | 96 +++++++++++++++++++ ROADMAP.md | 6 +- 4 files changed, 141 insertions(+), 16 deletions(-) create mode 100644 ComplexityTests/SparseKadin.lean diff --git a/Complexity.lean b/Complexity.lean index 1ba97f7042..dbc0963bcd 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1331,6 +1331,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 diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean index 89692ae1ba..8123e7d1e6 100644 --- a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean @@ -18,15 +18,15 @@ import Complexity.Computability.Complexity.Classes.Oracle.ListOracle import Complexity.Computability.Complexity.Classes.PH.Projection import Complexity.Computability.Complexity.CookLevin.Completeness import Complexity.Computability.Complexity.Problems.SAT.PolyTime -import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation -import Complexity.Computability.Probabilistic.Oracle.Composition import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic -import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation +import Complexity.Computability.Probabilistic.Oracle.Composition import Cslib.Foundations.Data.Polynomial.Monotone /-! @@ -34,7 +34,8 @@ import Cslib.Foundations.Data.Polynomial.Monotone If `NP` has a sparse polynomial-time Turing-complete set, that is a sparse `S ∈ NP` to which `SAT` is polynomial-time Turing reducible, then the polynomial hierarchy collapses to -`P^{NP[O(log n)]}` [Kadin][Kadin1989] [Hemaspaandra and Ogihara, Theorem 1.14][HemaspaandraOgihara2002]. +`P^{NP[O(log n)]}` (`Cslib.Complexity.PH_subset_PNPLog_of_sparse`) [Kadin][Kadin1989] +[Hemaspaandra and Ogihara, Theorem 1.14][HemaspaandraOgihara2002]. The proof follows the census argument of [Hemaspaandra and Ogihara, Theorem 1.14] [HemaspaandraOgihara2002]. The census of `S` up to length `m` is the number of members of `S` of @@ -47,15 +48,31 @@ length at most `m`; it is polynomial in `m` because `S` is sparse. (`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`). Hence one more request in `NP`, which guesses the list and a first certificate, decides a problem in `Σ₂`. -So `Σ₂ ⊆ P^{NP[O(log n)]}`. The Companion completes the proof by `Θ₂ ⊆ Σ₂ ∩ Π₂` and closure of -`Θ₂` under complement; here `PH = Σ₂` comes instead from the sparse form of the Karp–Lipton -theorem (`Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`). +So `Σ₂ ⊆ P^{NP[O(log n)]}`. The Companion completes the proof with `Θ₂ ⊆ Σ₂` and closure of `Θ₂` +under complement, which give `Σ₂ = Π₂`; here `PH = Σ₂` comes instead from the sparse form of the +Karp–Lipton theorem (`Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`). The reverse +inclusion `P^{NP[O(log n)]} ⊆ PH`, which with this gives the Companion's `PH = Θ₂`, is not proved +here. + +The hypothesis is the Turing-complete case. Kadin's abstract states the result for a sparse +`S ∈ NP` with `coNP ⊆ NP^S`, of which the Turing-complete case is a consequence; that form is not +formalized here. + +The algorithm (`Cslib.Complexity.KadinCensus.program`) runs `⌈log₂ (N + 1)⌉` rounds of binary +search (`Cslib.Complexity.KadinCensus.searchStepProgram`) on an interval containing the census, +where `N` is the polynomial census bound, each round making one request to the encodings of the +satisfiable formulas through the Cook–Levin reduction, and then makes one last request. The loop +is certified by `Cslib.Probability.IsOraclePPTOn.iterateWith_spec'`; every reachable interval lies +in `[0, N]`. ## Main definitions * `Cslib.Complexity.KadinCensus.language`: the `NP` problem asked by the algorithm, on triples `(a, k, b)`: `k` distinct short members of `S` exist, and if `b`, they also witness the first quantifier of a `Σ₂` problem. +* `Cslib.Complexity.KadinCensus.searchStep`: one round of binary search for a threshold. +* `Cslib.Complexity.KadinCensus.searchStepProgram`, `Cslib.Complexity.KadinCensus.program`: the + oracle programs. ## Main results @@ -65,6 +82,12 @@ theorem (`Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`). * `Cslib.Complexity.KadinCensus.mem_language_false_iff`, `Cslib.Complexity.KadinCensus.mem_language_census_true_iff`: the meaning of the requests. * `Cslib.Complexity.KadinCensus.language_mem_NP`: the requests form a problem in `NP`. +* `Cslib.Complexity.KadinCensus.fst_iterate_searchStep`: binary search finds the threshold. +* `Cslib.Complexity.KadinCensus.length_queriesWith_program_le`, + `Cslib.Complexity.KadinCensus.isOraclePPTOn_program`: the algorithm makes one request per round + plus one, and is strict oracle PPT. +* `Cslib.Complexity.SigmaP_two_subset_PNPLog_of_sparse`: `Σ₂ ⊆ P^{NP[O(log n)]}`. +* `Cslib.Complexity.PH_subset_PNPLog_of_sparse`: **Kadin's theorem**, `PH ⊆ P^{NP[O(log n)]}`. ## References @@ -298,7 +321,8 @@ theorem language_mem_NP (hS : S ∈ NP encBits) (hsparse : S ∈ SPARSE encBits) have hlist : (encList (encPair encBits encBits) y.1).length ≤ c * (m.eval n + 1) ^ d * (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) := by rw [length_encList] - have h := List.sum_le_length_nsmul (y.1.map fun sc => 2 * (encPair encBits encBits sc).length + 1) + have h := List.sum_le_length_nsmul + (y.1.map fun sc => 2 * (encPair encBits encBits sc).length + 1) (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) fun z hz => by obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hz exact hpair sc hsc @@ -327,7 +351,8 @@ def searchStep (P : ℕ → Bool) (st : ℕ × ℕ) : ℕ × ℕ := /-- A round keeps the threshold `C` of `P k = (k ≤ C)` inside the interval and halves it. -/ theorem searchStep_spec {C : ℕ} {st : ℕ × ℕ} (h₁ : st.1 ≤ C) (h₂ : C ≤ st.2) : - (searchStep (fun k => decide (k ≤ C)) st).1 ≤ C ∧ C ≤ (searchStep (fun k => decide (k ≤ C)) st).2 ∧ + (searchStep (fun k => decide (k ≤ C)) st).1 ≤ C ∧ + C ≤ (searchStep (fun k => decide (k ≤ C)) st).2 ∧ (searchStep (fun k => decide (k ≤ C)) st).2 - (searchStep (fun k => decide (k ≤ C)) st).1 ≤ (st.2 - st.1) / 2 := by unfold searchStep @@ -411,7 +436,8 @@ open Classical in theorem interpret_program (A : Set (List Bool)) (req fin : α × ℕ → List Bool) (N count : α → ℕ) (a : α) : OracleComp.interpret (m := Id) (languageOracle A) (program req fin N count a) = - decide (fin (a, ((searchStep fun k => decide (req (a, k) ∈ A))^[count a] (0, N a)).1) ∈ A) := by + decide (fin (a, ((searchStep fun k => decide (req (a, k) ∈ A))^[count a] (0, N a)).1) ∈ + A) := by rw [program, OracleComp.interpret_bind, OracleComp.interpret_id_iterate] simp only [interpret_searchStepProgram] exact interpret_queryBit A _ @@ -422,8 +448,8 @@ theorem length_queriesWith_program_le (answer : Unit × List Bool → List Bool) (OracleComp.queriesWith answer (program req fin N count a)).length ≤ count a + 1 := by rw [program, OracleComp.queriesWith_bind, List.length_append, queriesWith_queryBit, List.length_singleton] - exact Nat.add_le_add_right - (length_queriesWith_iterate_le answer (length_queriesWith_searchStepProgram_le answer req a) _ _) 1 + exact Nat.add_le_add_right (length_queriesWith_iterate_le answer + (length_queriesWith_searchStepProgram_le answer req a) _ _) 1 open Probability in /-- **The algorithm is strict oracle PPT** when the requests, the bound `N` and the count are @@ -484,10 +510,10 @@ theorem isOraclePPTOn_program {enc : α ↪ List Bool} {req fin : α × ℕ → (fun a => ⟨Nat.zero_le _, le_rfl⟩) (fun a i st _ hinv next hnext => by unfold searchStepProgram at hnext by_cases h : st.1 < st.2 - · rw [ite_eq_left_iff.mpr (fun h' => absurd h h'), OracleComp.interpret_map] at hnext + · simp only [h, ↓reduceIte, OracleComp.interpret_map] at hnext obtain ⟨b, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hnext cases b <;> simp only [Bool.false_eq_true, ↓reduceIte] <;> omega - · rw [ite_eq_right_iff.mpr (fun h' => absurd h' h), OracleComp.interpret_pure] at hnext + · simp only [h, ↓reduceIte, OracleComp.interpret_pure] at hnext rw [OracleComp.eq_of_mem_supportWith_pure hnext] exact hinv) hsize (fun a i st _ hinv => by diff --git a/ComplexityTests/SparseKadin.lean b/ComplexityTests/SparseKadin.lean new file mode 100644 index 0000000000..757c65b9de --- /dev/null +++ b/ComplexityTests/SparseKadin.lean @@ -0,0 +1,96 @@ +/- +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.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 diff --git a/ROADMAP.md b/ROADMAP.md index ec346a7149..936b854d5a 100644 --- a/ROADMAP.md +++ b/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 From 99e296a2cdb350fb3751a7ab0e3ea898e1fff30a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 11:58:59 -0400 Subject: [PATCH 09/12] test(Classes/Sparse): wrap a long line in the Kadin tests Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- ComplexityTests/SparseKadin.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/ComplexityTests/SparseKadin.lean b/ComplexityTests/SparseKadin.lean index 757c65b9de..7b29ca6ff6 100644 --- a/ComplexityTests/SparseKadin.lean +++ b/ComplexityTests/SparseKadin.lean @@ -64,8 +64,9 @@ example : OracleComp.interpret (m := Id) (languageOracle {w : List Bool | w.leng 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 := + (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 From 6d6914bb7c006bc3eef19899c0245095fae9ca39 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:44:21 -0400 Subject: [PATCH 10/12] refactor(Classes/Oracle): share the one-request program between Closure and BoundedQuery Move `queryBit`, its interpretation and request equations and its strict oracle PPT certificate into the new module `Classes/Oracle/QueryBit`, imported by both `Oracle/Closure` and `Oracle/BoundedQuery`. `PolyTimeOracleProgram.of_query` is now built from `queryBit` instead of repeating the request/map/take construction and its proofs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Classes/Oracle/BoundedQuery.lean | 36 +--------- .../Complexity/Classes/Oracle/Closure.lean | 18 ++--- .../Complexity/Classes/Oracle/QueryBit.lean | 72 +++++++++++++++++++ 4 files changed, 81 insertions(+), 46 deletions(-) create mode 100644 Complexity/Computability/Complexity/Classes/Oracle/QueryBit.lean diff --git a/Complexity.lean b/Complexity.lean index 97ffc768ce..26bdd1fa98 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1251,6 +1251,7 @@ public import Complexity.Computability.Complexity.Classes.Oracle.Lowness public import Complexity.Computability.Complexity.Classes.Oracle.Monotone public import Complexity.Computability.Complexity.Classes.Oracle.PP public import Complexity.Computability.Complexity.Classes.Oracle.PolyTime +public import Complexity.Computability.Complexity.Classes.Oracle.QueryBit public import Complexity.Computability.Complexity.Classes.Oracle.Space public import Complexity.Computability.Complexity.Classes.Oracle.TQBF public import Complexity.Computability.Complexity.Classes.P diff --git a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean index 76b7a32aba..9a3df0e025 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Complexity.Classes.Oracle +public import Complexity.Computability.Complexity.Classes.Oracle.QueryBit public import Complexity.Computability.Complexity.Problems.SAT import Complexity.Computability.Complexity.Classes.NP.Image import Complexity.Computability.Complexity.CookLevin.Completeness @@ -34,7 +34,6 @@ is closed under complement. ## Main definitions -* `Cslib.Complexity.queryBit`: one request, reading one bit of the reply. * `Cslib.Complexity.ComputableInPolyTimeWithOracleQueries`: polynomial time relative to an oracle with a bounded number of requests. * `Cslib.Complexity.PWithOracleQueries`: the problems so decided. @@ -46,8 +45,8 @@ is closed under complement. `.mono`, `.map`: forgetting and weakening the bound, and postprocessing. * `Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithOracleQueries`: polynomial time makes no request. -* `Cslib.Complexity.computableInPolyTimeWithOracleQueries_query`: one request decides membership - of a polynomial-time request word. +* `Cslib.Complexity.computableInPolyTimeWithOracleQueries_query`: one request + (`Cslib.Complexity.queryBit`) decides membership of a polynomial-time request word. * `Cslib.Complexity.compl_mem_PWithOracleQueries`, `Cslib.Complexity.compl_mem_PNPLog`: closure under complement. * `Cslib.Complexity.NP_subset_PWithOracleQueries_image_SAT`: one request to `SAT` decides a @@ -119,35 +118,6 @@ theorem _root_.Turing.MultiTapeTM.ComputableInPolyTime.computableInPolyTimeWithO ComputableInPolyTimeWithOracleQueries A r f input output := ⟨fun a => pure (f a), h.isOraclePPTOn, fun _ => ⟨rfl, by simp⟩⟩ -/-- **One request**: submit the word `w` and read the first bit of the reply. -/ -def queryBit (w : List Bool) : WordQueryComp Unit Bool := - (fun reply => decide (reply = [true])) <$> (List.take 1 <$> OracleComp.query ((), w)) - -open Classical in -/-- Against an oracle language, one request answers membership of its word. -/ -theorem interpret_queryBit (A : Set (List Bool)) (w : List Bool) : - OracleComp.interpret (m := Id) (languageOracle A) (queryBit w) = decide (w ∈ A) := by - change decide (List.take 1 (languageOracle A ((), w)) = [true]) = decide (w ∈ A) - rw [languageOracle_apply] - cases decide (w ∈ A) <;> rfl - -/-- One request makes one request. -/ -@[simp] -theorem queriesWith_queryBit (answer : Unit × List Bool → List Bool) (w : List Bool) : - OracleComp.queriesWith answer (queryBit w) = [((), w)] := by - simp [queryBit] - -/-- One request for a polynomial-time word is strict oracle PPT: the word is written on the query -buffer and one bit of the reply is read. -/ -theorem isOraclePPTOn_queryBit {req : α → List Bool} {input : α ↪ List Bool} - (hreq : ComputableInPolyTime req input encBits) : - IsOraclePPTOn input encBool - (fun a => OracleComp.interpret ProbOracleComp.query (queryBit (req a))) := by - simp only [queryBit, OracleComp.interpret_map, OracleComp.interpret_query] - exact (IsOraclePPTOn.query_take' () hreq (limit := fun _ => 1) - (ComputableInPolyTime.const 1)).map' - (ComputableInPolyTime.id'.decide_eq' (ComputableInPolyTime.const [true])) - open Classical in /-- **One request** to `A` for the polynomial-time word `req a` decides whether `req a ∈ A`. -/ theorem computableInPolyTimeWithOracleQueries_query {req : α → List Bool} diff --git a/Complexity/Computability/Complexity/Classes/Oracle/Closure.lean b/Complexity/Computability/Complexity/Classes/Oracle/Closure.lean index ad11c518c5..79bc4cf1f4 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/Closure.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/Closure.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Complexity.Classes.Oracle public import Complexity.Computability.Complexity.Reduction public import Complexity.Computability.Probabilistic.Oracle.Composition +import Complexity.Computability.Complexity.Classes.Oracle.QueryBit import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -23,7 +24,7 @@ Polynomial time relative to an oracle composes with polynomial-time pre- and pos `Cslib.Complexity.ComputableInPolyTimeWithOracle.map`), through the compositional rules of strict oracle PPT. One request decides the oracle language itself (`Cslib.Complexity.computableInPolyTimeWithOracle_mem`): the request is copied onto the query -buffer, and only the first bit of the reply is read. +buffer, and only the first bit of the reply is read (`Cslib.Complexity.queryBit`). Hence `P` relative to `A` contains `A` and lies inside `NP` relative to `A`, and both classes are closed under polynomial-time many-one reductions of the problem @@ -118,18 +119,9 @@ theorem PolyTimeOracleProgram.of_query {req : α → List Bool} {input : α ↪ {Admissible : Set (List Bool) → Prop} {Spec : (α → Bool) → Prop} (hreq : ComputableInPolyTime req input encBits) (hSpec : ∀ A : Set (List Bool), Admissible A → Spec (fun a => decide (req a ∈ A))) : - PolyTimeOracleProgram input encBool Admissible Spec := by - refine ⟨fun a => (fun reply => decide (reply = [true])) <$> - (List.take 1 <$> OracleComp.query ((), req a)), ?_, fun A hA => ?_⟩ - · simp only [OracleComp.interpret_map, OracleComp.interpret_query] - exact (IsOraclePPTOn.query_take' () hreq (limit := fun _ => 1) - (ComputableInPolyTime.const 1)).map' - (ComputableInPolyTime.id'.decide_eq' (ComputableInPolyTime.const [true])) - · convert hSpec A hA using 1 - funext a - change decide (List.take 1 (languageOracle A ((), req a)) = [true]) = decide (req a ∈ A) - rw [languageOracle_apply] - cases decide (req a ∈ A) <;> rfl + PolyTimeOracleProgram input encBool Admissible Spec := + ⟨fun a => queryBit (req a), isOraclePPTOn_queryBit hreq, fun A hA => by + simpa only [interpret_queryBit] using hSpec A hA⟩ open Classical in /-- **One request decides the oracle language.** The word is copied onto the query buffer and diff --git a/Complexity/Computability/Complexity/Classes/Oracle/QueryBit.lean b/Complexity/Computability/Complexity/Classes/Oracle/QueryBit.lean new file mode 100644 index 0000000000..701bbd70be --- /dev/null +++ b/Complexity/Computability/Complexity/Classes/Oracle/QueryBit.lean @@ -0,0 +1,72 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Complexity.Classes.Oracle +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic +import Complexity.Computability.Probabilistic.Oracle.Composition + +/-! +# One request to an oracle language + +`Cslib.Complexity.queryBit w` submits the word `w` and reads the first bit of the reply. Against +an oracle language `A` it returns `decide (w ∈ A)` and makes exactly the one request `w`; for a +polynomial-time word it is strict oracle PPT, since the word is written on the query buffer and +only one bit of the reply is read. The oracle closure rules and the bounded-query classes build +their one-request certificates from this program. + +## Main definitions + +* `Cslib.Complexity.queryBit`: one request, reading one bit of the reply. + +## Main results + +* `Cslib.Complexity.interpret_queryBit`: against `A`, the request answers membership in `A`. +* `Cslib.Complexity.queriesWith_queryBit`: the program makes exactly one request. +* `Cslib.Complexity.isOraclePPTOn_queryBit`: one request for a polynomial-time word is strict + oracle PPT. +-/ + +@[expose] public section + +namespace Cslib.Complexity + +open Probability Turing.MultiTapeTM + +variable {α : Type} + +/-- **One request**: submit the word `w` and read the first bit of the reply. -/ +def queryBit (w : List Bool) : WordQueryComp Unit Bool := + (fun reply => decide (reply = [true])) <$> (List.take 1 <$> OracleComp.query ((), w)) + +open Classical in +/-- Against an oracle language, one request answers membership of its word. -/ +theorem interpret_queryBit (A : Set (List Bool)) (w : List Bool) : + OracleComp.interpret (m := Id) (languageOracle A) (queryBit w) = decide (w ∈ A) := by + change decide (List.take 1 (languageOracle A ((), w)) = [true]) = decide (w ∈ A) + rw [languageOracle_apply] + cases decide (w ∈ A) <;> rfl + +/-- One request makes one request. -/ +@[simp] +theorem queriesWith_queryBit (answer : Unit × List Bool → List Bool) (w : List Bool) : + OracleComp.queriesWith answer (queryBit w) = [((), w)] := by + simp [queryBit] + +/-- One request for a polynomial-time word is strict oracle PPT: the word is written on the query +buffer and one bit of the reply is read. -/ +theorem isOraclePPTOn_queryBit {req : α → List Bool} {input : α ↪ List Bool} + (hreq : ComputableInPolyTime req input encBits) : + IsOraclePPTOn input encBool + (fun a => OracleComp.interpret ProbOracleComp.query (queryBit (req a))) := by + simp only [queryBit, OracleComp.interpret_map, OracleComp.interpret_query] + exact (IsOraclePPTOn.query_take' () hreq (limit := fun _ => 1) + (ComputableInPolyTime.const 1)).map' + (ComputableInPolyTime.id'.decide_eq' (ComputableInPolyTime.const [true])) + +end Cslib.Complexity From ab8bfa86a201d123a8ad4d9a05099c2a8af3026a Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:49:22 -0400 Subject: [PATCH 11/12] refactor(Classes/Sparse): move the list-oracle replay and shortMembers to general modules - The machine-level list-oracle replay (`oracleReplies_congr`, `oracleReplies_succ`, `listReplyStep`, `iterate_listReplyStep`, `computableInPolyTime_listReplyStep`) moves unchanged to the new companion `Machines/Turing/MultiTape/Probabilistic/Replay/ListOracle.lean`; `Classes/Oracle/ListOracle.lean` keeps only `exists_listOracle` and imports it. - `shortMembers` becomes `Cslib.BitString.shortMembers` in the new `Foundations/Data/BitString/ShortMembers.lean`, defined by filtering `shortWords n` by membership, with `mem_shortMembers` and `length_shortMembers`. - `Sparse/Turing.lean` gains the public census bound `exists_length_shortMembers_le` and derives `exists_length_encList_shortMembers_le` from it. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + .../Complexity/Classes/Oracle/ListOracle.lean | 150 +-------------- .../Complexity/Classes/Sparse/Turing.lean | 40 ++-- .../Probabilistic/Replay/ListOracle.lean | 180 ++++++++++++++++++ .../Data/BitString/ShortMembers.lean | 51 +++++ ComplexityTests/SparseTuring.lean | 2 +- 6 files changed, 256 insertions(+), 169 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/ListOracle.lean create mode 100644 Complexity/Foundations/Data/BitString/ShortMembers.lean diff --git a/Complexity.lean b/Complexity.lean index 1647daae11..b0c2b42bd2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2025,6 +2025,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Q public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.QueryTake public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Deterministic +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.ListOracle public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Oracle public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.ReplayInput @@ -2833,6 +2834,7 @@ public import Complexity.Foundations.Data.BitString.PartialAssignment public import Complexity.Foundations.Data.BitString.PartialAssignment.Counting public import Complexity.Foundations.Data.BitString.Prefix public import Complexity.Foundations.Data.BitString.Propagation +public import Complexity.Foundations.Data.BitString.ShortMembers public import Complexity.Foundations.Data.BitString.ShortWords public import Complexity.Foundations.Data.BitString.Sign public import Complexity.Foundations.Data.BitString.Support diff --git a/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean b/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean index acecabc80b..41cdf8890a 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean +++ b/Complexity/Computability/Complexity/Classes/Oracle/ListOracle.lean @@ -8,12 +8,11 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.Classes.Oracle -public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Oracle import Complexity.Computability.Complexity.Classes.Oracle.Deterministic import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List -import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.ListOracle /-! # Oracles given as finite lists @@ -27,23 +26,14 @@ is replaced by advice, or by a guessed list of its short members. The proof replays the coin-fixed run of a machine certifying the computation (`Cslib.Probability.IsOraclePPTOn.exists_fin_run_pure_false`) from its instruction-indexed -transcript of oracle replies (`Turing.MultiTapePTM.oracleReplies`). The transcript against the -list is built one bit at a time (`Turing.MultiTapePTM.listReplyStep`): each step replays the -transcript so far, and if the next instruction makes a query, looks its request up in the list. -The pending request of the instruction at index `i` has at most `i` symbols -(`Turing.MultiTapePTM.length_pendingRequest_replayPrefix_le`), so oracles that agree on the words -no longer than the clock give the same transcript +transcript of oracle replies, built against the list one bit at a time +(`Turing.MultiTapePTM.listReplyStep`, in +`Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/ListOracle.lean`). +Oracles that agree on the words no longer than the clock give the same transcript (`Turing.MultiTapePTM.oracleReplies_congr`). -## Main definitions - -* `Turing.MultiTapePTM.listReplyStep`: extend a transcript by the reply of a list oracle. - ## Main results -* `Turing.MultiTapePTM.oracleReplies_congr`: transcripts depend only on the replies to words no - longer than the clock. -* `Turing.MultiTapePTM.iterate_listReplyStep`: iterating the step builds the transcript. * `Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle`, `Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`: polynomial time relative to `S` is polynomial time with a list that agrees with `S` on short words. @@ -55,136 +45,6 @@ no longer than the clock give the same transcript @[expose] public section -namespace Turing.MultiTapePTM - -open Cslib MultiTapeMachine MultiTapeTM - -variable {k : ℕ} {Control Operation : Type} [DecidableEq Operation] - (machine : MultiTapePTM k Bool Control Operation) - -/-- **Transcripts depend only on short replies.** Oracles that agree on every word of length less -than the clock give the same transcript: the request pending before instruction `i` has at most -`i` symbols. -/ -theorem oracleReplies_congr {g g' : List Bool → Bool} {fuel : ℕ} (input : List Bool) - (h : ∀ w : List Bool, w.length < fuel → g w = g' w) : - machine.oracleReplies g fuel input = machine.oracleReplies g' fuel input := by - set t := machine.oracleReplies g fuel input - set t' := machine.oracleReplies g' fuel input - have hlen : t.length = fuel := machine.length_oracleReplies g fuel input - have hlen' : t'.length = fuel := machine.length_oracleReplies g' fuel input - have htake : ∀ i ≤ fuel, t.take i = t'.take i := by - intro i hi - induction i with - | zero => rfl - | succ i ih => - have hlt : i < fuel := hi - have ih := ih hlt.le - have hcfg : machine.replayPrefix input t i = machine.replayPrefix input t' i := by - simp only [replayPrefix, ih] - have hreq : (machine.pendingRequest (machine.replayPrefix input t i)).length < fuel := - lt_of_le_of_lt ((machine.length_pendingRequest_replayPrefix_le input t i).trans - (Nat.min_le_left _ _)) hlt - have hbit : t[i]'(by omega) = t'[i]'(by omega) := by - rw [← List.getD_eq_getElem t false, ← List.getD_eq_getElem t' false, - machine.getD_oracleReplies g fuel input i hlt, - machine.getD_oracleReplies g' fuel input i hlt] - dsimp only - rw [← hcfg, h _ hreq] - rw [List.take_succ_eq_append_getElem (by omega), List.take_succ_eq_append_getElem (by omega), - ih, hbit] - simpa only [List.take_of_length_le hlen.le, List.take_of_length_le hlen'.le] using - htake fuel le_rfl - -/-- Extend the transcript `answers` by one bit: replay it, and if the next instruction makes a -query, reply whether its request is in the list `ℓ`; otherwise pad with `false`. -/ -def listReplyStep (p : List Bool × List (List Bool)) (answers : List Bool) : List Bool := - let cfg := machine.replayConfig p.1 answers - answers ++ [if (machine.pendingQuery cfg).isSome then decide (machine.pendingRequest cfg ∈ p.2) - else false] - -/-- A canonical transcript one instruction longer extends the shorter one by the reply at its -last instruction. -/ -theorem oracleReplies_succ (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : - machine.oracleReplies g (fuel + 1) input = machine.oracleReplies g fuel input ++ - [let cfg := machine.replayConfig input (machine.oracleReplies g fuel input) - if (machine.pendingQuery cfg).isSome then g (machine.pendingRequest cfg) else false] := by - have hlen := machine.length_oracleReplies g (fuel + 1) input - have htake : (machine.oracleReplies g (fuel + 1) input).take fuel = - machine.oracleReplies g fuel input := by - unfold oracleReplies - rw [take_oracleRepliesFrom, Nat.min_eq_left (Nat.le_succ fuel)] - have hbit := machine.getD_oracleReplies g (fuel + 1) input fuel (Nat.lt_succ_self fuel) - rw [List.getD_eq_getElem _ _ (by omega)] at hbit - have hcfg : machine.replayPrefix input (machine.oracleReplies g (fuel + 1) input) fuel = - machine.replayConfig input (machine.oracleReplies g fuel input) := by - rw [replayPrefix, htake] - rw [hcfg] at hbit - calc machine.oracleReplies g (fuel + 1) input - = (machine.oracleReplies g (fuel + 1) input).take fuel ++ - [(machine.oracleReplies g (fuel + 1) input)[fuel]'(by omega)] := by - rw [← List.take_succ_eq_append_getElem (by omega), List.take_of_length_le (by omega)] - _ = _ := by rw [htake, hbit] - -/-- **Iterating the step builds the transcript** of the list oracle. -/ -theorem iterate_listReplyStep (input : List Bool) (ℓ : List (List Bool)) (fuel : ℕ) : - (machine.listReplyStep (input, ℓ))^[fuel] [] = - machine.oracleReplies (fun w => decide (w ∈ ℓ)) fuel input := by - induction fuel with - | zero => rfl - | succ fuel ih => - rw [Function.iterate_succ_apply', ih, oracleReplies_succ] - rfl - -section PolyTime - -variable [Finite Control] [Finite Operation] - -/-- The step is polynomial-time, jointly in the input, the list and the transcript. -/ -theorem computableInPolyTime_listReplyStep : - ComputableInPolyTime (fun x : (List Bool × List (List Bool)) × List Bool => - machine.listReplyStep x.1 x.2) (encPair (encPair encBits (encList encBits)) encBits) - encBits := by - let _ := Fintype.ofFinite Operation - have hpair : ComputableInPolyTime - (fun x : (List Bool × List (List Bool)) × List Bool => (x.1.1, x.2)) - (encPair (encPair encBits (encList encBits)) encBits) (encPair encBits encBits) := - (ComputableInPolyTime.fst _ _).fst'.prod (.snd _ _) - have hcfg : ComputableInPolyTime - (fun x : (List Bool × List (List Bool)) × List Bool => machine.replayConfig x.1.1 x.2) - (encPair (encPair encBits (encList encBits)) encBits) encFiniteConfig := - machine.replayConfig_pt.comp - (g := fun x : (List Bool × List (List Bool)) × List Bool => (x.1.1, x.2)) hpair - have hquery : ComputableInPolyTime - (fun x : (List Bool × List (List Bool)) × List Bool => - (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome) - (encPair (encPair encBits (encList encBits)) encBits) encBool := - (ComputableInPolyTime.of_finite Option.isSome).comp - (machine.pendingQuery_pt.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => - machine.replayConfig x.1.1 x.2) hcfg) - have hmem : ComputableInPolyTime - (fun x : (List Bool × List (List Bool)) × List Bool => - decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2)) - (encPair (encPair encBits (encList encBits)) encBits) encBool := - ComputableInPolyTime.decide_mem (ComputableInPolyTime.fst _ _).snd' - (machine.pendingRequest_pt.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => - machine.replayConfig x.1.1 x.2) hcfg) - have hbit : ComputableInPolyTime - (fun x : (List Bool × List (List Bool)) × List Bool => - if (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome then - decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2) else false) - (encPair (encPair encBits (encList encBits)) encBits) encBool := - ComputableInPolyTime.ite' hquery hmem (ComputableInPolyTime.const false) - have hsingle : ComputableInPolyTime (fun b : Bool => [b]) encBool encBits := - .of_eq fun _ => rfl - exact ComputableInPolyTime.bitsAppend (ComputableInPolyTime.snd _ _) - (hsingle.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => - if (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome then - decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2) else false) hbit) - -end PolyTime - -end Turing.MultiTapePTM - namespace Cslib.Complexity open Probability Turing.MultiTapeTM diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean b/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean index bf3ee4a31a..619858b321 100644 --- a/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean +++ b/Complexity/Computability/Complexity/Classes/Sparse/Turing.lean @@ -12,7 +12,7 @@ public import Complexity.Computability.Complexity.Classes.Oracle public import Complexity.Computability.Complexity.Classes.PH public import Complexity.Computability.Complexity.Classes.Sparse public import Complexity.Computability.Complexity.Problems.SAT -public import Mathlib.Data.Set.Finite.List +public import Complexity.Foundations.Data.BitString.ShortMembers import Complexity.Computability.Circuit.Boolean.Advice import Complexity.Computability.Circuit.Boolean.PolynomialTime import Complexity.Computability.Complexity.Classes.Oracle.ListOracle @@ -25,7 +25,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length Polynomial time relative to a sparse oracle language `S` is in `P/poly` (`Cslib.Complexity.PWithOracle_subset_PPolyOn`): on inputs of length `n` the oracle is asked only words of length at most `q n` for a polynomial `q`, and the list of the members of `S` of length -at most `q n` (`Cslib.Complexity.shortMembers`) has polynomial length because `S` is sparse. That +at most `q n` (`Cslib.BitString.shortMembers`) has polynomial length because `S` is sparse. That list is the advice; a finite list replaces the oracle in polynomial time (`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`), and hardwiring the advice (`Cslib.Circuits.Boolean.PPoly.of_advice`) gives circuits of polynomial size. This is one @@ -40,15 +40,11 @@ polynomial-time Turing-hard set, then `PH = NP^NP` [Hemaspaandra and Ogihara, Theorem 1.16][HemaspaandraOgihara2002] [Karp and Lipton][KarpLipton1980]. The sparse set need not lie in `NP`. -## Main definitions - -* `Cslib.Complexity.shortMembers`: a list of the members of a language of length at most `n`. - ## Main results -* `Cslib.Complexity.mem_shortMembers`: its members. -* `Cslib.Complexity.exists_length_encList_shortMembers_le`: for a sparse language, the encoded list - has polynomial length. +* `Cslib.Complexity.exists_length_shortMembers_le`, + `Cslib.Complexity.exists_length_encList_shortMembers_le`: for a sparse language, the list of short + members and its encoding have polynomial length. * `Cslib.Complexity.PWithOracle_subset_PPolyOn`: `P^S ⊆ P/poly` for sparse `S`. * `Cslib.Complexity.PH_eq_SigmaP_two_of_SAT_mem_PWithOracle`: a sparse Turing-hard set for `NP` collapses `PH` to `Σ₂`. @@ -64,29 +60,27 @@ The sparse set need not lie in `NP`. namespace Cslib.Complexity -open Circuits Circuits.Boolean Turing.MultiTapeTM Cslib.Logic.PL +open Circuits Circuits.Boolean Turing.MultiTapeTM Cslib.Logic.PL BitString variable {α : Type} {S : Set (List Bool)} -/-- The members of `S` of length at most `n`, listed in some order without repetition. -/ -noncomputable def shortMembers (S : Set (List Bool)) (n : ℕ) : List (List Bool) := - ((List.finite_length_le Bool n).subset - (fun _ hw => hw.2 : {w | w ∈ S ∧ w.length ≤ n} ⊆ {w | w.length ≤ n})).toFinset.toList - -@[simp] -theorem mem_shortMembers {n : ℕ} {w : List Bool} : w ∈ shortMembers S n ↔ w ∈ S ∧ w.length ≤ n := by - simp [shortMembers] +/-- **The census of a sparse language is polynomially bounded**: it has at most `c (n + 1) ^ d` +members of length at most `n`. -/ +theorem exists_length_shortMembers_le (hS : S ∈ SPARSE encBits) : + ∃ c d : ℕ, ∀ n, (shortMembers S n).length ≤ c * (n + 1) ^ d := by + classical + obtain ⟨c, d, hcard⟩ := exists_card_le_of_mem_SPARSE hS + refine ⟨c, d, fun n => ?_⟩ + rw [length_shortMembers] + exact hcard n _ fun w hw => by simpa [and_comm] using hw /-- **Short members of a sparse language have a short listing**: the encoded list of the members of length at most `n` has length at most `c (n + 1) ^ d`. -/ theorem exists_length_encList_shortMembers_le (hS : S ∈ SPARSE encBits) : ∃ c d : ℕ, ∀ n, (encList encBits (shortMembers S n)).length ≤ c * (n + 1) ^ d := by - obtain ⟨c, d, hcard⟩ := exists_card_le_of_mem_SPARSE hS + obtain ⟨c, d, hcensus⟩ := exists_length_shortMembers_le hS refine ⟨2 * c, d + 1, fun n => ?_⟩ - have hlen : (shortMembers S n).length ≤ c * (n + 1) ^ d := by - unfold shortMembers - rw [Finset.length_toList] - exact hcard n _ fun w hw => by simpa using hw + have hlen := hcensus n have hsum : ((shortMembers S n).map fun w => 2 * (encBits w).length + 1).sum ≤ (shortMembers S n).length * (2 * n + 1) := by have h := List.sum_le_length_nsmul ((shortMembers S n).map fun w => 2 * (encBits w).length + 1) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/ListOracle.lean b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/ListOracle.lean new file mode 100644 index 0000000000..bda8ed12dc --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/Replay/ListOracle.lean @@ -0,0 +1,180 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Oracle +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership + +/-! +# Replaying a list oracle + +The instruction-indexed transcript of oracle replies (`Turing.MultiTapePTM.oracleReplies`) of a +coin-fixed run depends only on the replies to words shorter than the clock: the pending request of +the instruction at index `i` has at most `i` symbols +(`Turing.MultiTapePTM.length_pendingRequest_replayPrefix_le`), so oracles that agree on those words +give the same transcript (`Turing.MultiTapePTM.oracleReplies_congr`). + +The transcript against a finite list of words is built one bit at a time +(`Turing.MultiTapePTM.listReplyStep`): each step replays the transcript so far, and if the next +instruction makes a query, looks its request up in the list. The step is polynomial-time jointly +in the input, the list and the transcript +(`Turing.MultiTapePTM.computableInPolyTime_listReplyStep`), so a finite list that agrees with an +oracle language on short words can replace it +(`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle`). + +## Main definitions + +* `Turing.MultiTapePTM.listReplyStep`: extend a transcript by the reply of a list oracle. + +## Main results + +* `Turing.MultiTapePTM.oracleReplies_congr`: transcripts depend only on the replies to words + shorter than the clock. +* `Turing.MultiTapePTM.oracleReplies_succ`: a transcript one instruction longer extends the + shorter one by the reply at its last instruction. +* `Turing.MultiTapePTM.iterate_listReplyStep`: iterating the step builds the transcript of the + list oracle. +* `Turing.MultiTapePTM.computableInPolyTime_listReplyStep`: the step is polynomial-time. + +## References + +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09], Section 3.4. +-/ + +@[expose] public section + +namespace Turing.MultiTapePTM + +open Cslib MultiTapeMachine MultiTapeTM + +variable {k : ℕ} {Control Operation : Type} [DecidableEq Operation] + (machine : MultiTapePTM k Bool Control Operation) + +/-- **Transcripts depend only on short replies.** Oracles that agree on every word of length less +than the clock give the same transcript: the request pending before instruction `i` has at most +`i` symbols. -/ +theorem oracleReplies_congr {g g' : List Bool → Bool} {fuel : ℕ} (input : List Bool) + (h : ∀ w : List Bool, w.length < fuel → g w = g' w) : + machine.oracleReplies g fuel input = machine.oracleReplies g' fuel input := by + set t := machine.oracleReplies g fuel input + set t' := machine.oracleReplies g' fuel input + have hlen : t.length = fuel := machine.length_oracleReplies g fuel input + have hlen' : t'.length = fuel := machine.length_oracleReplies g' fuel input + have htake : ∀ i ≤ fuel, t.take i = t'.take i := by + intro i hi + induction i with + | zero => rfl + | succ i ih => + have hlt : i < fuel := hi + have ih := ih hlt.le + have hcfg : machine.replayPrefix input t i = machine.replayPrefix input t' i := by + simp only [replayPrefix, ih] + have hreq : (machine.pendingRequest (machine.replayPrefix input t i)).length < fuel := + lt_of_le_of_lt ((machine.length_pendingRequest_replayPrefix_le input t i).trans + (Nat.min_le_left _ _)) hlt + have hbit : t[i]'(by omega) = t'[i]'(by omega) := by + rw [← List.getD_eq_getElem t false, ← List.getD_eq_getElem t' false, + machine.getD_oracleReplies g fuel input i hlt, + machine.getD_oracleReplies g' fuel input i hlt] + dsimp only + rw [← hcfg, h _ hreq] + rw [List.take_succ_eq_append_getElem (by omega), List.take_succ_eq_append_getElem (by omega), + ih, hbit] + simpa only [List.take_of_length_le hlen.le, List.take_of_length_le hlen'.le] using + htake fuel le_rfl + +/-- Extend the transcript `answers` by one bit: replay it, and if the next instruction makes a +query, reply whether its request is in the list `ℓ`; otherwise pad with `false`. -/ +def listReplyStep (p : List Bool × List (List Bool)) (answers : List Bool) : List Bool := + let cfg := machine.replayConfig p.1 answers + answers ++ [if (machine.pendingQuery cfg).isSome then decide (machine.pendingRequest cfg ∈ p.2) + else false] + +/-- A canonical transcript one instruction longer extends the shorter one by the reply at its +last instruction. -/ +theorem oracleReplies_succ (g : List Bool → Bool) (fuel : ℕ) (input : List Bool) : + machine.oracleReplies g (fuel + 1) input = machine.oracleReplies g fuel input ++ + [let cfg := machine.replayConfig input (machine.oracleReplies g fuel input) + if (machine.pendingQuery cfg).isSome then g (machine.pendingRequest cfg) else false] := by + have hlen := machine.length_oracleReplies g (fuel + 1) input + have htake : (machine.oracleReplies g (fuel + 1) input).take fuel = + machine.oracleReplies g fuel input := by + unfold oracleReplies + rw [take_oracleRepliesFrom, Nat.min_eq_left (Nat.le_succ fuel)] + have hbit := machine.getD_oracleReplies g (fuel + 1) input fuel (Nat.lt_succ_self fuel) + rw [List.getD_eq_getElem _ _ (by omega)] at hbit + have hcfg : machine.replayPrefix input (machine.oracleReplies g (fuel + 1) input) fuel = + machine.replayConfig input (machine.oracleReplies g fuel input) := by + rw [replayPrefix, htake] + rw [hcfg] at hbit + calc machine.oracleReplies g (fuel + 1) input + = (machine.oracleReplies g (fuel + 1) input).take fuel ++ + [(machine.oracleReplies g (fuel + 1) input)[fuel]'(by omega)] := by + rw [← List.take_succ_eq_append_getElem (by omega), List.take_of_length_le (by omega)] + _ = _ := by rw [htake, hbit] + +/-- **Iterating the step builds the transcript** of the list oracle. -/ +theorem iterate_listReplyStep (input : List Bool) (ℓ : List (List Bool)) (fuel : ℕ) : + (machine.listReplyStep (input, ℓ))^[fuel] [] = + machine.oracleReplies (fun w => decide (w ∈ ℓ)) fuel input := by + induction fuel with + | zero => rfl + | succ fuel ih => + rw [Function.iterate_succ_apply', ih, oracleReplies_succ] + rfl + +section PolyTime + +variable [Finite Control] [Finite Operation] + +/-- The step is polynomial-time, jointly in the input, the list and the transcript. -/ +theorem computableInPolyTime_listReplyStep : + ComputableInPolyTime (fun x : (List Bool × List (List Bool)) × List Bool => + machine.listReplyStep x.1 x.2) (encPair (encPair encBits (encList encBits)) encBits) + encBits := by + let _ := Fintype.ofFinite Operation + have hpair : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => (x.1.1, x.2)) + (encPair (encPair encBits (encList encBits)) encBits) (encPair encBits encBits) := + (ComputableInPolyTime.fst _ _).fst'.prod (.snd _ _) + have hcfg : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => machine.replayConfig x.1.1 x.2) + (encPair (encPair encBits (encList encBits)) encBits) encFiniteConfig := + machine.replayConfig_pt.comp + (g := fun x : (List Bool × List (List Bool)) × List Bool => (x.1.1, x.2)) hpair + have hquery : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => + (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome) + (encPair (encPair encBits (encList encBits)) encBits) encBool := + (ComputableInPolyTime.of_finite Option.isSome).comp + (machine.pendingQuery_pt.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => + machine.replayConfig x.1.1 x.2) hcfg) + have hmem : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => + decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2)) + (encPair (encPair encBits (encList encBits)) encBits) encBool := + ComputableInPolyTime.decide_mem (ComputableInPolyTime.fst _ _).snd' + (machine.pendingRequest_pt.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => + machine.replayConfig x.1.1 x.2) hcfg) + have hbit : ComputableInPolyTime + (fun x : (List Bool × List (List Bool)) × List Bool => + if (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome then + decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2) else false) + (encPair (encPair encBits (encList encBits)) encBits) encBool := + ComputableInPolyTime.ite' hquery hmem (ComputableInPolyTime.const false) + have hsingle : ComputableInPolyTime (fun b : Bool => [b]) encBool encBits := + .of_eq fun _ => rfl + exact ComputableInPolyTime.bitsAppend (ComputableInPolyTime.snd _ _) + (hsingle.comp (g := fun x : (List Bool × List (List Bool)) × List Bool => + if (machine.pendingQuery (machine.replayConfig x.1.1 x.2)).isSome then + decide (machine.pendingRequest (machine.replayConfig x.1.1 x.2) ∈ x.1.2) else false) hbit) + +end PolyTime + +end Turing.MultiTapePTM diff --git a/Complexity/Foundations/Data/BitString/ShortMembers.lean b/Complexity/Foundations/Data/BitString/ShortMembers.lean new file mode 100644 index 0000000000..38130b36c8 --- /dev/null +++ b/Complexity/Foundations/Data/BitString/ShortMembers.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.BitString.ShortWords + +/-! +# Short members of a language + +`Cslib.BitString.shortMembers S n` lists, without repetition, the members of a language +`S : Set (List Bool)` of length at most `n`: the binary words of length at most `n` +(`Cslib.BitString.shortWords`) that lie in `S`. + +## Main definitions + +* `Cslib.BitString.shortMembers`: the members of a language of length at most `n`. + +## Main results + +* `Cslib.BitString.mem_shortMembers`: its members. +* `Cslib.BitString.length_shortMembers`: its length is the number of short members. +-/ + +@[expose] public section + +namespace Cslib.BitString + +open Classical in +/-- The members of `S` of length at most `n`, listed in some order without repetition. -/ +noncomputable def shortMembers (S : Set (List Bool)) (n : ℕ) : List (List Bool) := + ((shortWords n).filter (· ∈ S)).toList + +variable {S : Set (List Bool)} {n : ℕ} + +/-- A word is listed exactly when it is a member of `S` of length at most `n`. -/ +@[simp] +theorem mem_shortMembers {w : List Bool} : w ∈ shortMembers S n ↔ w ∈ S ∧ w.length ≤ n := by + simp [shortMembers, and_comm] + +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] + +end Cslib.BitString diff --git a/ComplexityTests/SparseTuring.lean b/ComplexityTests/SparseTuring.lean index 43c1822e8c..14018de750 100644 --- a/ComplexityTests/SparseTuring.lean +++ b/ComplexityTests/SparseTuring.lean @@ -11,7 +11,7 @@ import Complexity.Computability.Complexity.Classes.Sparse.Turing namespace ComplexityTests.SparseTuring -open Cslib Cslib.Complexity Cslib.Circuits.Boolean Cslib.Logic.PL Turing.MultiTapeTM +open Cslib Cslib.BitString Cslib.Complexity Cslib.Circuits.Boolean Cslib.Logic.PL Turing.MultiTapeTM /-- The words consisting only of `true`s, a sparse language. -/ private def unary : Set (List Bool) := {w | ∀ b ∈ w, b = true} From 0f2f9bca2c6d531c0b4bc1d7e56dff870cff4fcc Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sat, 31 Oct 2026 12:56:25 -0400 Subject: [PATCH 12/12] refactor(Classes/Sparse): name Kadin's request components and reuse general APIs - `KadinCensus.Guess`, `check` and `check_eq_true_iff` bind the request as `(a, k, finalQuery)` and the checked input as `((a, k, finalQuery), (pairs, witness))` instead of projection chains. - The census list facts (`nodup_shortMembers`, `length_le_length_shortMembers`, `mem_iff_of_length_eq_length_shortMembers`) move to `Foundations/Data/BitString/ShortMembers`. - The duplicate-freeness scan becomes `List.not_any_one_lt_countP_iff_nodup` in `Foundations/Data/List/Counting`, for every type with decidable equality. - The loop request bound becomes `OracleComp.length_queriesWith_iterate_le` in `Classes/Oracle/BoundedQuery`, generalized to `r` requests per round. - `exists_clog_le_of_polynomiallyBounded` is replaced by the existing `PolynomiallyBounded.exists_clog_le_mul_log`, and the census bound by the public `exists_length_shortMembers_le` of `Sparse/Turing`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Classes/Oracle/BoundedQuery.lean | 23 +- .../Complexity/Classes/Sparse/Kadin.lean | 220 +++++++----------- .../Data/BitString/ShortMembers.lean | 32 +++ .../Foundations/Data/List/Counting.lean | 17 ++ ComplexityTests/SparseKadin.lean | 2 +- 5 files changed, 150 insertions(+), 144 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean b/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean index 9a3df0e025..6f8268f125 100644 --- a/Complexity/Computability/Complexity/Classes/Oracle/BoundedQuery.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean index 8123e7d1e6..9102ebc8f4 100644 --- a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean @@ -27,6 +27,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.Simulation import Complexity.Computability.Probabilistic.Oracle.Composition +import Complexity.Foundations.Data.List.Counting +import Complexity.Foundations.Data.Nat.PolynomialBound.Log import Cslib.Foundations.Data.Polynomial.Monotone /-! @@ -44,7 +46,7 @@ length at most `m`; it is polynomial in `m` because `S` is sparse. * With `S ∈ NP`, "the census is at least `k`" is a problem in `NP`: guess `k` distinct members, each with its certificate. Binary search finds the exact census with `O(log n)` such requests. * Given the exact census `k`, a list of `k` distinct short members of `S` lists them all - (`Cslib.Complexity.mem_iff_of_length_eq_length_shortMembers`), so it can replace the oracle `S` + (`Cslib.BitString.mem_iff_of_length_eq_length_shortMembers`), so it can replace the oracle `S` (`Cslib.Complexity.ComputableInPolyTimeWithOracle.exists_listOracle_bool`). Hence one more request in `NP`, which guesses the list and a first certificate, decides a problem in `Σ₂`. @@ -68,17 +70,14 @@ in `[0, N]`. ## Main definitions * `Cslib.Complexity.KadinCensus.language`: the `NP` problem asked by the algorithm, on triples - `(a, k, b)`: `k` distinct short members of `S` exist, and if `b`, they also witness the first - quantifier of a `Σ₂` problem. + `(a, k, finalQuery)`: `k` distinct short members of `S` exist, and if `finalQuery`, they also + witness the first quantifier of a `Σ₂` problem. * `Cslib.Complexity.KadinCensus.searchStep`: one round of binary search for a threshold. * `Cslib.Complexity.KadinCensus.searchStepProgram`, `Cslib.Complexity.KadinCensus.program`: the oracle programs. ## Main results -* `Cslib.Complexity.length_le_length_shortMembers`, - `Cslib.Complexity.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. * `Cslib.Complexity.KadinCensus.mem_language_false_iff`, `Cslib.Complexity.KadinCensus.mem_language_census_true_iff`: the meaning of the requests. * `Cslib.Complexity.KadinCensus.language_mem_NP`: the requests form a problem in `NP`. @@ -99,49 +98,10 @@ in `[0, N]`. namespace Cslib.Complexity -open Turing.MultiTapeTM +open Turing.MultiTapeTM BitString variable {α : Type} {S : Set (List Bool)} -/-! ### The census -/ - -theorem nodup_shortMembers (S : Set (List Bool)) (n : ℕ) : (shortMembers S n).Nodup := - Finset.nodup_toList _ - -/-- **The census bounds the lists of distinct short members.** -/ -theorem length_le_length_shortMembers {ℓ : List (List Bool)} {n : ℕ} (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)} {n : ℕ} (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 - -/-- The census of a sparse language is polynomially bounded. -/ -theorem exists_length_shortMembers_le (hS : S ∈ SPARSE encBits) : - ∃ c d : ℕ, ∀ n, (shortMembers S n).length ≤ c * (n + 1) ^ d := by - obtain ⟨c, d, hcard⟩ := exists_card_le_of_mem_SPARSE hS - refine ⟨c, d, fun n => ?_⟩ - unfold shortMembers - rw [Finset.length_toList] - exact hcard n _ fun w hw => by simpa using hw - /-! ### The requests -/ namespace KadinCensus @@ -149,11 +109,14 @@ namespace KadinCensus variable (S) (enc : α ↪ List Bool) (m p : Polynomial ℕ) (G : (α × List Bool) × List (List Bool) → Bool) -/-- A guess for the request `(a, k, b)`: `ℓ` lists `k` distinct members of `S` of length at most -`m |enc a|`, and if `b`, some word `w` of length `p |enc a|` has `G ((a, w), ℓ) = false`. -/ -def Guess (x : α × ℕ × Bool) (ℓ : List (List Bool)) : Prop := - ℓ.Nodup ∧ ℓ.length = x.2.1 ∧ (∀ s ∈ ℓ, s ∈ S ∧ s.length ≤ m.eval (enc x.1).length) ∧ - (x.2.2 = true → ∃ w : List Bool, w.length = p.eval (enc x.1).length ∧ G ((x.1, w), ℓ) = false) +/-- A guess for the request `(a, k, finalQuery)`: `ℓ` lists `k` distinct members of `S` of length +at most `m |enc a|`, and if `finalQuery`, some word `w` of length `p |enc a|` has +`G ((a, w), ℓ) = false`. -/ +def Guess : α × ℕ × Bool → List (List Bool) → Prop + | (a, k, finalQuery), ℓ => + ℓ.Nodup ∧ ℓ.length = k ∧ (∀ s ∈ ℓ, s ∈ S ∧ s.length ≤ m.eval (enc a).length) ∧ + (finalQuery = true → + ∃ w : List Bool, w.length = p.eval (enc a).length ∧ G ((a, w), ℓ) = false) /-- The requests that have a guess. -/ def language : Set (α × ℕ × Bool) := {x | ∃ ℓ, Guess S enc m p G x ℓ} @@ -163,7 +126,7 @@ noncomputable def census (a : α) : ℕ := (shortMembers S (m.eval (enc a).lengt variable {S enc m p G} -/-- **A request with `b = false` asks whether the census is at least `k`.** -/ +/-- **A request with `finalQuery = false` asks whether the census is at least `k`.** -/ theorem mem_language_false_iff {a : α} {k : ℕ} : (a, k, false) ∈ language S enc m p G ↔ k ≤ census S enc m a := by constructor @@ -178,9 +141,10 @@ theorem mem_language_false_iff {a : α} {k : ℕ} : fun h => absurd h Bool.false_ne_true⟩ exact mem_shortMembers.mp (List.mem_of_mem_take hs) -/-- **At the exact census, a request with `b = true` asks for the first quantifier.** If `G` -computes `g` whenever its list agrees with `S` on the words of length at most `m |enc a|`, the -request `(a, census, true)` asks whether some `w` of length `p |enc a|` has `g (a, w) = false`. -/ +/-- **At the exact census, a request with `finalQuery = true` asks for the first quantifier.** +If `G` computes `g` whenever its list agrees with `S` on the words of length at most `m |enc a|`, +the request `(a, census, true)` asks whether some `w` of length `p |enc a|` has +`g (a, w) = false`. -/ theorem mem_language_census_true_iff {a : α} {g : α × List Bool → Bool} (hG : ∀ w ℓ, w.length = p.eval (enc a).length → (∀ s : List Bool, s.length ≤ m.eval (enc a).length → (s ∈ ℓ ↔ s ∈ S)) → @@ -200,59 +164,43 @@ theorem mem_language_census_true_iff {a : α} {g : α × List Bool → Bool} /-! ### The requests are in `NP` -/ -/-- A duplicate-free list is one in which no entry occurs twice, tested by counting. -/ -theorem not_any_one_lt_countP_iff_nodup (l : List (List Bool)) : - (!(l.any fun s => decide (1 < l.countP fun t => decide (t = s)))) = true ↔ l.Nodup := by - have hc (s : List Bool) : (l.countP fun t => decide (t = s)) = l.count s := by - rw [List.count_eq_countP] - congr 1 - funext t - rw [Bool.eq_iff_iff] - simp - simp only [Bool.not_eq_true', List.any_eq_false, decide_eq_true_eq, 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 - variable (enc m p G) in -/-- The check of a witness `(pairs, w)` for the request `(a, k, b)`: the first components of -`pairs` are `k` distinct words of length at most `m |enc a|`, each with an accepted certificate of -the verifier `VS` of `S`, and if `b`, `w` has length `p |enc a|` and `G ((a, w), ℓ) = false`. -/ -def check (VS : List Bool × List Bool → Bool) (pS : Polynomial ℕ) - (z : (α × ℕ × Bool) × (List (List Bool × List Bool) × List Bool)) : Bool := - !((z.2.1.map Prod.fst).any fun s => - decide (1 < (z.2.1.map Prod.fst).countP fun t => decide (t = s))) && - decide ((z.2.1.map Prod.fst).length = z.1.2.1) && - !(z.2.1.any fun sc => !(decide (sc.1.length ≤ m.eval (enc z.1.1).length) && - decide (sc.2.length = pS.eval sc.1.length) && VS sc)) && - (!z.1.2.2 || (decide (z.2.2.length = p.eval (enc z.1.1).length) && - !G ((z.1.1, z.2.2), z.2.1.map Prod.fst))) - -theorem check_eq_true_iff {VS : List Bool × List Bool → Bool} {pS : Polynomial ℕ} - {x : α × ℕ × Bool} {y : List (List Bool × List Bool) × List Bool} : - check enc m p G VS pS (x, y) = true ↔ - (y.1.map Prod.fst).Nodup ∧ (y.1.map Prod.fst).length = x.2.1 ∧ - (∀ sc ∈ y.1, sc.1.length ≤ m.eval (enc x.1).length ∧ +/-- The check of a witness `(pairs, witness)` for the request `(a, k, finalQuery)`: the first +components of `pairs` are `k` distinct words of length at most `m |enc a|`, each with an accepted +certificate of the verifier `VS` of `S`, and if `finalQuery`, `witness` has length `p |enc a|` and +`G ((a, witness), ℓ) = false` for the list `ℓ` of the guessed words. -/ +def check (VS : List Bool × List Bool → Bool) (pS : Polynomial ℕ) : + (α × ℕ × Bool) × (List (List Bool × List Bool) × List Bool) → Bool + | ((a, k, finalQuery), (pairs, witness)) => + !((pairs.map Prod.fst).any fun s => + decide (1 < (pairs.map Prod.fst).countP fun t => decide (t = s))) && + decide ((pairs.map Prod.fst).length = k) && + !(pairs.any fun sc => !(decide (sc.1.length ≤ m.eval (enc a).length) && + decide (sc.2.length = pS.eval sc.1.length) && VS sc)) && + (!finalQuery || (decide (witness.length = p.eval (enc a).length) && + !G ((a, witness), pairs.map Prod.fst))) + +theorem check_eq_true_iff {VS : List Bool × List Bool → Bool} {pS : Polynomial ℕ} {a : α} + {k : ℕ} {finalQuery : Bool} {pairs : List (List Bool × List Bool)} {witness : List Bool} : + check enc m p G VS pS ((a, k, finalQuery), (pairs, witness)) = true ↔ + (pairs.map Prod.fst).Nodup ∧ (pairs.map Prod.fst).length = k ∧ + (∀ sc ∈ pairs, sc.1.length ≤ m.eval (enc a).length ∧ sc.2.length = pS.eval sc.1.length ∧ VS sc = true) ∧ - (x.2.2 = true → y.2.length = p.eval (enc x.1).length ∧ - G ((x.1, y.2), y.1.map Prod.fst) = false) := by - unfold check - rw [Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true, not_any_one_lt_countP_iff_nodup, - and_assoc, and_assoc] + (finalQuery = true → witness.length = p.eval (enc a).length ∧ + G ((a, witness), pairs.map Prod.fst) = false) := by + rw [check, Bool.and_eq_true, Bool.and_eq_true, Bool.and_eq_true, + List.not_any_one_lt_countP_iff_nodup, and_assoc, and_assoc] refine and_congr Iff.rfl (and_congr decide_eq_true_iff (and_congr ?_ ?_)) · simp [List.any_eq_false, and_assoc] - · cases x.2.2 <;> simp + · cases finalQuery <;> simp /-- The witnesses: the certificates of `S` are read by its verifier `VS`. -/ theorem language_eq_setOf_check {VS : List Bool × List Bool → Bool} {pS : Polynomial ℕ} (hSV : IsVerifier encBits pS VS S) : language S enc m p G = {x | ∃ y, check enc m p G VS pS (x, y) = true} := by classical - ext x - simp only [Set.mem_ofPred_eq, check_eq_true_iff] + ext ⟨a, k, finalQuery⟩ + simp only [Set.mem_ofPred_eq] constructor · rintro ⟨ℓ, hnd, hlen, hmem, hw⟩ have hcert (s : List Bool) (hs : s ∈ S) : @@ -262,15 +210,16 @@ theorem language_eq_setOf_check {VS : List Bool × List Bool → Bool} {pS : Pol rw [List.map_map] exact List.map_id' ℓ refine ⟨(ℓ.map fun s => (s, cert s), - if h : x.2.2 = true then (hw h).choose else []), by rw [hmap]; exact hnd, - by rw [hmap]; exact hlen, fun sc hsc => ?_, fun h => ?_⟩ + if h : finalQuery = true then (hw h).choose else []), check_eq_true_iff.mpr + ⟨by rw [hmap]; exact hnd, by rw [hmap]; exact hlen, fun sc hsc => ?_, fun h => ?_⟩⟩ · obtain ⟨s, hs, rfl⟩ := List.mem_map.mp hsc have hsS := (hmem s hs).1 simp only [cert, hsS, ↓reduceDIte] exact ⟨(hmem s hs).2, (hcert s hsS).choose_spec.1, (hcert s hsS).choose_spec.2⟩ · simp only [h, ↓reduceDIte, hmap] exact (hw h).choose_spec - · rintro ⟨⟨pairs, w⟩, hnd, hlen, hpairs, hw⟩ + · rintro ⟨⟨pairs, w⟩, hy⟩ + obtain ⟨hnd, hlen, hpairs, hw⟩ := check_eq_true_iff.mp hy refine ⟨pairs.map Prod.fst, hnd, hlen, fun s hs => ?_, fun h => ⟨w, hw h⟩⟩ obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hs obtain ⟨hlenS, hc, hV⟩ := hpairs sc hsc @@ -283,8 +232,20 @@ theorem computableInPolyTime_check {VS : List Bool × List Bool → Bool} {pS : ComputableInPolyTime (check enc m p G VS pS) (encPair (encPair enc (encPair encUnary encBool)) (encPair (encList (encPair encBits encBits)) encBits)) encBool := by - unfold check - fun_prop + -- the same function, with its components read by projections + have h : ComputableInPolyTime + (fun z : (α × ℕ × Bool) × (List (List Bool × List Bool) × List Bool) => + !((z.2.1.map Prod.fst).any fun s => + decide (1 < (z.2.1.map Prod.fst).countP fun t => decide (t = s))) && + decide ((z.2.1.map Prod.fst).length = z.1.2.1) && + !(z.2.1.any fun sc => !(decide (sc.1.length ≤ m.eval (enc z.1.1).length) && + decide (sc.2.length = pS.eval sc.1.length) && VS sc)) && + (!z.1.2.2 || (decide (z.2.2.length = p.eval (enc z.1.1).length) && + !G ((z.1.1, z.2.2), z.2.1.map Prod.fst)))) + (encPair (encPair enc (encPair encUnary encBool)) + (encPair (encList (encPair encBits encBits)) encBits)) encBool := by + fun_prop + exact h /-- **The requests form a problem in `NP`** when `S` is a sparse problem in `NP` and `G` is polynomial-time: a witness lists the guessed members with their certificates, and the word `w`. @@ -299,40 +260,43 @@ theorem language_mem_NP (hS : S ∈ NP encBits) (hsparse : S ∈ SPARSE encBits) (p := 2 * (Polynomial.C c * (m + 1) ^ d * (4 * m + 2 * pS.comp m + 3)) + 1 + p) (Decoder.pair (Decoder.list (Decoder.pair .bits .bits)) .bits) (computableInPolyTime_check hVS hG) (fun _ _ => Iff.rfl) fun x y hy => ?_ + obtain ⟨a, k, finalQuery⟩ := x + obtain ⟨pairs, w⟩ := y obtain ⟨hnd, hlen, hpairs, hw⟩ := check_eq_true_iff.mp hy - set n := (enc x.1).length - refine ⟨(y.1, if x.2.2 = true then y.2 else []), check_eq_true_iff.mpr + set n := (enc a).length + refine ⟨(pairs, if finalQuery = true then w else []), check_eq_true_iff.mpr ⟨hnd, hlen, hpairs, fun h => by simpa only [h, ↓reduceIte] using hw h⟩, ?_⟩ -- the guessed words are distinct short members of `S`, so there are at most census many - have hcount : y.1.length ≤ c * (m.eval n + 1) ^ d := by + have hcount : pairs.length ≤ c * (m.eval n + 1) ^ d := by have hle := length_le_length_shortMembers (S := S) (n := m.eval n) hnd fun s hs => by obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hs obtain ⟨hlenS, hc, hV⟩ := hpairs sc hsc exact ⟨(hSV sc.1).2 ⟨sc.2, by rw [encBits_apply]; exact hc, hV⟩, hlenS⟩ rw [List.length_map] at hle exact hle.trans (hcensus _) - have hpair (sc : List Bool × List Bool) (hsc : sc ∈ y.1) : + have hpair (sc : List Bool × List Bool) (hsc : sc ∈ pairs) : 2 * (encPair encBits encBits sc).length + 1 ≤ 4 * m.eval n + 2 * pS.eval (m.eval n) + 3 := by obtain ⟨hlenS, hc, -⟩ := hpairs sc hsc have hpS : pS.eval sc.1.length ≤ pS.eval (m.eval n) := pS.eval_mono hlenS rw [length_encPair, encBits_apply, encBits_apply, hc] omega - have hlist : (encList (encPair encBits encBits) y.1).length ≤ + have hlist : (encList (encPair encBits encBits) pairs).length ≤ c * (m.eval n + 1) ^ d * (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) := by rw [length_encList] have h := List.sum_le_length_nsmul - (y.1.map fun sc => 2 * (encPair encBits encBits sc).length + 1) + (pairs.map fun sc => 2 * (encPair encBits encBits sc).length + 1) (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) fun z hz => by obtain ⟨sc, hsc, rfl⟩ := List.mem_map.mp hz exact hpair sc hsc rw [List.length_map, smul_eq_mul] at h exact h.trans (Nat.mul_le_mul_right _ hcount) - have hword : (if x.2.2 = true then y.2 else []).length ≤ p.eval n := by + have hword : (if finalQuery = true then w else []).length ≤ p.eval n := by split_ifs with h · exact (hw h).1.le · exact Nat.zero_le _ - have hn : n ≤ (encPair enc (encPair encUnary encBool) x).length := length_le_encPair_left _ _ _ + have hn : n ≤ (encPair enc (encPair encUnary encBool) (a, k, finalQuery)).length := + length_le_encPair_left enc (encPair encUnary encBool) (a, k, finalQuery) refine le_trans ?_ (Polynomial.eval_mono _ hn) rw [length_encPair, encBits_apply] simp only [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_pow, Polynomial.eval_C, @@ -415,17 +379,6 @@ theorem length_queriesWith_searchStepProgram_le (answer : Unit × List Bool → unfold searchStepProgram split_ifs <;> simp -/-- A loop whose rounds make at most one request each makes at most one request per round. -/ -theorem length_queriesWith_iterate_le {State : Type} (answer : Unit × List Bool → List Bool) - {step : State → WordQueryComp Unit State} - (h : ∀ st, (OracleComp.queriesWith answer (step st)).length ≤ 1) (n : ℕ) (st : State) : - (OracleComp.queriesWith answer (OracleComp.iterate n step st)).length ≤ n := by - induction n with - | zero => simp - | succ n ih => - rw [OracleComp.iterate_succ, OracleComp.queriesWith_bind, List.length_append] - exact Nat.add_le_add ih (h _) - /-- The algorithm: `count a` rounds of binary search from `(0, N a)` with the requests `req`, then one request `fin (a, lo)` at the threshold found. -/ def program (req fin : α × ℕ → List Bool) (N count : α → ℕ) (a : α) : WordQueryComp Unit Bool := @@ -448,8 +401,8 @@ theorem length_queriesWith_program_le (answer : Unit × List Bool → List Bool) (OracleComp.queriesWith answer (program req fin N count a)).length ≤ count a + 1 := by rw [program, OracleComp.queriesWith_bind, List.length_append, queriesWith_queryBit, List.length_singleton] - exact Nat.add_le_add_right (length_queriesWith_iterate_le answer - (length_queriesWith_searchStepProgram_le answer req a) _ _) 1 + exact Nat.add_le_add_right ((OracleComp.length_queriesWith_iterate_le answer + (length_queriesWith_searchStepProgram_le answer req a) _ _).trans (Nat.mul_one _).le) 1 open Probability in /-- **The algorithm is strict oracle PPT** when the requests, the bound `N` and the count are @@ -535,21 +488,6 @@ end KadinCensus /-! ### Kadin's theorem -/ -/-- A polynomially bounded quantity has a logarithmic number of bits: `⌈log₂ N n⌉ ≤ K log₂ n + K`. --/ -theorem exists_clog_le_of_polynomiallyBounded {N : ℕ → ℕ} (hN : PolynomiallyBounded N) : - ∃ K : ℕ, ∀ n, Nat.clog 2 (N n) ≤ K * Nat.log 2 n + K := by - obtain ⟨e, f, h⟩ := polynomiallyBounded_iff_le.mp hN - refine ⟨f + e, fun n => Nat.clog_le_of_le_pow ?_⟩ - have hn : n + 1 ≤ 2 ^ (Nat.log 2 n + 1) := Nat.lt_pow_succ_log_self (by norm_num) n - have he : e ≤ 2 ^ e := (Nat.lt_two_pow_self).le - calc N n ≤ e * (n + 1) ^ f := h n - _ ≤ 2 ^ e * (2 ^ (Nat.log 2 n + 1)) ^ f := - Nat.mul_le_mul he (Nat.pow_le_pow_left hn f) - _ = 2 ^ (f * Nat.log 2 n + f + e) := by rw [← pow_mul, ← pow_add]; ring_nf - _ ≤ 2 ^ ((f + e) * Nat.log 2 n + (f + e)) := - Nat.pow_le_pow_right (by norm_num) (by nlinarith [Nat.zero_le (Nat.log 2 n)]) - open Classical in /-- **`Σ₂ ⊆ P^{NP[O(log n)]}` under a sparse Turing-complete set for `NP`.** Binary search with requests to `SAT` finds the census of `S` up to the length of the oracle words, and one more @@ -589,8 +527,8 @@ theorem SigmaP_two_subset_PNPLog_of_sparse (hsparse : S ∈ SPARSE encBits) (hS have hcount : ComputableInPolyTime count enc encUnary := (ComputableInPolyTime.unary_clog_const 2).comp (ComputableInPolyTime.unary_add' hN (ComputableInPolyTime.const 1)) - obtain ⟨K, hK⟩ := exists_clog_le_of_polynomiallyBounded - (N := fun n => c * (m.eval n + 1) ^ d + 1) (by fun_prop) + obtain ⟨K, hK⟩ := PolynomiallyBounded.exists_clog_le_mul_log + (s := fun n => c * (m.eval n + 1) ^ d + 1) (by fun_prop) let prog := KadinCensus.program (fun x => encCNF (red (x.1, x.2, false))) (fun x => encCNF (red (x.1, x.2, true))) N count refine mem_PNPLog_of_mem_PWithOracleQueries (c := K + 1) image_SAT_mem_NP diff --git a/Complexity/Foundations/Data/BitString/ShortMembers.lean b/Complexity/Foundations/Data/BitString/ShortMembers.lean index 38130b36c8..76f0d40ff2 100644 --- a/Complexity/Foundations/Data/BitString/ShortMembers.lean +++ b/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 diff --git a/Complexity/Foundations/Data/List/Counting.lean b/Complexity/Foundations/Data/List/Counting.lean index 26257d1b84..62d41ada54 100644 --- a/Complexity/Foundations/Data/List/Counting.lean +++ b/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 α) : diff --git a/ComplexityTests/SparseKadin.lean b/ComplexityTests/SparseKadin.lean index 7b29ca6ff6..888a1025dd 100644 --- a/ComplexityTests/SparseKadin.lean +++ b/ComplexityTests/SparseKadin.lean @@ -10,7 +10,7 @@ import Complexity.Computability.Complexity.Classes.Sparse.Kadin namespace ComplexityTests.SparseKadin -open Cslib Cslib.Complexity Turing.MultiTapeTM +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}