feat: PCP theorem, interactive proof classes, and complexity class containments

Complexitylib/Classes.lean

@@ -53,13 +53,17 @@ public import Complexitylib.Classes.PPoly.Uniform.Unrolling.Serializer.Transitio
 public import Complexitylib.Classes.PPoly.Uniform.Preprocessing
 public import Complexitylib.Classes.PPoly.Uniform.Containment
 public import Complexitylib.Classes.NP
+public import Complexitylib.Classes.Interactive
+public import Complexitylib.Classes.PCP
 public import Complexitylib.Classes.Randomized
 public import Complexitylib.Classes.Randomized.GoodSeed
 public import Complexitylib.Classes.Randomized.CircuitAmplification
 public import Complexitylib.Classes.Randomized.PPoly
 public import Complexitylib.Classes.Pairing
 public import Complexitylib.Classes.FNP
 public import Complexitylib.Classes.NP.Witness
+public import Complexitylib.Classes.PH
+public import Complexitylib.Classes.PH.SipserLautemann
 public import Complexitylib.Classes.NP.Reduction
 public import Complexitylib.Classes.NP.CoNP
 public import Complexitylib.Classes.NP.Closure
@@ -68,6 +72,30 @@ public import Complexitylib.Classes.L.PolynomialTime
 public import Complexitylib.Classes.Exponential
 public import Complexitylib.Classes.DTISP
 public import Complexitylib.Classes.Containments
+public import Complexitylib.Classes.Containments.Defs
+public import Complexitylib.Classes.Containments.Internal.ConfigCount
+public import Complexitylib.Classes.Containments.Internal.LogSpaceBound
+public import Complexitylib.Classes.Containments.Internal.ReachSet
+public import Complexitylib.Classes.Containments.Internal.ConfigGraph
+public import Complexitylib.Classes.Containments.Internal.BoundedReach
+public import Complexitylib.Classes.Containments.Internal.CodeSearch
+public import Complexitylib.Classes.Containments.Internal.ReachIn
+public import Complexitylib.Classes.Containments.Internal.SavitchBound
+public import Complexitylib.Classes.Containments.Internal.InductiveCounting
+public import Complexitylib.Classes.Containments.Internal.ComplementSpace
+public import Complexitylib.Classes.Containments.Internal.PHSubsetPSPACE
+public import Complexitylib.Classes.Containments.Internal.PPSubsetPSPACE
+public import Complexitylib.Classes.Containments.Internal.IPSubsetPSPACE
+public import Complexitylib.Classes.Containments.CoNLSubsetNL
+public import Complexitylib.Classes.Containments.IPSubsetPSPACE
+public import Complexitylib.Classes.Containments.NLSubsetCoNL
+public import Complexitylib.Classes.Containments.NLSubsetP
+public import Complexitylib.Classes.Containments.NPSPACESubsetPSPACE
+public import Complexitylib.Classes.Containments.PHSubsetPSPACE
+public import Complexitylib.Classes.Containments.PPSubsetPSPACE
+public import Complexitylib.Classes.Containments.PSPACESubsetEXP
+public import Complexitylib.Classes.Containments.PSPACESubsetIP
+public import Complexitylib.Classes.Containments.PSPACESubsetNPSPACE
 public import Complexitylib.Classes.Hierarchy
 import Complexitylib.Classes.NP.Internal.PairSplitTM
 

Complexitylib/Classes/Containments/CoNLSubsetNL.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.L
+
+/-!
+# `coNL ⊆ NL`
+
+⚠️ Unreviewed by Bolton
+
+The reverse half of the Immerman–Szelepcsényi theorem.
+
+Either inclusion implies the other, and this file proves that reduction unconditionally: `coNL`
+is the complement class of `NL`, so complementing both sides of one inclusion produces the other.
+Only one direction therefore has to be proved by inductive counting — see `NLSubsetCoNL`.
+
+## Main results
+
+- `coNL_subset_NL_of_NL_subset_coNL`, `NL_subset_coNL_of_coNL_subset_NL` — the two directions are
+  equivalent
+- `NL_eq_coNL_of_NL_subset_coNL` — either one settles `NL = coNL`
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-- **`coNL ⊆ NL`** (Immerman–Szelepcsényi). -/
+def CoNLSubsetNL : Prop := coNL ⊆ NL
+
+/-- One inclusion gives the other: complementing `Lᶜ ∈ NL` turns membership in `coNL` into
+membership in `NL`. -/
+theorem coNL_subset_NL_of_NL_subset_coNL (h : NL ⊆ coNL) : coNL ⊆ NL := by
+  intro L hL
+  have h₁ : Lᶜ ∈ NL := hL
+  have h₂ : (Lᶜ)ᶜ ∈ NL := h h₁
+  rwa [compl_compl] at h₂
+
+/-- The mirror implication. -/
+theorem NL_subset_coNL_of_coNL_subset_NL (h : coNL ⊆ NL) : NL ⊆ coNL := by
+  intro L hL
+  have h₁ : Lᶜ ∈ coNL := by
+    show (Lᶜ)ᶜ ∈ NL
+    rwa [compl_compl]
+  exact h h₁
+
+/-- Either inclusion settles the equality. -/
+theorem NL_eq_coNL_of_NL_subset_coNL (h : NL ⊆ coNL) : NL = coNL :=
+  subset_antisymm h (coNL_subset_NL_of_NL_subset_coNL h)
+
+end Complexity

Complexitylib/Classes/Containments/Defs.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Models.TuringMachine.ChoiceTape
+public import Mathlib.Data.Nat.Log
+
+/-!
+# The configuration graph and its bounded reachability rounds
+
+The space-bounded containments — `NL ⊆ P`, `NL ⊆ coNL`, Savitch's theorem — all read a
+computation as a walk in the *configuration graph*: the nondeterministic step relation on
+configurations. This file holds the three definitions those arguments share, so that theorem
+statements about them can be read without opening any proof internals.
+
+## Main definitions
+
+- `NTM.Succ` — one nondeterministic step, as a relation on configurations
+- `NTM.ReachesCfg` — its reflexive-transitive closure
+- `NTM.reachSet` — the configurations reached within a fixed number of rounds of
+  successor-closure, i.e. the state of a breadth-first search after that many rounds
+- `NTM.ReachesCfgIn`, `NTM.ReachesCfgLe` — reachability in exactly, and in at most, a given
+  number of steps; the step count is what Savitch's recursion halves
+- `logWindow` — a concrete `O(log n)` search window
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-- The search window of a log-space machine. A machine's own space function is an arbitrary
+`O(log n)` function, which a program cannot evaluate; this concrete bound can be computed from
+the input length alone, and enlarging the window is harmless. -/
+def logWindow (C D n : ℕ) : ℕ := C * Nat.log 2 n + D
+
+namespace NTM
+
+variable {k : ℕ}
+
+/-- One step of the configuration graph: a non-halted configuration has the two successors its
+transition functions produce. -/
+def Succ (tm : NTM k) (c c' : Cfg k tm.Q) : Prop :=
+  c.state ≠ tm.qhalt ∧ ∃ b, c' = tm.stepCfg b c
+
+/-- Reachability in the configuration graph. -/
+def ReachesCfg (tm : NTM k) : Cfg k tm.Q → Cfg k tm.Q → Prop :=
+  Relation.ReflTransGen tm.Succ
+
+/-- Reachability in exactly `t` steps of the configuration graph. -/
+inductive ReachesCfgIn (tm : NTM k) : ℕ → Cfg k tm.Q → Cfg k tm.Q → Prop
+  /-- No steps: a configuration reaches itself. -/
+  | refl (c : Cfg k tm.Q) : ReachesCfgIn tm 0 c c
+  /-- One step followed by a shorter walk. -/
+  | head {c c' c'' : Cfg k tm.Q} {t : ℕ} (hstep : tm.Succ c c')
+      (hrest : ReachesCfgIn tm t c' c'') : ReachesCfgIn tm (t + 1) c c''
+
+/-- Reachability in at most `t` steps. Halted configurations have no successors, so a walk
+cannot be padded and the bounded notion is genuinely weaker than the exact one. -/
+def ReachesCfgLe (tm : NTM k) (t : ℕ) (c c' : Cfg k tm.Q) : Prop :=
+  ∃ s ≤ t, tm.ReachesCfgIn s c c'
+
+/-- The configurations reachable from `c₀` within `t` rounds of successor-closure. -/
+def reachSet (tm : NTM k) (c₀ : Cfg k tm.Q) : ℕ → Set (Cfg k tm.Q)
+  | 0 => {c₀}
+  | t + 1 => reachSet tm c₀ t ∪ {c' | ∃ c ∈ reachSet tm c₀ t, tm.Succ c c'}
+
+end NTM
+
+end Complexity

Complexitylib/Classes/Containments/IPSubsetPSPACE.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.Interactive
+public import Complexitylib.Classes.Containments.Internal.IPSubsetPSPACE
+public import Complexitylib.Classes.Containments.Internal.IPAssemble
+public import Complexitylib.Classes.P.Defs
+
+/-!
+# `IP ⊆ PSPACE`
+
+⚠️ Unreviewed by Bolton
+
+The easy half of `IP = PSPACE`.
+
+The value of an interactive protocol on an input is the acceptance probability against an optimal
+prover, and that value is the root of a finite game tree: the prover's moves maximize, the
+verifier's coins average. Polynomial space evaluates the tree depth-first, holding one path of
+messages at a time — the tree is exponentially wide but only polynomially deep, since both the
+round count and the message lengths are polynomially bounded.
+
+## How the proof runs
+
+Three steps, none of which builds a machine by hand.
+
+**The maximum over prover strategies becomes a finite recursion.** A strategy is a function on
+*all* transcripts, so the supremum `IP` quantifies is a priori a supremum over an infinite set.
+`Protocol.gval` (in `Internal.IPGameTree`) *is* that maximum, written as a recursion down the
+transcript tree: at a node the coins still in play are those consistent with the verifier messages
+recorded above it, a round splits them by the verifier's next message
+(`Protocol.consFinset_append`), and the prover picks, for each such message, the reply maximizing
+the count below. `Protocol.sval_le_gval` says no bounded strategy beats it and
+`Protocol.sval_optStrategy` says one attains it, so `Protocol.mem_iff_gval` turns membership into
+one comparison, `2 ^ coins(|x|) < 2 · gval(x)`. That the value never exceeds the coin space
+(`Protocol.gval_le_card`) is what keeps every count inside `coins(|x|) + 1` bits.
+
+**The recursion becomes a walk.** `Protocol.gvalR_zero_enum` and `Protocol.gvalR_succ_enum` write
+it as two counter loops, and `Complexity.IPM.step` (in `Internal.IPSem`) walks it on a stack: one
+frame per round carrying the two message counters, a running sum and a running maximum, with a
+leaf frame carrying the coin counter and its tally. `IPM.run_frame` proves every pushed frame
+comes back with its subtree's value, within `IPM.runBound` steps.
+
+**The walk becomes a machine.** `IPM.ipStep` is that walk written inside the polynomial-time
+algebra, `IPM.ipStep_encSst` proves the square commutes, and
+`Complexity.SpaceIter.mem_PSPACE_of_iterate` supplies the machine — the same last step Savitch's
+theorem takes. The leaf test is a single scan: carrying each frame's transcript body inside the
+frame makes the consistency check a per-frame condition, so it may be taken in any order, even
+though `Protocol.replay` runs the rounds in the opposite order to the stack.
+
+## Main results
+
+- `Protocol.transcript_congr` — strategy extensionality for the transcript
+- `Protocol.mem_iff_gval` — membership is a comparison of the game-tree value
+- `Protocol.walk_decides` — the stack walk ends with the membership bit
+- `IP_subset_PSPACE` — the containment
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-- **`IP ⊆ PSPACE`**: the optimal prover's acceptance probability is the value of a
+polynomially deep game tree, evaluated depth-first in polynomial space. -/
+theorem IP_subset_PSPACE : IP ⊆ PSPACE := IP_subset_PSPACE_internal
+
+/-- **What the game tree computes.** `Protocol.gval` is the number of coin strings on which the
+best bounded prover convinces the verifier; membership is that count exceeding half the coin
+space. -/
+theorem IP_membership_is_game_value {L : Language} (hL : L ∈ IP) :
+    ∃ prot : Protocol, ∀ x : List Bool, x ∈ L ↔
+      2 ^ prot.coins x.length
+        < 2 * prot.gval x (prot.coins x.length) (prot.msgLen x.length)
+            (prot.rounds x.length) [] := by
+  obtain ⟨prot, _, _, _, _, _, _, hcomp, hsound⟩ := hL
+  exact ⟨prot, fun x => Protocol.mem_iff_gval prot x hcomp hsound⟩
+
+/-- Shamir's theorem needs only the other half now. -/
+theorem IP_eq_PSPACE_of_pspace_subset_ip (h : PSPACE ⊆ IP) : IP = PSPACE :=
+  subset_antisymm IP_subset_PSPACE h
+
+end Complexity