From 0cd989d04013b4547c9b8d19768e359c85c6fdc9 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Fri, 24 Jul 2026 12:53:38 -0700 Subject: [PATCH 1/2] feat(Classes): define the polynomial hierarchy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Define certificate quantifiers over the pair codec (polyExistsLang / polyForallLang and their class operators), the levels SigmaP / PiP by the standard recursion through complement classes, and PH as their union. Prove quantifier and class-level complement duality, monotonicity, the recursion laws, and level inclusions, the latter conditional on the single machine-engineering seam `pairFst ∈ FP` (first-component pair decoding), isolated as a hypothesis following the WitnessNTMConstruction pattern. Ported from leanprover/cslib#192, re-proved against this library's machine model and Set-based languages. Co-Authored-By: Claude Fable 5 --- Complexitylib/Classes.lean | 1 + Complexitylib/Classes/PH.lean | 299 ++++++++++++++++++++++++++++++++++ 2 files changed, 300 insertions(+) create mode 100644 Complexitylib/Classes/PH.lean diff --git a/Complexitylib/Classes.lean b/Complexitylib/Classes.lean index dc8ceb19..560697cd 100644 --- a/Complexitylib/Classes.lean +++ b/Complexitylib/Classes.lean @@ -58,6 +58,7 @@ import Complexitylib.Classes.Randomized.PPoly import Complexitylib.Classes.Pairing import Complexitylib.Classes.FNP import Complexitylib.Classes.NP.Witness +import Complexitylib.Classes.PH import Complexitylib.Classes.NP.Reduction import Complexitylib.Classes.L import Complexitylib.Classes.L.PolynomialTime diff --git a/Complexitylib/Classes/PH.lean b/Complexitylib/Classes/PH.lean new file mode 100644 index 00000000..12ec6727 --- /dev/null +++ b/Complexitylib/Classes/PH.lean @@ -0,0 +1,299 @@ +/- +Copyright (c) 2026 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ +import Complexitylib.Classes.Containments +import Complexitylib.Encoding.Pairing +import Mathlib.Algebra.Polynomial.Eval.Defs + +/-! +# The polynomial hierarchy + +This file defines the polynomial hierarchy via certificate quantifiers, following +the quantified-formula definition (Arora–Barak Definition 5.4, stated over the +library's `pair` codec): `polyExistsLang p L` holds of `x` when some witness `w` +of length at most `p.eval |x|` puts the encoded pair `pair x w` in `L`, and +`polyForallLang p L` requires this of every such witness. Lifting these to class +operators gives the levels `SigmaP 0 = P`, `SigmaP (n + 1) = +polyExistsClass (PiP n)`, `PiP n = complClass (SigmaP n)`, and their union `PH`. + +The level inclusions `SigmaP n ⊆ SigmaP (n + 1)` and `PiP n ⊆ PiP (n + 1)` are +proved relative to a single machine-engineering seam, stated as the hypothesis +`pairFst ∈ FP`: decoding the first component of a canonical pair is +polynomial-time computable. This follows the interface-isolation pattern of +`Complexitylib.Classes.NP.Witness` — every set-theoretic consequence is proved +unconditionally here, and the one remaining TM construction can land later +without touching this file's statements. All other results are unconditional. + +## Main definitions + +- `polyExistsLang`, `polyForallLang` — witness quantifiers on languages +- `polyExistsClass`, `polyForallClass` — the induced operators on classes +- `pairFst` — first-component decoder for the pairing codec +- `SigmaP`, `PiP`, `PH` — the hierarchy levels and their union + +## Main results + +- `compl_polyExistsLang` / `compl_polyForallLang` — quantifier duality +- `complClass_polyExistsClass` / `complClass_polyForallClass` — class duality +- `complClass_P` — `P` is closed under language complement, as a class equation +- `SigmaP_zero`, `PiP_zero`, `SigmaP_succ`, `PiP_succ` — recursion laws +- `P_subset_polyExistsClass_P` / `P_subset_polyForallClass_P` — base inclusions + (given `pairFst ∈ FP`) +- `SigmaP_subset_SigmaP_succ` / `PiP_subset_PiP_succ` — level inclusions + (given `pairFst ∈ FP`) +- `SigmaP_subset_PH`, `P_subset_PH` + +## TODO + +- Implement the `pairFst ∈ FP` seam: split the input with a + `pairSplitCoreTM`-style scanner and copy the decoded first component to the + output tape, packaging the result as `TM.ComputesInTime`. +- Relate `SigmaP 1` to the NTM-based `NP` through the witness characterization + interface in `Complexitylib.Classes.NP.Witness`. +-/ + +namespace Complexity + +/-! ## Witness quantifiers on languages -/ + +/-- The language of inputs `x` admitting a witness `w` of length at most +`p.eval |x|` such that the encoded pair `pair x w` lies in `L`. -/ +def polyExistsLang (p : Polynomial ℕ) (L : Language) : Language := + {x | ∃ w, w.length ≤ p.eval x.length ∧ pair x w ∈ L} + +/-- The language of inputs `x` such that every witness `w` of length at most +`p.eval |x|` puts the encoded pair `pair x w` in `L`. -/ +def polyForallLang (p : Polynomial ℕ) (L : Language) : Language := + {x | ∀ w, w.length ≤ p.eval x.length → pair x w ∈ L} + +/-- Membership in `polyExistsLang` unfolds to a bounded existential. -/ +@[simp] theorem mem_polyExistsLang {p : Polynomial ℕ} {L : Language} {x : List Bool} : + x ∈ polyExistsLang p L ↔ ∃ w, w.length ≤ p.eval x.length ∧ pair x w ∈ L := + Iff.rfl + +/-- Membership in `polyForallLang` unfolds to a bounded universal. -/ +@[simp] theorem mem_polyForallLang {p : Polynomial ℕ} {L : Language} {x : List Bool} : + x ∈ polyForallLang p L ↔ ∀ w, w.length ≤ p.eval x.length → pair x w ∈ L := + Iff.rfl + +/-- Complementing a bounded existential yields a bounded universal over the +complement: some-witness failure is all-witness exclusion. -/ +theorem compl_polyExistsLang (p : Polynomial ℕ) (L : Language) : + (polyExistsLang p L)ᶜ = polyForallLang p Lᶜ := by + ext x + simp [polyExistsLang, polyForallLang] + +/-- Complementing a bounded universal yields a bounded existential over the +complement. -/ +theorem compl_polyForallLang (p : Polynomial ℕ) (L : Language) : + (polyForallLang p L)ᶜ = polyExistsLang p Lᶜ := by + ext x + simp [polyExistsLang, polyForallLang] + +/-! ## Quantifier operators on classes -/ + +/-- The class of languages expressible as a polynomially-bounded existential +over some language of `C`. -/ +def polyExistsClass (C : Set Language) : Set Language := + {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = polyExistsLang p L'} + +/-- The class of languages expressible as a polynomially-bounded universal +over some language of `C`. -/ +def polyForallClass (C : Set Language) : Set Language := + {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = polyForallLang p L'} + +/-- `polyExistsClass` is monotone in the base class. -/ +theorem polyExistsClass_mono {C D : Set Language} (h : C ⊆ D) : + polyExistsClass C ⊆ polyExistsClass D := by + rintro L ⟨p, L', hL', rfl⟩ + exact ⟨p, L', h hL', rfl⟩ + +/-- `polyForallClass` is monotone in the base class. -/ +theorem polyForallClass_mono {C D : Set Language} (h : C ⊆ D) : + polyForallClass C ⊆ polyForallClass D := by + rintro L ⟨p, L', hL', rfl⟩ + exact ⟨p, L', h hL', rfl⟩ + +/-- `complClass` is monotone. -/ +theorem complClass_mono {C D : Set Language} (h : C ⊆ D) : + complClass C ⊆ complClass D := + fun _ hL => h hL + +/-- Class-level quantifier duality: the complement class of a bounded +existential class is the bounded universal class over the complement class. -/ +theorem complClass_polyExistsClass (C : Set Language) : + complClass (polyExistsClass C) = polyForallClass (complClass C) := by + ext L + simp only [mem_complClass, polyExistsClass, polyForallClass, Set.mem_setOf_eq] + constructor + · rintro ⟨p, L', hL', hEq⟩ + refine ⟨p, L'ᶜ, by simpa [mem_complClass, compl_compl] using hL', ?_⟩ + rw [← compl_compl L, hEq, compl_polyExistsLang] + · rintro ⟨p, L', hL', rfl⟩ + exact ⟨p, L'ᶜ, hL', by rw [compl_polyForallLang]⟩ + +/-- Class-level quantifier duality: the complement class of a bounded universal +class is the bounded existential class over the complement class. -/ +theorem complClass_polyForallClass (C : Set Language) : + complClass (polyForallClass C) = polyExistsClass (complClass C) := by + ext L + simp only [mem_complClass, polyExistsClass, polyForallClass, Set.mem_setOf_eq] + constructor + · rintro ⟨p, L', hL', hEq⟩ + refine ⟨p, L'ᶜ, by simpa [mem_complClass, compl_compl] using hL', ?_⟩ + rw [← compl_compl L, hEq, compl_polyForallLang] + · rintro ⟨p, L', hL', rfl⟩ + exact ⟨p, L'ᶜ, hL', by rw [compl_polyExistsLang]⟩ + +/-! ## The pair decoder seam -/ + +/-- Decode the first component of a canonical pair, returning `[]` on malformed +inputs. Statements below take the hypothesis `pairFst ∈ FP` — the one remaining +machine construction of this development (see the module docstring). -/ +def pairFst (z : List Bool) : List Bool := + ((unpair? z).map Prod.fst).getD [] + +/-- `pairFst` recovers the first component of a canonical pair. -/ +@[simp] theorem pairFst_pair (x y : List Bool) : pairFst (pair x y) = x := by + simp [pairFst] + +/-! ## Base inclusions -/ + +/-- `P` is closed under complement, stated as a class equation. -/ +theorem complClass_P : complClass P = P := by + ext L + exact ⟨fun h => compl_compl L ▸ P_compl h, fun h => P_compl h⟩ + +/-- Every language of `P` is a bounded existential over `P`: take the zero +witness bound, so the only witness is `[]`, and decide `pair x []` by decoding +the first component and running the original decider. -/ +theorem P_subset_polyExistsClass_P (hpair : pairFst ∈ FP) : + P ⊆ polyExistsClass P := by + intro L hL + refine ⟨0, pairFst ⁻¹' L, mem_P_preimage hpair hL, ?_⟩ + ext x + simp only [mem_polyExistsLang, Polynomial.eval_zero, Nat.le_zero, + List.length_eq_zero_iff, Set.mem_preimage] + constructor + · intro hx + exact ⟨[], rfl, by simpa using hx⟩ + · rintro ⟨w, rfl, hmem⟩ + simpa using hmem + +/-- Every language of `P` is a bounded universal over `P`: with the zero +witness bound the only witness is `[]`, decided as in +`P_subset_polyExistsClass_P`. -/ +theorem P_subset_polyForallClass_P (hpair : pairFst ∈ FP) : + P ⊆ polyForallClass P := by + intro L hL + refine ⟨0, pairFst ⁻¹' L, mem_P_preimage hpair hL, ?_⟩ + ext x + simp only [mem_polyForallLang, Polynomial.eval_zero, Nat.le_zero, + List.length_eq_zero_iff, Set.mem_preimage] + constructor + · rintro hx w rfl + simpa using hx + · intro h + simpa using h [] rfl + +/-! ## The hierarchy -/ + +/-- The Σ levels of the polynomial hierarchy: `SigmaP 0 = P` and +`SigmaP (n + 1)` is a bounded existential over the complement class of +`SigmaP n` (that is, over `PiP n`). -/ +def SigmaP : ℕ → Set Language + | 0 => P + | n + 1 => polyExistsClass (complClass (SigmaP n)) + +/-- The Π levels of the polynomial hierarchy: `PiP n` is the complement class +of `SigmaP n`. -/ +def PiP (n : ℕ) : Set Language := + complClass (SigmaP n) + +/-- The polynomial hierarchy: the union of all Σ levels. -/ +def PH : Set Language := + ⋃ n : ℕ, SigmaP n + +/-- The zeroth Σ level is `P`. -/ +@[simp] theorem SigmaP_zero : SigmaP 0 = P := rfl + +/-- The complement class of a Σ level is the corresponding Π level. -/ +@[simp] theorem complClass_SigmaP (n : ℕ) : complClass (SigmaP n) = PiP n := rfl + +/-- The complement class of a Π level is the corresponding Σ level. -/ +@[simp] theorem complClass_PiP (n : ℕ) : complClass (PiP n) = SigmaP n := by + rw [PiP, complClass_complClass] + +/-- The zeroth Π level is `P`, since `P` is closed under complement. -/ +@[simp] theorem PiP_zero : PiP 0 = P := by + rw [PiP, SigmaP_zero, complClass_P] + +/-- Recursion law for Σ levels: `SigmaP (n + 1)` is a bounded existential over +`PiP n`. -/ +theorem SigmaP_succ (n : ℕ) : SigmaP (n + 1) = polyExistsClass (PiP n) := rfl + +/-- Recursion law for Π levels: `PiP (n + 1)` is a bounded universal over +`SigmaP n`. -/ +theorem PiP_succ (n : ℕ) : PiP (n + 1) = polyForallClass (SigmaP n) := by + rw [PiP] + show complClass (polyExistsClass (complClass (SigmaP n))) = _ + rw [complClass_polyExistsClass, complClass_complClass] + +/-- The first Σ level is the bounded existential closure of `P` — the +certificate form of `NP`. -/ +theorem SigmaP_one : SigmaP 1 = polyExistsClass P := by + rw [SigmaP_succ, PiP_zero] + +/-- The first Π level is the bounded universal closure of `P` — the +certificate form of `coNP`. -/ +theorem PiP_one : PiP 1 = polyForallClass P := by + rw [PiP_succ, SigmaP_zero] + +/-! ## Level inclusions -/ + +/-- Both level inclusions, proved simultaneously by induction: the base case is +the pair of base inclusions of `P`, and each successor case is monotonicity of +the opposite quantifier applied to the other component. -/ +private theorem piP_sigmaP_subset_succ (hpair : pairFst ∈ FP) (n : ℕ) : + PiP n ⊆ PiP (n + 1) ∧ SigmaP n ⊆ SigmaP (n + 1) := by + induction n with + | zero => + constructor + · rw [PiP_zero, PiP_one] + exact P_subset_polyForallClass_P hpair + · rw [SigmaP_zero, SigmaP_one] + exact P_subset_polyExistsClass_P hpair + | succ n ih => + constructor + · rw [PiP_succ, PiP_succ] + exact polyForallClass_mono ih.2 + · rw [SigmaP_succ, SigmaP_succ] + exact polyExistsClass_mono ih.1 + +/-- Each Σ level is contained in the next. -/ +theorem SigmaP_subset_SigmaP_succ (hpair : pairFst ∈ FP) (n : ℕ) : + SigmaP n ⊆ SigmaP (n + 1) := + (piP_sigmaP_subset_succ hpair n).2 + +/-- Each Π level is contained in the next. -/ +theorem PiP_subset_PiP_succ (hpair : pairFst ∈ FP) (n : ℕ) : + PiP n ⊆ PiP (n + 1) := + (piP_sigmaP_subset_succ hpair n).1 + +/-! ## PH -/ + +/-- Membership in `PH` is membership in some Σ level. -/ +theorem mem_PH_iff {L : Language} : L ∈ PH ↔ ∃ n : ℕ, L ∈ SigmaP n := + Set.mem_iUnion + +/-- Every Σ level is contained in the hierarchy. -/ +theorem SigmaP_subset_PH (n : ℕ) : SigmaP n ⊆ PH := + fun _ h => Set.mem_iUnion.mpr ⟨n, h⟩ + +/-- `P` is contained in the polynomial hierarchy. -/ +theorem P_subset_PH : P ⊆ PH := + SigmaP_subset_PH 0 + +end Complexity From 262dd34425fd0f81b45de77d38cfae65fdc9eaee Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 22 Aug 2026 17:19:07 -0700 Subject: [PATCH 2/2] feat(PH): make the level inclusions unconditional and relocate generic lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Close the `pairFst ∈ FP` seam: the projection is the `fstBlockTM` scanner of Cobham's algebra, so `pairFst_mem_FP` is `Cobham.fstBlock_mem_FP`, and the base and level inclusions of the hierarchy no longer take a hypothesis. The polynomial-time facts about the pairing codec are broadly useful, so they get their own surface file `Classes/P/Pairing.lean` (`pairFst_mem_FP`, `pairSnd_mem_FP`, `mem_FP_pair`, `mem_FP_pair_right`, `mem_P_preimage_pairFst/Snd`). `complClass_mono` moves next to `complClass` in `Classes/Time.lean` and `complClass_P` next to `P_compl` in `Classes/Containments.lean`. The unused `SigmaP_one` / `PiP_one` are dropped. Co-Authored-By: Claude Fable 5 --- Complexitylib/Classes/Containments.lean | 5 ++ Complexitylib/Classes/P.lean | 1 + Complexitylib/Classes/P/Pairing.lean | 60 ++++++++++++++++++ Complexitylib/Classes/PH.lean | 83 ++++++------------------- Complexitylib/Classes/Time.lean | 4 ++ 5 files changed, 89 insertions(+), 64 deletions(-) create mode 100644 Complexitylib/Classes/P/Pairing.lean diff --git a/Complexitylib/Classes/Containments.lean b/Complexitylib/Classes/Containments.lean index 2c1188a0..79d02bdd 100644 --- a/Complexitylib/Classes/Containments.lean +++ b/Complexitylib/Classes/Containments.lean @@ -233,6 +233,11 @@ theorem P_compl {L : Language} (h : L ∈ P) : Lᶜ ∈ P := by have hpow : f =O (· ^ (k + 1)) := hbig.trans (BigO.pow_le_pow_succ k) exact BigO.add (BigO.const_mul_left 2 hpow) (BigO.const_le_pow 4 (k + 1)) +/-- `P` is closed under complement, stated as a class equation. -/ +theorem complClass_P : complClass P = P := by + ext L + exact ⟨fun h => compl_compl L ▸ P_compl h, fun h => P_compl h⟩ + /-- **DSPACE ⊆ NSPACE**: every language decidable by a DTM in space `O(S)` is also decidable by an NTM in space `O(S)`, via the `TM.toNTM` embedding. -/ theorem DSPACE_subset_NSPACE (S : ℕ → ℕ) : DSPACE S ⊆ NSPACE S := by diff --git a/Complexitylib/Classes/P.lean b/Complexitylib/Classes/P.lean index e893763f..06aba803 100644 --- a/Complexitylib/Classes/P.lean +++ b/Complexitylib/Classes/P.lean @@ -13,6 +13,7 @@ public import Complexitylib.Classes.P.Preimage public import Complexitylib.Classes.P.UnaryLength public import Complexitylib.Classes.P.FinsetDomain public import Complexitylib.Classes.P.Cobham +public import Complexitylib.Classes.P.Pairing import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput /-! diff --git a/Complexitylib/Classes/P/Pairing.lean b/Complexitylib/Classes/P/Pairing.lean new file mode 100644 index 00000000..bb5ca6a2 --- /dev/null +++ b/Complexitylib/Classes/P/Pairing.lean @@ -0,0 +1,60 @@ +/- +Copyright (c) 2026 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ +module +public import Complexitylib.Classes.P.Cobham.Internal +public import Complexitylib.Classes.P.Preimage + +/-! +# Polynomial-time pairing and unpairing + +The pairing codec `pair` of `Complexitylib.Encoding.Pairing` is the library's +canonical way to hand a machine two strings at once. This file records that the +codec is polynomial-time in both directions: pairing two polynomial-time values +is polynomial-time, and so are the projections `pairFst` / `pairSnd`, whose +scanners are the block machines of Cobham's algebra. + +## Main results + +- `pairFst_mem_FP`, `pairSnd_mem_FP` — the projections are polynomial-time +- `mem_FP_pair` — pairing two polynomial-time functions is polynomial-time +- `mem_FP_pair_right` — pairing a polynomial-time value with the input itself +- `mem_P_preimage_pairFst`, `mem_P_preimage_pairSnd` — deciding a language of + one component of a pair is polynomial-time +-/ + +@[expose] public section + +namespace Complexity + +/-! ## Polynomial-time facts -/ + +/-- **The first projection is polynomial-time.** -/ +theorem pairFst_mem_FP : pairFst ∈ FP := Cobham.fstBlock_mem_FP + +/-- **The second projection is polynomial-time.** -/ +theorem pairSnd_mem_FP : pairSnd ∈ FP := Cobham.sndBlock_mem_FP + +/-- **Pairing is polynomial-time**: two polynomial-time functions can be +evaluated on a common input and paired in polynomial time. -/ +theorem mem_FP_pair {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : + (fun z => pair (a z) (b z)) ∈ FP := + Cobham.pairFn_mem_FP ha hb + +/-- Pairing the input on the right of a polynomial-time value is polynomial-time. +This is `mem_FP_pairWithInput`; the mirror image is `mem_FP_pair id_mem_FP hf`. -/ +theorem mem_FP_pair_right {f : List Bool → List Bool} (hf : f ∈ FP) : + (fun x => pair (f x) x) ∈ FP := + mem_FP_pairWithInput hf + +/-- A language of the first component of a pair is polynomial-time decidable. -/ +theorem mem_P_preimage_pairFst {L : Language} (hL : L ∈ P) : pairFst ⁻¹' L ∈ P := + mem_P_preimage pairFst_mem_FP hL + +/-- A language of the second component of a pair is polynomial-time decidable. -/ +theorem mem_P_preimage_pairSnd {L : Language} (hL : L ∈ P) : pairSnd ⁻¹' L ∈ P := + mem_P_preimage pairSnd_mem_FP hL + +end Complexity diff --git a/Complexitylib/Classes/PH.lean b/Complexitylib/Classes/PH.lean index 275f5637..ae011c8a 100644 --- a/Complexitylib/Classes/PH.lean +++ b/Complexitylib/Classes/PH.lean @@ -5,7 +5,7 @@ Authors: Bolton Bailey -/ module public import Complexitylib.Classes.Containments -public import Complexitylib.Encoding.Pairing +public import Complexitylib.Classes.P.Pairing public import Mathlib.Algebra.Polynomial.Eval.Defs /-! @@ -19,38 +19,29 @@ of length at most `p.eval |x|` puts the encoded pair `pair x w` in `L`, and operators gives the levels `SigmaP 0 = P`, `SigmaP (n + 1) = polyExistsClass (PiP n)`, `PiP n = complClass (SigmaP n)`, and their union `PH`. -The level inclusions `SigmaP n ⊆ SigmaP (n + 1)` and `PiP n ⊆ PiP (n + 1)` are -proved relative to a single machine-engineering seam, stated as the hypothesis -`pairFst ∈ FP`: decoding the first component of a canonical pair is -polynomial-time computable. This follows the interface-isolation pattern of -`Complexitylib.Classes.NP.Witness` — every set-theoretic consequence is proved -unconditionally here, and the one remaining TM construction can land later -without touching this file's statements. All other results are unconditional. +The level inclusions `SigmaP n ⊆ SigmaP (n + 1)` and `PiP n ⊆ PiP (n + 1)` need +one computational fact: decoding the first component of a canonical pair is +polynomial-time computable (`pairFst_mem_FP`, from +`Complexitylib.Classes.P.Pairing`), so every result in this file is +unconditional. ## Main definitions - `polyExistsLang`, `polyForallLang` — witness quantifiers on languages - `polyExistsClass`, `polyForallClass` — the induced operators on classes -- `pairFst` — first-component decoder for the pairing codec - `SigmaP`, `PiP`, `PH` — the hierarchy levels and their union ## Main results - `compl_polyExistsLang` / `compl_polyForallLang` — quantifier duality - `complClass_polyExistsClass` / `complClass_polyForallClass` — class duality -- `complClass_P` — `P` is closed under language complement, as a class equation - `SigmaP_zero`, `PiP_zero`, `SigmaP_succ`, `PiP_succ` — recursion laws - `P_subset_polyExistsClass_P` / `P_subset_polyForallClass_P` — base inclusions - (given `pairFst ∈ FP`) - `SigmaP_subset_SigmaP_succ` / `PiP_subset_PiP_succ` — level inclusions - (given `pairFst ∈ FP`) - `SigmaP_subset_PH`, `P_subset_PH` ## TODO -- Implement the `pairFst ∈ FP` seam: split the input with a - `pairSplitCoreTM`-style scanner and copy the decoded first component to the - output tape, packaging the result as `TM.ComputesInTime`. - Relate `SigmaP 1` to the NTM-based `NP` through the witness characterization interface in `Complexitylib.Classes.NP.Witness`. -/ @@ -119,11 +110,6 @@ theorem polyForallClass_mono {C D : Set Language} (h : C ⊆ D) : rintro L ⟨p, L', hL', rfl⟩ exact ⟨p, L', h hL', rfl⟩ -/-- `complClass` is monotone. -/ -theorem complClass_mono {C D : Set Language} (h : C ⊆ D) : - complClass C ⊆ complClass D := - fun _ hL => h hL - /-- Class-level quantifier duality: the complement class of a bounded existential class is the bounded universal class over the complement class. -/ theorem complClass_polyExistsClass (C : Set Language) : @@ -150,32 +136,14 @@ theorem complClass_polyForallClass (C : Set Language) : · rintro ⟨p, L', hL', rfl⟩ exact ⟨p, L'ᶜ, hL', by rw [compl_polyExistsLang]⟩ -/-! ## The pair decoder seam -/ - -/-- Decode the first component of a canonical pair, returning `[]` on malformed -inputs. Statements below take the hypothesis `pairFst ∈ FP` — the one remaining -machine construction of this development (see the module docstring). -/ -def pairFst (z : List Bool) : List Bool := - ((unpair? z).map Prod.fst).getD [] - -/-- `pairFst` recovers the first component of a canonical pair. -/ -@[simp] theorem pairFst_pair (x y : List Bool) : pairFst (pair x y) = x := by - simp [pairFst] - /-! ## Base inclusions -/ -/-- `P` is closed under complement, stated as a class equation. -/ -theorem complClass_P : complClass P = P := by - ext L - exact ⟨fun h => compl_compl L ▸ P_compl h, fun h => P_compl h⟩ - /-- Every language of `P` is a bounded existential over `P`: take the zero witness bound, so the only witness is `[]`, and decide `pair x []` by decoding the first component and running the original decider. -/ -theorem P_subset_polyExistsClass_P (hpair : pairFst ∈ FP) : - P ⊆ polyExistsClass P := by +theorem P_subset_polyExistsClass_P : P ⊆ polyExistsClass P := by intro L hL - refine ⟨0, pairFst ⁻¹' L, mem_P_preimage hpair hL, ?_⟩ + refine ⟨0, pairFst ⁻¹' L, mem_P_preimage_pairFst hL, ?_⟩ ext x simp only [mem_polyExistsLang, Polynomial.eval_zero, Nat.le_zero, List.length_eq_zero_iff, Set.mem_preimage] @@ -188,10 +156,9 @@ theorem P_subset_polyExistsClass_P (hpair : pairFst ∈ FP) : /-- Every language of `P` is a bounded universal over `P`: with the zero witness bound the only witness is `[]`, decided as in `P_subset_polyExistsClass_P`. -/ -theorem P_subset_polyForallClass_P (hpair : pairFst ∈ FP) : - P ⊆ polyForallClass P := by +theorem P_subset_polyForallClass_P : P ⊆ polyForallClass P := by intro L hL - refine ⟨0, pairFst ⁻¹' L, mem_P_preimage hpair hL, ?_⟩ + refine ⟨0, pairFst ⁻¹' L, mem_P_preimage_pairFst hL, ?_⟩ ext x simp only [mem_polyForallLang, Polynomial.eval_zero, Nat.le_zero, List.length_eq_zero_iff, Set.mem_preimage] @@ -244,30 +211,20 @@ theorem PiP_succ (n : ℕ) : PiP (n + 1) = polyForallClass (SigmaP n) := by show complClass (polyExistsClass (complClass (SigmaP n))) = _ rw [complClass_polyExistsClass, complClass_complClass] -/-- The first Σ level is the bounded existential closure of `P` — the -certificate form of `NP`. -/ -theorem SigmaP_one : SigmaP 1 = polyExistsClass P := by - rw [SigmaP_succ, PiP_zero] - -/-- The first Π level is the bounded universal closure of `P` — the -certificate form of `coNP`. -/ -theorem PiP_one : PiP 1 = polyForallClass P := by - rw [PiP_succ, SigmaP_zero] - /-! ## Level inclusions -/ /-- Both level inclusions, proved simultaneously by induction: the base case is the pair of base inclusions of `P`, and each successor case is monotonicity of the opposite quantifier applied to the other component. -/ -private theorem piP_sigmaP_subset_succ (hpair : pairFst ∈ FP) (n : ℕ) : +private theorem piP_sigmaP_subset_succ (n : ℕ) : PiP n ⊆ PiP (n + 1) ∧ SigmaP n ⊆ SigmaP (n + 1) := by induction n with | zero => constructor - · rw [PiP_zero, PiP_one] - exact P_subset_polyForallClass_P hpair - · rw [SigmaP_zero, SigmaP_one] - exact P_subset_polyExistsClass_P hpair + · rw [PiP_zero, PiP_succ, SigmaP_zero] + exact P_subset_polyForallClass_P + · rw [SigmaP_zero, SigmaP_succ, PiP_zero] + exact P_subset_polyExistsClass_P | succ n ih => constructor · rw [PiP_succ, PiP_succ] @@ -276,14 +233,12 @@ private theorem piP_sigmaP_subset_succ (hpair : pairFst ∈ FP) (n : ℕ) : exact polyExistsClass_mono ih.1 /-- Each Σ level is contained in the next. -/ -theorem SigmaP_subset_SigmaP_succ (hpair : pairFst ∈ FP) (n : ℕ) : - SigmaP n ⊆ SigmaP (n + 1) := - (piP_sigmaP_subset_succ hpair n).2 +theorem SigmaP_subset_SigmaP_succ (n : ℕ) : SigmaP n ⊆ SigmaP (n + 1) := + (piP_sigmaP_subset_succ n).2 /-- Each Π level is contained in the next. -/ -theorem PiP_subset_PiP_succ (hpair : pairFst ∈ FP) (n : ℕ) : - PiP n ⊆ PiP (n + 1) := - (piP_sigmaP_subset_succ hpair n).1 +theorem PiP_subset_PiP_succ (n : ℕ) : PiP n ⊆ PiP (n + 1) := + (piP_sigmaP_subset_succ n).1 /-! ## PH -/ diff --git a/Complexitylib/Classes/Time.lean b/Complexitylib/Classes/Time.lean index 07704fc8..f5290fdd 100644 --- a/Complexitylib/Classes/Time.lean +++ b/Complexitylib/Classes/Time.lean @@ -52,4 +52,8 @@ def complClass (C : Set Language) : Set Language := theorem complClass_complClass (C : Set Language) : complClass (complClass C) = C := by ext L; simp [complClass] +/-- `complClass` is monotone. -/ +theorem complClass_mono {C D : Set Language} (h : C ⊆ D) : complClass C ⊆ complClass D := + fun _ hL => h hL + end Complexity