From 040d3e96b0241a1fe94fb2955778d9e6590a5e97 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 30 Nov 2025 20:35:50 -0800
Subject: [PATCH 1/6] feat: add initial definitions for complexity classes

---
 Cslib/Complexity/Class.lean    | 192 +++++++++++++++++++++++++++++++++
 Cslib/Complexity/Encoding.lean | 103 ++++++++++++++++++
 2 files changed, 295 insertions(+)
 create mode 100644 Cslib/Complexity/Class.lean
 create mode 100644 Cslib/Complexity/Encoding.lean

diff --git a/Cslib/Complexity/Class.lean b/Cslib/Complexity/Class.lean
new file mode 100644
index 00000000..8a093638
--- /dev/null
+++ b/Cslib/Complexity/Class.lean
@@ -0,0 +1,192 @@
+
+import Cslib.Complexity.Encoding
+import Cslib.Computability.Automata.Acceptor
+import Mathlib.Computability.TMComputable
+
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+
+/--
+The type of decision problems on bitstrings.
+
+We define these as functions from lists of booleans to booleans,
+implictly assuming the usual encodings.
+We define this as an auxiliary definition to decision problems on arbitrary types to avoid
+confusion with encodings.
+
+TODO: Replace with Typedef or abbrev?
+TODO: Bool or Prop?
+-/
+structure BitstringDecisionProblem where
+  toFun : List Bool → Bool
+
+instance : CoeFun BitstringDecisionProblem (fun _ ↦ List Bool → Bool) :=
+  ⟨BitstringDecisionProblem.toFun⟩
+
+instance : Membership (List Bool) BitstringDecisionProblem :=
+  ⟨fun X x ↦ X x⟩
+
+instance : HasCompl BitstringDecisionProblem :=
+  ⟨fun X ↦ ⟨fun x ↦ not (X x)⟩⟩
+
+/--
+The type of complexity classes over an alphabet `α` (which we require to be nontrivial and finite).
+We define these as sets of languages.
+-/
+abbrev ComplexityClass := Set BitstringDecisionProblem
+
+/--
+A simple definition to abstract the notion of a poly-time Turing machine into a predicate.
+-/
+def isComputableInPolyTime {α β : Type} (ea : FinEncoding α) (eb : FinEncoding β) (f : α → β) :=
+  Nonempty (TM2ComputableInPolyTime ea eb f)
+
+/--
+The class P is the set of decision problems
+decidable in polynomial time by a deterministic Turing machine.
+-/
+def P : ComplexityClass :=
+  { L | isComputableInPolyTime finEncodingListBool finEncodingBoolBool L.toFun }
+
+/--
+The list of all bitstrings of length `n` or less.
+-/
+def bitstringsUpToLength : ℕ → List (List Bool)
+  | 0     => [[]]
+  | n + 1 => (bitstringsUpToLength n)
+             ++ ((bitstringsUpToLength n) >>= fun bs ↦ [bs ++ [false], bs ++ [true]])
+
+
+/--
+Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
+defines a new decision problem to determine, for an input string `x`,
+whether all strings `w` of length at most `p (|x|)` satisfy `L (x, w)`.
+
+Reference:
+- https://en.wikipedia.org/wiki/Polynomial_hierarchy#Quantified_Boolean_formulae_definition
+-/
+def BitstringDecisionProblem.universallyQuantifyOverPolynomial
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    BitstringDecisionProblem :=
+  ⟨fun x ↦ List.all (bitstringsUpToLength (p.eval x.length)) fun w ↦ L (encode_list_bool_prod_list_bool (x, w))⟩
+
+/--
+Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
+defines a new decision problem to determine, for an input string `x`,
+whether there exists a string `w` of length at most `p (|x|)` such that `L (x, w)` holds.
+
+Reference:
+- https://en.wikipedia.org/wiki/Polynomial_hierarchy#Quantified_Boolean_formulae_definition
+-/
+def BitstringDecisionProblem.existentiallyQuantifyOverPolynomial
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    BitstringDecisionProblem :=
+  ⟨fun x ↦ List.any (bitstringsUpToLength (p.eval x.length)) fun w ↦ L (encode_list_bool_prod_list_bool (x, w))⟩
+
+
+def ComplexityClass.polyUniversallyQuantify (C : ComplexityClass) :
+    ComplexityClass :=
+  { L | ∃ p : Polynomial ℕ, ∃ L' ∈ C,
+      L = BitstringDecisionProblem.universallyQuantifyOverPolynomial p L' }
+
+notation "∀ᴾ" C => ComplexityClass.polyUniversallyQuantify C
+
+def ComplexityClass.polyExistentiallyQuantify (C : ComplexityClass) :
+    ComplexityClass :=
+  { L | ∃ p : Polynomial ℕ, ∃ L' ∈ C,
+      L = BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L' }
+
+notation "∃ᴾ" C => ComplexityClass.polyExistentiallyQuantify C
+
+
+-- /--
+-- The polynomial time hierarchy is defined by mutual induction as follows:
+
+-- Σᴾ 0 = Πᴾ 0 = P
+-- Σᴾ n+1 = ∃ᵖ Σᴾ n
+-- Πᴾ n+1 = ∀ᵖ Σᴾ n
+-- -/
+mutual
+  def SigmaPolyTimeHierarchy : ℕ → ComplexityClass
+    | 0     => P
+    | n + 1 => (SigmaPolyTimeHierarchy n).polyExistentiallyQuantify
+
+  def PiPolyTimeHierarchy : ℕ → ComplexityClass
+    | 0     => P
+    | n + 1 => (SigmaPolyTimeHierarchy n).polyUniversallyQuantify
+end
+
+notation "Σᴾ" n => SigmaPolyTimeHierarchy n
+notation "Πᴾ" n => PiPolyTimeHierarchy n
+
+def PolyTimeHierarchy : ComplexityClass :=
+  { L | ∃ n : ℕ, L ∈ Σᴾ n }
+
+/--
+Pi n contained in Sigma n+1
+-/
+lemma PiPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
+    (n : ℕ) : (Πᴾ n) ⊆ Σᴾ (n + 1) := by
+  sorry
+
+/--
+Pi n contained in Pi n+1
+-/
+lemma PiPolyTimeHierarchy_subset_PiPolyTimeHierarchy_succ
+    (n : ℕ) : (Πᴾ n) ⊆ Πᴾ (n + 1) := by
+  sorry
+
+/--
+Sigma n contained in Pi n+1
+-/
+lemma SigmaPolyTimeHierarchy_subset_PiPolyTimeHierarchy_succ
+    (n : ℕ) : (Σᴾ n) ⊆ Πᴾ (n + 1) := by
+  sorry
+
+/--
+Sigma n contained in Sigma n+1
+-/
+lemma SigmaPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
+    (n : ℕ) : (Σᴾ n) ⊆ Σᴾ (n + 1) := by
+  sorry
+
+lemma PolyTimeHierarchy_eq_union_sigma :
+  PolyTimeHierarchy = ⋃ n : ℕ, Σᴾ n := by
+  ext L
+  simp [PolyTimeHierarchy]
+
+lemma PolyTimeHierarchy_eq_union_pi :
+  PolyTimeHierarchy = ⋃ n : ℕ, Πᴾ n := by
+  sorry
+
+/--
+The class NP is the set of decision problems
+such that there exists a polynomial `p` over ℕ and a poly-time Turing machine
+where for all `x`, `L x = true` iff there exists a `w` of length at most `p (|x|)`
+such that the Turing machine accepts the pair `(x,w)`.
+
+See Definition 2.1 in Arora-Barak (2009).
+-/
+def NP : ComplexityClass := Σᴾ 1
+
+/--
+The class coNP is the set of decision problems
+whose complements are in NP.
+-/
+def coNP : ComplexityClass := Πᴾ 1
+
+def BPP : ComplexityClass := sorry
+
+def RP : ComplexityClass := sorry
+
+def coRP : ComplexityClass := sorry
+
+def ZPP : ComplexityClass := RP ∩ coRP
+
+-- Might be more difficult.
+def PSPACE : ComplexityClass := sorry
+
+end ComplexityTheory
diff --git a/Cslib/Complexity/Encoding.lean b/Cslib/Complexity/Encoding.lean
new file mode 100644
index 00000000..8230ea99
--- /dev/null
+++ b/Cslib/Complexity/Encoding.lean
@@ -0,0 +1,103 @@
+
+
+import Mathlib.Computability.Encoding
+import Mathlib.Data.List.SplitOn
+
+open Computability
+
+section Encodings
+/-
+These encodings are used in the formalization of complexity classes such as P and NP.
+
+Note that in a Zulip discussion thread, Daniel Weber contributed some more general encodings.
+We might eventually want to replace these with his more general versions.
+
+see: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/with/453031558
+-/
+
+def finEncodingListBool : Computability.FinEncoding (List Bool) where
+  Γ := Bool
+  encode := id
+  decode := Option.some
+  decode_encode _ := rfl
+  ΓFin := Bool.fintype
+
+@[simp]
+lemma splitOnP_isNone_map_some {α : Type} (l : List α) :
+    List.splitOnP Option.isNone (l.map some) = [l.map some] := by
+  induction l with
+  | nil => rfl
+  | cons hd tl ih =>
+    simp [ih]
+
+@[simp]
+lemma splitOnP_append_cons {α : Type} (l1 l2 : List α)
+    (a : α) (P : α → Bool) (hPa : P a = true) :
+    List.splitOnP P (l1 ++ a :: l2)
+    = List.splitOnP P l1 ++ List.splitOnP P l2 := by
+  induction l1 with
+  | nil => simp [hPa]
+  | cons hd tl ih =>
+    obtain ⟨hd1, tl1, h1'⟩ := List.exists_cons_of_ne_nil (List.splitOnP_ne_nil P tl)
+    by_cases hPh : P hd <;> simp [*]
+
+@[simp]
+lemma getLeft?_comp_inl {α β : Type*} :
+    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
+  ext
+  simp
+
+@[simp]
+lemma getLeft?_comp_inr {α β : Type*} :
+    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
+  ext
+  simp
+
+@[simp]
+lemma getRight?_comp_inl {α β : Type*} :
+    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
+  ext
+  simp
+
+@[simp]
+lemma getRight?_comp_inr {α β : Type*} :
+    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
+  ext
+  simp
+
+@[simp]
+lemma List.filterMap_none {α β : Type*} (l : List α) :
+    l.filterMap (fun _ ↦ @Option.none β) = [] := by
+  induction l <;> simp [*]
+
+def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
+    Computability.FinEncoding (α × β) where
+  Γ := ea.Γ ⊕ eb.Γ
+  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
+  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
+      (eb.decode (x.filterMap Sum.getRight?))
+  decode_encode x := by
+    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
+  ΓFin := inferInstance
+
+def encode_list_bool_prod_list_bool :
+    (List Bool × List Bool) → List (Bool) :=
+  fun ⟨l1, l2⟩ ↦ ((l1.map some) ++ [none] ++ (l2.map some)).flatMap (fun
+    | some b => [true, b]
+    | none   => [false, false])
+
+def finEncodingListBoolProdListBool : Computability.FinEncoding (List Bool × List Bool) where
+  Γ := Option Bool
+  encode := fun ⟨l1, l2⟩ ↦ (l1.map some) ++ [none] ++ (l2.map some)
+  decode := fun l ↦
+    match l.splitOnP Option.isNone with
+    | [l1, l2] => some (l1.map (Option.getD · false), l2.map (Option.getD · false))
+    | _ => none
+  decode_encode := by
+    intro (l1, l2)
+    simp
+  ΓFin := instFintypeOption
+
+
+
+end Encodings

From d076c9cc0fdca1765d247b7364d24cfd84d5f0db Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 10 Dec 2025 16:15:05 -0800
Subject: [PATCH 2/6] eric's suggestions

---
 Cslib/Complexity/Class.lean | 68 ++++++++++++++++++++-----------------
 1 file changed, 37 insertions(+), 31 deletions(-)

diff --git a/Cslib/Complexity/Class.lean b/Cslib/Complexity/Class.lean
index 8a093638..7a3f3963 100644
--- a/Cslib/Complexity/Class.lean
+++ b/Cslib/Complexity/Class.lean
@@ -14,34 +14,21 @@ The type of decision problems on bitstrings.
 
 We define these as functions from lists of booleans to booleans,
 implictly assuming the usual encodings.
-We define this as an auxiliary definition to decision problems on arbitrary types to avoid
-confusion with encodings.
 
-TODO: Replace with Typedef or abbrev?
-TODO: Bool or Prop?
+TODO: An Decision Problem type over arbitrary types.
 -/
-structure BitstringDecisionProblem where
-  toFun : List Bool → Bool
-
-instance : CoeFun BitstringDecisionProblem (fun _ ↦ List Bool → Bool) :=
-  ⟨BitstringDecisionProblem.toFun⟩
-
-instance : Membership (List Bool) BitstringDecisionProblem :=
-  ⟨fun X x ↦ X x⟩
-
-instance : HasCompl BitstringDecisionProblem :=
-  ⟨fun X ↦ ⟨fun x ↦ not (X x)⟩⟩
+abbrev BitstringDecisionProblem := List Bool → Bool
 
 /--
-The type of complexity classes over an alphabet `α` (which we require to be nontrivial and finite).
-We define these as sets of languages.
+The type of complexity classes over bitstrings.
+We define these as sets of `BitstringDecisionProblem`s.
 -/
 abbrev ComplexityClass := Set BitstringDecisionProblem
 
 /--
 A simple definition to abstract the notion of a poly-time Turing machine into a predicate.
 -/
-def isComputableInPolyTime {α β : Type} (ea : FinEncoding α) (eb : FinEncoding β) (f : α → β) :=
+def IsComputableInPolyTime {α β : Type} (ea : FinEncoding α) (eb : FinEncoding β) (f : α → β) :=
   Nonempty (TM2ComputableInPolyTime ea eb f)
 
 /--
@@ -49,16 +36,22 @@ The class P is the set of decision problems
 decidable in polynomial time by a deterministic Turing machine.
 -/
 def P : ComplexityClass :=
-  { L | isComputableInPolyTime finEncodingListBool finEncodingBoolBool L.toFun }
+  { L | IsComputableInPolyTime finEncodingListBool finEncodingBoolBool L }
 
 /--
-The list of all bitstrings of length `n` or less.
+The list of all bitstrings of exactly length `n`, in lexicographic order.
 -/
-def bitstringsUpToLength : ℕ → List (List Bool)
+def bitstringsOfLength : ℕ → List (List Bool)
   | 0     => [[]]
-  | n + 1 => (bitstringsUpToLength n)
-             ++ ((bitstringsUpToLength n) >>= fun bs ↦ [bs ++ [false], bs ++ [true]])
+  | n + 1 => (bitstringsOfLength n) >>= fun bs ↦ [bs ++ [false], bs ++ [true]]
+
+/--
+The list of all bitstrings of length `n` or less.
 
+Ordered first by length, then lexicographically.
+-/
+def bitstringsUpToLength (n : ℕ) : List (List Bool) :=
+  (List.range (n + 1)) >>= bitstringsOfLength
 
 /--
 Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
@@ -71,7 +64,9 @@ Reference:
 def BitstringDecisionProblem.universallyQuantifyOverPolynomial
     (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
     BitstringDecisionProblem :=
-  ⟨fun x ↦ List.all (bitstringsUpToLength (p.eval x.length)) fun w ↦ L (encode_list_bool_prod_list_bool (x, w))⟩
+  fun x ↦
+    List.all (bitstringsUpToLength (p.eval x.length)) fun w ↦
+      L (encode_list_bool_prod_list_bool (x, w))
 
 /--
 Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
@@ -84,7 +79,8 @@ Reference:
 def BitstringDecisionProblem.existentiallyQuantifyOverPolynomial
     (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
     BitstringDecisionProblem :=
-  ⟨fun x ↦ List.any (bitstringsUpToLength (p.eval x.length)) fun w ↦ L (encode_list_bool_prod_list_bool (x, w))⟩
+  fun x ↦ List.any (bitstringsUpToLength (p.eval x.length)) fun w ↦
+    L (encode_list_bool_prod_list_bool (x, w))
 
 
 def ComplexityClass.polyUniversallyQuantify (C : ComplexityClass) :
@@ -92,44 +88,54 @@ def ComplexityClass.polyUniversallyQuantify (C : ComplexityClass) :
   { L | ∃ p : Polynomial ℕ, ∃ L' ∈ C,
       L = BitstringDecisionProblem.universallyQuantifyOverPolynomial p L' }
 
-notation "∀ᴾ" C => ComplexityClass.polyUniversallyQuantify C
+notation "∀ᴾ " C => ComplexityClass.polyUniversallyQuantify C
 
 def ComplexityClass.polyExistentiallyQuantify (C : ComplexityClass) :
     ComplexityClass :=
   { L | ∃ p : Polynomial ℕ, ∃ L' ∈ C,
       L = BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L' }
 
-notation "∃ᴾ" C => ComplexityClass.polyExistentiallyQuantify C
+notation "∃ᴾ " C => ComplexityClass.polyExistentiallyQuantify C
 
 
 -- /--
 -- The polynomial time hierarchy is defined by mutual induction as follows:
 
 -- Σᴾ 0 = Πᴾ 0 = P
--- Σᴾ n+1 = ∃ᵖ Σᴾ n
+-- Σᴾ n+1 = ∃ᵖ Πᴾ n
 -- Πᴾ n+1 = ∀ᵖ Σᴾ n
 -- -/
 mutual
   def SigmaPolyTimeHierarchy : ℕ → ComplexityClass
     | 0     => P
-    | n + 1 => (SigmaPolyTimeHierarchy n).polyExistentiallyQuantify
+    | n + 1 => (PiPolyTimeHierarchy n).polyExistentiallyQuantify
 
   def PiPolyTimeHierarchy : ℕ → ComplexityClass
     | 0     => P
     | n + 1 => (SigmaPolyTimeHierarchy n).polyUniversallyQuantify
 end
 
-notation "Σᴾ" n => SigmaPolyTimeHierarchy n
-notation "Πᴾ" n => PiPolyTimeHierarchy n
+notation "Σᴾ " n => SigmaPolyTimeHierarchy n
+notation "Πᴾ " n => PiPolyTimeHierarchy n
 
 def PolyTimeHierarchy : ComplexityClass :=
   { L | ∃ n : ℕ, L ∈ Σᴾ n }
 
+lemma SigmaPolyTimeHierarchy_succ
+    (n : ℕ) : (Σᴾ (n + 1)) = (Πᴾ n).polyExistentiallyQuantify :=
+  rfl
+
 /--
 Pi n contained in Sigma n+1
 -/
 lemma PiPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
     (n : ℕ) : (Πᴾ n) ⊆ Σᴾ (n + 1) := by
+  rw [SigmaPolyTimeHierarchy_succ]
+  rw [Set.subset_def]
+  intro x hx_mem
+  simp [ComplexityClass.polyExistentiallyQuantify]
+  -- TODO if x ∈ Πᴾ n, then the language of pairs (x, ∅) is in Πᴾ n
+
   sorry
 
 /--

From 8a3bb20e12b9dcb902170d70208fe1237acab179 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 10 Dec 2025 16:48:50 -0800
Subject: [PATCH 3/6] move files

---
 Cslib/Complexity/Encoding.lean                | 103 ------------------
 .../Languages/ComplexityClass.lean}           |  31 +++---
 2 files changed, 16 insertions(+), 118 deletions(-)
 delete mode 100644 Cslib/Complexity/Encoding.lean
 rename Cslib/{Complexity/Class.lean => Computability/Languages/ComplexityClass.lean} (91%)

diff --git a/Cslib/Complexity/Encoding.lean b/Cslib/Complexity/Encoding.lean
deleted file mode 100644
index 8230ea99..00000000
--- a/Cslib/Complexity/Encoding.lean
+++ /dev/null
@@ -1,103 +0,0 @@
-
-
-import Mathlib.Computability.Encoding
-import Mathlib.Data.List.SplitOn
-
-open Computability
-
-section Encodings
-/-
-These encodings are used in the formalization of complexity classes such as P and NP.
-
-Note that in a Zulip discussion thread, Daniel Weber contributed some more general encodings.
-We might eventually want to replace these with his more general versions.
-
-see: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/with/453031558
--/
-
-def finEncodingListBool : Computability.FinEncoding (List Bool) where
-  Γ := Bool
-  encode := id
-  decode := Option.some
-  decode_encode _ := rfl
-  ΓFin := Bool.fintype
-
-@[simp]
-lemma splitOnP_isNone_map_some {α : Type} (l : List α) :
-    List.splitOnP Option.isNone (l.map some) = [l.map some] := by
-  induction l with
-  | nil => rfl
-  | cons hd tl ih =>
-    simp [ih]
-
-@[simp]
-lemma splitOnP_append_cons {α : Type} (l1 l2 : List α)
-    (a : α) (P : α → Bool) (hPa : P a = true) :
-    List.splitOnP P (l1 ++ a :: l2)
-    = List.splitOnP P l1 ++ List.splitOnP P l2 := by
-  induction l1 with
-  | nil => simp [hPa]
-  | cons hd tl ih =>
-    obtain ⟨hd1, tl1, h1'⟩ := List.exists_cons_of_ne_nil (List.splitOnP_ne_nil P tl)
-    by_cases hPh : P hd <;> simp [*]
-
-@[simp]
-lemma getLeft?_comp_inl {α β : Type*} :
-    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
-  ext
-  simp
-
-@[simp]
-lemma getLeft?_comp_inr {α β : Type*} :
-    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
-  ext
-  simp
-
-@[simp]
-lemma getRight?_comp_inl {α β : Type*} :
-    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
-  ext
-  simp
-
-@[simp]
-lemma getRight?_comp_inr {α β : Type*} :
-    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
-  ext
-  simp
-
-@[simp]
-lemma List.filterMap_none {α β : Type*} (l : List α) :
-    l.filterMap (fun _ ↦ @Option.none β) = [] := by
-  induction l <;> simp [*]
-
-def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
-    Computability.FinEncoding (α × β) where
-  Γ := ea.Γ ⊕ eb.Γ
-  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
-  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
-      (eb.decode (x.filterMap Sum.getRight?))
-  decode_encode x := by
-    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
-  ΓFin := inferInstance
-
-def encode_list_bool_prod_list_bool :
-    (List Bool × List Bool) → List (Bool) :=
-  fun ⟨l1, l2⟩ ↦ ((l1.map some) ++ [none] ++ (l2.map some)).flatMap (fun
-    | some b => [true, b]
-    | none   => [false, false])
-
-def finEncodingListBoolProdListBool : Computability.FinEncoding (List Bool × List Bool) where
-  Γ := Option Bool
-  encode := fun ⟨l1, l2⟩ ↦ (l1.map some) ++ [none] ++ (l2.map some)
-  decode := fun l ↦
-    match l.splitOnP Option.isNone with
-    | [l1, l2] => some (l1.map (Option.getD · false), l2.map (Option.getD · false))
-    | _ => none
-  decode_encode := by
-    intro (l1, l2)
-    simp
-  ΓFin := instFintypeOption
-
-
-
-end Encodings
diff --git a/Cslib/Complexity/Class.lean b/Cslib/Computability/Languages/ComplexityClass.lean
similarity index 91%
rename from Cslib/Complexity/Class.lean
rename to Cslib/Computability/Languages/ComplexityClass.lean
index 7a3f3963..256ceb82 100644
--- a/Cslib/Complexity/Class.lean
+++ b/Cslib/Computability/Languages/ComplexityClass.lean
@@ -1,8 +1,19 @@
 
-import Cslib.Complexity.Encoding
+import Cslib.Foundations.Data.Encoding
 import Cslib.Computability.Automata.Acceptor
 import Mathlib.Computability.TMComputable
 
+/-!
+# Complexity Classes
+
+This file contains the definition of `ComplexityClass`es over bitstring decision problems,
+as well as several standard complexity classes such as P, NP, and the polynomial time hierarchy.
+
+## TODO
+
+- Define other complexity classes such as BPP, RP, coRP, ZPP, PSPACE.
+- Prove basic inclusions between these classes.
+-/
 
 open Computability Turing
 
@@ -115,6 +126,7 @@ mutual
     | n + 1 => (SigmaPolyTimeHierarchy n).polyUniversallyQuantify
 end
 
+-- TODO bind more tightly
 notation "Σᴾ " n => SigmaPolyTimeHierarchy n
 notation "Πᴾ " n => PiPolyTimeHierarchy n
 
@@ -132,10 +144,10 @@ lemma PiPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
     (n : ℕ) : (Πᴾ n) ⊆ Σᴾ (n + 1) := by
   rw [SigmaPolyTimeHierarchy_succ]
   rw [Set.subset_def]
-  intro x hx_mem
-  simp [ComplexityClass.polyExistentiallyQuantify]
+  intro L hL_mem
+  simp? [ComplexityClass.polyExistentiallyQuantify]
   -- TODO if x ∈ Πᴾ n, then the language of pairs (x, ∅) is in Πᴾ n
-
+  use 0
   sorry
 
 /--
@@ -184,15 +196,4 @@ whose complements are in NP.
 -/
 def coNP : ComplexityClass := Πᴾ 1
 
-def BPP : ComplexityClass := sorry
-
-def RP : ComplexityClass := sorry
-
-def coRP : ComplexityClass := sorry
-
-def ZPP : ComplexityClass := RP ∩ coRP
-
--- Might be more difficult.
-def PSPACE : ComplexityClass := sorry
-
 end ComplexityTheory

From 7b705587f8ccffb46d1a616e315126bbbc323404 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Wed, 10 Dec 2025 16:53:05 -0800
Subject: [PATCH 4/6] move file

---
 Cslib/Foundations/Data/Encoding.lean | 101 +++++++++++++++++++++++++++
 1 file changed, 101 insertions(+)
 create mode 100644 Cslib/Foundations/Data/Encoding.lean

diff --git a/Cslib/Foundations/Data/Encoding.lean b/Cslib/Foundations/Data/Encoding.lean
new file mode 100644
index 00000000..e85d02f7
--- /dev/null
+++ b/Cslib/Foundations/Data/Encoding.lean
@@ -0,0 +1,101 @@
+
+
+import Mathlib.Computability.Encoding
+import Mathlib.Data.List.SplitOn
+
+open Computability
+
+section Encodings
+/-
+These encodings are used in the formalization of complexity classes such as P and NP.
+Note that in a Zulip discussion thread, Daniel Weber contributed some more general encodings.
+We might eventually want to replace these with his more general versions.
+see: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Formalise.20the.20proposition.20P.20.E2.89.A0NP/with/453031558
+-/
+
+def finEncodingListBool : Computability.FinEncoding (List Bool) where
+  Γ := Bool
+  encode := id
+  decode := Option.some
+  decode_encode _ := rfl
+  ΓFin := Bool.fintype
+
+@[simp]
+lemma splitOnP_isNone_map_some {α : Type} (l : List α) :
+    List.splitOnP Option.isNone (l.map some) = [l.map some] := by
+  induction l with
+  | nil => rfl
+  | cons hd tl ih =>
+    simp [ih]
+
+@[simp]
+lemma splitOnP_append_cons {α : Type} (l1 l2 : List α)
+    (a : α) (P : α → Bool) (hPa : P a = true) :
+    List.splitOnP P (l1 ++ a :: l2)
+    = List.splitOnP P l1 ++ List.splitOnP P l2 := by
+  induction l1 with
+  | nil => simp [hPa]
+  | cons hd tl ih =>
+    obtain ⟨hd1, tl1, h1'⟩ := List.exists_cons_of_ne_nil (List.splitOnP_ne_nil P tl)
+    by_cases hPh : P hd <;> simp [*]
+
+@[simp]
+lemma getLeft?_comp_inl {α β : Type*} :
+    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
+  ext
+  simp
+
+@[simp]
+lemma getLeft?_comp_inr {α β : Type*} :
+    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
+  ext
+  simp
+
+@[simp]
+lemma getRight?_comp_inl {α β : Type*} :
+    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
+  ext
+  simp
+
+@[simp]
+lemma getRight?_comp_inr {α β : Type*} :
+    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
+  ext
+  simp
+
+@[simp]
+lemma List.filterMap_none {α β : Type*} (l : List α) :
+    l.filterMap (fun _ ↦ @Option.none β) = [] := by
+  induction l <;> simp [*]
+
+def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
+    Computability.FinEncoding (α × β) where
+  Γ := ea.Γ ⊕ eb.Γ
+  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
+  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
+      (eb.decode (x.filterMap Sum.getRight?))
+  decode_encode x := by
+    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
+  ΓFin := inferInstance
+
+def encode_list_bool_prod_list_bool :
+    (List Bool × List Bool) → List (Bool) :=
+  fun ⟨l1, l2⟩ ↦ ((l1.map some) ++ [none] ++ (l2.map some)).flatMap (fun
+    | some b => [true, b]
+    | none   => [false, false])
+
+def finEncodingListBoolProdListBool : Computability.FinEncoding (List Bool × List Bool) where
+  Γ := Option Bool
+  encode := fun ⟨l1, l2⟩ ↦ (l1.map some) ++ [none] ++ (l2.map some)
+  decode := fun l ↦
+    match l.splitOnP Option.isNone with
+    | [l1, l2] => some (l1.map (Option.getD · false), l2.map (Option.getD · false))
+    | _ => none
+  decode_encode := by
+    intro (l1, l2)
+    simp
+  ΓFin := instFintypeOption
+
+
+
+end Encodings

From a164a719b259ccdd257134868f99fdff24bac732 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 11 Dec 2025 11:41:37 -0800
Subject: [PATCH 5/6] additional development

---
 .../Languages/ComplexityClass.lean            | 329 +++++++++++++-----
 Cslib/Foundations/Data/Encoding.lean          |  73 +---
 2 files changed, 256 insertions(+), 146 deletions(-)

diff --git a/Cslib/Computability/Languages/ComplexityClass.lean b/Cslib/Computability/Languages/ComplexityClass.lean
index 256ceb82..b13f5c4a 100644
--- a/Cslib/Computability/Languages/ComplexityClass.lean
+++ b/Cslib/Computability/Languages/ComplexityClass.lean
@@ -24,17 +24,11 @@ namespace ComplexityTheory
 The type of decision problems on bitstrings.
 
 We define these as functions from lists of booleans to booleans,
-implictly assuming the usual encodings.
+implicitly assuming the usual encodings.
 
 TODO: An Decision Problem type over arbitrary types.
 -/
-abbrev BitstringDecisionProblem := List Bool → Bool
-
-/--
-The type of complexity classes over bitstrings.
-We define these as sets of `BitstringDecisionProblem`s.
--/
-abbrev ComplexityClass := Set BitstringDecisionProblem
+abbrev BitstringDecisionProblem : Type := List Bool → Bool
 
 /--
 A simple definition to abstract the notion of a poly-time Turing machine into a predicate.
@@ -42,13 +36,6 @@ A simple definition to abstract the notion of a poly-time Turing machine into a
 def IsComputableInPolyTime {α β : Type} (ea : FinEncoding α) (eb : FinEncoding β) (f : α → β) :=
   Nonempty (TM2ComputableInPolyTime ea eb f)
 
-/--
-The class P is the set of decision problems
-decidable in polynomial time by a deterministic Turing machine.
--/
-def P : ComplexityClass :=
-  { L | IsComputableInPolyTime finEncodingListBool finEncodingBoolBool L }
-
 /--
 The list of all bitstrings of exactly length `n`, in lexicographic order.
 -/
@@ -64,6 +51,11 @@ Ordered first by length, then lexicographically.
 def bitstringsUpToLength (n : ℕ) : List (List Bool) :=
   (List.range (n + 1)) >>= bitstringsOfLength
 
+@[simp]
+lemma bitstringsUpToLength_zero :
+    bitstringsUpToLength 0 = [[]] := by
+  rfl
+
 /--
 Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
 defines a new decision problem to determine, for an input string `x`,
@@ -93,107 +85,288 @@ def BitstringDecisionProblem.existentiallyQuantifyOverPolynomial
   fun x ↦ List.any (bitstringsUpToLength (p.eval x.length)) fun w ↦
     L (encode_list_bool_prod_list_bool (x, w))
 
+@[simp]
+lemma BitstringDecisionProblem.universallyQuantifyOverPolynomial_complement
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    (L.universallyQuantifyOverPolynomial p)ᶜ =
+      (Lᶜ).existentiallyQuantifyOverPolynomial p := by
+  unfold universallyQuantifyOverPolynomial
+  unfold existentiallyQuantifyOverPolynomial
+  ext x
+  simp [List.not_any_eq_all_not] -- Add to push Bool.not
+
+@[simp]
+lemma BitstringDecisionProblem.existentiallyQuantifyOverPolynomial_complement
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    (L.existentiallyQuantifyOverPolynomial p)ᶜ =
+      (Lᶜ).universallyQuantifyOverPolynomial p := by
+  unfold universallyQuantifyOverPolynomial
+  unfold existentiallyQuantifyOverPolynomial
+  ext x
+  simp [List.not_all_eq_any_not] -- Add to push Bool.not
+
+
+
+/--
+The type of complexity classes over bitstrings.
+We define these as sets of `BitstringDecisionProblem`s.
+-/
+abbrev ComplexityClass : Type := Set BitstringDecisionProblem
+
+namespace ComplexityClass
+
+/--
+The class P is the set of decision problems
+decidable in polynomial time by a deterministic Turing machine.
+-/
+def P : ComplexityClass :=
+  { L | IsComputableInPolyTime finEncodingListBool finEncodingBoolBool L }
+
+/--
+The complement of a complexity class `C` is the set of decision problems
+whose complements are in `C`.
+
+Note that this is distinct from the complement of `C` as a set, which would be
+the set of decision problems not in `C`.
+-/
+def complement (C : ComplexityClass) : ComplexityClass :=
+  { L | (Lᶜ ∈ C) }
 
-def ComplexityClass.polyUniversallyQuantify (C : ComplexityClass) :
+@[simp]
+lemma complement_complement (C : ComplexityClass) :
+    C.complement.complement = C := by
+  ext L
+  simp [complement, Set.mem_setOf_eq, compl_compl]
+
+@[simp]
+lemma P_complement : P.complement = P := by
+  ext L
+  sorry
+
+def polyUniversallyQuantify (C : ComplexityClass) :
     ComplexityClass :=
   { L | ∃ p : Polynomial ℕ, ∃ L' ∈ C,
       L = BitstringDecisionProblem.universallyQuantifyOverPolynomial p L' }
 
-notation "∀ᴾ " C => ComplexityClass.polyUniversallyQuantify C
+notation "∀ᴾ " C => polyUniversallyQuantify C
 
-def ComplexityClass.polyExistentiallyQuantify (C : ComplexityClass) :
+def polyExistentiallyQuantify (C : ComplexityClass) :
     ComplexityClass :=
   { L | ∃ p : Polynomial ℕ, ∃ L' ∈ C,
       L = BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L' }
 
-notation "∃ᴾ " C => ComplexityClass.polyExistentiallyQuantify C
+notation "∃ᴾ " C => polyExistentiallyQuantify C
+
+/--
+The class NP is the set of decision problems
+such that there exists a polynomial `p` over ℕ and a poly-time Turing machine
+where for all `x`, `L x = true` iff there exists a `w` of length at most `p (|x|)`
+such that the Turing machine accepts the pair `(x,w)`.
+
+See Definition 2.1 in Arora-Barak (2009).
+-/
+def NP : ComplexityClass := ∃ᴾ P
 
+/--
+The class coNP is the set of decision problems
+whose complements are in NP.
+-/
+def coNP : ComplexityClass := ∀ᴾ P
 
--- /--
--- The polynomial time hierarchy is defined by mutual induction as follows:
+@[simp]
+lemma polyUniversallyQuantify_complement
+    (C : ComplexityClass) :
+    (∀ᴾ C).complement = ∃ᴾ (C.complement) := by
+  unfold complement polyExistentiallyQuantify polyUniversallyQuantify
+  ext L
+  simp only [Set.mem_setOf_eq]
+  refine exists_congr ?_
+  intro p
+  constructor
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : Lᶜᶜ = BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L'ᶜ := by
+      rw [h_eq]
+      simp
+    use L'ᶜ
+    simp only [compl_compl] at *
+    exact And.symm ⟨h_eq, hL'⟩
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : Lᶜ = BitstringDecisionProblem.universallyQuantifyOverPolynomial p L'ᶜ := by
+      rw [h_eq]
+      simp
+    use L'ᶜ
+
+@[simp]
+lemma polyExistentiallyQuantify_complement
+    (C : ComplexityClass) :
+    (∃ᴾ C).complement = ∀ᴾ (C.complement) := by
+  unfold complement polyExistentiallyQuantify polyUniversallyQuantify
+  ext L
+  simp only [Set.mem_setOf_eq]
+  refine exists_congr ?_
+  intro p
+  constructor
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : Lᶜᶜ = BitstringDecisionProblem.universallyQuantifyOverPolynomial p L'ᶜ := by
+      rw [h_eq]
+      simp
+    use L'ᶜ
+    simp only [compl_compl] at *
+    exact And.symm ⟨h_eq, hL'⟩
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : Lᶜ = BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L'ᶜ := by
+      rw [h_eq]
+      simp
+    use L'ᶜ
+
+lemma complement_mono
+    {C D : ComplexityClass} (h : C ⊆ D) :
+    C.complement ⊆ D.complement := by
+  unfold complement
+  simp only [Set.subset_def]
+  intro L hL
+  simp only [Set.mem_setOf_eq] at hL ⊢
+  exact h hL
+
+lemma complement_mono_iff
+    {C D : ComplexityClass} :
+    C ⊆ D ↔ C.complement ⊆ D.complement := by
+  constructor
+  · exact complement_mono
+  · intro h
+    have h' := complement_mono h
+    rw [complement_complement C, complement_complement D] at h'
+    exact h'
+
+lemma polyUniversallyQuantify_mono
+    {C D : ComplexityClass} (h : C ⊆ D) :
+    (∀ᴾ C) ⊆ (∀ᴾ D) := by
+  unfold polyUniversallyQuantify
+  simp only [Set.subset_def]
+  intro L hL
+  rcases hL with ⟨p, L', hL', h_eq⟩
+  use p
+  use L'
+  exact ⟨h hL', h_eq⟩
+
+lemma polyExistentiallyQuantify_mono
+    {C D : ComplexityClass} (h : C ⊆ D) :
+    (∃ᴾ C) ⊆ (∃ᴾ D) := by
+  unfold polyExistentiallyQuantify
+  simp only [Set.subset_def]
+  intro L hL
+  rcases hL with ⟨p, L', hL', h_eq⟩
+  use p
+  use L'
+  exact ⟨h hL', h_eq⟩
+
+
+lemma P_subset_NP : P ⊆ NP := by
+  unfold NP
+  sorry
 
--- Σᴾ 0 = Πᴾ 0 = P
--- Σᴾ n+1 = ∃ᵖ Πᴾ n
--- Πᴾ n+1 = ∀ᵖ Σᴾ n
--- -/
-mutual
-  def SigmaPolyTimeHierarchy : ℕ → ComplexityClass
-    | 0     => P
-    | n + 1 => (PiPolyTimeHierarchy n).polyExistentiallyQuantify
+lemma P_subset_coNP : P ⊆ coNP := by
+  unfold coNP
+  rw [complement_mono_iff]
+  simp only [P_complement, polyUniversallyQuantify_complement]
+  exact P_subset_NP
 
-  def PiPolyTimeHierarchy : ℕ → ComplexityClass
-    | 0     => P
-    | n + 1 => (SigmaPolyTimeHierarchy n).polyUniversallyQuantify
-end
+/--
+The Sigma levels of the polynomial time hierarchy.
+
+Σᴾ 0 = P
+Σᴾ n+1 = ∃ᴾ (Σᴾ n).complement
+-/
+def SigmaPolyTimeHierarchy : ℕ → ComplexityClass
+  | 0     => P
+  | n + 1 => (SigmaPolyTimeHierarchy n).complement.polyExistentiallyQuantify
+
+/--
+The Pi levels of the polynomial time hierarchy, defined as the complement of the Sigma levels.
+
+Πᴾ n = (Σᴾ n).complement
+-/
+def PiPolyTimeHierarchy (n : ℕ) : ComplexityClass :=
+  (SigmaPolyTimeHierarchy n).complement
 
 -- TODO bind more tightly
-notation "Σᴾ " n => SigmaPolyTimeHierarchy n
-notation "Πᴾ " n => PiPolyTimeHierarchy n
+scoped notation "Σᴾ" => SigmaPolyTimeHierarchy
+scoped notation "Πᴾ" => PiPolyTimeHierarchy
 
 def PolyTimeHierarchy : ComplexityClass :=
   { L | ∃ n : ℕ, L ∈ Σᴾ n }
 
-lemma SigmaPolyTimeHierarchy_succ
-    (n : ℕ) : (Σᴾ (n + 1)) = (Πᴾ n).polyExistentiallyQuantify :=
-  rfl
+@[simp]
+lemma SigmaPolyTimeHierarchy_zero : Σᴾ 0 = P := rfl
 
-/--
-Pi n contained in Sigma n+1
--/
-lemma PiPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
-    (n : ℕ) : (Πᴾ n) ⊆ Σᴾ (n + 1) := by
-  rw [SigmaPolyTimeHierarchy_succ]
-  rw [Set.subset_def]
-  intro L hL_mem
-  simp? [ComplexityClass.polyExistentiallyQuantify]
-  -- TODO if x ∈ Πᴾ n, then the language of pairs (x, ∅) is in Πᴾ n
-  use 0
-  sorry
+@[simp]
+lemma PiPolyTimeHierarchy_zero : Πᴾ 0 = P.complement := rfl
+
+@[simp]
+lemma SigmaPolyTimeHierarchy_one : Σᴾ 1 = NP := by
+  simp [SigmaPolyTimeHierarchy, NP]
+
+@[simp]
+lemma PiPolyTimeHierarchy_one : Πᴾ 1 = coNP := by
+  simp [PiPolyTimeHierarchy, coNP, NP]
+
+lemma SigmaPolyTimeHierarchy_succ
+    (n : ℕ) : Σᴾ (n + 1) = ∃ᴾ (Πᴾ n) := by
+  simp only [SigmaPolyTimeHierarchy, PiPolyTimeHierarchy]
+
+lemma PiPolyTimeHierarchy_succ
+    (n : ℕ) : Πᴾ (n + 1) = ∀ᴾ (Σᴾ n) := by
+  simp only [PiPolyTimeHierarchy, SigmaPolyTimeHierarchy,
+    complement_complement,
+    polyExistentiallyQuantify_complement]
+
+@[simp]
+lemma PiPolyTimeHierarchy_complement
+    (n : ℕ) : (Πᴾ n).complement = Σᴾ n := by
+  simp [PiPolyTimeHierarchy, complement_complement]
+
+@[simp]
+lemma SigmaPolyTimeHierarchy_complement
+    (n : ℕ) : (Σᴾ n).complement = Πᴾ n := by
+  simp [PiPolyTimeHierarchy]
+
+private lemma PolyTimeHierarchy_subset_aux (n : ℕ) :
+    (Πᴾ n) ⊆ (Πᴾ (n + 1)) ∧ (Σᴾ n) ⊆ Σᴾ (n + 1) := by
+  induction n with
+  | zero =>
+    simp only [SigmaPolyTimeHierarchy_succ, PiPolyTimeHierarchy_succ]
+    simp only [PiPolyTimeHierarchy_zero, P_complement, SigmaPolyTimeHierarchy_zero]
+    constructor
+    · exact P_subset_coNP
+    · exact P_subset_NP
+  | succ n ih =>
+    simp only [SigmaPolyTimeHierarchy_succ, PiPolyTimeHierarchy_succ] at *
+    obtain ⟨ih_pi, ih_sigma⟩ := ih
+    constructor
+    · apply polyUniversallyQuantify_mono
+      exact ih_sigma
+    · apply polyExistentiallyQuantify_mono
+      exact ih_pi
 
 /--
 Pi n contained in Pi n+1
 -/
 lemma PiPolyTimeHierarchy_subset_PiPolyTimeHierarchy_succ
     (n : ℕ) : (Πᴾ n) ⊆ Πᴾ (n + 1) := by
-  sorry
-
-/--
-Sigma n contained in Pi n+1
--/
-lemma SigmaPolyTimeHierarchy_subset_PiPolyTimeHierarchy_succ
-    (n : ℕ) : (Σᴾ n) ⊆ Πᴾ (n + 1) := by
-  sorry
+  exact (PolyTimeHierarchy_subset_aux n).1
 
 /--
 Sigma n contained in Sigma n+1
 -/
 lemma SigmaPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
     (n : ℕ) : (Σᴾ n) ⊆ Σᴾ (n + 1) := by
-  sorry
+  exact (PolyTimeHierarchy_subset_aux n).2
 
 lemma PolyTimeHierarchy_eq_union_sigma :
   PolyTimeHierarchy = ⋃ n : ℕ, Σᴾ n := by
   ext L
   simp [PolyTimeHierarchy]
 
-lemma PolyTimeHierarchy_eq_union_pi :
-  PolyTimeHierarchy = ⋃ n : ℕ, Πᴾ n := by
-  sorry
-
-/--
-The class NP is the set of decision problems
-such that there exists a polynomial `p` over ℕ and a poly-time Turing machine
-where for all `x`, `L x = true` iff there exists a `w` of length at most `p (|x|)`
-such that the Turing machine accepts the pair `(x,w)`.
-
-See Definition 2.1 in Arora-Barak (2009).
--/
-def NP : ComplexityClass := Σᴾ 1
-
-/--
-The class coNP is the set of decision problems
-whose complements are in NP.
--/
-def coNP : ComplexityClass := Πᴾ 1
+end ComplexityClass
 
 end ComplexityTheory
diff --git a/Cslib/Foundations/Data/Encoding.lean b/Cslib/Foundations/Data/Encoding.lean
index e85d02f7..f33bac71 100644
--- a/Cslib/Foundations/Data/Encoding.lean
+++ b/Cslib/Foundations/Data/Encoding.lean
@@ -20,63 +20,6 @@ def finEncodingListBool : Computability.FinEncoding (List Bool) where
   decode_encode _ := rfl
   ΓFin := Bool.fintype
 
-@[simp]
-lemma splitOnP_isNone_map_some {α : Type} (l : List α) :
-    List.splitOnP Option.isNone (l.map some) = [l.map some] := by
-  induction l with
-  | nil => rfl
-  | cons hd tl ih =>
-    simp [ih]
-
-@[simp]
-lemma splitOnP_append_cons {α : Type} (l1 l2 : List α)
-    (a : α) (P : α → Bool) (hPa : P a = true) :
-    List.splitOnP P (l1 ++ a :: l2)
-    = List.splitOnP P l1 ++ List.splitOnP P l2 := by
-  induction l1 with
-  | nil => simp [hPa]
-  | cons hd tl ih =>
-    obtain ⟨hd1, tl1, h1'⟩ := List.exists_cons_of_ne_nil (List.splitOnP_ne_nil P tl)
-    by_cases hPh : P hd <;> simp [*]
-
-@[simp]
-lemma getLeft?_comp_inl {α β : Type*} :
-    Sum.getLeft? ∘ @Sum.inl α β = Option.some := by
-  ext
-  simp
-
-@[simp]
-lemma getLeft?_comp_inr {α β : Type*} :
-    Sum.getLeft? ∘ @Sum.inr α β = fun x ↦ Option.none := by
-  ext
-  simp
-
-@[simp]
-lemma getRight?_comp_inl {α β : Type*} :
-    Sum.getRight? ∘ @Sum.inl α β = fun x ↦ Option.none := by
-  ext
-  simp
-
-@[simp]
-lemma getRight?_comp_inr {α β : Type*} :
-    Sum.getRight? ∘ @Sum.inr α β = Option.some := by
-  ext
-  simp
-
-@[simp]
-lemma List.filterMap_none {α β : Type*} (l : List α) :
-    l.filterMap (fun _ ↦ @Option.none β) = [] := by
-  induction l <;> simp [*]
-
-def finEncodingPair {α β : Type*} (ea : FinEncoding α) (eb : FinEncoding β) :
-    Computability.FinEncoding (α × β) where
-  Γ := ea.Γ ⊕ eb.Γ
-  encode x := (ea.encode x.1).map .inl ++ (eb.encode x.2).map .inr
-  decode x := Option.map₂ Prod.mk (ea.decode (x.filterMap Sum.getLeft?))
-      (eb.decode (x.filterMap Sum.getRight?))
-  decode_encode x := by
-    simp [List.filterMap_append, ea.decode_encode, eb.decode_encode]
-  ΓFin := inferInstance
 
 def encode_list_bool_prod_list_bool :
     (List Bool × List Bool) → List (Bool) :=
@@ -84,18 +27,12 @@ def encode_list_bool_prod_list_bool :
     | some b => [true, b]
     | none   => [false, false])
 
-def finEncodingListBoolProdListBool : Computability.FinEncoding (List Bool × List Bool) where
-  Γ := Option Bool
-  encode := fun ⟨l1, l2⟩ ↦ (l1.map some) ++ [none] ++ (l2.map some)
-  decode := fun l ↦
-    match l.splitOnP Option.isNone with
-    | [l1, l2] => some (l1.map (Option.getD · false), l2.map (Option.getD · false))
-    | _ => none
-  decode_encode := by
-    intro (l1, l2)
-    simp
-  ΓFin := instFintypeOption
+def decode_list_bool_prod_list_bool :
+    List (Bool) → Option (List Bool × List Bool) := sorry
 
+lemma decode_encode_list_bool_prod_list_bool :
+    ∀ x : List Bool × List Bool,
+      decode_list_bool_prod_list_bool (encode_list_bool_prod_list_bool x) = some x := sorry
 
 
 end Encodings

From b8e7025fded56530a42e5b7087e3386651c897b3 Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 11 Dec 2025 11:46:40 -0800
Subject: [PATCH 6/6] note todos

---
 Cslib/Computability/Languages/ComplexityClass.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Cslib/Computability/Languages/ComplexityClass.lean b/Cslib/Computability/Languages/ComplexityClass.lean
index b13f5c4a..2c7fd7f9 100644
--- a/Cslib/Computability/Languages/ComplexityClass.lean
+++ b/Cslib/Computability/Languages/ComplexityClass.lean
@@ -141,6 +141,8 @@ lemma complement_complement (C : ComplexityClass) :
 @[simp]
 lemma P_complement : P.complement = P := by
   ext L
+  -- TODO requires showing that Bool.not is poly time,
+  -- and composition of poly-time functions is poly-time
   sorry
 
 def polyUniversallyQuantify (C : ComplexityClass) :
@@ -263,6 +265,11 @@ lemma polyExistentiallyQuantify_mono
 
 lemma P_subset_NP : P ⊆ NP := by
   unfold NP
+  unfold polyExistentiallyQuantify
+  intro L hL
+  simp only [Set.mem_setOf_eq]
+  use 0
+  -- TODO requires proving that pairing operations are poly-time
   sorry
 
 lemma P_subset_coNP : P ⊆ coNP := by