refactor(classes): split the Inclusions hub into narrow modules

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

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

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
 

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
 

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

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

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

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

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