diff --git a/Complexity.lean b/Complexity.lean
index edb9075dde..041e616c8e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -627,6 +627,7 @@ public import Complexity.Computability.Complexity.Classes.PH.SipserLautemann
 public import Complexity.Computability.Complexity.Classes.PP
 public import Complexity.Computability.Complexity.Classes.PP.Bit
 public import Complexity.Computability.Complexity.Classes.PP.Characterization
+public import Complexity.Computability.Complexity.Classes.PP.Closure
 public import Complexity.Computability.Complexity.Classes.PP.Oracle
 public import Complexity.Computability.Complexity.Classes.PP.TruthTable
 public import Complexity.Computability.Complexity.Classes.Padding
@@ -658,6 +659,7 @@ public import Complexity.Computability.Complexity.Classes.SharpP.Space
 public import Complexity.Computability.Complexity.Classes.SharpP.WeightedReplay
 public import Complexity.Computability.Complexity.Classes.Space
 public import Complexity.Computability.Complexity.Classes.Space.Basic
+public import Complexity.Computability.Complexity.Classes.Space.Closure
 public import Complexity.Computability.Complexity.Classes.Space.GeneralizedGeography
 public import Complexity.Computability.Complexity.Classes.Space.GeneralizedGeography.Membership
 public import Complexity.Computability.Complexity.Classes.Space.GeneralizedGeography.Reduction
diff --git a/Complexity/Computability/Complexity/Classes/BPP.lean b/Complexity/Computability/Complexity/Classes/BPP.lean
index 2a06671364..e7e0e96a1f 100644
--- a/Complexity/Computability/Complexity/Classes/BPP.lean
+++ b/Complexity/Computability/Complexity/Classes/BPP.lean
@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Computability.Complexity.Classes.P
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Encoding
@@ -44,6 +45,7 @@ The probability is written as a count over the random strings, which are functio
   with bounded error.
 * `Cslib.Complexity.compl_mem_BPP`, `Cslib.Complexity.BPP_eq_preimage_compl_BPP`: `BPP` is closed
   under complement.
+* `Cslib.Complexity.P_subset_BPP`: a decider is a bounded-error verifier ignoring its random string.
 
 ## References
 
@@ -111,4 +113,14 @@ theorem BPP_eq_preimage_compl_BPP (enc : α ↪ List Bool) : BPP enc = compl ⁻
   refine ⟨compl_mem_BPP, fun hA => ?_⟩
   simpa using compl_mem_BPP hA
 
+/-- **`P ⊆ BPP`**: a decider is a bounded-error verifier ignoring its random string, of length
+`0`. -/
+theorem P_subset_BPP {enc : α ↪ List Bool} : P enc ⊆ BPP enc := by
+  rintro A ⟨f, hf, hA⟩
+  refine ⟨0, fun x => f x.1, hf.comp (.fst enc encBits),
+    fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩
+  · simp [(hA a).mp ha]
+  · have : f a = false := by simpa [hA a] using ha
+    simp [this]
+
 end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Classes/BPP/Collapse.lean b/Complexity/Computability/Complexity/Classes/BPP/Collapse.lean
index c167b13ce0..8f838ab156 100644
--- a/Complexity/Computability/Complexity/Classes/BPP/Collapse.lean
+++ b/Complexity/Computability/Complexity/Classes/BPP/Collapse.lean
@@ -10,7 +10,6 @@ module
 public import Complexity.Computability.Complexity.Classes.BPP
 public import Complexity.Computability.Complexity.Classes.NP
 public import Complexity.Computability.Complexity.Classes.P
-import Complexity.Computability.Complexity.Classes.Inclusions
 import Complexity.Computability.Complexity.Classes.PH.Collapse
 import Complexity.Computability.Complexity.Classes.PH.SipserLautemann
 
diff --git a/Complexity/Computability/Complexity/Classes/BPP/Derandomization.lean b/Complexity/Computability/Complexity/Classes/BPP/Derandomization.lean
index 90e9c59894..dea789eb46 100644
--- a/Complexity/Computability/Complexity/Classes/BPP/Derandomization.lean
+++ b/Complexity/Computability/Complexity/Classes/BPP/Derandomization.lean
@@ -15,7 +15,6 @@ public import Complexity.Computability.Languages.Slice
 import Complexity.Computability.Circuit.Boolean.PolynomialTime
 import Complexity.Computability.Circuit.Boolean.Substitution
 import Complexity.Computability.Complexity.Classes.BPP.Derandomization.Generator
-import Complexity.Computability.Complexity.Classes.Inclusions
 import Complexity.Foundations.Data.Nat.PolynomialBound.Log
 import Complexity.Tactic.PolyTime
 
diff --git a/Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean b/Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean
index 0da74bec24..d296bed9ac 100644
--- a/Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean
+++ b/Complexity/Computability/Complexity/Classes/BPP/WorstCaseHardness.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Classes.BPP.Derandomization
 public import Complexity.Computability.Complexity.HardnessEncoding.PolyTime
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.BPP
 
 /-!
 # `P = BPP` from exponential worst-case circuit lower bounds
diff --git a/Complexity/Computability/Complexity/Classes/Counting/Space.lean b/Complexity/Computability/Complexity/Classes/Counting/Space.lean
index 7bd1aebd7b..5f9a7ee4ca 100644
--- a/Complexity/Computability/Complexity/Classes/Counting/Space.lean
+++ b/Complexity/Computability/Complexity/Classes/Counting/Space.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.SharpP.Space
 public import Complexity.Computability.Complexity.Classes.ModP
 public import Complexity.Computability.Complexity.Classes.PP.Characterization
-public import Complexity.Computability.Complexity.Classes.Inclusions
+public import Complexity.Computability.Complexity.Classes.Space.Closure
 public import Complexity.Computability.Complexity.Classes.Oracle.Space
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
diff --git a/Complexity/Computability/Complexity/Classes/Inclusions.lean b/Complexity/Computability/Complexity/Classes/Inclusions.lean
index 911530c9ec..5302eacba6 100644
--- a/Complexity/Computability/Complexity/Classes/Inclusions.lean
+++ b/Complexity/Computability/Complexity/Classes/Inclusions.lean
@@ -9,8 +9,9 @@ module
 
 public import Complexity.Computability.Complexity.Classes.EXP
 public import Complexity.Computability.Complexity.Classes.PH
-public import Complexity.Computability.Complexity.Classes.PP
+public import Complexity.Computability.Complexity.Classes.PP.Closure
 public import Complexity.Computability.Complexity.Reduction
+public import Complexity.Computability.Complexity.Classes.Space.Closure
 public import Complexity.Computability.Complexity.Classes.Space.Savitch
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
@@ -25,7 +26,11 @@ import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 # Inclusions between complexity classes
 
 The inclusions between the standard classes that papers cite in their preliminaries
-[Arora and Barak, Chapters 2, 4, 5 and 7][AroraBarak09], [Sipser, Chapters 8 and 10][Sipser2013]:
+[Arora and Barak, Chapters 2, 4, 5 and 7][AroraBarak09], [Sipser, Chapters 8 and 10][Sipser2013].
+This module proves the inclusions that need several classes at once and imports the narrower
+modules for the others: `P ⊆ BPP` is in `Complexity.Computability.Complexity.Classes.BPP`, the
+closure properties of `PP` in `Complexity.Computability.Complexity.Classes.PP.Closure`, and those
+of `PSPACE` in `Complexity.Computability.Complexity.Classes.Space.Closure`.
 
 * `P ⊆ BPP` (`Cslib.Complexity.P_subset_BPP`): a decider ignores its random string.
 * `NP ⊆ PP` (`Cslib.Complexity.NP_subset_PP`): accept on half of the random strings outright, and
@@ -60,18 +65,11 @@ inclusions of the chains are elsewhere: `P ⊆ PSPACE` (`Cslib.Complexity.P_subs
 
 ## Main results
 
-* `Cslib.Complexity.P_subset_BPP`, `Cslib.Complexity.NP_subset_PP`.
-* `Cslib.Complexity.compl_mem_PP`, `Cslib.Complexity.PP_eq_preimage_compl_PP`.
-* `Cslib.Complexity.coNP_subset_PP`.
 * `Turing.MultiTapeNTM.RunsInTime.runsInSpace`: space is at most time.
 * `Turing.MultiTapeNTM.DecidesInTime.decidesInSpace`: a time-bounded decider is a space-bounded
   one.
 * `Cslib.Complexity.NP_subset_NPSPACE`, `Cslib.Complexity.NP_subset_PSPACE`.
 * `Cslib.Complexity.PSPACE_subset_EXP`, `Cslib.Complexity.NP_subset_EXP`.
-* `Cslib.Complexity.mem_PSPACE_iff_computableTidilyInO`: `PSPACE` in the quantitative calculus.
-* `Cslib.Complexity.mem_PSPACE_iff_computableTidilyInPolySpace`: `PSPACE` within polynomial space.
-* `Cslib.Complexity.compl_mem_PSPACE`, `Cslib.Complexity.PolyTimeReducible.mem_PSPACE`,
-  `Cslib.Complexity.setOf_exists_mem_PSPACE`: closure properties of `PSPACE`.
 * `Cslib.Complexity.SigmaP_subset_PSPACE`, `Cslib.Complexity.PH_subset_PSPACE`.
 * `Cslib.Complexity.SigmaP_subset_EXP`, `Cslib.Complexity.SigmaP_subset_NEXP`.
 
@@ -133,107 +131,6 @@ open _root_.Turing _root_.Turing.MultiTapeTM Filter
 
 variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 
-/-! ### Probabilistic classes -/
-
-/-- **`P ⊆ BPP`**: a decider is a bounded-error verifier ignoring its random string, of length
-`0`. -/
-theorem P_subset_BPP : P enc ⊆ BPP enc := by
-  rintro A ⟨f, hf, hA⟩
-  refine ⟨0, fun x => f x.1, hf.comp (.fst enc encBits),
-    fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩
-  · simp [(hA a).mp ha]
-  · have : f a = false := by simpa [hA a] using ha
-    simp [this]
-
-/-- Counting the words of length `n + 1` by their first bit. -/
-private theorem card_filter_ofFn_succ (n : ℕ) (P : List Bool → Prop) [DecidablePred P] :
-    (Finset.univ.filter fun r : Fin (n + 1) → Bool => P (List.ofFn r)).card =
-      (Finset.univ.filter fun w : Fin n → Bool => P (false :: List.ofFn w)).card +
-        (Finset.univ.filter fun w : Fin n → Bool => P (true :: List.ofFn w)).card := by
-  simp only [Finset.card_filter]
-  rw [← (Fin.consEquiv fun _ : Fin (n + 1) => Bool).sum_comp, Fintype.sum_prod_type,
-    Fintype.sum_bool, add_comm]
-  simp [List.ofFn_succ, Fin.consEquiv]
-
-/-- **`NP ⊆ PP`** [Gill][Gill1977]: on random strings `b :: w`, accept when `b = false` and run
-the verifier on `w` when `b = true`. The majority accepts exactly when the verifier accepts some
-certificate. -/
-theorem NP_subset_PP : NP enc ⊆ PP enc := by
-  rintro A ⟨p, V, hV, hA⟩
-  let V' (x : α × List Bool) : Bool := !(x.2.headD false) || V (x.1, x.2.tail)
-  have hV' : ComputableTidilyInPolyTime V' (encPair enc encBits) encBool :=
-    ComputableTidilyInPolyTime.bool_or.comp
-      ((ComputableTidilyInPolyTime.bool_not.comp
-        ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp (.snd _ _))).prod
-        (hV.tidy.comp ((ComputableTidilyInPolyTime.fst _ _).prod
-          (ComputableTidilyInPolyTime.bitsTail.comp (.snd _ _)))))
-  refine ⟨p + 1, V', .of_tidy hV', fun a => ?_⟩
-  have hcount (m : ℕ) : acceptCount V' a (m + 1) = 2 ^ m + acceptCount V a m := by
-    rw [acceptCount, card_filter_ofFn_succ m fun l => V' (a, l) = true]
-    simp [V', acceptCount]
-  have heval : (p + 1).eval (enc a).length = p.eval (enc a).length + 1 := by simp
-  rw [heval, hcount, hA a, ← acceptCount_pos_iff, pow_succ]
-  omega
-
-/-- **`PP` is closed under complement** [Gill][Gill1977]. On random strings `b₁ :: b₂ :: w`,
-accept when `b₁ = b₂ = false` and on `b₁ = false, b₂ = true` only for `w` all zeros, and reject
-what the verifier accepts on `w` when `b₁ = true`. With `acc` accepted and `rej` rejected strings
-of length `m`, this accepts `2 ^ m + 1 + 2 * rej` of the `4 * 2 ^ m` strings, more than half
-exactly when `2 * acc ≤ 2 ^ m`. -/
-theorem compl_mem_PP (hA : A ∈ PP enc) : Aᶜ ∈ PP enc := by
-  rw [mem_PP_iff_tidy] at hA ⊢
-  obtain ⟨p, V, hV, hA⟩ := hA
-  let V' (x : α × List Bool) : Bool :=
-    if x.2.headD false then !V (x.1, x.2.tail.tail)
-    else !(x.2.tail.headD false) || !(x.2.tail.tail.any fun b => b)
-  have hV' : ComputableTidilyInPolyTime V' (encPair enc encBits) encBool := by
-    have hw : ComputableTidilyInPolyTime (fun x : α × List Bool => x.2.tail.tail)
-        (encPair enc encBits) encBits :=
-      ComputableTidilyInPolyTime.bitsTail.comp
-        (ComputableTidilyInPolyTime.bitsTail.comp (.snd _ _))
-    exact ComputableTidilyInPolyTime.cond
-      ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp (.snd _ _))
-      (ComputableTidilyInPolyTime.bool_not.comp
-        (hV.comp ((ComputableTidilyInPolyTime.fst _ _).prod hw)))
-      (ComputableTidilyInPolyTime.bool_or.comp
-        ((ComputableTidilyInPolyTime.bool_not.comp
-          ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp
-            (ComputableTidilyInPolyTime.bitsTail.comp (.snd _ _)))).prod
-          (ComputableTidilyInPolyTime.bool_not.comp
-            (ComputableTidilyInPolyTime.bitsAnyWithInput (test := fun _ b => b) hw
-              (.snd _ _)))))
-  refine ⟨p + 2, V', hV', fun a => ?_⟩
-  -- exactly one word of length `m` is all zeros
-  have hzero (m : ℕ) : (Finset.univ.filter fun w : Fin m → Bool =>
-      ((List.ofFn w).any fun b => b) = false).card = 1 := by
-    refine Finset.card_eq_one.mpr ⟨fun _ => false, Finset.ext fun w => ?_⟩
-    simp only [Finset.mem_filter, Finset.mem_univ, true_and, List.any_eq_false, List.mem_ofFn,
-      forall_exists_index, forall_apply_eq_imp_iff, Finset.mem_singleton, Bool.not_eq_true]
-    exact ⟨fun h => funext h, fun h i => by rw [h]⟩
-  have hcount (m : ℕ) : acceptCount V' a (m + 1 + 1) = 2 ^ m + 1 +
-      2 * (Finset.univ.filter fun w : Fin m → Bool => V (a, List.ofFn w) = false).card := by
-    rw [acceptCount, card_filter_ofFn_succ (m + 1) fun l => V' (a, l) = true,
-      card_filter_ofFn_succ m fun l => V' (a, false :: l) = true,
-      card_filter_ofFn_succ m fun l => V' (a, true :: l) = true]
-    simp only [V', List.headD_cons, List.tail_cons, Bool.false_eq_true, ↓reduceIte, Bool.not_false,
-      Bool.true_or, Bool.not_true, Bool.false_or, Finset.filter_true, Finset.card_univ,
-      Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, Bool.not_eq_true', hzero]
-    ring
-  have heval : (p + 2).eval (enc a).length = p.eval (enc a).length + 1 + 1 := by simp
-  have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length)
-  rw [heval, hcount, Set.mem_compl_iff, hA a, pow_succ, pow_succ]
-  omega
-
-/-- `PP` equals its preimage under complement. -/
-theorem PP_eq_preimage_compl_PP (enc : α ↪ List Bool) : PP enc = compl ⁻¹' PP enc := by
-  ext A
-  refine ⟨compl_mem_PP, fun hA => ?_⟩
-  simpa using compl_mem_PP hA
-
-/-- **`coNP ⊆ PP`**: `NP ⊆ PP` and `PP` is closed under complement. -/
-theorem coNP_subset_PP : coNP enc ⊆ PP enc := fun _ hA => by
-  simpa using compl_mem_PP (NP_subset_PP hA)
-
 /-! ### Space -/
 
 /-- **`NP ⊆ NPSPACE`**: a nondeterministic machine deciding a problem in polynomial time visits at
@@ -343,184 +240,6 @@ theorem PSPACE_subset_EXP : PSPACE enc ⊆ EXP enc := by
 theorem NP_subset_EXP : NP enc ⊆ EXP enc :=
   NP_subset_PSPACE.trans PSPACE_subset_EXP
 
-/-! ### Closure properties of `PSPACE` -/
-
-/-- **`PSPACE` in the quantitative calculus**: a problem is in `PSPACE` exactly when a Boolean
-function deciding it is tidily computable within some time and within space polynomial in the
-length of the encoded instance. -/
-theorem mem_PSPACE_iff_computableTidilyInO : A ∈ PSPACE enc ↔ ∃ (f : α → Bool) (T S : α → ℕ),
-    ComputableTidilyInO f enc encBool T S ∧ PolyBounded (fun a => (enc a).length) S ∧
-      ∀ a, a ∈ A ↔ f a = true := by
-  constructor
-  · rintro ⟨f, ⟨t, s, hs, hf⟩, hA⟩
-    obtain ⟨c, hc⟩ := ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace hf
-    exact ⟨f, fun a => 2 * t a + 3 * s a + c, s, .of_bounds hc (c + 1) (fun a => by nlinarith)
-      (fun a => by nlinarith) fun a => by
-        simp only [encBool_apply, List.length_singleton]
-        exact Nat.mul_pos (Nat.succ_pos c) (Nat.succ_pos (s a)),
-      hs, hA⟩
-  · rintro ⟨f, T, S, ⟨c, hc, -⟩, hS, hA⟩
-    exact ⟨f, ⟨_, _, (PolyBounded.const c).mul (hS.add (.const 1)), hc.computableInTimeAndSpace⟩,
-      hA⟩
-
-/-- **`PSPACE` within polynomial space**: a problem is in `PSPACE` exactly when a Boolean function
-deciding it is tidily computable within space polynomial in the length of the encoded instance
-(`Turing.MultiTapeTM.ComputableTidilyInPolySpace`). -/
-theorem mem_PSPACE_iff_computableTidilyInPolySpace : A ∈ PSPACE enc ↔
-    ∃ f : α → Bool, ComputableTidilyInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true := by
-  rw [mem_PSPACE_iff_computableTidilyInO]
-  constructor
-  · rintro ⟨f, T, S, hf, hS, hA⟩
-    exact ⟨f, ⟨T, S, hS, hf⟩, hA⟩
-  · rintro ⟨f, ⟨T, S, hS, hf⟩, hA⟩
-    exact ⟨f, T, S, hf, hS, hA⟩
-
-/-- A Boolean function computable within polynomial space decides a problem in `PSPACE`. -/
-theorem mem_PSPACE_of_computableTidilyInPolySpace {f : α → Bool}
-    (hf : ComputableTidilyInPolySpace f enc encBool) (hA : ∀ a, a ∈ A ↔ f a = true) :
-    A ∈ PSPACE enc :=
-  mem_PSPACE_iff_computableTidilyInPolySpace.mpr ⟨f, hf, hA⟩
-
-/-- **`PSPACE` is closed under complement**: negate the answer. -/
-theorem compl_mem_PSPACE (hA : A ∈ PSPACE enc) : Aᶜ ∈ PSPACE enc := by
-  obtain ⟨f, T, S, hf, hS, hA⟩ := mem_PSPACE_iff_computableTidilyInO.mp hA
-  have hnot := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
-    Bool.not).inO_one.comp_linear hf
-  refine mem_PSPACE_iff_computableTidilyInO.mpr ⟨_, T, S, hnot, hS, fun a => ?_⟩
-  simp [hA a]
-
-/-- **`PSPACE` is closed under polynomial-time reductions.** -/
-theorem PolyTimeReducible.mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set β}
-    (h : PolyTimeReducible enc encB A B) (hB : B ∈ PSPACE encB) : A ∈ PSPACE enc := by
-  obtain ⟨g, hg, hAB⟩ := h
-  obtain ⟨f, T, S, hf, hS, hB⟩ := mem_PSPACE_iff_computableTidilyInO.mp hB
-  obtain ⟨Tg, Sg, hSg, hgO⟩ := ComputableTidilyInPolySpace.of_polyTime hg.tidy
-  exact mem_PSPACE_iff_computableTidilyInO.mpr ⟨f ∘ g, _, _, hf.comp hgO,
-    hSg.add (hS.comp hg.polyBounded_length), fun a => (hAB a).trans (hB (g a))⟩
-
-/-- The edges of the graph on words of width `n + 1` whose reachability within two steps from the
-all-zero word to the all-one word is a bounded existential over `f`: an edge from the all-zero word
-to `true :: w` when `f (x, w)`, and from every word starting with `true` to the all-one word. -/
-private def existsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (u v : List Bool) : Bool :=
-  if !(u.any fun b => b) && v.headD false then f (x, v.tail)
-  else u.headD false && !(v.any fun b => !b)
-
-/-- Savitch's algorithm at depth `1` on the edges of `existsEdge` decides the bounded
-existential. -/
-private theorem savitch_existsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (n : ℕ) :
-    Cslib.Reachability.savitch (existsEdge f x) (n + 1) 1 (List.replicate (n + 1) false)
-      (List.replicate (n + 1) true) = true ↔ ∃ w : List Bool, w.length = n ∧ f (x, w) = true := by
-  rw [Cslib.Reachability.savitch_eq]
-  simp only [Cslib.Reachability.reach, List.any_eq_true, Cslib.BitString.mem_enumList,
-    Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq]
-  constructor
-  · rintro ⟨m, hm, h₁ | h₁, h₂ | h₂⟩
-    · subst h₁
-      exact absurd h₂ (by simp [List.replicate_succ])
-    · subst h₁
-      refine ⟨List.replicate n true, List.length_replicate .., ?_⟩
-      simpa [existsEdge, List.replicate_succ] using h₂
-    · subst h₂
-      refine ⟨List.replicate n true, List.length_replicate .., ?_⟩
-      simpa [existsEdge, List.replicate_succ] using h₁
-    · obtain ⟨b, w, rfl⟩ := List.exists_cons_of_length_eq_add_one hm
-      refine ⟨w, by simpa using hm, ?_⟩
-      cases b <;> simp_all [existsEdge, List.replicate_succ]
-  · rintro ⟨w, hw, hf⟩
-    refine ⟨true :: w, by simp [hw], Or.inr ?_, Or.inr ?_⟩
-    · simp [existsEdge, List.replicate_succ, hf]
-    · simp [existsEdge, List.replicate_succ]
-
-/-- **`PSPACE` is closed under polynomially bounded existential quantification**: if `B ⊆ β × List
-Bool` is in `PSPACE` and `ℓ` is polynomial-time, then so is the set of the `x` for which some word
-`w` of length `ℓ x` has `(x, w) ∈ B`. The candidates are enumerated in place: this is reachability
-within two steps between two words of width `ℓ x + 1` (`existsEdge`), which Savitch's algorithm
-decides at depth `1`, reusing the space of the decider of `B` for every candidate
-(`Cslib.Reachability.computableTidilyInO_savitch`). -/
-theorem setOf_exists_mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set (β × List Bool)}
-    {ℓ : β → ℕ} (hB : B ∈ PSPACE (encPair encB encBits))
-    (hℓ : ComputableTidilyInPolyTime ℓ encB encUnary) :
-    {x | ∃ w : List Bool, w.length = ℓ x ∧ (x, w) ∈ B} ∈ PSPACE encB := by
-  obtain ⟨f, T, S, hf, hS, hB⟩ := mem_PSPACE_iff_computableTidilyInO.mp hB
-  set encQ := encPair encB (encPair encBits encBits)
-  -- the edge test: polynomial-time tests around one call of the decider of `B`
-  have hg : ComputableTidilyInPolyTime (fun q : β × List Bool × List Bool => (q.1, q.2.2.tail))
-      encQ (encPair encB encBits) :=
-    (ComputableTidilyInPolyTime.fst _ _).prod
-      (ComputableTidilyInPolyTime.bitsTail.comp
-        ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _)))
-  have hc : ComputableTidilyInPolyTime
-      (fun q : β × List Bool × List Bool => !(q.2.1.any fun b => b) && q.2.2.headD false)
-      encQ encBool :=
-    ComputableTidilyInPolyTime.bool_and.comp
-      ((ComputableTidilyInPolyTime.bool_not.comp
-        (ComputableTidilyInPolyTime.bitsAnyWithInput (test := fun _ b => b)
-          ((ComputableTidilyInPolyTime.fst _ _).comp (.snd _ _)) (.snd _ _))).prod
-        ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp
-          ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _))))
-  have he : ComputableTidilyInPolyTime
-      (fun q : β × List Bool × List Bool => q.2.1.headD false && !(q.2.2.any fun b => !b))
-      encQ encBool :=
-    ComputableTidilyInPolyTime.bool_and.comp
-      (((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp
-        ((ComputableTidilyInPolyTime.fst _ _).comp (.snd _ _))).prod
-        (ComputableTidilyInPolyTime.bool_not.comp
-          (ComputableTidilyInPolyTime.bitsAnyWithInput (test := fun _ b => !b)
-            ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _))
-            (ComputableTidilyInPolyTime.bool_not.comp (.snd _ _)))))
-  obtain ⟨Tg, Sg, hSg, hgO⟩ := ComputableTidilyInPolySpace.of_polyTime hg
-  obtain ⟨Tc, Sc, hSc, hcO⟩ := ComputableTidilyInPolySpace.of_polyTime hc
-  obtain ⟨Te, Se, hSe, heO⟩ := ComputableTidilyInPolySpace.of_polyTime he
-  have hedge := hcO.ite (hf.comp hgO) heO
-  -- the arguments of Savitch's algorithm
-  have hin : ComputableTidilyInPolyTime
-      (fun x => (x, ℓ x + 1, 1, List.replicate (ℓ x + 1) false, List.replicate (ℓ x + 1) true))
-      encB (Cslib.Reachability.encArgs encB) := by
-    have hw : ComputableTidilyInPolyTime (fun x => ℓ x + 1) encB encUnary :=
-      ComputableTidilyInPolyTime.unary_add.comp (hℓ.prod (.const 1))
-    exact ComputableTidilyInPolyTime.id'.prod (hw.prod ((ComputableTidilyInPolyTime.const 1).prod
-      (((ComputableTidilyInPolyTime.bitsReplicate false).comp hw).prod
-        ((ComputableTidilyInPolyTime.bitsReplicate true).comp hw))))
-  obtain ⟨Ti, Si, hSi, hinO⟩ := ComputableTidilyInPolySpace.of_polyTime hin
-  have h := Cslib.Reachability.computableTidilyInO_savitch (edge := existsEdge f) (par := id)
-    hedge hinO (fun _ => List.length_replicate ..) fun _ => List.length_replicate ..
-  -- the space is polynomial
-  have hSedge : PolyBounded (fun q => (encQ q).length) fun q =>
-      Sc q + if !(q.2.1.any fun b => b) && q.2.2.headD false then Sg q + S (q.1, q.2.2.tail)
-        else Se q :=
-    (hSc.add (hSg.add (hS.comp hg.polyBounded_length) |>.add hSe)).mono fun q => by
-      split_ifs <;> omega
-  obtain ⟨cE, dE, hcE⟩ := hSedge.exists_le
-  have hℓ' : PolyBounded (fun x => (encB x).length) ℓ :=
-    hℓ.polyBounded_length.mono fun x => by simp [encUnary_apply]
-  have hG : PolyBounded (fun x => (encB x).length)
-      fun x => 2 * (encB x).length + 3 * ℓ x + 6 :=
-    (((PolyBounded.const 2).mul .self).add ((PolyBounded.const 3).mul hℓ')).add (.const 6)
-  have hpow : PolyBounded (fun x => (encB x).length)
-      fun x => cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE :=
-    PolyBounded.comp (size' := id) (v := fun n => cE * n ^ dE)
-      (PolyBounded.of_polynomiallyBounded (bound := fun n => cE * n ^ dE) id (by fun_prop)) hG
-  refine mem_PSPACE_iff_computableTidilyInO.mpr ⟨_, _, _, h, ?_, fun x => ?_⟩
-  · refine (((hSi.add ((PolyBounded.const 2).mul (hℓ'.add (.const 3)))).add .self).add
-      hpow).mono fun x => ?_
-    have hmax : Cslib.Reachability.edgeMax (fun q : β × List Bool × List Bool =>
-        Sc q + if (!(q.2.1.any fun b => b) && q.2.2.headD false) = true then
-          Sg q + S (q.1, q.2.2.tail) else Se q) x (ℓ x + 1) ≤
-        cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE :=
-      listMax_le fun u hu => listMax_le fun v hv => by
-        refine (hcE _).trans (Nat.mul_le_mul_left cE (Nat.pow_le_pow_left ?_ dE))
-        simp only [encQ, length_encPair, encBits_apply, Cslib.BitString.mem_enumList.mp hu,
-          Cslib.BitString.mem_enumList.mp hv]
-        omega
-    change Si x + (1 + 1) * (1 + (ℓ x + 1) + 1) + (encB x).length +
-        Cslib.Reachability.edgeMax (fun q : β × List Bool × List Bool =>
-          Sc q + if (!(q.2.1.any fun b => b) && q.2.2.headD false) = true then
-            Sg q + S (q.1, q.2.2.tail) else Se q) x (ℓ x + 1) ≤
-      Si x + 2 * (ℓ x + 3) + (encB x).length + cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE
-    omega
-  · simp only [Set.mem_ofPred_eq, hB, id]
-    exact (savitch_existsEdge f x (ℓ x)).symm
-
 /-! ### The polynomial hierarchy -/
 
 /-- The pairs `(a, u)` from which alternating quantifiers over blocks of certificates of the
diff --git a/Complexity/Computability/Complexity/Classes/PP/Characterization.lean b/Complexity/Computability/Complexity/Classes/PP/Characterization.lean
index 5296b62bcc..7fc7e3ac43 100644
--- a/Complexity/Computability/Complexity/Classes/PP/Characterization.lean
+++ b/Complexity/Computability/Complexity/Classes/PP/Characterization.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Classes.PP
 public import Complexity.Computability.Complexity.Reduction
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.PP.Closure
 import Complexity.Computability.Complexity.Classes.SharpP.Closure
 import Complexity.Computability.Complexity.Classes.SharpP.Combinators
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
diff --git a/Complexity/Computability/Complexity/Classes/PP/Closure.lean b/Complexity/Computability/Complexity/Classes/PP/Closure.lean
new file mode 100644
index 0000000000..2249247544
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/PP/Closure.lean
@@ -0,0 +1,134 @@
+/-
+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.NP
+public import Complexity.Computability.Complexity.Classes.PP
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+
+/-!
+# Closure properties of `PP`
+
+`PP` contains `NP` [Gill][Gill1977]: on random strings `b :: w`, accept when `b = false` and run the
+verifier on `w` when `b = true`, so the majority accepts exactly when some certificate does. `PP` is
+closed under complement [Gill][Gill1977]: with two more random bits, accept on a quarter of the
+random strings and one more, and on half of them reject what the verifier accepts; the majority
+accepts exactly when the verifier accepts at most half of its random strings. Hence also
+`coNP ⊆ PP`.
+
+## Main results
+
+* `Cslib.Complexity.NP_subset_PP`, `Cslib.Complexity.coNP_subset_PP`.
+* `Cslib.Complexity.compl_mem_PP`, `Cslib.Complexity.PP_eq_preimage_compl_PP`: closure under
+  complement.
+
+## References
+
+* [J. Gill, *Computational complexity of probabilistic Turing machines*][Gill1977]
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity
+
+open _root_.Turing _root_.Turing.MultiTapeTM
+
+variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
+
+/-- Counting the words of length `n + 1` by their first bit. -/
+private theorem card_filter_ofFn_succ (n : ℕ) (P : List Bool → Prop) [DecidablePred P] :
+    (Finset.univ.filter fun r : Fin (n + 1) → Bool => P (List.ofFn r)).card =
+      (Finset.univ.filter fun w : Fin n → Bool => P (false :: List.ofFn w)).card +
+        (Finset.univ.filter fun w : Fin n → Bool => P (true :: List.ofFn w)).card := by
+  simp only [Finset.card_filter]
+  rw [← (Fin.consEquiv fun _ : Fin (n + 1) => Bool).sum_comp, Fintype.sum_prod_type,
+    Fintype.sum_bool, add_comm]
+  simp [List.ofFn_succ, Fin.consEquiv]
+
+/-- **`NP ⊆ PP`** [Gill][Gill1977]: on random strings `b :: w`, accept when `b = false` and run
+the verifier on `w` when `b = true`. The majority accepts exactly when the verifier accepts some
+certificate. -/
+theorem NP_subset_PP : NP enc ⊆ PP enc := by
+  rintro A ⟨p, V, hV, hA⟩
+  let V' (x : α × List Bool) : Bool := !(x.2.headD false) || V (x.1, x.2.tail)
+  have hV' : ComputableTidilyInPolyTime V' (encPair enc encBits) encBool :=
+    ComputableTidilyInPolyTime.bool_or.comp
+      ((ComputableTidilyInPolyTime.bool_not.comp
+        ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp (.snd _ _))).prod
+        (hV.tidy.comp ((ComputableTidilyInPolyTime.fst _ _).prod
+          (ComputableTidilyInPolyTime.bitsTail.comp (.snd _ _)))))
+  refine ⟨p + 1, V', .of_tidy hV', fun a => ?_⟩
+  have hcount (m : ℕ) : acceptCount V' a (m + 1) = 2 ^ m + acceptCount V a m := by
+    rw [acceptCount, card_filter_ofFn_succ m fun l => V' (a, l) = true]
+    simp [V', acceptCount]
+  have heval : (p + 1).eval (enc a).length = p.eval (enc a).length + 1 := by simp
+  rw [heval, hcount, hA a, ← acceptCount_pos_iff, pow_succ]
+  omega
+
+/-- **`PP` is closed under complement** [Gill][Gill1977]. On random strings `b₁ :: b₂ :: w`,
+accept when `b₁ = b₂ = false` and on `b₁ = false, b₂ = true` only for `w` all zeros, and reject
+what the verifier accepts on `w` when `b₁ = true`. With `acc` accepted and `rej` rejected strings
+of length `m`, this accepts `2 ^ m + 1 + 2 * rej` of the `4 * 2 ^ m` strings, more than half
+exactly when `2 * acc ≤ 2 ^ m`. -/
+theorem compl_mem_PP (hA : A ∈ PP enc) : Aᶜ ∈ PP enc := by
+  rw [mem_PP_iff_tidy] at hA ⊢
+  obtain ⟨p, V, hV, hA⟩ := hA
+  let V' (x : α × List Bool) : Bool :=
+    if x.2.headD false then !V (x.1, x.2.tail.tail)
+    else !(x.2.tail.headD false) || !(x.2.tail.tail.any fun b => b)
+  have hV' : ComputableTidilyInPolyTime V' (encPair enc encBits) encBool := by
+    have hw : ComputableTidilyInPolyTime (fun x : α × List Bool => x.2.tail.tail)
+        (encPair enc encBits) encBits :=
+      ComputableTidilyInPolyTime.bitsTail.comp
+        (ComputableTidilyInPolyTime.bitsTail.comp (.snd _ _))
+    exact ComputableTidilyInPolyTime.cond
+      ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp (.snd _ _))
+      (ComputableTidilyInPolyTime.bool_not.comp
+        (hV.comp ((ComputableTidilyInPolyTime.fst _ _).prod hw)))
+      (ComputableTidilyInPolyTime.bool_or.comp
+        ((ComputableTidilyInPolyTime.bool_not.comp
+          ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp
+            (ComputableTidilyInPolyTime.bitsTail.comp (.snd _ _)))).prod
+          (ComputableTidilyInPolyTime.bool_not.comp
+            (ComputableTidilyInPolyTime.bitsAnyWithInput (test := fun _ b => b) hw
+              (.snd _ _)))))
+  refine ⟨p + 2, V', hV', fun a => ?_⟩
+  -- exactly one word of length `m` is all zeros
+  have hzero (m : ℕ) : (Finset.univ.filter fun w : Fin m → Bool =>
+      ((List.ofFn w).any fun b => b) = false).card = 1 := by
+    refine Finset.card_eq_one.mpr ⟨fun _ => false, Finset.ext fun w => ?_⟩
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and, List.any_eq_false, List.mem_ofFn,
+      forall_exists_index, forall_apply_eq_imp_iff, Finset.mem_singleton, Bool.not_eq_true]
+    exact ⟨fun h => funext h, fun h i => by rw [h]⟩
+  have hcount (m : ℕ) : acceptCount V' a (m + 1 + 1) = 2 ^ m + 1 +
+      2 * (Finset.univ.filter fun w : Fin m → Bool => V (a, List.ofFn w) = false).card := by
+    rw [acceptCount, card_filter_ofFn_succ (m + 1) fun l => V' (a, l) = true,
+      card_filter_ofFn_succ m fun l => V' (a, false :: l) = true,
+      card_filter_ofFn_succ m fun l => V' (a, true :: l) = true]
+    simp only [V', List.headD_cons, List.tail_cons, Bool.false_eq_true, ↓reduceIte, Bool.not_false,
+      Bool.true_or, Bool.not_true, Bool.false_or, Finset.filter_true, Finset.card_univ,
+      Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, Bool.not_eq_true', hzero]
+    ring
+  have heval : (p + 2).eval (enc a).length = p.eval (enc a).length + 1 + 1 := by simp
+  have hsum := acceptCount_add_card_filter_eq_false (V := V) (a := a) (n := p.eval (enc a).length)
+  rw [heval, hcount, Set.mem_compl_iff, hA a, pow_succ, pow_succ]
+  omega
+
+/-- `PP` equals its preimage under complement. -/
+theorem PP_eq_preimage_compl_PP (enc : α ↪ List Bool) : PP enc = compl ⁻¹' PP enc := by
+  ext A
+  refine ⟨compl_mem_PP, fun hA => ?_⟩
+  simpa using compl_mem_PP hA
+
+/-- **`coNP ⊆ PP`**: `NP ⊆ PP` and `PP` is closed under complement. -/
+theorem coNP_subset_PP : coNP enc ⊆ PP enc := fun _ hA => by
+  simpa using compl_mem_PP (NP_subset_PP hA)
+
+end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Classes/PP/TruthTable.lean b/Complexity/Computability/Complexity/Classes/PP/TruthTable.lean
index 5ba796259e..771caad248 100644
--- a/Complexity/Computability/Complexity/Classes/PP/TruthTable.lean
+++ b/Complexity/Computability/Complexity/Classes/PP/TruthTable.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.PP
 public import Complexity.Computability.Complexity.Classes.SharpP
 public import Complexity.Computability.Complexity.Reduction.TruthTable
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.PP.Closure
 import Complexity.Computability.Complexity.Classes.PP.Characterization
 import Complexity.Computability.Complexity.Classes.SharpP.Products
 import Complexity.Computability.Complexity.Classes.SharpP.PolyTime
diff --git a/Complexity/Computability/Complexity/Classes/Space/Closure.lean b/Complexity/Computability/Complexity/Classes/Space/Closure.lean
new file mode 100644
index 0000000000..dc0a519b5a
--- /dev/null
+++ b/Complexity/Computability/Complexity/Classes/Space/Closure.lean
@@ -0,0 +1,233 @@
+/-
+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.Space
+public import Complexity.Computability.Complexity.Reduction
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace
+import Complexity.Computability.Complexity.Classes.Space.Savitch
+import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
+
+/-!
+# Characterizations and closure properties of `PSPACE`
+
+A problem is in `PSPACE` exactly when a Boolean function deciding it is tidily computable within
+some time and space polynomial in the length of the encoded instance
+(`Cslib.Complexity.mem_PSPACE_iff_computableTidilyInO`,
+`Cslib.Complexity.mem_PSPACE_iff_computableTidilyInPolySpace`). `PSPACE` is closed under
+complement, under polynomial-time reductions, and under polynomially bounded existential
+quantification [Arora and Barak, Chapter 4][AroraBarak09]. The existential quantifier over the
+words `w` of length `ℓ` is reachability within two steps from the all-zero word to the all-one word
+of width `ℓ + 1`, along edges to `true :: w` for the accepted `w` and from every word starting with
+`true` to the all-one word; Savitch's algorithm decides it at depth `1`, enumerating the candidates
+in place and reusing the space of the decider for each.
+
+## Main results
+
+* `Cslib.Complexity.mem_PSPACE_iff_computableTidilyInO`: `PSPACE` in the quantitative calculus.
+* `Cslib.Complexity.mem_PSPACE_iff_computableTidilyInPolySpace`,
+  `Cslib.Complexity.mem_PSPACE_of_computableTidilyInPolySpace`: `PSPACE` within polynomial space.
+* `Cslib.Complexity.compl_mem_PSPACE`, `Cslib.Complexity.PolyTimeReducible.mem_PSPACE`,
+  `Cslib.Complexity.setOf_exists_mem_PSPACE`: closure properties of `PSPACE`.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09]
+* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013]
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity
+
+open _root_.Turing _root_.Turing.MultiTapeTM Filter
+
+variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
+
+
+/-- **`PSPACE` in the quantitative calculus**: a problem is in `PSPACE` exactly when a Boolean
+function deciding it is tidily computable within some time and within space polynomial in the
+length of the encoded instance. -/
+theorem mem_PSPACE_iff_computableTidilyInO : A ∈ PSPACE enc ↔ ∃ (f : α → Bool) (T S : α → ℕ),
+    ComputableTidilyInO f enc encBool T S ∧ PolyBounded (fun a => (enc a).length) S ∧
+      ∀ a, a ∈ A ↔ f a = true := by
+  constructor
+  · rintro ⟨f, ⟨t, s, hs, hf⟩, hA⟩
+    obtain ⟨c, hc⟩ := ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace hf
+    exact ⟨f, fun a => 2 * t a + 3 * s a + c, s, .of_bounds hc (c + 1) (fun a => by nlinarith)
+      (fun a => by nlinarith) fun a => by
+        simp only [encBool_apply, List.length_singleton]
+        exact Nat.mul_pos (Nat.succ_pos c) (Nat.succ_pos (s a)),
+      hs, hA⟩
+  · rintro ⟨f, T, S, ⟨c, hc, -⟩, hS, hA⟩
+    exact ⟨f, ⟨_, _, (PolyBounded.const c).mul (hS.add (.const 1)), hc.computableInTimeAndSpace⟩,
+      hA⟩
+
+/-- **`PSPACE` within polynomial space**: a problem is in `PSPACE` exactly when a Boolean function
+deciding it is tidily computable within space polynomial in the length of the encoded instance
+(`Turing.MultiTapeTM.ComputableTidilyInPolySpace`). -/
+theorem mem_PSPACE_iff_computableTidilyInPolySpace : A ∈ PSPACE enc ↔
+    ∃ f : α → Bool, ComputableTidilyInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true := by
+  rw [mem_PSPACE_iff_computableTidilyInO]
+  constructor
+  · rintro ⟨f, T, S, hf, hS, hA⟩
+    exact ⟨f, ⟨T, S, hS, hf⟩, hA⟩
+  · rintro ⟨f, ⟨T, S, hS, hf⟩, hA⟩
+    exact ⟨f, T, S, hf, hS, hA⟩
+
+/-- A Boolean function computable within polynomial space decides a problem in `PSPACE`. -/
+theorem mem_PSPACE_of_computableTidilyInPolySpace {f : α → Bool}
+    (hf : ComputableTidilyInPolySpace f enc encBool) (hA : ∀ a, a ∈ A ↔ f a = true) :
+    A ∈ PSPACE enc :=
+  mem_PSPACE_iff_computableTidilyInPolySpace.mpr ⟨f, hf, hA⟩
+
+/-- **`PSPACE` is closed under complement**: negate the answer. -/
+theorem compl_mem_PSPACE (hA : A ∈ PSPACE enc) : Aᶜ ∈ PSPACE enc := by
+  obtain ⟨f, T, S, hf, hS, hA⟩ := mem_PSPACE_iff_computableTidilyInO.mp hA
+  have hnot := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool)
+    Bool.not).inO_one.comp_linear hf
+  refine mem_PSPACE_iff_computableTidilyInO.mpr ⟨_, T, S, hnot, hS, fun a => ?_⟩
+  simp [hA a]
+
+/-- **`PSPACE` is closed under polynomial-time reductions.** -/
+theorem PolyTimeReducible.mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set β}
+    (h : PolyTimeReducible enc encB A B) (hB : B ∈ PSPACE encB) : A ∈ PSPACE enc := by
+  obtain ⟨g, hg, hAB⟩ := h
+  obtain ⟨f, T, S, hf, hS, hB⟩ := mem_PSPACE_iff_computableTidilyInO.mp hB
+  obtain ⟨Tg, Sg, hSg, hgO⟩ := ComputableTidilyInPolySpace.of_polyTime hg.tidy
+  exact mem_PSPACE_iff_computableTidilyInO.mpr ⟨f ∘ g, _, _, hf.comp hgO,
+    hSg.add (hS.comp hg.polyBounded_length), fun a => (hAB a).trans (hB (g a))⟩
+
+/-- The edges of the graph on words of width `n + 1` whose reachability within two steps from the
+all-zero word to the all-one word is a bounded existential over `f`: an edge from the all-zero word
+to `true :: w` when `f (x, w)`, and from every word starting with `true` to the all-one word. -/
+private def existsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (u v : List Bool) : Bool :=
+  if !(u.any fun b => b) && v.headD false then f (x, v.tail)
+  else u.headD false && !(v.any fun b => !b)
+
+/-- Savitch's algorithm at depth `1` on the edges of `existsEdge` decides the bounded
+existential. -/
+private theorem savitch_existsEdge {β : Type} (f : β × List Bool → Bool) (x : β) (n : ℕ) :
+    Cslib.Reachability.savitch (existsEdge f x) (n + 1) 1 (List.replicate (n + 1) false)
+      (List.replicate (n + 1) true) = true ↔ ∃ w : List Bool, w.length = n ∧ f (x, w) = true := by
+  rw [Cslib.Reachability.savitch_eq]
+  simp only [Cslib.Reachability.reach, List.any_eq_true, Cslib.BitString.mem_enumList,
+    Bool.and_eq_true, Bool.or_eq_true, decide_eq_true_eq]
+  constructor
+  · rintro ⟨m, hm, h₁ | h₁, h₂ | h₂⟩
+    · subst h₁
+      exact absurd h₂ (by simp [List.replicate_succ])
+    · subst h₁
+      refine ⟨List.replicate n true, List.length_replicate .., ?_⟩
+      simpa [existsEdge, List.replicate_succ] using h₂
+    · subst h₂
+      refine ⟨List.replicate n true, List.length_replicate .., ?_⟩
+      simpa [existsEdge, List.replicate_succ] using h₁
+    · obtain ⟨b, w, rfl⟩ := List.exists_cons_of_length_eq_add_one hm
+      refine ⟨w, by simpa using hm, ?_⟩
+      cases b <;> simp_all [existsEdge, List.replicate_succ]
+  · rintro ⟨w, hw, hf⟩
+    refine ⟨true :: w, by simp [hw], Or.inr ?_, Or.inr ?_⟩
+    · simp [existsEdge, List.replicate_succ, hf]
+    · simp [existsEdge, List.replicate_succ]
+
+/-- **`PSPACE` is closed under polynomially bounded existential quantification**: if `B ⊆ β × List
+Bool` is in `PSPACE` and `ℓ` is polynomial-time, then so is the set of the `x` for which some word
+`w` of length `ℓ x` has `(x, w) ∈ B`. The candidates are enumerated in place: this is reachability
+within two steps between two words of width `ℓ x + 1` (`existsEdge`), which Savitch's algorithm
+decides at depth `1`, reusing the space of the decider of `B` for every candidate
+(`Cslib.Reachability.computableTidilyInO_savitch`). -/
+theorem setOf_exists_mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set (β × List Bool)}
+    {ℓ : β → ℕ} (hB : B ∈ PSPACE (encPair encB encBits))
+    (hℓ : ComputableTidilyInPolyTime ℓ encB encUnary) :
+    {x | ∃ w : List Bool, w.length = ℓ x ∧ (x, w) ∈ B} ∈ PSPACE encB := by
+  obtain ⟨f, T, S, hf, hS, hB⟩ := mem_PSPACE_iff_computableTidilyInO.mp hB
+  set encQ := encPair encB (encPair encBits encBits)
+  -- the edge test: polynomial-time tests around one call of the decider of `B`
+  have hg : ComputableTidilyInPolyTime (fun q : β × List Bool × List Bool => (q.1, q.2.2.tail))
+      encQ (encPair encB encBits) :=
+    (ComputableTidilyInPolyTime.fst _ _).prod
+      (ComputableTidilyInPolyTime.bitsTail.comp
+        ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _)))
+  have hc : ComputableTidilyInPolyTime
+      (fun q : β × List Bool × List Bool => !(q.2.1.any fun b => b) && q.2.2.headD false)
+      encQ encBool :=
+    ComputableTidilyInPolyTime.bool_and.comp
+      ((ComputableTidilyInPolyTime.bool_not.comp
+        (ComputableTidilyInPolyTime.bitsAnyWithInput (test := fun _ b => b)
+          ((ComputableTidilyInPolyTime.fst _ _).comp (.snd _ _)) (.snd _ _))).prod
+        ((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp
+          ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _))))
+  have he : ComputableTidilyInPolyTime
+      (fun q : β × List Bool × List Bool => q.2.1.headD false && !(q.2.2.any fun b => !b))
+      encQ encBool :=
+    ComputableTidilyInPolyTime.bool_and.comp
+      (((ComputableTidilyInPolyTime.headD (encA := encBool) false).comp
+        ((ComputableTidilyInPolyTime.fst _ _).comp (.snd _ _))).prod
+        (ComputableTidilyInPolyTime.bool_not.comp
+          (ComputableTidilyInPolyTime.bitsAnyWithInput (test := fun _ b => !b)
+            ((ComputableTidilyInPolyTime.snd _ _).comp (.snd _ _))
+            (ComputableTidilyInPolyTime.bool_not.comp (.snd _ _)))))
+  obtain ⟨Tg, Sg, hSg, hgO⟩ := ComputableTidilyInPolySpace.of_polyTime hg
+  obtain ⟨Tc, Sc, hSc, hcO⟩ := ComputableTidilyInPolySpace.of_polyTime hc
+  obtain ⟨Te, Se, hSe, heO⟩ := ComputableTidilyInPolySpace.of_polyTime he
+  have hedge := hcO.ite (hf.comp hgO) heO
+  -- the arguments of Savitch's algorithm
+  have hin : ComputableTidilyInPolyTime
+      (fun x => (x, ℓ x + 1, 1, List.replicate (ℓ x + 1) false, List.replicate (ℓ x + 1) true))
+      encB (Cslib.Reachability.encArgs encB) := by
+    have hw : ComputableTidilyInPolyTime (fun x => ℓ x + 1) encB encUnary :=
+      ComputableTidilyInPolyTime.unary_add.comp (hℓ.prod (.const 1))
+    exact ComputableTidilyInPolyTime.id'.prod (hw.prod ((ComputableTidilyInPolyTime.const 1).prod
+      (((ComputableTidilyInPolyTime.bitsReplicate false).comp hw).prod
+        ((ComputableTidilyInPolyTime.bitsReplicate true).comp hw))))
+  obtain ⟨Ti, Si, hSi, hinO⟩ := ComputableTidilyInPolySpace.of_polyTime hin
+  have h := Cslib.Reachability.computableTidilyInO_savitch (edge := existsEdge f) (par := id)
+    hedge hinO (fun _ => List.length_replicate ..) fun _ => List.length_replicate ..
+  -- the space is polynomial
+  have hSedge : PolyBounded (fun q => (encQ q).length) fun q =>
+      Sc q + if !(q.2.1.any fun b => b) && q.2.2.headD false then Sg q + S (q.1, q.2.2.tail)
+        else Se q :=
+    (hSc.add (hSg.add (hS.comp hg.polyBounded_length) |>.add hSe)).mono fun q => by
+      split_ifs <;> omega
+  obtain ⟨cE, dE, hcE⟩ := hSedge.exists_le
+  have hℓ' : PolyBounded (fun x => (encB x).length) ℓ :=
+    hℓ.polyBounded_length.mono fun x => by simp [encUnary_apply]
+  have hG : PolyBounded (fun x => (encB x).length)
+      fun x => 2 * (encB x).length + 3 * ℓ x + 6 :=
+    (((PolyBounded.const 2).mul .self).add ((PolyBounded.const 3).mul hℓ')).add (.const 6)
+  have hpow : PolyBounded (fun x => (encB x).length)
+      fun x => cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE :=
+    PolyBounded.comp (size' := id) (v := fun n => cE * n ^ dE)
+      (PolyBounded.of_polynomiallyBounded (bound := fun n => cE * n ^ dE) id (by fun_prop)) hG
+  refine mem_PSPACE_iff_computableTidilyInO.mpr ⟨_, _, _, h, ?_, fun x => ?_⟩
+  · refine (((hSi.add ((PolyBounded.const 2).mul (hℓ'.add (.const 3)))).add .self).add
+      hpow).mono fun x => ?_
+    have hmax : Cslib.Reachability.edgeMax (fun q : β × List Bool × List Bool =>
+        Sc q + if (!(q.2.1.any fun b => b) && q.2.2.headD false) = true then
+          Sg q + S (q.1, q.2.2.tail) else Se q) x (ℓ x + 1) ≤
+        cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE :=
+      listMax_le fun u hu => listMax_le fun v hv => by
+        refine (hcE _).trans (Nat.mul_le_mul_left cE (Nat.pow_le_pow_left ?_ dE))
+        simp only [encQ, length_encPair, encBits_apply, Cslib.BitString.mem_enumList.mp hu,
+          Cslib.BitString.mem_enumList.mp hv]
+        omega
+    change Si x + (1 + 1) * (1 + (ℓ x + 1) + 1) + (encB x).length +
+        Cslib.Reachability.edgeMax (fun q : β × List Bool × List Bool =>
+          Sc q + if (!(q.2.1.any fun b => b) && q.2.2.headD false) = true then
+            Sg q + S (q.1, q.2.2.tail) else Se q) x (ℓ x + 1) ≤
+      Si x + 2 * (ℓ x + 3) + (encB x).length + cE * (2 * (encB x).length + 3 * ℓ x + 6) ^ dE
+    omega
+  · simp only [Set.mem_ofPred_eq, hB, id]
+    exact (savitch_existsEdge f x (ℓ x)).symm
+
+end Cslib.Complexity
diff --git a/Complexity/Computability/Complexity/Classes/Space/TM2.lean b/Complexity/Computability/Complexity/Classes/Space/TM2.lean
index c4dbc7d5ab..546b22cdf6 100644
--- a/Complexity/Computability/Complexity/Classes/Space/TM2.lean
+++ b/Complexity/Computability/Complexity/Classes/Space/TM2.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.TM2.PolySpace
-public import Complexity.Computability.Complexity.Classes.Inclusions
+public import Complexity.Computability.Complexity.Classes.Space.Closure
 
 /-!
 # Polynomial-space Mathlib stack machines decide problems in PSPACE
diff --git a/ComplexityTests/ArthurMerlin.lean b/ComplexityTests/ArthurMerlin.lean
index 7e3a1b4ff9..1afc92970d 100644
--- a/ComplexityTests/ArthurMerlin.lean
+++ b/ComplexityTests/ArthurMerlin.lean
@@ -8,7 +8,7 @@ import Complexity.Computability.Complexity.Classes.ArthurMerlin.Collapse
 import Complexity.Computability.Complexity.Classes.ArthurMerlin.GraphNonIsomorphism
 import Complexity.Computability.Complexity.Classes.ArthurMerlin.PH
 import Complexity.Computability.Complexity.Classes.ArthurMerlin.SetLowerBound
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.BPP
 import Complexity.Computability.Complexity.CookLevin.Completeness
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
diff --git a/ComplexityTests/OneWayMetacomplexity.lean b/ComplexityTests/OneWayMetacomplexity.lean
index d157863fb1..a2e9a3ac00 100644
--- a/ComplexityTests/OneWayMetacomplexity.lean
+++ b/ComplexityTests/OneWayMetacomplexity.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.BPP
 import Complexity.Crypto.Computational.OneWay.BPP
 import Complexity.Crypto.Computational.OneWay.MCSP
 import Complexity.Crypto.Computational.OneWay.NP
diff --git a/ComplexityTests/PPTruthTable.lean b/ComplexityTests/PPTruthTable.lean
index 0c5433358b..19905fa163 100644
--- a/ComplexityTests/PPTruthTable.lean
+++ b/ComplexityTests/PPTruthTable.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Classes.PP.TruthTable
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.PP.Closure
 import Complexity.Computability.Complexity.Classes.PP.Characterization
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
diff --git a/ComplexityTests/ResourceBoundsPlain.lean b/ComplexityTests/ResourceBoundsPlain.lean
index 5a6d4afa1f..4b875ae2f9 100644
--- a/ComplexityTests/ResourceBoundsPlain.lean
+++ b/ComplexityTests/ResourceBoundsPlain.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 
-import Complexity.Computability.Complexity.Classes.Inclusions
+import Complexity.Computability.Complexity.Classes.Space.Closure
 import Complexity.Computability.Complexity.Classes.Space.TQBF.Membership
 import Complexity.Computability.Complexity.Parameterized
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpace.Plain