diff --git a/Complexitylib/Classes.lean b/Complexitylib/Classes.lean
index 674ffd6a..0855f28e 100644
--- a/Complexitylib/Classes.lean
+++ b/Complexitylib/Classes.lean
@@ -60,6 +60,8 @@ 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
diff --git a/Complexitylib/Classes/P/Cobham/Internal.lean b/Complexitylib/Classes/P/Cobham/Internal.lean
index 8ad44aad..5e52e8df 100644
--- a/Complexitylib/Classes/P/Cobham/Internal.lean
+++ b/Complexitylib/Classes/P/Cobham/Internal.lean
@@ -13,9 +13,13 @@ public import Complexitylib.Classes.P.Cobham.Internal.ConsBit
 public import Complexitylib.Classes.P.Cobham.Internal.Reorder
 public import Complexitylib.Classes.P.Cobham.Internal.Vec
 public import Complexitylib.Classes.P.Cobham.Internal.Algebra
+public import Complexitylib.Classes.P.Cobham.Internal.PolyLen
+public import Complexitylib.Classes.P.Cobham.Internal.StringOps
 public import Complexitylib.Classes.P.Cobham.Internal.Encoding
 public import Complexitylib.Classes.P.Cobham.Internal.StepAlgebra
 public import Complexitylib.Classes.P.Cobham.Internal.Simulate
+public import Complexitylib.Classes.P.Cobham.Internal.ChoiceSim
+public import Complexitylib.Classes.P.Cobham.Internal.BlockLoop
 public import Complexitylib.Classes.P.Cobham.Internal.IterateLayout
 public import Complexitylib.Classes.P.Cobham.Internal.Iterate
 public import Complexitylib.Classes.P.Cobham.Internal.TakeLen
diff --git a/Complexitylib/Classes/P/Cobham/Internal/BlockLoop.lean b/Complexitylib/Classes/P/Cobham/Internal/BlockLoop.lean
new file mode 100644
index 00000000..8a0a9a86
--- /dev/null
+++ b/Complexitylib/Classes/P/Cobham/Internal/BlockLoop.lean
@@ -0,0 +1,386 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.Cobham.Internal.ChoiceSim
+public import Complexitylib.Classes.P.Cobham.Internal.PolyLen
+public import Complexitylib.Classes.P.Cobham.Internal.StringOps
+
+/-!
+# Looping over the blocks of a string inside the algebra
+
+Amplified acceptance is a majority vote over the blocks of a random seed. Both
+that vote and the outer disjunction over shift blocks are limited recursions
+over a *ruler* whose length is the iteration count: at the step whose tail is
+`y`, the block index is `|y|`, so the block itself is cut out of the source
+string by a `drop` of `|y| · |τ|` bits — a length `smash` produces — followed
+by a `take` of `|τ|`. No state has to be threaded through the recursion.
+
+## Main definitions
+
+- `Cobham.blockAtIdx` — the `j`-th block of a string at a given width
+- `Cobham.acceptCountAux` — unary count of blocks on which the path accepts
+- `Cobham.majorityFlag` — the amplified majority verdict as a flag
+
+## Main results
+
+- `Cobham.acceptCountAux_length` — the count is the number of accepting blocks
+- `Cobham.acceptCountAux_mem`, `Cobham.majorityFlag_mem` — both are in the
+  algebra
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Cobham
+
+variable {k : ℕ}
+
+/-- The `j`-th block of `s` at width `w`. -/
+def blockAtIdx (w : ℕ) (s : List Bool) (j : ℕ) : List Bool := (s.drop (j * w)).take w
+
+/-- The block of `s` selected by the ruler `idx` at the width of `τ`. -/
+def blockOf (τ s idx : List Bool) : List Bool :=
+  (s.drop (Complexity.smash idx τ).length).take τ.length
+
+@[simp] theorem blockOf_eq (τ s idx : List Bool) :
+    blockOf τ s idx = blockAtIdx τ.length s idx.length := by
+  rw [blockOf, blockAtIdx, smash_length]
+
+theorem blockOf_mem {n : ℕ} {gτ gs gidx : (Fin n → List Bool) → List Bool}
+    (hτ : Cobham gτ) (hs : Cobham gs) (hidx : Cobham gidx) :
+    Cobham fun v : Fin n → List Bool => blockOf (gτ v) (gs v) (gidx v) :=
+  (takeFn hτ (dropFn (comp₂ Cobham.smash hidx hτ) hs)).of_eq fun _ => rfl
+
+/-! ## Counting accepting blocks -/
+
+/-- Unary count of the blocks of `s` on which the path of `tm` accepts: one bit
+per accepting block. The recursion runs once per bit of `ρ`, and the block
+index at each step is the length of the remaining tail. -/
+noncomputable def acceptCountAux (tm : NTM k) (u x τ s : List Bool) : List Bool → List Bool
+  | [] => []
+  | _ :: y =>
+      caseBit₀ (acceptChoiceFn tm u x (blockOf τ s y))
+        (false :: acceptCountAux tm u x τ s y) (acceptCountAux tm u x τ s y)
+
+/-- The count is the number of accepting block indices below `|ρ|`. -/
+theorem acceptCountAux_length (tm : NTM k) (u x τ s ρ : List Bool) :
+    (acceptCountAux tm u x τ s ρ).length
+      = ∑ j ∈ Finset.range ρ.length,
+          (if acceptChoiceFn tm u x (blockAtIdx τ.length s j) = [true] then 1 else 0) := by
+  induction ρ with
+  | nil => simp [acceptCountAux]
+  | cons β y ih =>
+      have hflag := acceptChoiceFn_flag tm u x (blockOf τ s y)
+      rw [acceptCountAux, List.length_cons, Finset.sum_range_succ, ← ih]
+      rcases hflag with hf | hf
+      · rw [hf]
+        simp only [caseBit₀_cons, cond_true, List.length_cons]
+        rw [if_pos (by rw [← blockOf_eq]; exact hf)]
+      · rw [hf]
+        simp only [caseBit₀_cons, cond_false]
+        rw [if_neg (by rw [← blockOf_eq, hf]; simp)]
+        omega
+
+/-- The step of the counting recursion. -/
+private noncomputable def countStep (tm : NTM k) (w : Fin 6 → List Bool) : List Bool :=
+  caseBit₀ (acceptChoiceFn tm (w 2) (w 3) (blockOf (w 4) (w 5) (w 0)))
+    (false :: w 1) (w 1)
+
+private theorem countStep_mem (tm : NTM k) : Cobham (countStep tm) := by
+  have hcons : Cobham fun w : Fin 6 → List Bool => false :: w 1 :=
+    (Cobham.comp (Cobham.bit false) fun _ : Fin 1 => Cobham.proj 1).of_eq fun _ => rfl
+  exact (iteFn
+    (acceptChoiceFn_mem tm (Cobham.proj 2) (Cobham.proj 3)
+      (blockOf_mem (Cobham.proj 4) (Cobham.proj 5) (Cobham.proj 0)))
+    hcons (Cobham.proj 1)).of_eq fun _ => rfl
+
+private theorem recNotation_count (tm : NTM k) (u x τ s ρ : List Bool) :
+    recNotation (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+        (countStep tm) ρ ![u, x, τ, s]
+      = acceptCountAux tm u x τ s ρ := by
+  induction ρ with
+  | nil => rfl
+  | cons β y ih =>
+      rw [recNotation_cons, acceptCountAux]
+      cases β <;>
+        · simp only [cond_false, cond_true, countStep, Fin.cons_zero, Fin.cons_one]
+          rw [show (Fin.cons y (Fin.cons (recNotation
+              (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+              (countStep tm) y ![u, x, τ, s]) ![u, x, τ, s]) : Fin 6 → List Bool) 2 = u from rfl,
+            show (Fin.cons y (Fin.cons (recNotation
+              (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+              (countStep tm) y ![u, x, τ, s]) ![u, x, τ, s]) : Fin 6 → List Bool) 3 = x from rfl,
+            show (Fin.cons y (Fin.cons (recNotation
+              (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+              (countStep tm) y ![u, x, τ, s]) ![u, x, τ, s]) : Fin 6 → List Bool) 4 = τ from rfl,
+            show (Fin.cons y (Fin.cons (recNotation
+              (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+              (countStep tm) y ![u, x, τ, s]) ![u, x, τ, s]) : Fin 6 → List Bool) 5 = s from rfl,
+            ih]
+
+private theorem recNotation_count_length (tm : NTM k) (ρ : List Bool)
+    (v : Fin 4 → List Bool) :
+    (recNotation (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+      (countStep tm) ρ v).length ≤ ρ.length := by
+  induction ρ with
+  | nil => simp
+  | cons β y ih =>
+      rw [recNotation_cons, List.length_cons]
+      have hstep : ∀ (a b : List Bool) (w' : Fin 4 → List Bool),
+          (countStep tm (Fin.cons a (Fin.cons b w'))).length ≤ b.length + 1 := by
+        intro a b w'
+        show (caseBit₀ (acceptChoiceFn tm _ _ _) (false :: b) b).length ≤ b.length + 1
+        rcases hc : acceptChoiceFn tm ((Fin.cons a (Fin.cons b w') : Fin 6 → List Bool) 2)
+            ((Fin.cons a (Fin.cons b w') : Fin 6 → List Bool) 3)
+            (blockOf ((Fin.cons a (Fin.cons b w') : Fin 6 → List Bool) 4)
+              ((Fin.cons a (Fin.cons b w') : Fin 6 → List Bool) 5)
+              ((Fin.cons a (Fin.cons b w') : Fin 6 → List Bool) 0)) with _ | ⟨d, z⟩
+        · simp
+        · cases d <;> simp
+      cases β <;>
+        · simp only [cond_false, cond_true]
+          have := hstep y (recNotation
+            (fun _ : Fin 4 → List Bool => ([] : List Bool)) (countStep tm)
+            (countStep tm) y v) v
+          omega
+
+/-- **The count is in the algebra.** -/
+theorem acceptCountAux_mem {n : ℕ} (tm : NTM k)
+    {gu gx gτ gs gρ : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hs : Cobham gs)
+    (hρ : Cobham gρ) :
+    Cobham fun v : Fin n → List Bool =>
+      acceptCountAux tm (gu v) (gx v) (gτ v) (gs v) (gρ v) := by
+  have hrec := Cobham.boundedRec (g := fun _ : Fin 4 → List Bool => ([] : List Bool))
+    (h₀ := countStep tm) (h₁ := countStep tm)
+    (j := fun w : Fin 5 → List Bool => w 0)
+    Cobham.empty (countStep_mem tm) (countStep_mem tm) (Cobham.proj 0)
+    (by
+      intro ρ v
+      simpa using recNotation_count_length tm ρ v)
+  have hg : ∀ i : Fin 5, Cobham (![gρ, gu, gx, gτ, gs] i) := by
+    intro i
+    match i with
+    | 0 => exact hρ
+    | 1 => exact hu
+    | 2 => exact hx
+    | 3 => exact hτ
+    | 4 => exact hs
+  refine (Cobham.comp hrec hg).of_eq fun v => ?_
+  have htail : (Fin.tail fun i => ![gρ, gu, gx, gτ, gs] i v)
+      = ![gu v, gx v, gτ v, gs v] := by
+    funext i
+    match i with
+    | 0 => rfl
+    | 1 => rfl
+    | 2 => rfl
+    | 3 => rfl
+  show recNotation _ _ _ (gρ v) (Fin.tail fun i => ![gρ, gu, gx, gτ, gs] i v) = _
+  rw [htail, recNotation_count]
+
+/-! ## The amplified verdict -/
+
+/-- The amplified majority verdict as a flag: strictly more than half of the
+`|ρ|` blocks of `s` accept. -/
+noncomputable def majorityFlag (tm : NTM k) (u x τ s ρ : List Bool) : List Bool :=
+  notBit (lenLeFlag ρ (acceptCountAux tm u x τ s ρ ++ acceptCountAux tm u x τ s ρ))
+
+theorem majorityFlag_flag (tm : NTM k) (u x τ s ρ : List Bool) :
+    majorityFlag tm u x τ s ρ = [true] ∨ majorityFlag tm u x τ s ρ = [false] := by
+  rw [majorityFlag]
+  rcases lenLeFlag_flag ρ (acceptCountAux tm u x τ s ρ ++ acceptCountAux tm u x τ s ρ)
+    with h | h <;> rw [h] <;> simp [notBit]
+
+theorem majorityFlag_eq_true_iff (tm : NTM k) (u x τ s ρ : List Bool) :
+    majorityFlag tm u x τ s ρ = [true] ↔
+      ρ.length < 2 * (acceptCountAux tm u x τ s ρ).length := by
+  rw [majorityFlag, notBit_eq_true_iff (lenLeFlag_flag _ _)]
+  constructor
+  · intro h
+    by_contra hcon
+    rw [Nat.not_lt] at hcon
+    have htrue : lenLeFlag ρ
+        (acceptCountAux tm u x τ s ρ ++ acceptCountAux tm u x τ s ρ) = [true] := by
+      rw [lenLeFlag_eq_true_iff, List.length_append]
+      omega
+    rw [htrue] at h
+    exact absurd h (by simp)
+  · intro h
+    rcases lenLeFlag_flag ρ
+      (acceptCountAux tm u x τ s ρ ++ acceptCountAux tm u x τ s ρ) with h' | h'
+    · rw [lenLeFlag_eq_true_iff, List.length_append] at h'
+      omega
+    · exact h'
+
+theorem majorityFlag_mem {n : ℕ} (tm : NTM k)
+    {gu gx gτ gs gρ : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hs : Cobham gs)
+    (hρ : Cobham gρ) :
+    Cobham fun v : Fin n → List Bool =>
+      majorityFlag tm (gu v) (gx v) (gτ v) (gs v) (gρ v) :=
+  (notFn (lenLeFlag_mem hρ
+    (appendFn (acceptCountAux_mem tm hu hx hτ hs hρ)
+      (acceptCountAux_mem tm hu hx hτ hs hρ)))).of_eq fun _ => rfl
+
+/-- The verdict sought at a shift: the amplified majority, or its negation. -/
+noncomputable def verdictFlag (tm : NTM k) (b : Bool) (u x τ s ρ : List Bool) :
+    List Bool :=
+  bif b then majorityFlag tm u x τ s ρ else notBit (majorityFlag tm u x τ s ρ)
+
+theorem verdictFlag_flag (tm : NTM k) (b : Bool) (u x τ s ρ : List Bool) :
+    verdictFlag tm b u x τ s ρ = [true] ∨ verdictFlag tm b u x τ s ρ = [false] := by
+  cases b
+  · rw [verdictFlag]
+    simp only [Bool.cond_false]
+    rcases majorityFlag_flag tm u x τ s ρ with h | h <;> rw [h] <;> simp [notBit]
+  · rw [verdictFlag]
+    simp only [Bool.cond_true]
+    exact majorityFlag_flag tm u x τ s ρ
+
+theorem verdictFlag_mem {n : ℕ} (tm : NTM k) (b : Bool)
+    {gu gx gτ gs gρ : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hs : Cobham gs)
+    (hρ : Cobham gρ) :
+    Cobham fun v : Fin n → List Bool =>
+      verdictFlag tm b (gu v) (gx v) (gτ v) (gs v) (gρ v) := by
+  cases b
+  · exact (notFn (majorityFlag_mem tm hu hx hτ hs hρ)).of_eq fun _ => rfl
+  · exact (majorityFlag_mem tm hu hx hτ hs hρ).of_eq fun _ => rfl
+
+/-! ## Disjunction over shifts -/
+
+/-- Disjunction of the verdict over the shift blocks of `wit`: the recursion
+runs once per bit of the shift ruler, and at each step the shift block is cut
+from `wit` at the index given by the remaining tail. -/
+noncomputable def anyShiftAux (tm : NTM k) (b : Bool) (u x τ ρ σ r wit : List Bool) :
+    List Bool → List Bool
+  | [] => [false]
+  | _ :: y =>
+      orBit (verdictFlag tm b u x τ (xorSuffix r (padTo σ (blockOf σ wit y))) ρ)
+        (anyShiftAux tm b u x τ ρ σ r wit y)
+
+theorem anyShiftAux_flag (tm : NTM k) (b : Bool) (u x τ ρ σ r wit ι : List Bool) :
+    anyShiftAux tm b u x τ ρ σ r wit ι = [true] ∨
+      anyShiftAux tm b u x τ ρ σ r wit ι = [false] := by
+  induction ι with
+  | nil => exact Or.inr rfl
+  | cons β y ih => exact orBit_flag (verdictFlag_flag _ _ _ _ _ _ _) ih
+
+/-- **The disjunction is exactly an existential over shift indices.** -/
+theorem anyShiftAux_eq_true_iff (tm : NTM k) (b : Bool)
+    (u x τ ρ σ r wit ι : List Bool) :
+    anyShiftAux tm b u x τ ρ σ r wit ι = [true] ↔
+      ∃ i < ι.length,
+        verdictFlag tm b u x τ
+          (xorSuffix r (padTo σ (blockAtIdx σ.length wit i))) ρ = [true] := by
+  induction ι with
+  | nil => simp [anyShiftAux]
+  | cons β y ih =>
+      rw [anyShiftAux,
+        orBit_eq_true_iff (verdictFlag_flag _ _ _ _ _ _ _) (anyShiftAux_flag _ _ _ _ _ _ _ _ _ _),
+        ih, List.length_cons]
+      rw [blockOf_eq]
+      constructor
+      · rintro (h | ⟨i, hi, hv⟩)
+        · exact ⟨y.length, by omega, h⟩
+        · exact ⟨i, by omega, hv⟩
+      · rintro ⟨i, hi, hv⟩
+        rcases Nat.lt_or_ge i y.length with hlt | hge
+        · exact Or.inr ⟨i, hlt, hv⟩
+        · have : i = y.length := by omega
+          subst this
+          exact Or.inl hv
+
+/-- The step of the shift recursion. -/
+private noncomputable def shiftStep (tm : NTM k) (b : Bool) (w : Fin 9 → List Bool) :
+    List Bool :=
+  orBit (verdictFlag tm b (w 2) (w 3) (w 4)
+    (xorSuffix (w 7) (padTo (w 6) (blockOf (w 6) (w 8) (w 0)))) (w 5)) (w 1)
+
+private theorem shiftStep_mem (tm : NTM k) (b : Bool) : Cobham (shiftStep tm b) :=
+  (orFn (verdictFlag_mem tm b (Cobham.proj 2) (Cobham.proj 3) (Cobham.proj 4)
+      (xorSuffix_mem (Cobham.proj 7)
+        (padFn (Cobham.proj 6)
+          (blockOf_mem (Cobham.proj 6) (Cobham.proj 8) (Cobham.proj 0))))
+      (Cobham.proj 5))
+    (Cobham.proj 1)).of_eq fun _ => rfl
+
+private theorem recNotation_anyShift (tm : NTM k) (b : Bool)
+    (u x τ ρ σ r wit ι : List Bool) :
+    recNotation (fun _ : Fin 7 → List Bool => ([false] : List Bool)) (shiftStep tm b)
+        (shiftStep tm b) ι ![u, x, τ, ρ, σ, r, wit]
+      = anyShiftAux tm b u x τ ρ σ r wit ι := by
+  induction ι with
+  | nil => rfl
+  | cons β y ih =>
+      rw [recNotation_cons, anyShiftAux]
+      cases β <;>
+        · show shiftStep tm b (Fin.cons y (Fin.cons _ ![u, x, τ, ρ, σ, r, wit])) = _
+          rw [shiftStep]
+          show orBit (verdictFlag tm b u x τ (xorSuffix r (padTo σ (blockOf σ wit y))) ρ)
+              (recNotation (fun _ : Fin 7 → List Bool => ([false] : List Bool))
+                (shiftStep tm b) (shiftStep tm b) y ![u, x, τ, ρ, σ, r, wit]) = _
+          rw [ih]
+
+private theorem recNotation_anyShift_length (tm : NTM k) (b : Bool) (ι : List Bool)
+    (v : Fin 7 → List Bool) :
+    (recNotation (fun _ : Fin 7 → List Bool => ([false] : List Bool)) (shiftStep tm b)
+      (shiftStep tm b) ι v).length ≤ 1 := by
+  induction ι with
+  | nil => simp
+  | cons β y ih =>
+      rw [recNotation_cons]
+      have hstep : ∀ (a c : List Bool) (w' : Fin 7 → List Bool),
+          (shiftStep tm b (Fin.cons a (Fin.cons c w'))).length ≤ 1 := by
+        intro a c w'
+        rw [shiftStep, orBit_length]
+      cases β <;> simpa using hstep y _ v
+
+/-- **The disjunction over shifts is in the algebra.** -/
+theorem anyShiftAux_mem {n : ℕ} (tm : NTM k) (b : Bool)
+    {gu gx gτ gρ gσ gr gwit gι : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hτ : Cobham gτ) (hρ : Cobham gρ)
+    (hσ : Cobham gσ) (hr : Cobham gr) (hwit : Cobham gwit) (hι : Cobham gι) :
+    Cobham fun v : Fin n → List Bool =>
+      anyShiftAux tm b (gu v) (gx v) (gτ v) (gρ v) (gσ v) (gr v) (gwit v) (gι v) := by
+  have hrec := Cobham.boundedRec
+    (g := fun _ : Fin 7 → List Bool => ([false] : List Bool))
+    (h₀ := shiftStep tm b) (h₁ := shiftStep tm b)
+    (j := fun _ : Fin 8 → List Bool => ([false] : List Bool))
+    (Cobham.const _) (shiftStep_mem tm b) (shiftStep_mem tm b) (Cobham.const _)
+    (by
+      intro ι v
+      simpa using recNotation_anyShift_length tm b ι v)
+  have hg : ∀ i : Fin 8, Cobham (![gι, gu, gx, gτ, gρ, gσ, gr, gwit] i) := by
+    intro i
+    match i with
+    | 0 => exact hι
+    | 1 => exact hu
+    | 2 => exact hx
+    | 3 => exact hτ
+    | 4 => exact hρ
+    | 5 => exact hσ
+    | 6 => exact hr
+    | 7 => exact hwit
+  refine (Cobham.comp hrec hg).of_eq fun v => ?_
+  have htail : (Fin.tail fun i => ![gι, gu, gx, gτ, gρ, gσ, gr, gwit] i v)
+      = ![gu v, gx v, gτ v, gρ v, gσ v, gr v, gwit v] := by
+    funext i
+    match i with
+    | 0 => rfl
+    | 1 => rfl
+    | 2 => rfl
+    | 3 => rfl
+    | 4 => rfl
+    | 5 => rfl
+    | 6 => rfl
+  show recNotation _ _ _ (gι v) (Fin.tail fun i => ![gι, gu, gx, gτ, gρ, gσ, gr, gwit] i v) = _
+  rw [htail, recNotation_anyShift]
+
+end Cobham
+
+end Complexity
diff --git a/Complexitylib/Classes/P/Cobham/Internal/ChoiceSim.lean b/Complexitylib/Classes/P/Cobham/Internal/ChoiceSim.lean
new file mode 100644
index 00000000..a1bc6638
--- /dev/null
+++ b/Complexitylib/Classes/P/Cobham/Internal/ChoiceSim.lean
@@ -0,0 +1,594 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.Cobham.Internal.Simulate
+public import Complexitylib.Models.TuringMachine.ChoiceTape
+
+/-!
+# Encoding the start of a nondeterministic path
+
+`NTM.choiceTM` runs one path of a nondeterministic machine deterministically,
+reading its choice bits from the last work tape. To simulate such a run inside
+Cobham's algebra, the starting configuration must be encoded with the choice
+string already on that tape and its head parked on the first bit.
+
+This file supplies that encoder — `Cobham.initChoiceFn`, the counterpart of
+`Cobham.initFn` — together with its algebra membership and the identification
+with `Cobham.cfgCode` of the intended configuration.
+
+## Main definitions
+
+- `Cobham.choiceTape` — the choice string on a tape, head at cell 1
+- `Cobham.choiceCfg` — the starting configuration of `NTM.choiceTM`
+- `Cobham.initChoiceFn` — its encoding, as a function of the two strings
+
+## Main results
+
+- `Cobham.initChoiceFn_mem` — the encoder is in the algebra
+- `Cobham.initChoiceFn_eq` — the encoder computes `cfgCode` of `choiceCfg`
+- `Cobham.dropChoice_choiceCfg` — forgetting the choice tape gives the
+  nondeterministic machine's own initial configuration
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Cobham
+
+variable {k : ℕ}
+
+/-- The choice string on a tape, with the head parked on the first bit. -/
+def choiceTape (c : List Bool) : Tape := ⟨1, (Tape.init (c.map Γ.ofBool)).cells⟩
+
+@[simp] theorem choiceTape_head (c : List Bool) : (choiceTape c).head = 1 := rfl
+
+@[simp] theorem choiceTape_cells (c : List Bool) :
+    (choiceTape c).cells = (Tape.init (c.map Γ.ofBool)).cells := rfl
+
+/-- The starting configuration of `NTM.choiceTM tm`: the input on the input
+tape, the choice string on the appended choice tape. -/
+noncomputable def choiceCfg (tm : NTM k) (x c : List Bool) : Cfg (k + 1) tm.Q where
+  state := tm.qstart
+  input := Tape.init (x.map Γ.ofBool)
+  work := fun i => if i = Fin.last k then choiceTape c else Tape.init []
+  output := Tape.init []
+
+/-- Forgetting the choice tape gives the nondeterministic machine's own
+initial configuration. -/
+@[simp] theorem dropChoice_choiceCfg (tm : NTM k) (x c : List Bool) :
+    NTM.dropChoice (choiceCfg tm x c) = tm.initCfg x := by
+  refine Cfg.ext rfl rfl ?_ rfl
+  funext i
+  rw [NTM.dropChoice, choiceCfg]
+  simp [(Fin.castSucc_lt_last i).ne]
+
+/-- The encoded starting configuration of a nondeterministic path. Everything
+but the input tape's and the choice tape's right half-blocks is a constant of
+the machine. -/
+noncomputable def initChoiceFn (tm : NTM k) (R x c : List Bool) : List Bool :=
+  padTo R (stateCode tm.qstart) ++
+    (padTo R [] ++ (padTo R (symCode Γ.start ++ encodeBits x) ++
+      ((List.replicate (k + 1) (padTo R [] ++ padTo R (symCode Γ.start))).flatten ++
+        (padTo R (symCode Γ.start) ++ padTo R (encodeBits c)))))
+
+/-- **The encoder is in the algebra.** -/
+theorem initChoiceFn_mem {n : ℕ} (tm : NTM k)
+    {gR gx gc : (Fin n → List Bool) → List Bool} (hR : Cobham gR) (hx : Cobham gx)
+    (hc : Cobham gc) :
+    Cobham fun v : Fin n → List Bool => initChoiceFn tm (gR v) (gx v) (gc v) :=
+  (appendFn (padFn hR (Cobham.const _))
+    (appendFn (padFn hR Cobham.empty)
+      (appendFn (padFn hR (appendFn (Cobham.const _) (encodeBitsFn hx)))
+        (appendFn
+          (repeatFn (appendFn (padFn hR Cobham.empty)
+            (padFn hR (Cobham.const _))) (k + 1))
+          (appendFn (padFn hR (Cobham.const _))
+            (padFn hR (encodeBitsFn hc))))))).of_eq fun _ => rfl
+
+private theorem flatten_tapesBlocks' (W : ℕ) : ∀ ts : List Tape,
+    (tapesBlocks W ts).flatten
+      = (ts.map fun t => padTo (blockRuler W) (leftCode t)
+          ++ padTo (blockRuler W) (rightCode t W)).flatten := by
+  intro ts
+  induction ts with
+  | nil => rfl
+  | cons t ts ih =>
+      rw [tapesBlocks, List.flatMap_cons, List.flatten_append, ← tapesBlocks, ih,
+        List.map_cons, List.flatten_cons, tapeBlocks]
+      simp
+
+private theorem cellsCode_of_bits' (x : List Bool) :
+    ∀ (t : Tape) (i : ℕ), (∀ j, ∀ _ : j < x.length, t.cells (i + j) = Γ.ofBool x[j]) →
+      cellsCode t i x.length = encodeBits x := by
+  induction x with
+  | nil => intro t i _; rfl
+  | cons b x ih =>
+      intro t i hcells
+      rw [List.length_cons, cellsCode_succ_left, encodeBits_cons,
+        show t.cells i = Γ.ofBool b from by simpa using hcells 0 (by simp)]
+      congr 1
+      exact ih t (i + 1) fun j hj => by
+        have := hcells (j + 1) (by rw [List.length_cons]; omega)
+        rw [show i + 1 + j = i + (j + 1) from by omega]
+        simpa using this
+
+private theorem cellsCode_of_blank' (t : Tape) (i w : ℕ)
+    (h : ∀ j < w, t.cells (i + j) = Γ.blank) :
+    cellsCode t i w = List.replicate (2 * w) false := by
+  induction w generalizing i with
+  | zero => rfl
+  | succ w ih =>
+      rw [cellsCode_succ_left, show t.cells i = Γ.blank from by simpa using h 0 (by omega),
+        ih (i + 1) fun j hj => by
+          rw [show i + 1 + j = i + (j + 1) from by omega]; exact h (j + 1) (by omega),
+        show 2 * (w + 1) = 2 + 2 * w from by omega, List.replicate_add]
+      rfl
+
+/-- The right half-block of a tape carrying `y` from cell `1`, head at cell 1. -/
+private theorem padTo_rightCode_choiceTape (W : ℕ) (c : List Bool) (hc : c.length ≤ W) :
+    padTo (blockRuler W) (rightCode (choiceTape c) W)
+      = padTo (blockRuler W) (encodeBits c) := by
+  have h1 : cellsCode (choiceTape c) 1 c.length = encodeBits c :=
+    cellsCode_of_bits' c _ 1 fun j hj => by
+      rw [choiceTape_cells, show 1 + j = j + 1 from by omega, Tape.init_cells_succ]
+      have hjm : j < (c.map Γ.ofBool).length := by simpa using hj
+      rw [List.getElem?_eq_getElem hjm]
+      simp
+  have h2 : cellsCode (choiceTape c) (1 + c.length) (W - c.length)
+      = List.replicate (2 * (W - c.length)) false :=
+    cellsCode_of_blank' _ _ _ fun j _ => by
+      rw [choiceTape_cells, show 1 + c.length + j = (c.length + j) + 1 from by omega,
+        Tape.init_cells_succ, List.getElem?_eq_none (by simp)]
+      rfl
+  have hcells : cellsCode (choiceTape c) 1 W
+      = encodeBits c ++ List.replicate (2 * (W - c.length)) false := by
+    rw [show W = c.length + (W - c.length) from by omega,
+      cellsCode_add _ 1 c.length _]
+    rw [h1]
+    congr 1
+    rw [show c.length + (W - c.length) - c.length = W - c.length from by omega]
+    exact h2
+  rw [rightCode, choiceTape_head, show W + 1 - 1 = W from by omega, hcells,
+    padTo_append_replicate]
+
+/-- **The encoder computes the encoding of the starting configuration.** -/
+theorem initChoiceFn_eq (tm : NTM k) (W : ℕ) (x c : List Bool)
+    (hx : x.length ≤ W) (hc : c.length ≤ W) :
+    initChoiceFn tm (blockRuler W) x c = cfgCode W (choiceCfg tm x c) := by
+  set R := blockRuler W with hR
+  have hin : padTo R (rightCode (Tape.init (x.map Γ.ofBool)) W)
+      = padTo R (symCode Γ.start ++ encodeBits x) := by
+    have h0 : cellsCode (Tape.init (x.map Γ.ofBool)) 0 1 = symCode Γ.start := by
+      rw [cellsCode_succ_left, cellsCode_zero, List.append_nil, Tape.init_cells_zero]
+    have h1 : cellsCode (Tape.init (x.map Γ.ofBool)) 1 x.length = encodeBits x :=
+      cellsCode_of_bits' x _ 1 fun j hj => by
+        rw [show 1 + j = j + 1 from by omega, Tape.init_cells_succ]
+        have hjm : j < (x.map Γ.ofBool).length := by simpa using hj
+        rw [List.getElem?_eq_getElem hjm]
+        simp
+    have h2 : cellsCode (Tape.init (x.map Γ.ofBool)) (1 + x.length) (W - x.length)
+        = List.replicate (2 * (W - x.length)) false :=
+      cellsCode_of_blank' _ _ _ fun j _ => by
+        rw [show 1 + x.length + j = (x.length + j) + 1 from by omega,
+          Tape.init_cells_succ, List.getElem?_eq_none (by simp)]
+        rfl
+    have hcells : cellsCode (Tape.init (x.map Γ.ofBool)) 0 (W + 1)
+        = symCode Γ.start ++ (encodeBits x
+            ++ List.replicate (2 * (W - x.length)) false) := by
+      rw [show W + 1 = 1 + (x.length + (W - x.length)) from by omega,
+        cellsCode_add _ 0 1 _, cellsCode_add _ (0 + 1) x.length _]
+      simp only [Nat.zero_add]
+      rw [h0, h1, h2]
+    rw [rightCode, Tape.init_head, Nat.sub_zero, hcells, ← List.append_assoc,
+      padTo_append_replicate]
+  have hblank : padTo R (rightCode (Tape.init []) W) = padTo R (symCode Γ.start) := by
+    have h0 : cellsCode (Tape.init ([] : List Γ)) 0 1 = symCode Γ.start := by
+      rw [cellsCode_succ_left, cellsCode_zero, List.append_nil, Tape.init_cells_zero]
+    have h2 : cellsCode (Tape.init ([] : List Γ)) 1 W
+        = List.replicate (2 * W) false :=
+      cellsCode_of_blank' _ _ _ fun j _ => by
+        rw [show 1 + j = j + 1 from by omega, Tape.init_nil_cells_succ]
+    have hcells : cellsCode (Tape.init ([] : List Γ)) 0 (W + 1)
+        = symCode Γ.start ++ List.replicate (2 * W) false := by
+      rw [show W + 1 = 1 + W from by omega, cellsCode_add _ 0 1 W]
+      simp only [Nat.zero_add]
+      rw [h0, h2]
+    rw [rightCode, Tape.init_head, Nat.sub_zero, hcells, padTo_append_replicate]
+  have hleft : ∀ contents : List Γ, leftCode (Tape.init contents) = [] := fun _ => rfl
+  have hcleft : leftCode (choiceTape c) = symCode Γ.start := by
+    rw [leftCode, choiceTape_head, leftCodeFrom_succ, leftCodeFrom_zero,
+      List.append_nil, choiceTape_cells, Tape.init_cells_zero]
+  have hct : cfgTapes (choiceCfg tm x c)
+      = Tape.init (x.map Γ.ofBool)
+          :: (List.replicate (k + 1) (Tape.init []) ++ [choiceTape c]) := by
+    rw [cfgTapes]
+    congr 1
+    show (Tape.init [] : Tape) :: List.ofFn (fun i : Fin (k + 1) =>
+        if i = Fin.last k then choiceTape c else (Tape.init [] : Tape))
+      = List.replicate (k + 1) (Tape.init []) ++ [choiceTape c]
+    rw [List.ofFn_succ']
+    have hcast : (List.ofFn fun i : Fin k =>
+        (if i.castSucc = Fin.last k then choiceTape c else (Tape.init [] : Tape)))
+        = List.replicate k (Tape.init []) := by
+      rw [show (fun i : Fin k =>
+          (if i.castSucc = Fin.last k then choiceTape c else (Tape.init [] : Tape)))
+          = fun _ : Fin k => (Tape.init [] : Tape) from by
+        funext i
+        rw [if_neg (Fin.castSucc_lt_last i).ne]]
+      rw [List.ofFn_const]
+    rw [hcast, if_pos rfl, List.replicate_succ]
+    simp
+  rw [cfgCode, cfgBlocks_eq, List.flatten_cons, flatten_tapesBlocks', hct]
+  simp only [List.map_cons, List.map_nil, List.map_append, List.map_replicate,
+    List.flatten_cons, List.flatten_nil, List.flatten_append, List.append_nil,
+    hleft, hcleft]
+  rw [hin, hblank, padTo_rightCode_choiceTape W c hc]
+  show _ = padTo R (stateCode tm.qstart) ++ _
+  rw [initChoiceFn]
+  simp only [← hR, List.append_assoc]
+
+/-! ## Iterating the encoded step from a choice configuration -/
+
+/-- Every tape of a run from a choice configuration keeps its left-end
+marker. -/
+theorem runCfg_choiceCfg_startInvariant (tm : NTM k) (x c : List Bool) (n : ℕ) :
+    (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n).input.StartInvariant ∧
+      (∀ i, ((TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n).work i).StartInvariant) ∧
+      (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n).output.StartInvariant := by
+  induction n with
+  | zero =>
+      refine ⟨Tape.StartInvariant.init_ofBool x, fun i => ?_, Tape.StartInvariant.init_nil⟩
+      show (if i = Fin.last k then choiceTape c else Tape.init []).StartInvariant
+      split
+      · exact Tape.StartInvariant.init_ofBool c
+      · exact Tape.StartInvariant.init_nil
+  | succ n ih =>
+      rw [TM.runCfg_succ]
+      cases hs : (NTM.choiceTM tm).step (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n) with
+      | none => rw [Option.getD_none]; exact ih
+      | some c' =>
+          rw [Option.getD_some]
+          exact TM.step_startInvariant _ hs ih.1 ih.2.1 ih.2.2
+
+/-- After `n` steps of a run from a choice configuration every head is within
+`n + 1` cells of the start: the choice head begins one cell in. -/
+theorem runCfg_choiceCfg_head_le (tm : NTM k) (x c : List Bool) (n : ℕ) :
+    (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n).input.head ≤ n + 1 ∧
+      (∀ i, ((TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n).work i).head ≤ n + 1) ∧
+      (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n).output.head ≤ n + 1 := by
+  induction n with
+  | zero =>
+      refine ⟨by simp [choiceCfg], fun i => ?_, by simp [choiceCfg]⟩
+      show (if i = Fin.last k then choiceTape c else Tape.init []).head ≤ 0 + 1
+      split <;> simp
+  | succ n ih =>
+      rw [TM.runCfg_succ]
+      cases hs : (NTM.choiceTM tm).step (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n) with
+      | none =>
+          rw [Option.getD_none]
+          exact ⟨by omega, fun i => by have := ih.2.1 i; omega, by omega⟩
+      | some c' =>
+          rw [Option.getD_some]
+          obtain ⟨h1, h2, h3⟩ := TM.step_head_le _ hs
+          exact ⟨by omega, fun i => by have := h2 i; have := ih.2.1 i; omega, by omega⟩
+
+/-- The invariants of a choice run, in the form the encoding lemmas want. -/
+theorem cfgTapes_runCfg_choiceCfg_inv (tm : NTM k) (x c : List Bool) (n W : ℕ)
+    (hn : n + 1 ≤ W) :
+    (∀ t ∈ cfgTapes (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n), t.StartInvariant) ∧
+      (∀ t ∈ cfgTapes (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n), t.head ≤ W) := by
+  obtain ⟨i1, w1, o1⟩ := runCfg_choiceCfg_startInvariant tm x c n
+  obtain ⟨i2, w2, o2⟩ := runCfg_choiceCfg_head_le tm x c n
+  constructor <;> intro t ht <;>
+    · rw [cfgTapes, List.mem_cons, List.mem_cons, List.mem_ofFn] at ht
+      rcases ht with rfl | rfl | ⟨i, rfl⟩
+      · first | exact i1 | omega
+      · first | exact o1 | omega
+      · first | exact w1 i | (have := w2 i; omega)
+
+/-- **The encoded iteration tracks a choice run.** -/
+theorem iterate_stepFn_choice (tm : NTM k) (W : ℕ) (x c : List Bool)
+    (hq : Fintype.card tm.Q ≤ blockWidth W) :
+    ∀ n : ℕ, n + 1 ≤ W →
+      (stepFn (NTM.choiceTM tm) (blockRuler W))^[n] (cfgCode W (choiceCfg tm x c))
+        = cfgCode W (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n) := by
+  intro n
+  induction n with
+  | zero => intro _; rfl
+  | succ n ih =>
+      intro hn
+      obtain ⟨hinv, hW⟩ := cfgTapes_runCfg_choiceCfg_inv tm x c n W (by omega)
+      rw [Function.iterate_succ_apply', ih (by omega), TM.runCfg_succ]
+      cases hs : (NTM.choiceTM tm).step (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) n) with
+      | none =>
+          rw [Option.getD_none]
+          exact stepFn_halted _ (TM.step_eq_none_iff_halted.mp hs) hq hW
+      | some c' =>
+          rw [Option.getD_some]
+          have hgood := stepActs_forall₂ _ _ hinv hW
+          refine stepFn_eq _ hs hq hW ?_ ?_ hgood
+          · exact hinv _ (by simp [cfgTapes])
+          · intro i
+            exact hinv _ (by
+              rw [cfgTapes]
+              exact List.mem_cons_of_mem _ (List.mem_cons_of_mem _
+                (List.mem_ofFn.mpr ⟨i, rfl⟩)))
+
+/-! ## Running the path inside the algebra -/
+
+@[simp] theorem initChoiceFn_length (tm : NTM k) (R x c : List Bool) :
+    (initChoiceFn tm R x c).length = (2 * (k + 3) + 1) * R.length := by
+  rw [initChoiceFn]
+  simp only [List.length_append, padTo_length, List.length_flatten,
+    List.map_replicate, List.sum_replicate]
+  simp
+  ring
+
+/-- The encoded run stays inside its blocks. -/
+theorem iterate_stepFn_choice_length_le (tm : NTM k) (R x c : List Bool) (n : ℕ) :
+    ((stepFn (NTM.choiceTM tm) R)^[n] (initChoiceFn tm R x c)).length
+      ≤ (2 * (k + 3) + 1) * R.length := by
+  induction n with
+  | zero => exact (initChoiceFn_length tm R x c).le
+  | succ n ih =>
+      rw [Function.iterate_succ_apply']
+      exact stepFn_length_le _ R _ ih
+
+/-- The encoded configuration after running the path for `|c|` steps, under a
+ruler derived from the clock string `u`. -/
+noncomputable def runChoiceFn (tm : NTM k) (u x c : List Bool) : List Bool :=
+  (stepFn (NTM.choiceTM tm) (clockRuler u))^[c.length]
+    (initChoiceFn tm (clockRuler u) x c)
+
+/-- **Running the path is in the algebra.** -/
+theorem runChoiceFn_mem {n : ℕ} (tm : NTM k)
+    {gu gx gc : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hc : Cobham gc) :
+    Cobham fun v : Fin n → List Bool => runChoiceFn tm (gu v) (gx v) (gc v) := by
+  have hstage :=
+    iterFn (n := 3)
+      (e := fun w : Fin 3 → List Bool =>
+        initChoiceFn tm (clockRuler (w 1)) (w 2) (w 0))
+      (f := fun w : Fin 4 → List Bool =>
+        stepFn (NTM.choiceTM tm) (clockRuler (w 2)) (w 0))
+      (j := fun w : Fin 4 → List Bool =>
+        (List.replicate (2 * (k + 3) + 1) (clockRuler (w 2))).flatten)
+      (initChoiceFn_mem tm (clockRulerFn (Cobham.proj 1)) (Cobham.proj 2) (Cobham.proj 0))
+      (stepFn_mem _ (clockRulerFn (Cobham.proj 2)) (Cobham.proj 0))
+      (repeatFn (clockRulerFn (Cobham.proj 2)) _)
+      (by
+        intro c v
+        have hlen := iterate_stepFn_choice_length_le tm (clockRuler (v 1)) (v 2) (v 0) c.length
+        simp only [List.length_flatten, List.map_replicate, List.sum_replicate]
+        simpa using hlen)
+  have hg : ∀ i : Fin 4, Cobham (![gc, gc, gu, gx] i) := by
+    intro i
+    match i with
+    | 0 => exact hc
+    | 1 => exact hc
+    | 2 => exact hu
+    | 3 => exact hx
+  refine (Cobham.comp hstage hg).of_eq fun v => ?_
+  rfl
+
+/-! ## Reading the verdict -/
+
+/-- The output tape's two half-blocks after the run, rewound to cell `0`. -/
+noncomputable def outPairChoiceFn (tm : NTM k) (u x c : List Bool) : List Bool :=
+  (rewindFn (clockRuler u))^[u.length]
+    (blockAt (clockRuler u) (runChoiceFn tm u x c) 3
+      ++ blockAt (clockRuler u) (runChoiceFn tm u x c) 4)
+
+/-- **The rewind stage is in the algebra.** -/
+theorem outPairChoiceFn_mem {n : ℕ} (tm : NTM k)
+    {gu gx gc : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hc : Cobham gc) :
+    Cobham fun v : Fin n → List Bool => outPairChoiceFn tm (gu v) (gx v) (gc v) := by
+  have hstage :=
+    iterFn (n := 3)
+      (e := fun w : Fin 3 → List Bool =>
+        blockAt (clockRuler (w 0)) (runChoiceFn tm (w 0) (w 1) (w 2)) 3
+          ++ blockAt (clockRuler (w 0)) (runChoiceFn tm (w 0) (w 1) (w 2)) 4)
+      (f := fun w : Fin 4 → List Bool => rewindFn (clockRuler (w 1)) (w 0))
+      (j := fun w : Fin 4 → List Bool => clockRuler (w 1) ++ clockRuler (w 1))
+      (appendFn
+        (blockFn (clockRulerFn (Cobham.proj 0))
+          (runChoiceFn_mem tm (Cobham.proj 0) (Cobham.proj 1) (Cobham.proj 2)) 3)
+        (blockFn (clockRulerFn (Cobham.proj 0))
+          (runChoiceFn_mem tm (Cobham.proj 0) (Cobham.proj 1) (Cobham.proj 2)) 4))
+      (rewindFn_mem (clockRulerFn (Cobham.proj 1)) (Cobham.proj 0))
+      (appendFn (clockRulerFn (Cobham.proj 1)) (clockRulerFn (Cobham.proj 1)))
+      (by
+        intro c v
+        show ((rewindFn (clockRuler (v 0)))^[c.length]
+            (blockAt (clockRuler (v 0)) (runChoiceFn tm (v 0) (v 1) (v 2)) 3
+              ++ blockAt (clockRuler (v 0)) (runChoiceFn tm (v 0) (v 1) (v 2)) 4)).length
+          ≤ (clockRuler (v 0) ++ clockRuler (v 0)).length
+        rw [List.length_append]
+        refine le_trans (iterate_rewindFn_length_le _ _ ?_ _) (by omega)
+        rw [List.length_append, blockAt, blockAt, List.length_take, List.length_take]
+        omega)
+  have hg : ∀ i : Fin 4, Cobham (![gu, gu, gx, gc] i) := by
+    intro i
+    match i with
+    | 0 => exact hu
+    | 1 => exact hu
+    | 2 => exact hx
+    | 3 => exact hc
+  refine (Cobham.comp hstage hg).of_eq fun v => ?_
+  rfl
+
+/-- The verdict of the path: the machine halted with `1` on output cell `1`. -/
+noncomputable def acceptChoiceFn (tm : NTM k) (u x c : List Bool) : List Bool :=
+  andBit
+    (matchPrefix (stateCode tm.qhalt) (blockAt (clockRuler u) (runChoiceFn tm u x c) 0))
+    (matchPrefix (symCode Γ.one)
+      (((outPairChoiceFn tm u x c).drop (clockRuler u).length).drop 2))
+
+/-- The verdict is a genuine one-bit flag. -/
+theorem acceptChoiceFn_flag (tm : NTM k) (u x c : List Bool) :
+    acceptChoiceFn tm u x c = [true] ∨ acceptChoiceFn tm u x c = [false] :=
+  andBit_flag _ _
+
+/-- **The verdict is in the algebra.** -/
+theorem acceptChoiceFn_mem {n : ℕ} (tm : NTM k)
+    {gu gx gc : (Fin n → List Bool) → List Bool}
+    (hu : Cobham gu) (hx : Cobham gx) (hc : Cobham gc) :
+    Cobham fun v : Fin n → List Bool => acceptChoiceFn tm (gu v) (gx v) (gc v) :=
+  andFn
+    (matchPrefixFn (blockFn (clockRulerFn hu) (runChoiceFn_mem tm hu hx hc) 0) _)
+    (matchPrefixFn
+      (dropFn (Cobham.const (List.replicate 2 false))
+        (dropFn (clockRulerFn hu) (outPairChoiceFn_mem tm hu hx hc))) _)
+
+/-! ## The run is the nondeterministic trace -/
+
+/-- The choice bits found on the choice tape are the bits of `c`. -/
+theorem choiceStream_choiceCfg (tm : NTM k) (x c : List Bool) (j : ℕ) (hj : j < c.length) :
+    NTM.choiceStream (choiceCfg tm x c) j = c[j] := by
+  have hwork : (choiceCfg tm x c).work (Fin.last k) = choiceTape c := by
+    simp [choiceCfg]
+  rw [NTM.choiceStream, hwork, choiceTape_head, choiceTape_cells,
+    show 1 + j = j + 1 from by omega, Tape.init_cells_succ]
+  have hjm : j < (c.map Γ.ofBool).length := by simpa using hj
+  rw [List.getElem?_eq_getElem hjm]
+  cases hb : c[j] <;> simp [hb, Γ.ofBool]
+
+/-- **The deterministic run from a choice configuration is the trace.** -/
+theorem dropChoice_runCfg_choiceCfg (tm : NTM k) (T : ℕ) (x c : List Bool) :
+    NTM.dropChoice (TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) T)
+      = tm.trace T (fun j => NTM.choiceStream (choiceCfg tm x c) j.val) (tm.initCfg x) := by
+  obtain ⟨c', t, hle, hreach, hstop, heq⟩ :=
+    NTM.choiceTM_simulates tm T (choiceCfg tm x c)
+      (by
+        have hwork : (choiceCfg tm x c).work (Fin.last k) = choiceTape c := by
+          simp [choiceCfg]
+        rw [hwork]
+        exact Tape.StartInvariant.init_ofBool c)
+      (by
+        have hwork : (choiceCfg tm x c).work (Fin.last k) = choiceTape c := by
+          simp [choiceCfg]
+        rw [hwork, choiceTape_head])
+  have hrun : TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) T = c' := by
+    have hpart : TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) t = c' :=
+      TM.runCfg_of_reachesIn _ hreach
+    rcases Nat.lt_or_ge t T with hlt | hge
+    · have hhalt := hstop hlt
+      rw [show T = t + (T - t) from by omega, TM.runCfg_add, hpart,
+        TM.runCfg_of_halted _ hhalt]
+    · have : t = T := by omega
+      rw [← this, hpart]
+  rw [hrun]
+  simpa using heq
+
+/-! ## The verdict is the path's verdict -/
+
+private theorem andBit_eq_true_iff {x y : List Bool}
+    (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) :
+    andBit x y = [true] ↔ x = [true] ∧ y = [true] := by
+  rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> simp [andBit]
+
+/-- The predicate the verdict computes: after `|c|` steps along the choice bits
+of `c`, the machine has halted with `1` on the first output cell. -/
+def PathAccepts (tm : NTM k) (x c : List Bool) : Prop :=
+  (tm.trace c.length (fun j => c[j.val]'j.isLt) (tm.initCfg x)).state = tm.qhalt ∧
+    (tm.trace c.length (fun j => c[j.val]'j.isLt) (tm.initCfg x)).output.cells 1 = Γ.one
+
+/-- **The algebra's verdict is the path's verdict.** -/
+theorem acceptChoiceFn_eq_true_iff (tm : NTM k) (u x c : List Bool)
+    (hlen : x.length + c.length + Fintype.card tm.Q + 3 ≤ u.length) :
+    acceptChoiceFn tm u x c = [true] ↔ PathAccepts tm x c := by
+  classical
+  have hu1 : 1 ≤ u.length := by omega
+  have hR : clockRuler u = blockRuler (u.length - 1) := clockRuler_eq hu1
+  have hq : Fintype.card tm.Q ≤ blockWidth (u.length - 1) := by
+    rw [blockWidth]; omega
+  set W := u.length - 1 with hWdef
+  set c' := TM.runCfg (NTM.choiceTM tm) (choiceCfg tm x c) c.length with hc'def
+  have hrun : runChoiceFn tm u x c = cfgCode W c' := by
+    rw [runChoiceFn, hR, initChoiceFn_eq tm W x c (by omega) (by omega),
+      iterate_stepFn_choice tm W x c hq c.length (by omega)]
+  -- the state half
+  have hQcard : Fintype.card (NTM.choiceTM tm).Q = Fintype.card tm.Q := rfl
+  have hblk0 : (cfgBlocks W c')[0]'(by rw [cfgBlocks_length]; omega)
+      = padTo (blockRuler W) (stateCode c'.state) := rfl
+  have hstate : blockAt (clockRuler u) (runChoiceFn tm u x c) 0
+      = padTo (blockRuler W) (stateCode c'.state) := by
+    rw [hrun, hR, blockAt_cfgCode W c' 0 (by rw [cfgBlocks_length]; omega), hblk0]
+  have hcard : (stateCode c'.state).length = (stateCode tm.qhalt).length := by
+    rw [stateCode_length, stateCode_length]
+    exact hQcard
+  have hstateiff : matchPrefix (stateCode tm.qhalt)
+      (blockAt (clockRuler u) (runChoiceFn tm u x c) 0) = [true] ↔ c'.state = tm.qhalt := by
+    rw [hstate, matchPrefix_eq_true_iff,
+      padTo_eq_append _ _ (by
+        rw [stateCode_length, blockRuler_length, hQcard, blockWidth]
+        omega)]
+    constructor
+    · rintro ⟨t, ht⟩
+      have := List.append_inj_left ht hcard.symm
+      exact (stateCode_injective this).symm
+    · intro h
+      rw [h]
+      exact ⟨_, rfl⟩
+  -- the output half
+  obtain ⟨hinvs, hheads⟩ := cfgTapes_runCfg_choiceCfg_inv tm x c c.length W (by omega)
+  have hmem : c'.output ∈ cfgTapes c' := by simp [cfgTapes]
+  have hinv : c'.output.StartInvariant := hinvs _ hmem
+  have hhead : c'.output.head ≤ W := hheads _ hmem
+  obtain ⟨hb3, hb4⟩ := blockAt_cfgCode_tape W c' 1 (by rw [cfgTapes_length]; omega)
+  have hidx : (cfgTapes c')[1]'(by rw [cfgTapes_length]; omega) = c'.output := rfl
+  rw [hidx, show 2 * 1 + 1 = 3 from rfl] at hb3
+  rw [hidx, show 2 * 1 + 2 = 4 from rfl] at hb4
+  have hpair : blockAt (clockRuler u) (runChoiceFn tm u x c) 3
+      ++ blockAt (clockRuler u) (runChoiceFn tm u x c) 4 = pairCode W c'.output := by
+    rw [hrun, hR, hb3, hb4, pairCode]
+  have hrew : outPairChoiceFn tm u x c
+      = pairCode W { head := 0, cells := c'.output.cells } := by
+    rw [outPairChoiceFn, hpair, hR, iterate_rewindFn c'.output hinv hhead u.length,
+      rewound c'.output (by omega)]
+  have hdrop : ((outPairChoiceFn tm u x c).drop (clockRuler u).length).drop 2
+      = cellsCode c'.output 1 W := by
+    rw [hrew, hR, drop_pairCode_rewound, show W + 1 = 1 + W from by omega,
+      cellsCode_add c'.output 0 1 W]
+    rw [cellsCode_succ_left, cellsCode_zero, List.append_nil]
+    cases c'.output.cells 0 <;> simp [symCode]
+  have houtiff : matchPrefix (symCode Γ.one)
+      (((outPairChoiceFn tm u x c).drop (clockRuler u).length).drop 2) = [true]
+      ↔ c'.output.cells 1 = Γ.one := by
+    rw [hdrop, show W = 1 + (W - 1) from by omega, cellsCode_add c'.output 1 1 (W - 1),
+      matchPrefix_eq_true_iff]
+    have hcell : cellsCode c'.output 1 1 = symCode (c'.output.cells 1) := by
+      rw [cellsCode_succ_left, cellsCode_zero, List.append_nil]
+    rw [hcell]
+    constructor
+    · rintro ⟨t, ht⟩
+      have hl : (symCode Γ.one).length = (symCode (c'.output.cells 1)).length := by
+        cases c'.output.cells 1 <;> rfl
+      exact (symCode_injective (List.append_inj_left ht hl)).symm
+    · rintro h
+      rw [h]
+      exact ⟨_, rfl⟩
+  -- assemble
+  rw [acceptChoiceFn, andBit_eq_true_iff (matchPrefix_flag _ _) (matchPrefix_flag _ _),
+    hstateiff, houtiff]
+  have htrace : NTM.dropChoice c' = tm.trace c.length (fun j => c[j.val]'j.isLt)
+      (tm.initCfg x) := by
+    rw [hc'def, dropChoice_runCfg_choiceCfg]
+    congr 1
+    funext j
+    exact choiceStream_choiceCfg tm x c j.val j.isLt
+  have hstate' : c'.state = (tm.trace c.length (fun j => c[j.val]'j.isLt)
+      (tm.initCfg x)).state := by rw [← htrace]; rfl
+  have hout' : c'.output = (tm.trace c.length (fun j => c[j.val]'j.isLt)
+      (tm.initCfg x)).output := by rw [← htrace]; rfl
+  rw [hstate', hout']
+  rfl
+
+end Cobham
+
+end Complexity
diff --git a/Complexitylib/Classes/P/Cobham/Internal/PolyLen.lean b/Complexitylib/Classes/P/Cobham/Internal/PolyLen.lean
new file mode 100644
index 00000000..9eeb09dc
--- /dev/null
+++ b/Complexitylib/Classes/P/Cobham/Internal/PolyLen.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.Cobham.Internal.Algebra
+public import Mathlib.Algebra.Polynomial.Eval.Degree
+
+/-!
+# Polynomial lengths inside the algebra
+
+A computation in Cobham's algebra measures sizes by string lengths, so a
+polynomial time or space bound has to be available as a *string of that
+length*. `smash` multiplies lengths and concatenation adds them, so Horner's
+scheme builds, for any polynomial with natural coefficients, a member of the
+algebra whose output has exactly the polynomial's value as its length.
+
+## Main definitions
+
+- `Cobham.hornerEval` — Horner evaluation of a coefficient list
+- `Cobham.lenOfCoeffs` — the string realizing that value as its length
+- `Cobham.polyLen` — the same for a `Polynomial ℕ`
+
+## Main results
+
+- `Cobham.lenOfCoeffs_mem`, `Cobham.polyLen_mem` — both are in the algebra
+- `Cobham.polyLen_length` — `polyLen q s` has length exactly `q.eval |s|`
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Cobham
+
+/-- Horner evaluation of a coefficient list, lowest coefficient first. -/
+def hornerEval : List ℕ → ℕ → ℕ
+  | [], _ => 0
+  | a :: as, n => a + n * hornerEval as n
+
+/-- The string whose length is the Horner value of the coefficient list at
+`|s|`: constants contribute blocks of that many bits, and each multiplication
+by `|s|` is one `smash`. -/
+def lenOfCoeffs : List ℕ → List Bool → List Bool
+  | [], _ => []
+  | a :: as, s => List.replicate a false ++ Complexity.smash s (lenOfCoeffs as s)
+
+@[simp] theorem lenOfCoeffs_length (as : List ℕ) (s : List Bool) :
+    (lenOfCoeffs as s).length = hornerEval as s.length := by
+  induction as with
+  | nil => rfl
+  | cons a as ih =>
+      rw [lenOfCoeffs, hornerEval, List.length_append, List.length_replicate,
+        smash_length, ih]
+
+/-- **The Horner string is in the algebra.** -/
+theorem lenOfCoeffs_mem {n : ℕ} (as : List ℕ)
+    {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => lenOfCoeffs as (g v) := by
+  induction as with
+  | nil => exact (Cobham.const []).of_eq fun _ => rfl
+  | cons a as ih =>
+      exact (appendFn (Cobham.const (List.replicate a false))
+        (comp₂ Cobham.smash hg ih)).of_eq fun _ => by simp [lenOfCoeffs]
+
+/-- Horner evaluation of a truncated coefficient sequence is the truncated
+power sum. -/
+theorem hornerEval_map_range (f : ℕ → ℕ) (d n : ℕ) :
+    hornerEval ((List.range d).map f) n = ∑ i ∈ Finset.range d, f i * n ^ i := by
+  induction d generalizing f with
+  | zero => rfl
+  | succ d ih =>
+      rw [List.range_succ_eq_map, List.map_cons, List.map_map, hornerEval,
+        ih (f ∘ Nat.succ), Finset.sum_range_succ' (fun i => f i * n ^ i) d]
+      simp only [Function.comp_apply, pow_zero, mul_one]
+      have hmul : n * ∑ i ∈ Finset.range d, f (i + 1) * n ^ i
+          = ∑ i ∈ Finset.range d, f (i + 1) * n ^ (i + 1) := by
+        rw [Finset.mul_sum]
+        exact Finset.sum_congr rfl fun i _ => by ring
+      rw [hmul]
+      omega
+
+/-- The string realizing a polynomial's value as its length. -/
+noncomputable def polyLen (q : Polynomial ℕ) (s : List Bool) : List Bool :=
+  lenOfCoeffs ((List.range (q.natDegree + 1)).map q.coeff) s
+
+/-- **The polynomial's value is the string's length.** -/
+@[simp] theorem polyLen_length (q : Polynomial ℕ) (s : List Bool) :
+    (polyLen q s).length = q.eval s.length := by
+  rw [polyLen, lenOfCoeffs_length, hornerEval_map_range, Polynomial.eval_eq_sum_range]
+
+/-- **The polynomial-length string is in the algebra.** -/
+theorem polyLen_mem {n : ℕ} (q : Polynomial ℕ)
+    {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => polyLen q (g v) :=
+  lenOfCoeffs_mem _ hg
+
+end Cobham
+
+end Complexity
diff --git a/Complexitylib/Classes/P/Cobham/Internal/StringOps.lean b/Complexitylib/Classes/P/Cobham/Internal/StringOps.lean
new file mode 100644
index 00000000..3fb6b3a8
--- /dev/null
+++ b/Complexitylib/Classes/P/Cobham/Internal/StringOps.lean
@@ -0,0 +1,278 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.Cobham.Internal.Algebra
+
+/-!
+# Length tests and bitwise operations inside the algebra
+
+Two utilities the algebra needs for block-structured data: comparing the
+lengths of two strings, and taking the bitwise exclusive-or of two strings of
+equal length.
+
+Both are built from the dispatchers of
+`Complexitylib.Classes.P.Cobham.Internal.Blocks`: a length comparison is a
+`drop` followed by an emptiness test, and the exclusive-or is one limited
+recursion whose step reads the matching bit of the second argument through a
+ruler cut to the right width.
+
+## Main definitions
+
+- `Cobham.lenLeFlag`, `Cobham.lenEqFlag` — length comparison flags
+- `Cobham.xorSuffix` — exclusive-or of a string with the matching suffix of a
+  second string
+
+## Main results
+
+- `Cobham.lenLeFlag_eq_true_iff`, `Cobham.lenEqFlag_eq_true_iff`
+- `Cobham.lenLeFlag_mem`, `Cobham.lenEqFlag_mem`
+- `Cobham.andBit_eq_true_iff` — conjunction of flags
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Cobham
+
+/-- Conjunction of two flags is `[true]` exactly when both are. -/
+theorem andBit_eq_true_iff {x y : List Bool}
+    (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) :
+    andBit x y = [true] ↔ x = [true] ∧ y = [true] := by
+  rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> simp [andBit]
+
+/-- Disjunction of two flags is `[true]` exactly when one is. -/
+theorem orBit_eq_true_iff {x y : List Bool}
+    (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) :
+    orBit x y = [true] ↔ x = [true] ∨ y = [true] := by
+  rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> simp [orBit]
+
+/-- Disjunction of flags is a flag. -/
+theorem orBit_flag {x y : List Bool}
+    (hx : x = [true] ∨ x = [false]) (hy : y = [true] ∨ y = [false]) :
+    orBit x y = [true] ∨ orBit x y = [false] := by
+  rcases hx with rfl | rfl <;> rcases hy with rfl | rfl <;> simp [orBit]
+
+/-- A disjunction is always exactly one bit long. -/
+theorem orBit_length (x y : List Bool) : (orBit x y).length = 1 := by
+  rw [orBit]
+  rcases x with _ | ⟨a, x⟩
+  · rcases y with _ | ⟨c, y⟩
+    · rfl
+    · cases c <;> rfl
+  · cases a
+    · rcases y with _ | ⟨c, y⟩
+      · rfl
+      · cases c <;> rfl
+    · rfl
+
+/-- Negation of a flag. -/
+theorem notBit_eq_true_iff {x : List Bool} (hx : x = [true] ∨ x = [false]) :
+    notBit x = [true] ↔ x = [false] := by
+  rcases hx with rfl | rfl <;> simp [notBit]
+
+/-- The flag `|b| ≤ |a|`: nothing is left of `b` after dropping `|a|` bits. -/
+def lenLeFlag (a b : List Bool) : List Bool := notBit (nonemptyFlag (b.drop a.length))
+
+/-- The flag `|a| = |b|`. -/
+def lenEqFlag (a b : List Bool) : List Bool := andBit (lenLeFlag a b) (lenLeFlag b a)
+
+theorem lenLeFlag_flag (a b : List Bool) :
+    lenLeFlag a b = [true] ∨ lenLeFlag a b = [false] := by
+  rw [lenLeFlag, nonemptyFlag]
+  rcases hb : b.drop a.length with _ | ⟨c, z⟩
+  · exact Or.inl rfl
+  · cases c <;> exact Or.inr rfl
+
+@[simp] theorem lenLeFlag_eq_true_iff (a b : List Bool) :
+    lenLeFlag a b = [true] ↔ b.length ≤ a.length := by
+  rw [lenLeFlag, nonemptyFlag]
+  rcases hb : b.drop a.length with _ | ⟨c, z⟩
+  · have : b.length ≤ a.length := by
+      have := List.length_drop (i := a.length) (l := b)
+      rw [hb] at this
+      simp at this
+      omega
+    simp [notBit, this]
+  · have hlt : a.length < b.length := by
+      have hlen := List.length_drop (i := a.length) (l := b)
+      rw [hb] at hlen
+      simp at hlen
+      omega
+    cases c <;> simp [notBit, Nat.not_le.mpr hlt]
+
+theorem lenEqFlag_flag (a b : List Bool) :
+    lenEqFlag a b = [true] ∨ lenEqFlag a b = [false] := by
+  rw [lenEqFlag]
+  rcases lenLeFlag_flag a b with h | h <;> rcases lenLeFlag_flag b a with h' | h' <;>
+    rw [h, h'] <;> simp [andBit]
+
+@[simp] theorem lenEqFlag_eq_true_iff (a b : List Bool) :
+    lenEqFlag a b = [true] ↔ a.length = b.length := by
+  rw [lenEqFlag, andBit_eq_true_iff (lenLeFlag_flag a b) (lenLeFlag_flag b a),
+    lenLeFlag_eq_true_iff, lenLeFlag_eq_true_iff]
+  omega
+
+/-- **The length tests are in the algebra.** -/
+theorem lenLeFlag_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool}
+    (ha : Cobham ga) (hb : Cobham gb) :
+    Cobham fun v : Fin n → List Bool => lenLeFlag (ga v) (gb v) :=
+  (notFn (nonemptyFn (dropFn ha hb))).of_eq fun _ => rfl
+
+theorem lenEqFlag_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool}
+    (ha : Cobham ga) (hb : Cobham gb) :
+    Cobham fun v : Fin n → List Bool => lenEqFlag (ga v) (gb v) :=
+  (andFn (lenLeFlag_mem ha hb) (lenLeFlag_mem hb ha)).of_eq fun _ => rfl
+
+/-! ## Exclusive-or -/
+
+/-- Exclusive-or of `a` with the suffix of `b` of the same length. The bit of
+`b` paired with the head of `a` sits at index `|b| - |x| - 1`, which is the
+length of `b.drop (|x| + 1)` — a ruler the algebra can build from the
+recursion's own tail. -/
+def xorSuffix : List Bool → List Bool → List Bool
+  | [], _ => []
+  | true :: x, b =>
+      caseBit₀ (notBit (bitAt (b.drop (false :: x).length) b))
+        (true :: xorSuffix x b) (false :: xorSuffix x b)
+  | false :: x, b =>
+      caseBit₀ (bitAt (b.drop (false :: x).length) b)
+        (true :: xorSuffix x b) (false :: xorSuffix x b)
+
+@[simp] theorem xorSuffix_nil (b : List Bool) : xorSuffix [] b = [] := rfl
+
+@[simp] theorem xorSuffix_length (a b : List Bool) :
+    (xorSuffix a b).length = a.length := by
+  induction a with
+  | nil => rfl
+  | cons β x ih =>
+      cases β <;>
+        · rw [xorSuffix]
+          rcases hb : (bitAt (b.drop (false :: x).length) b) with _ | ⟨d, z⟩
+          · simp [notBit, ih]
+          · cases d <;> simp [notBit, ih]
+
+/-- The bit read at the matching position. -/
+private theorem bitAt_drop_eq (x b : List Bool) (h : x.length < b.length) :
+    bitAt (b.drop (false :: x).length) b
+      = [b[b.length - x.length - 1]'(by omega)] := by
+  have hlen : (b.drop (false :: x).length).length = b.length - x.length - 1 := by
+    rw [List.length_drop, List.length_cons]
+    omega
+  rw [bitAt, hlen]
+  have hd : b.drop (b.length - x.length - 1)
+      = b[b.length - x.length - 1]'(by omega) :: b.drop (b.length - x.length) := by
+    have hcons := List.drop_eq_getElem_cons (l := b) (i := b.length - x.length - 1)
+      (by omega)
+    rw [hcons, show b.length - x.length - 1 + 1 = b.length - x.length from by omega]
+  rw [hd]
+  cases b[b.length - x.length - 1]'(by omega) <;> rfl
+
+/-- **The exclusive-or is the pointwise one against the matching suffix.** -/
+theorem xorSuffix_eq_zipWith (a b : List Bool) (h : a.length ≤ b.length) :
+    xorSuffix a b = List.zipWith xor a (b.drop (b.length - a.length)) := by
+  induction a with
+  | nil => simp
+  | cons β x ih =>
+      have hx : x.length < b.length := by
+        rw [List.length_cons] at h
+        omega
+      have hdrop : b.drop (b.length - (β :: x).length)
+          = b[b.length - x.length - 1]'(by omega) :: b.drop (b.length - x.length) := by
+        have h1 : b.length - (β :: x).length = b.length - x.length - 1 := by
+          rw [List.length_cons]
+          omega
+        have hcons := List.drop_eq_getElem_cons (l := b) (i := b.length - x.length - 1)
+          (by omega)
+        rw [h1, hcons, show b.length - x.length - 1 + 1 = b.length - x.length from by omega]
+      rw [hdrop, List.zipWith_cons_cons, ← ih (by omega)]
+      cases β <;>
+        · rw [xorSuffix, bitAt_drop_eq x b hx]
+          cases b[b.length - x.length - 1]'(by omega) <;> simp [notBit]
+
+/-- Two strings of equal length are combined bit by bit. -/
+theorem xorSuffix_eq_zipWith_of_length (a b : List Bool) (h : a.length = b.length) :
+    xorSuffix a b = List.zipWith xor a b := by
+  rw [xorSuffix_eq_zipWith a b h.le, h]
+  simp
+
+/-- The step functions of the exclusive-or recursion. -/
+private def xorStep (β : Bool) (w : Fin 3 → List Bool) : List Bool :=
+  caseBit₀
+    ((bif β then notBit else id) (bitAt ((w 2).drop (false :: w 0).length) (w 2)))
+    (true :: w 1) (false :: w 1)
+
+private theorem xorStep_mem (β : Bool) : Cobham (xorStep β) := by
+  have hprepend : Cobham fun w : Fin 3 → List Bool => false :: w 0 :=
+    (Cobham.comp (Cobham.bit false) fun _ : Fin 1 => Cobham.proj 0).of_eq fun _ => rfl
+  have hbit : Cobham fun w : Fin 3 → List Bool =>
+      bitAt ((w 2).drop (false :: w 0).length) (w 2) :=
+    (comp₂ bitAtFn (dropFn hprepend (Cobham.proj 2)) (Cobham.proj 2)).of_eq fun _ => rfl
+  have hcons1 : Cobham fun w : Fin 3 → List Bool => true :: w 1 :=
+    (Cobham.comp (Cobham.bit true) fun _ : Fin 1 => Cobham.proj 1).of_eq fun _ => rfl
+  have hcons0 : Cobham fun w : Fin 3 → List Bool => false :: w 1 :=
+    (Cobham.comp (Cobham.bit false) fun _ : Fin 1 => Cobham.proj 1).of_eq fun _ => rfl
+  cases β
+  · exact (iteFn hbit hcons1 hcons0).of_eq fun _ => rfl
+  · exact (iteFn (notFn hbit) hcons1 hcons0).of_eq fun _ => rfl
+
+private theorem xorStep_length (β : Bool) (w : Fin 3 → List Bool) :
+    (xorStep β w).length = (w 1).length + 1 := by
+  rw [xorStep]
+  rcases hc : ((bif β then notBit else id)
+      (bitAt ((w 2).drop (false :: w 0).length) (w 2))) with _ | ⟨d, z⟩
+  · simp
+  · cases d <;> simp
+
+private theorem recNotation_xor (a b : List Bool) :
+    recNotation (fun _ : Fin 1 → List Bool => ([] : List Bool)) (xorStep false)
+      (xorStep true) a (fun _ => b) = xorSuffix a b := by
+  induction a with
+  | nil => rfl
+  | cons β x ih =>
+      cases β <;>
+        · rw [recNotation_cons, xorSuffix]
+          simp only [cond_false, cond_true, xorStep, Fin.cons_zero, Fin.cons_one, id]
+          rw [ih]
+          rfl
+
+private theorem recNotation_xor_length (a b : List Bool) :
+    (recNotation (fun _ : Fin 1 → List Bool => ([] : List Bool)) (xorStep false)
+      (xorStep true) a (fun _ => b)).length ≤ a.length := by
+  rw [recNotation_xor, xorSuffix_length]
+
+/-- **The exclusive-or is in the algebra.** -/
+theorem xorSuffix_mem {n : ℕ} {ga gb : (Fin n → List Bool) → List Bool}
+    (ha : Cobham ga) (hb : Cobham gb) :
+    Cobham fun v : Fin n → List Bool => xorSuffix (ga v) (gb v) := by
+  have hrec := Cobham.boundedRec (g := fun _ : Fin 1 → List Bool => ([] : List Bool))
+    (h₀ := xorStep false) (h₁ := xorStep true)
+    (j := fun w : Fin 2 → List Bool => w 0)
+    Cobham.empty (xorStep_mem false) (xorStep_mem true) (Cobham.proj 0)
+    (by
+      intro x v
+      have := recNotation_xor_length x (v 0)
+      have hv : (fun _ : Fin 1 => v 0) = v := by
+        funext i
+        rw [Subsingleton.elim i 0]
+      rw [hv] at this
+      simpa using this)
+  have hg : ∀ i : Fin 2, Cobham (![ga, gb] i) := by
+    intro i
+    match i with
+    | 0 => exact ha
+    | 1 => exact hb
+  refine (Cobham.comp hrec hg).of_eq fun v => ?_
+  have hb2 : (Fin.tail fun i => ![ga, gb] i v) = fun _ : Fin 1 => gb v := by
+    funext i
+    rw [Subsingleton.elim i 0]
+    rfl
+  show recNotation _ _ _ (ga v) (Fin.tail fun i => ![ga, gb] i v) = _
+  rw [hb2, recNotation_xor]
+
+end Cobham
+
+end Complexity
diff --git a/Complexitylib/Classes/P/DecisionFn.lean b/Complexitylib/Classes/P/DecisionFn.lean
new file mode 100644
index 00000000..8c0a4632
--- /dev/null
+++ b/Complexitylib/Classes/P/DecisionFn.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.Preimage
+public import Complexitylib.Languages.Contains
+
+/-!
+# From a polynomial-time decision function to membership in `P`
+
+A language whose verdict is computed by a polynomial-time *function* is in
+`P`. This is the bridge that lets a development establish membership in `P`
+by exhibiting a function — in particular by building one in Cobham's algebra,
+where `Complexitylib.Classes.P.Cobham` supplies `CobhamFP_eq_FP` — instead of
+constructing a decider machine by hand.
+
+The proof reads the verdict off the output through the polynomial-time
+language `Language.containsOne`: a verdict string is accepted exactly when it
+contains a `1`, and `P` is closed under polynomial-time preimages.
+
+## Main results
+
+- `mem_P_of_decisionFn` — a verdict function in `FP` puts its language in `P`
+- `mem_P_of_decisionFn_bool` — the same with a `Bool`-valued verdict
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-- **A polynomial-time verdict function decides a polynomial-time language.**
+If `f ∈ FP` and `x ∈ L` exactly when `f x` contains a `1`-bit, then `L ∈ P`. -/
+theorem mem_P_of_decisionFn {f : List Bool → List Bool} {L : Language}
+    (hf : f ∈ FP) (hL : ∀ x, x ∈ L ↔ ∃ b ∈ f x, b = true) : L ∈ P := by
+  have hpre : L = f ⁻¹' Language.containsOne := by
+    ext x
+    rw [Set.mem_preimage, Language.mem_containsOne]
+    exact hL x
+  rw [hpre]
+  exact mem_P_preimage hf containsOne_mem_P
+
+/-- The `Bool`-valued form: a polynomial-time function that emits the verdict
+as a one-bit string decides its language. -/
+theorem mem_P_of_decisionFn_bool {g : List Bool → Bool} {L : Language}
+    (hf : (fun x => [g x]) ∈ FP) (hL : ∀ x, x ∈ L ↔ g x = true) : L ∈ P := by
+  refine mem_P_of_decisionFn hf (fun x => ?_)
+  rw [hL x]
+  simp
+
+end Complexity
diff --git a/Complexitylib/Classes/PH.lean b/Complexitylib/Classes/PH.lean
new file mode 100644
index 00000000..e8e8f15f
--- /dev/null
+++ b/Complexitylib/Classes/PH.lean
@@ -0,0 +1,298 @@
+/-
+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.Containments
+public import Complexitylib.Classes.P.Cobham.Internal.FstBlock
+public import Complexitylib.Encoding.Pairing
+public import Mathlib.Algebra.Polynomial.Eval.Defs
+
+/-!
+# The polynomial hierarchy
+
+This file defines the polynomial hierarchy via certificate quantifiers, following
+the quantified-formula definition (Arora–Barak Definition 5.4, stated over the
+library's `pair` codec): `polyExistsLang p L` holds of `x` when some witness `w`
+of length at most `p.eval |x|` puts the encoded pair `pair x w` in `L`, and
+`polyForallLang p L` requires this of every such witness. Lifting these to class
+operators gives the levels `SigmaP 0 = P`, `SigmaP (n + 1) =
+polyExistsClass (PiP n)`, `PiP n = complClass (SigmaP n)`, and their union `PH`.
+
+The level inclusions `SigmaP n ⊆ SigmaP (n + 1)` and `PiP n ⊆ PiP (n + 1)` need
+one computational fact: decoding the first component of a canonical pair is
+polynomial-time computable. That is `pairFst_mem_FP`, which reuses the payload
+scanner `Cobham.fstBlock` of Cobham's algebra, so every result in this file is
+unconditional.
+
+## Main definitions
+
+- `polyExistsLang`, `polyForallLang` — witness quantifiers on languages
+- `polyExistsClass`, `polyForallClass` — the induced operators on classes
+- `pairFst` — first-component decoder for the pairing codec
+- `SigmaP`, `PiP`, `PH` — the hierarchy levels and their union
+
+## Main results
+
+- `compl_polyExistsLang` / `compl_polyForallLang` — quantifier duality
+- `complClass_polyExistsClass` / `complClass_polyForallClass` — class duality
+- `complClass_P` — `P` is closed under language complement, as a class equation
+- `SigmaP_zero`, `PiP_zero`, `SigmaP_succ`, `PiP_succ` — recursion laws
+- `pairFst_mem_FP` — the pair decoder is polynomial-time
+- `P_subset_polyExistsClass_P` / `P_subset_polyForallClass_P` — base inclusions
+- `SigmaP_subset_SigmaP_succ` / `PiP_subset_PiP_succ` — level inclusions
+- `SigmaP_subset_PH`, `P_subset_PH`
+
+## TODO
+
+- Relate `SigmaP 1` to the NTM-based `NP` through the witness characterization
+  interface in `Complexitylib.Classes.NP.Witness`.
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-! ## Witness quantifiers on languages -/
+
+/-- The language of inputs `x` admitting a witness `w` of length at most
+`p.eval |x|` such that the encoded pair `pair x w` lies in `L`. -/
+def polyExistsLang (p : Polynomial ℕ) (L : Language) : Language :=
+  {x | ∃ w, w.length ≤ p.eval x.length ∧ pair x w ∈ L}
+
+/-- The language of inputs `x` such that every witness `w` of length at most
+`p.eval |x|` puts the encoded pair `pair x w` in `L`. -/
+def polyForallLang (p : Polynomial ℕ) (L : Language) : Language :=
+  {x | ∀ w, w.length ≤ p.eval x.length → pair x w ∈ L}
+
+/-- Membership in `polyExistsLang` unfolds to a bounded existential. -/
+@[simp] theorem mem_polyExistsLang {p : Polynomial ℕ} {L : Language} {x : List Bool} :
+    x ∈ polyExistsLang p L ↔ ∃ w, w.length ≤ p.eval x.length ∧ pair x w ∈ L :=
+  Iff.rfl
+
+/-- Membership in `polyForallLang` unfolds to a bounded universal. -/
+@[simp] theorem mem_polyForallLang {p : Polynomial ℕ} {L : Language} {x : List Bool} :
+    x ∈ polyForallLang p L ↔ ∀ w, w.length ≤ p.eval x.length → pair x w ∈ L :=
+  Iff.rfl
+
+/-- Complementing a bounded existential yields a bounded universal over the
+complement: some-witness failure is all-witness exclusion. -/
+theorem compl_polyExistsLang (p : Polynomial ℕ) (L : Language) :
+    (polyExistsLang p L)ᶜ = polyForallLang p Lᶜ := by
+  ext x
+  simp [polyExistsLang, polyForallLang]
+
+/-- Complementing a bounded universal yields a bounded existential over the
+complement. -/
+theorem compl_polyForallLang (p : Polynomial ℕ) (L : Language) :
+    (polyForallLang p L)ᶜ = polyExistsLang p Lᶜ := by
+  ext x
+  simp [polyExistsLang, polyForallLang]
+
+/-! ## Quantifier operators on classes -/
+
+/-- The class of languages expressible as a polynomially-bounded existential
+over some language of `C`. -/
+def polyExistsClass (C : Set Language) : Set Language :=
+  {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = polyExistsLang p L'}
+
+/-- The class of languages expressible as a polynomially-bounded universal
+over some language of `C`. -/
+def polyForallClass (C : Set Language) : Set Language :=
+  {L | ∃ (p : Polynomial ℕ), ∃ L' ∈ C, L = polyForallLang p L'}
+
+/-- `polyExistsClass` is monotone in the base class. -/
+theorem polyExistsClass_mono {C D : Set Language} (h : C ⊆ D) :
+    polyExistsClass C ⊆ polyExistsClass D := by
+  rintro L ⟨p, L', hL', rfl⟩
+  exact ⟨p, L', h hL', rfl⟩
+
+/-- `polyForallClass` is monotone in the base class. -/
+theorem polyForallClass_mono {C D : Set Language} (h : C ⊆ D) :
+    polyForallClass C ⊆ polyForallClass D := by
+  rintro L ⟨p, L', hL', rfl⟩
+  exact ⟨p, L', h hL', rfl⟩
+
+/-- `complClass` is monotone. -/
+theorem complClass_mono {C D : Set Language} (h : C ⊆ D) :
+    complClass C ⊆ complClass D :=
+  fun _ hL => h hL
+
+/-- Class-level quantifier duality: the complement class of a bounded
+existential class is the bounded universal class over the complement class. -/
+theorem complClass_polyExistsClass (C : Set Language) :
+    complClass (polyExistsClass C) = polyForallClass (complClass C) := by
+  ext L
+  simp only [mem_complClass, polyExistsClass, polyForallClass, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨p, L', hL', hEq⟩
+    refine ⟨p, L'ᶜ, by simpa [mem_complClass, compl_compl] using hL', ?_⟩
+    rw [← compl_compl L, hEq, compl_polyExistsLang]
+  · rintro ⟨p, L', hL', rfl⟩
+    exact ⟨p, L'ᶜ, hL', by rw [compl_polyForallLang]⟩
+
+/-- Class-level quantifier duality: the complement class of a bounded universal
+class is the bounded existential class over the complement class. -/
+theorem complClass_polyForallClass (C : Set Language) :
+    complClass (polyForallClass C) = polyExistsClass (complClass C) := by
+  ext L
+  simp only [mem_complClass, polyExistsClass, polyForallClass, Set.mem_setOf_eq]
+  constructor
+  · rintro ⟨p, L', hL', hEq⟩
+    refine ⟨p, L'ᶜ, by simpa [mem_complClass, compl_compl] using hL', ?_⟩
+    rw [← compl_compl L, hEq, compl_polyForallLang]
+  · rintro ⟨p, L', hL', rfl⟩
+    exact ⟨p, L'ᶜ, hL', by rw [compl_polyExistsLang]⟩
+
+/-! ## The pair decoder seam -/
+
+/-- Decode the first component of a canonical pair. This is the payload scanner
+`Cobham.fstBlock` of Cobham's algebra: it reads doubled bits up to the
+separator, so on a canonical pair it returns the first component, and on
+malformed input it returns the bits decoded so far. Only its behaviour on
+canonical pairs is used. -/
+def pairFst (z : List Bool) : List Bool := Cobham.fstBlock z
+
+/-- `pairFst` recovers the first component of a canonical pair. -/
+@[simp] theorem pairFst_pair (x y : List Bool) : pairFst (pair x y) = x :=
+  Cobham.fstBlock_pair x y
+
+/-- **Decoding the first component is polynomial-time.** The scanner is one of
+the bespoke transducers of Cobham's soundness direction. -/
+theorem pairFst_mem_FP : pairFst ∈ FP := Cobham.fstBlock_mem_FP
+
+/-! ## Base inclusions -/
+
+/-- `P` is closed under complement, stated as a class equation. -/
+theorem complClass_P : complClass P = P := by
+  ext L
+  exact ⟨fun h => compl_compl L ▸ P_compl h, fun h => P_compl h⟩
+
+/-- Every language of `P` is a bounded existential over `P`: take the zero
+witness bound, so the only witness is `[]`, and decide `pair x []` by decoding
+the first component and running the original decider. -/
+theorem P_subset_polyExistsClass_P : P ⊆ polyExistsClass P := by
+  intro L hL
+  refine ⟨0, pairFst ⁻¹' L, mem_P_preimage pairFst_mem_FP hL, ?_⟩
+  ext x
+  simp only [mem_polyExistsLang, Polynomial.eval_zero, Nat.le_zero,
+    List.length_eq_zero_iff, Set.mem_preimage]
+  constructor
+  · intro hx
+    exact ⟨[], rfl, by simpa using hx⟩
+  · rintro ⟨w, rfl, hmem⟩
+    simpa using hmem
+
+/-- Every language of `P` is a bounded universal over `P`: with the zero
+witness bound the only witness is `[]`, decided as in
+`P_subset_polyExistsClass_P`. -/
+theorem P_subset_polyForallClass_P : P ⊆ polyForallClass P := by
+  intro L hL
+  refine ⟨0, pairFst ⁻¹' L, mem_P_preimage pairFst_mem_FP hL, ?_⟩
+  ext x
+  simp only [mem_polyForallLang, Polynomial.eval_zero, Nat.le_zero,
+    List.length_eq_zero_iff, Set.mem_preimage]
+  constructor
+  · rintro hx w rfl
+    simpa using hx
+  · intro h
+    simpa using h [] rfl
+
+/-! ## The hierarchy -/
+
+/-- The Σ levels of the polynomial hierarchy: `SigmaP 0 = P` and
+`SigmaP (n + 1)` is a bounded existential over the complement class of
+`SigmaP n` (that is, over `PiP n`). -/
+def SigmaP : ℕ → Set Language
+  | 0 => P
+  | n + 1 => polyExistsClass (complClass (SigmaP n))
+
+/-- The Π levels of the polynomial hierarchy: `PiP n` is the complement class
+of `SigmaP n`. -/
+def PiP (n : ℕ) : Set Language :=
+  complClass (SigmaP n)
+
+/-- The polynomial hierarchy: the union of all Σ levels. -/
+def PH : Set Language :=
+  ⋃ n : ℕ, SigmaP n
+
+/-- The zeroth Σ level is `P`. -/
+@[simp] theorem SigmaP_zero : SigmaP 0 = P := rfl
+
+/-- The complement class of a Σ level is the corresponding Π level. -/
+@[simp] theorem complClass_SigmaP (n : ℕ) : complClass (SigmaP n) = PiP n := rfl
+
+/-- The complement class of a Π level is the corresponding Σ level. -/
+@[simp] theorem complClass_PiP (n : ℕ) : complClass (PiP n) = SigmaP n := by
+  rw [PiP, complClass_complClass]
+
+/-- The zeroth Π level is `P`, since `P` is closed under complement. -/
+@[simp] theorem PiP_zero : PiP 0 = P := by
+  rw [PiP, SigmaP_zero, complClass_P]
+
+/-- Recursion law for Σ levels: `SigmaP (n + 1)` is a bounded existential over
+`PiP n`. -/
+theorem SigmaP_succ (n : ℕ) : SigmaP (n + 1) = polyExistsClass (PiP n) := rfl
+
+/-- Recursion law for Π levels: `PiP (n + 1)` is a bounded universal over
+`SigmaP n`. -/
+theorem PiP_succ (n : ℕ) : PiP (n + 1) = polyForallClass (SigmaP n) := by
+  rw [PiP]
+  show complClass (polyExistsClass (complClass (SigmaP n))) = _
+  rw [complClass_polyExistsClass, complClass_complClass]
+
+/-- The first Σ level is the bounded existential closure of `P` — the
+certificate form of `NP`. -/
+theorem SigmaP_one : SigmaP 1 = polyExistsClass P := by
+  rw [SigmaP_succ, PiP_zero]
+
+/-- The first Π level is the bounded universal closure of `P` — the
+certificate form of `coNP`. -/
+theorem PiP_one : PiP 1 = polyForallClass P := by
+  rw [PiP_succ, SigmaP_zero]
+
+/-! ## Level inclusions -/
+
+/-- Both level inclusions, proved simultaneously by induction: the base case is
+the pair of base inclusions of `P`, and each successor case is monotonicity of
+the opposite quantifier applied to the other component. -/
+private theorem piP_sigmaP_subset_succ (n : ℕ) :
+    PiP n ⊆ PiP (n + 1) ∧ SigmaP n ⊆ SigmaP (n + 1) := by
+  induction n with
+  | zero =>
+    constructor
+    · rw [PiP_zero, PiP_one]
+      exact P_subset_polyForallClass_P
+    · rw [SigmaP_zero, SigmaP_one]
+      exact P_subset_polyExistsClass_P
+  | succ n ih =>
+    constructor
+    · rw [PiP_succ, PiP_succ]
+      exact polyForallClass_mono ih.2
+    · rw [SigmaP_succ, SigmaP_succ]
+      exact polyExistsClass_mono ih.1
+
+/-- Each Σ level is contained in the next. -/
+theorem SigmaP_subset_SigmaP_succ (n : ℕ) : SigmaP n ⊆ SigmaP (n + 1) :=
+  (piP_sigmaP_subset_succ n).2
+
+/-- Each Π level is contained in the next. -/
+theorem PiP_subset_PiP_succ (n : ℕ) : PiP n ⊆ PiP (n + 1) :=
+  (piP_sigmaP_subset_succ n).1
+
+/-! ## PH -/
+
+/-- Membership in `PH` is membership in some Σ level. -/
+theorem mem_PH_iff {L : Language} : L ∈ PH ↔ ∃ n : ℕ, L ∈ SigmaP n :=
+  Set.mem_iUnion
+
+/-- Every Σ level is contained in the hierarchy. -/
+theorem SigmaP_subset_PH (n : ℕ) : SigmaP n ⊆ PH :=
+  fun _ h => Set.mem_iUnion.mpr ⟨n, h⟩
+
+/-- `P` is contained in the polynomial hierarchy. -/
+theorem P_subset_PH : P ⊆ PH :=
+  SigmaP_subset_PH 0
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann.lean b/Complexitylib/Classes/PH/SipserLautemann.lean
new file mode 100644
index 00000000..75d0fd06
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann.lean
@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.DecisionFn
+public import Complexitylib.Classes.PH
+public import Complexitylib.Classes.PH.SipserLautemann.Matrix
+public import Complexitylib.Classes.PH.SipserLautemann.Verdict
+
+/-!
+# The Sipser–Lautemann theorem
+
+⚠️ Unreviewed by Bolton
+
+The Sipser–Lautemann theorem (Arora–Barak Theorem 7.15) places bounded-error
+probabilistic polynomial time inside the second level of the polynomial
+hierarchy: `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ`. This file states that containment against the
+library's concrete `BPP` (`Complexitylib.Classes.Randomized`) and the
+certificate-quantifier levels `SigmaP` / `PiP` (`Complexitylib.Classes.PH`),
+and proves it: `sipserLautemann`.
+
+## How it is proved
+
+The development lives in the `SipserLautemann` subdirectory:
+
+- `Covering` — Lautemann's covering lemma in both directions, by counting
+  shifts of an event in the seed space;
+- `TimeBound` — the acceptance probability is frozen past the halting time, so
+  a machine's arbitrary time bound may be replaced by a dominating polynomial;
+- `Amplified` — majority amplification plus the covering lemma give the `∃∀`
+  characterization `x ∈ L ↔ ∃ shifts, ∀ seeds, some shift accepts`, and its
+  complementary form for `x ∉ L`;
+- `Encode` — bitstring codecs for seeds and shift tuples;
+- `Matrix` — the quantifier-free matrix as a language of encoded triples, and
+  the identity exhibiting `L` and `Lᶜ` as polynomially bounded `∃∀` forms over
+  it;
+- `Verdict` — the matrix verdict as a member of Cobham's algebra, hence in
+  `FP`.
+
+What remained was the polynomial-time decidability of the matrix, isolated as
+the interfaces `MatrixInP` and — as a statement about a *function* —
+`MatrixVerdictInFP`. It is discharged by `matrixVerdictInFP` with no machine
+construction at all: `CobhamFP_eq_FP` turns it into a programming task inside
+Cobham's algebra, and `mem_P_of_decisionFn_bool` converts the result back to
+`P`. The verdict is computed in `SipserLautemann.Verdict` — decode the triple
+with the payload scanners, build the trial count and seed length as `smash`
+lengths from the polynomial time bound, and take the disjunction over shift
+blocks of the majority vote over trial blocks — with each trial one run of the
+machine along the choice bits of its block, via `NTM.choiceTM` and its
+in-algebra simulation in `Complexitylib.Classes.P.Cobham.Internal.ChoiceSim`.
+The matrix is taken at a *polynomial* time bound, which is what makes the
+per-trial step count computable from the input; `TimeBound` supplies the
+normalization.
+
+## Main definitions
+
+- `SipserLautemann` — the statement `BPP ⊆ SigmaP 2 ∩ PiP 2`
+- `MatrixInP` — the polynomial-time decidability interface for the matrix
+- `MatrixVerdictInFP` — the same interface as a statement about a function
+
+## Main results
+
+- `sipserLautemann` — **the theorem**, `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ`
+- `BPP_subset_SigmaP_two`, `BPP_subset_PiP_two`, `BPP_subset_PH` — its halves
+  and the corollary
+- `matrixVerdictInFP` — the matrix interface, discharged
+- `sipserLautemann_of_matrixInP`, `sipserLautemann_of_verdictInFP` — the
+  theorem from either form of the interface
+- `matrixInP_of_verdictInFP` — the function form implies the language form
+- `mem_SigmaP_two_of_matrixInP`, `mem_PiP_two_of_matrixInP` — the two halves
+- `sipserLautemann_iff` — the statement splits into its `Σ₂` and `Π₂` halves
+- `sipserLautemann_of_subset_SigmaP` — the `Σ₂` half suffices, given that
+  `BPP` is closed under complement
+- `BPP_subset_SigmaP_two_of_sipserLautemann`,
+  `BPP_subset_PiP_two_of_sipserLautemann` — the two halves
+- `BPP_subset_PH_of_sipserLautemann` — `BPP ⊆ PH`
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-- **Sipser–Lautemann**: bounded-error probabilistic polynomial time lies in
+the second level of the polynomial hierarchy, `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ`.
+
+Stated as a `Prop` so that results can depend on it explicitly; it is proved
+from the `MatrixInP` interface by `sipserLautemann_of_matrixInP`. -/
+def SipserLautemann : Prop :=
+  BPP ⊆ SigmaP 2 ∩ PiP 2
+
+/-- **The matrix-decidability interface.** For every machine and every
+polynomial time bound, the quantifier-free matrix of the Lautemann
+characterization is decidable in deterministic polynomial time.
+
+A decider parses `pair (pair x w) r`, computes the per-trial step count
+`pt.eval |x|` and the amplified seed length from it, decodes the shift tuple
+and the seed, and for each shift runs the fixed machine on the shifted seed,
+block by block, taking the majority verdict; all of this is polynomial in the
+input length. Isolating it here keeps the probabilistic and combinatorial
+content of the theorem free of machine engineering. -/
+def MatrixInP : Prop :=
+  ∀ (k : ℕ) (tm : NTM k) (pt : Polynomial ℕ) (b : Bool),
+    Lautemann.matrixLang tm pt.eval b ∈ P
+
+/-- **The matrix interface as a function statement.** For every machine and
+every polynomial time bound, the matrix verdict is computable in deterministic
+polynomial time.
+
+This is the form to discharge: by `CobhamFP_eq_FP` it suffices to build the
+verdict inside Cobham's algebra, with `NTM.choiceTM_simulates` supplying the
+semantics of running the machine along given choice bits. -/
+def MatrixVerdictInFP : Prop :=
+  ∀ (k : ℕ) (tm : NTM k) (pt : Polynomial ℕ) (b : Bool),
+    (fun z => [Lautemann.matrixVerdict tm pt.eval b z]) ∈ FP
+
+/-- A polynomial-time verdict function gives the polynomial-time matrix
+language. -/
+theorem matrixInP_of_verdictInFP (h : MatrixVerdictInFP) : MatrixInP :=
+  fun k tm pt b =>
+    mem_P_of_decisionFn_bool (h k tm pt b)
+      (fun z => Lautemann.mem_matrixLang_iff_verdict tm pt.eval b z)
+
+/-- Every `BPP` language is in `Σ₂ᵖ`, given the matrix interface. -/
+theorem mem_SigmaP_two_of_matrixInP (hmatrix : MatrixInP) {L : Language}
+    (hL : L ∈ BPP) : L ∈ SigmaP 2 := by
+  obtain ⟨d, hd⟩ := Set.mem_iUnion.mp hL
+  obtain ⟨k, tm, f, hhalt, haccept, hreject, hO⟩ := hd
+  obtain ⟨pt, hpt⟩ := BigO.pow_polynomial_bound hO
+  obtain ⟨hq, hp⟩ := Lautemann.boundPoly_bounds (f := pt.eval) (P := pt) (fun n => le_rfl)
+  have haccept' : tm.AcceptsWithProb L pt.eval (2 / 3) :=
+    NTM.acceptsWithProb_of_le hhalt hpt haccept
+  have hreject' : tm.RejectsWithProb L pt.eval (1 / 3) :=
+    NTM.rejectsWithProb_of_le hhalt hpt hreject
+  have hEq := Lautemann.eq_polyExistsLang_of_boundedError haccept' hreject' hp hq
+  show L ∈ SigmaP (1 + 1)
+  rw [SigmaP_succ, PiP_one]
+  exact ⟨(Lautemann.boundPoly pt + 1) * Lautemann.boundPoly pt, _,
+    ⟨Lautemann.boundPoly pt, _, hmatrix k tm pt true, rfl⟩, hEq⟩
+
+/-- Every `BPP` language is in `Π₂ᵖ`, given the matrix interface: the
+complementary covering characterization puts the complement in `Σ₂ᵖ`. -/
+theorem mem_PiP_two_of_matrixInP (hmatrix : MatrixInP) {L : Language}
+    (hL : L ∈ BPP) : L ∈ PiP 2 := by
+  obtain ⟨d, hd⟩ := Set.mem_iUnion.mp hL
+  obtain ⟨k, tm, f, hhalt, haccept, hreject, hO⟩ := hd
+  obtain ⟨pt, hpt⟩ := BigO.pow_polynomial_bound hO
+  obtain ⟨hq, hp⟩ := Lautemann.boundPoly_bounds (f := pt.eval) (P := pt) (fun n => le_rfl)
+  have haccept' : tm.AcceptsWithProb L pt.eval (2 / 3) :=
+    NTM.acceptsWithProb_of_le hhalt hpt haccept
+  have hreject' : tm.RejectsWithProb L pt.eval (1 / 3) :=
+    NTM.rejectsWithProb_of_le hhalt hpt hreject
+  have hEq := Lautemann.compl_eq_polyExistsLang_of_boundedError haccept' hreject' hp hq
+  show Lᶜ ∈ SigmaP (1 + 1)
+  rw [SigmaP_succ, PiP_one]
+  exact ⟨(Lautemann.boundPoly pt + 1) * Lautemann.boundPoly pt, _,
+    ⟨Lautemann.boundPoly pt, _, hmatrix k tm pt false, rfl⟩, hEq⟩
+
+/-- **The Sipser–Lautemann theorem**, given the matrix-decidability
+interface: `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ`. -/
+theorem sipserLautemann_of_matrixInP (hmatrix : MatrixInP) : SipserLautemann :=
+  fun _ hL => ⟨mem_SigmaP_two_of_matrixInP hmatrix hL, mem_PiP_two_of_matrixInP hmatrix hL⟩
+
+/-- **The Sipser–Lautemann theorem**, given the matrix interface in its
+function form. -/
+theorem sipserLautemann_of_verdictInFP (h : MatrixVerdictInFP) : SipserLautemann :=
+  sipserLautemann_of_matrixInP (matrixInP_of_verdictInFP h)
+
+/-- The statement splits into its two halves: containment in `Σ₂ᵖ` and
+containment in `Π₂ᵖ`. -/
+theorem sipserLautemann_iff : SipserLautemann ↔ BPP ⊆ SigmaP 2 ∧ BPP ⊆ PiP 2 :=
+  Set.subset_inter_iff
+
+/-- The `Σ₂ᵖ` half of the statement. -/
+theorem BPP_subset_SigmaP_two_of_sipserLautemann (h : SipserLautemann) :
+    BPP ⊆ SigmaP 2 :=
+  fun _ hL => (h hL).1
+
+/-- The `Π₂ᵖ` half of the statement. -/
+theorem BPP_subset_PiP_two_of_sipserLautemann (h : SipserLautemann) :
+    BPP ⊆ PiP 2 :=
+  fun _ hL => (h hL).2
+
+/-- The `Σ₂ᵖ` half implies the full statement, given that `BPP` is closed under
+complement: a language of `BPP` lies in `Π₂ᵖ` exactly when its complement lies
+in `Σ₂ᵖ`, and the complement is again a `BPP` language. -/
+theorem sipserLautemann_of_subset_SigmaP (hcompl : ∀ L ∈ BPP, Lᶜ ∈ BPP)
+    (h : BPP ⊆ SigmaP 2) : SipserLautemann :=
+  fun L hL => ⟨h hL, h (hcompl L hL)⟩
+
+/-- Sipser–Lautemann puts `BPP` inside the polynomial hierarchy. -/
+theorem BPP_subset_PH_of_sipserLautemann (h : SipserLautemann) : BPP ⊆ PH :=
+  fun _ hL => SigmaP_subset_PH 2 (h hL).1
+
+/-- **The matrix interface holds.** The verdict is computed inside Cobham's
+algebra — decode the triple with the payload scanners, build the trial count
+and seed length as `smash` lengths from the time bound, and take the
+disjunction over shift blocks of the majority vote over trial blocks, each
+trial being one run of the machine along the choice bits of its block — and
+`CobhamFP_eq_FP` makes that a polynomial-time function. -/
+theorem matrixVerdictInFP : MatrixVerdictInFP :=
+  fun _ tm pt b => Lautemann.matrixVerdict_mem_FP tm pt b
+
+/-- **The Sipser–Lautemann theorem**: bounded-error probabilistic polynomial
+time lies in the second level of the polynomial hierarchy,
+`BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ` (Arora–Barak Theorem 7.15). -/
+theorem sipserLautemann : SipserLautemann :=
+  sipserLautemann_of_verdictInFP matrixVerdictInFP
+
+/-- `BPP ⊆ Σ₂ᵖ`. -/
+theorem BPP_subset_SigmaP_two : BPP ⊆ SigmaP 2 :=
+  BPP_subset_SigmaP_two_of_sipserLautemann sipserLautemann
+
+/-- `BPP ⊆ Π₂ᵖ`. -/
+theorem BPP_subset_PiP_two : BPP ⊆ PiP 2 :=
+  BPP_subset_PiP_two_of_sipserLautemann sipserLautemann
+
+/-- **`BPP` lies inside the polynomial hierarchy.** -/
+theorem BPP_subset_PH : BPP ⊆ PH :=
+  BPP_subset_PH_of_sipserLautemann sipserLautemann
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann/Amplified.lean b/Complexitylib/Classes/PH/SipserLautemann/Amplified.lean
new file mode 100644
index 00000000..2cbb499b
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann/Amplified.lean
@@ -0,0 +1,185 @@
+/-
+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.PH.SipserLautemann.Covering
+public import Complexitylib.Classes.Randomized
+public import Complexitylib.Models.TuringMachine.Repetition.Correctness
+
+/-!
+# The amplified Lautemann characterization
+
+Combining majority amplification with the covering lemma of
+`Complexitylib.Classes.PH.SipserLautemann.Covering`, this file proves the
+`∃∀` characterization at the heart of the Sipser–Lautemann theorem.
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Lautemann
+
+variable {k : ℕ}
+
+/-- `13 K²  < 2 ^ K` from `K = 11` on: the numeric fact making the amplified
+seed count smaller than the amplified error denominator. -/
+private theorem thirteen_mul_sq_lt_two_pow : ∀ K, 11 ≤ K → 13 * K ^ 2 < 2 ^ K := by
+  intro K
+  induction K with
+  | zero => intro h; omega
+  | succ n ih =>
+    intro _
+    rcases Nat.lt_or_ge n 11 with hn | hn
+    · have hn10 : n = 10 := by omega
+      subst hn10
+      norm_num
+    · have hprev := ih (by omega)
+      calc 13 * (n + 1) ^ 2 ≤ 2 * (13 * n ^ 2) := by nlinarith
+        _ < 2 * 2 ^ n := by omega
+        _ = 2 ^ (n + 1) := by rw [pow_succ]; ring
+
+/-- Amplification exponent for inputs of length `n`: the amplified error is
+`2 ^ (-ampExp f n)`. It is taken large enough to dominate the amplified seed
+length, which is what the covering lemma's soundness direction needs. -/
+def ampExp (f : ℕ → ℕ) (n : ℕ) : ℕ := f n + 11
+
+/-- Number of independent trials of the source machine, an odd count so that
+majority votes cannot tie. -/
+def ampRuns (f : ℕ → ℕ) (n : ℕ) : ℕ := 12 * ampExp f n + 1
+
+/-- Number of shifts used to cover the seed space: one more than the seed
+length, so that the degenerate zero-length seed space is still covered. -/
+def ampShifts (f : ℕ → ℕ) (n : ℕ) : ℕ := ampRuns f n * f n + 1
+
+/-- The amplified accepting event: the long seeds on which a strict majority
+of the `ampRuns f n` independent trials accepts. -/
+def ampEvent (tm : NTM k) (f : ℕ → ℕ) (x : List Bool) :
+    Finset (Fin (ampRuns f x.length * f x.length) → Bool) :=
+  Finset.univ.filter fun w =>
+    blockMajority (NTM.repeatAcceptEvent tm x (f x.length)) w = true
+
+/-- Membership in the amplified event is the majority verdict. -/
+@[simp] theorem mem_ampEvent (tm : NTM k) (f : ℕ → ℕ) (x : List Bool)
+    (w : Fin (ampRuns f x.length * f x.length) → Bool) :
+    w ∈ ampEvent tm f x ↔
+      blockMajority (NTM.repeatAcceptEvent tm x (f x.length)) w = true := by
+  simp [ampEvent]
+
+/-- The complement of the amplified event is the majority-rejecting event. -/
+theorem compl_ampEvent (tm : NTM k) (f : ℕ → ℕ) (x : List Bool) :
+    (ampEvent tm f x)ᶜ = Finset.univ.filter fun w =>
+      blockMajority (NTM.repeatAcceptEvent tm x (f x.length)) w = false := by
+  ext w
+  simp [ampEvent, Bool.not_eq_true]
+
+/-- Membership in the complement of the amplified event is the rejecting
+majority verdict. Not a `simp` lemma: `simp` reaches the same normal form
+through `Finset.mem_compl` and `mem_ampEvent`. -/
+theorem mem_compl_ampEvent (tm : NTM k) (f : ℕ → ℕ) (x : List Bool)
+    (w : Fin (ampRuns f x.length * f x.length) → Bool) :
+    w ∈ (ampEvent tm f x)ᶜ ↔
+      blockMajority (NTM.repeatAcceptEvent tm x (f x.length)) w = false := by
+  rw [compl_ampEvent]
+  simp
+
+/-- The number of shifts is below the amplified error denominator. -/
+theorem ampShifts_lt_two_pow_ampExp (f : ℕ → ℕ) (n : ℕ) :
+    ampShifts f n < 2 ^ ampExp f n := by
+  have hK : 11 ≤ ampExp f n := by simp [ampExp]
+  have hfn : f n ≤ ampExp f n := by simp [ampExp]
+  have hnum : ampShifts f n ≤ 13 * (ampExp f n) ^ 2 := by
+    have hmul : ampRuns f n * f n ≤ (12 * ampExp f n + 1) * ampExp f n :=
+      Nat.mul_le_mul_left _ hfn
+    simp only [ampShifts, ampRuns] at *
+    nlinarith
+  exact lt_of_le_of_lt hnum (thirteen_mul_sq_lt_two_pow _ hK)
+
+/-- **Completeness.** On an accepted input the amplified event fails with
+probability at most `2 ^ (-ampExp f n)`, so the covering lemma supplies
+`ampShifts f n` shifts covering the whole seed space. -/
+theorem exists_covers_of_mem {tm : NTM k} {L : Language} {f : ℕ → ℕ}
+    (haccept : tm.AcceptsWithProb L f (2 / 3)) {x : List Bool} (hx : x ∈ L) :
+    ∃ u : Fin (ampShifts f x.length) →
+        Fin (ampRuns f x.length * f x.length) → Bool,
+      Covers (ampEvent tm f x) u := by
+  have hE : 2 / 3 ≤ eventProb (NTM.repeatAcceptEvent tm x (f x.length)) := by
+    rw [← NTM.acceptProb_eq_eventProb_repeatAcceptEvent]
+    exact haccept x hx
+  have herr : eventProb (ampEvent tm f x)ᶜ ≤ 1 / 2 ^ ampExp f x.length := by
+    rw [compl_ampEvent]
+    exact eventProb_blockMajority_false_le_two_pow (f x.length) (ampExp f x.length) _ hE
+  refine exists_covers_of_eventProb_compl_le _ ?_ herr
+  have hK : 1 ≤ ampExp f x.length := by simp [ampExp]
+  have := Nat.mul_le_mul_right (ampShifts f x.length) hK
+  simp only [ampShifts, one_mul] at this ⊢
+  omega
+
+/-- **Soundness.** On a rejected input the amplified event holds with
+probability at most `2 ^ (-ampExp f n)`, which is too small for
+`ampShifts f n` shifts of it to cover the seed space. -/
+theorem not_covers_of_notMem {tm : NTM k} {L : Language} {f : ℕ → ℕ}
+    (hreject : tm.RejectsWithProb L f (1 / 3)) {x : List Bool} (hx : x ∉ L)
+    (u : Fin (ampShifts f x.length) → Fin (ampRuns f x.length * f x.length) → Bool) :
+    ¬ Covers (ampEvent tm f x) u := by
+  have hE : eventProb (NTM.repeatAcceptEvent tm x (f x.length)) ≤ 1 / 3 := by
+    rw [← NTM.acceptProb_eq_eventProb_repeatAcceptEvent]
+    exact hreject x hx
+  have herr : eventProb (ampEvent tm f x) ≤ 1 / 2 ^ ampExp f x.length :=
+    eventProb_blockMajority_true_le_two_pow (f x.length) (ampExp f x.length) _ hE
+  exact not_covers_of_eventProb_le _ (ampShifts_lt_two_pow_ampExp f x.length) herr u
+
+/-- **The Lautemann characterization.** For a bounded-error machine deciding
+`L`, membership is equivalent to the existence of a tuple of shifts whose
+translates of the amplified accepting event cover the seed space — an `∃∀`
+form with a deterministic, polynomially-checkable matrix. -/
+theorem mem_iff_exists_covers {tm : NTM k} {L : Language} {f : ℕ → ℕ}
+    (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3))
+    (x : List Bool) :
+    x ∈ L ↔ ∃ u : Fin (ampShifts f x.length) →
+        Fin (ampRuns f x.length * f x.length) → Bool, Covers (ampEvent tm f x) u := by
+  constructor
+  · exact fun hx => exists_covers_of_mem haccept hx
+  · intro hcov
+    by_contra hx
+    obtain ⟨u, hu⟩ := hcov
+    exact not_covers_of_notMem hreject hx u hu
+
+/-- **The complementary Lautemann characterization.** Non-membership is
+equivalent to the existence of shifts covering the seed space with translates
+of the majority-*rejecting* event. Together with `mem_iff_exists_covers` this
+puts both `L` and its complement in the same `∃∀` form, which is what places
+`BPP` in `Σ₂ᵖ ∩ Π₂ᵖ` rather than only in `Σ₂ᵖ`. -/
+theorem notMem_iff_exists_covers_compl {tm : NTM k} {L : Language} {f : ℕ → ℕ}
+    (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3))
+    (x : List Bool) :
+    x ∉ L ↔ ∃ u : Fin (ampShifts f x.length) →
+        Fin (ampRuns f x.length * f x.length) → Bool, Covers (ampEvent tm f x)ᶜ u := by
+  constructor
+  · intro hx
+    have hE : eventProb (NTM.repeatAcceptEvent tm x (f x.length)) ≤ 1 / 3 := by
+      rw [← NTM.acceptProb_eq_eventProb_repeatAcceptEvent]
+      exact hreject x hx
+    have herr : eventProb ((ampEvent tm f x)ᶜ)ᶜ ≤ 1 / 2 ^ ampExp f x.length := by
+      rw [compl_compl]
+      exact eventProb_blockMajority_true_le_two_pow (f x.length) (ampExp f x.length) _ hE
+    refine exists_covers_of_eventProb_compl_le _ ?_ herr
+    have hK : 1 ≤ ampExp f x.length := by simp [ampExp]
+    have := Nat.mul_le_mul_right (ampShifts f x.length) hK
+    simp only [ampShifts, one_mul] at this ⊢
+    omega
+  · intro hcov hx
+    obtain ⟨u, hu⟩ := hcov
+    have hE : 2 / 3 ≤ eventProb (NTM.repeatAcceptEvent tm x (f x.length)) := by
+      rw [← NTM.acceptProb_eq_eventProb_repeatAcceptEvent]
+      exact haccept x hx
+    have herr : eventProb (ampEvent tm f x)ᶜ ≤ 1 / 2 ^ ampExp f x.length := by
+      rw [compl_ampEvent]
+      exact eventProb_blockMajority_false_le_two_pow (f x.length) (ampExp f x.length) _ hE
+    exact not_covers_of_eventProb_le _ (ampShifts_lt_two_pow_ampExp f x.length) herr u hu
+
+end Lautemann
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann/Covering.lean b/Complexitylib/Classes/PH/SipserLautemann/Covering.lean
new file mode 100644
index 00000000..070b9b70
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann/Covering.lean
@@ -0,0 +1,211 @@
+/-
+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.EventProb
+
+/-!
+# Lautemann's covering lemma
+
+The combinatorial core of the Sipser–Lautemann theorem, stated for an event
+`E` in the seed space `Fin m → Bool` and the XOR shift action on that space.
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Lautemann
+
+variable {m t k : ℕ}
+
+/-- XOR shift of a seed by a vector. -/
+def shift (r u : Fin m → Bool) : Fin m → Bool := fun i => xor (r i) (u i)
+
+@[simp] theorem shift_shift (r u : Fin m → Bool) : shift (shift r u) u = r := by
+  funext i
+  simp [shift]
+
+/-- The shift action is symmetric in its two arguments. -/
+theorem shift_comm (r u : Fin m → Bool) : shift r u = shift u r := by
+  funext i
+  simp [shift, Bool.xor_comm]
+
+/-- Shifting by a fixed vector is an involutive equivalence of the seed space. -/
+def shiftEquiv (u : Fin m → Bool) : (Fin m → Bool) ≃ (Fin m → Bool) where
+  toFun r := shift r u
+  invFun r := shift r u
+  left_inv r := shift_shift r u
+  right_inv r := shift_shift r u
+
+/-- The `t` shifts `u 0, …, u (t-1)` of the event `E` cover the whole seed
+space: every seed lands in `E` after at least one of them. -/
+def Covers (E : Finset (Fin m → Bool)) (u : Fin t → Fin m → Bool) : Prop :=
+  ∀ r, ∃ i, shift r (u i) ∈ E
+
+/-- Shifting is measure preserving: the seeds carried into `E` by a fixed
+shift are as many as the elements of `E`. -/
+theorem card_filter_shift_mem (E : Finset (Fin m → Bool)) (u : Fin m → Bool) :
+    (Finset.univ.filter fun r => shift r u ∈ E).card = E.card := by
+  have hset : (Finset.univ.filter fun r => shift r u ∈ E) = E.image (fun v => shift v u) := by
+    ext r
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]
+    constructor
+    · intro h
+      exact ⟨shift r u, h, by simp⟩
+    · rintro ⟨v, hv, rfl⟩
+      simpa using hv
+  have hinj : Function.Injective (fun v : Fin m → Bool => shift v u) := by
+    intro a b hab
+    have := congrArg (fun w => shift w u) hab
+    simpa using this
+  rw [hset, Finset.card_image_of_injective _ hinj]
+
+/-- The number of seeds is `2 ^ m`. -/
+theorem card_univ_seed : (Finset.univ : Finset (Fin m → Bool)).card = 2 ^ m := by
+  rw [Finset.card_univ, card_finArrowBool]
+
+/-- The number of `t`-tuples of shift vectors is `(2 ^ m) ^ t`. -/
+theorem card_univ_shifts :
+    (Finset.univ : Finset (Fin t → Fin m → Bool)).card = (2 ^ m) ^ t := by
+  rw [Finset.card_univ, Fintype.card_fun, card_finArrowBool, Fintype.card_fin]
+
+/-- **Existence of covering shifts.** If the complement of `E` is small enough
+that `2 ^ m` translates of its `m`-fold product miss the whole shift space,
+some `m`-tuple of shifts covers every seed. This is the counting form of the
+probabilistic argument: a uniformly random tuple fails to cover a fixed seed
+with probability `(1 - eventProb E) ^ m`, and a union bound over the `2 ^ m`
+seeds leaves a covering tuple. -/
+theorem exists_covers_of_card (E : Finset (Fin m → Bool))
+    (h : 2 ^ m * (2 ^ m - E.card) ^ t < (2 ^ m) ^ t) :
+    ∃ u : Fin t → Fin m → Bool, Covers E u := by
+  classical
+  set bad : Finset (Fin t → Fin m → Bool) :=
+    Finset.univ.filter (fun u => ¬ Covers E u) with hbad
+  have hsub : bad ⊆ Finset.univ.biUnion (fun r : Fin m → Bool =>
+      Fintype.piFinset (fun _ : Fin t => Finset.univ.filter fun v => shift r v ∉ E)) := by
+    intro u hu
+    simp only [hbad, Finset.mem_filter, Finset.mem_univ, true_and, Covers, not_forall] at hu
+    obtain ⟨r, hr⟩ := hu
+    simp only [not_exists] at hr
+    exact Finset.mem_biUnion.mpr ⟨r, Finset.mem_univ r, by
+      simp only [Fintype.mem_piFinset, Finset.mem_filter, Finset.mem_univ, true_and]
+      exact fun i => hr i⟩
+  have hfiber : ∀ r : Fin m → Bool,
+      (Fintype.piFinset (fun _ : Fin t => Finset.univ.filter fun v => shift r v ∉ E)).card
+        = (2 ^ m - E.card) ^ t := by
+    intro r
+    rw [Fintype.card_piFinset]
+    have hone : (Finset.univ.filter fun v => shift r v ∉ E).card = 2 ^ m - E.card := by
+      have : (Finset.univ.filter fun v => shift r v ∉ E)
+          = Finset.univ.filter fun v => shift v r ∈ Eᶜ := by
+        ext v
+        simp [shift_comm v r]
+      rw [this, card_filter_shift_mem Eᶜ r, Finset.card_compl, card_finArrowBool]
+    simp [hone]
+  have hcard : bad.card < (2 ^ m) ^ t := by
+    calc bad.card
+        ≤ (Finset.univ.biUnion (fun r : Fin m → Bool =>
+            Fintype.piFinset (fun _ : Fin t => Finset.univ.filter fun v => shift r v ∉ E))).card :=
+          Finset.card_le_card hsub
+      _ ≤ ∑ _r : Fin m → Bool, (2 ^ m - E.card) ^ t := by
+          refine le_trans (Finset.card_biUnion_le) ?_
+          exact Finset.sum_le_sum fun r _ => le_of_eq (hfiber r)
+      _ = 2 ^ m * (2 ^ m - E.card) ^ t := by
+          rw [Finset.sum_const, card_univ_seed]
+          simp
+      _ < (2 ^ m) ^ t := h
+  have hex : ∃ u : Fin t → Fin m → Bool, u ∉ bad := by
+    by_contra hcon
+    simp only [not_exists, not_not] at hcon
+    have : (Finset.univ : Finset (Fin t → Fin m → Bool)) ⊆ bad := fun u _ => hcon u
+    have hle := Finset.card_le_card this
+    rw [card_univ_shifts] at hle
+    omega
+  obtain ⟨u, hu⟩ := hex
+  refine ⟨u, ?_⟩
+  simpa [hbad] using hu
+
+/-- **No covering when the event is small.** If `t` copies of `E` cannot fill
+the seed space by cardinality alone, no tuple of `t` shifts covers it. -/
+theorem not_covers_of_card (E : Finset (Fin m → Bool)) (h : t * E.card < 2 ^ m)
+    (u : Fin t → Fin m → Bool) : ¬ Covers E u := by
+  classical
+  intro hcov
+  have hsub : (Finset.univ : Finset (Fin m → Bool)) ⊆
+      Finset.univ.biUnion (fun i : Fin t => Finset.univ.filter fun r => shift r (u i) ∈ E) := by
+    intro r _
+    obtain ⟨i, hi⟩ := hcov r
+    exact Finset.mem_biUnion.mpr ⟨i, Finset.mem_univ i, by simp [hi]⟩
+  have hle := Finset.card_le_card hsub
+  rw [card_univ_seed] at hle
+  have hbound : (Finset.univ.biUnion (fun i : Fin t =>
+      Finset.univ.filter fun r => shift r (u i) ∈ E)).card ≤ t * E.card := by
+    refine le_trans Finset.card_biUnion_le ?_
+    calc ∑ i : Fin t, (Finset.univ.filter fun r => shift r (u i) ∈ E).card
+        = ∑ _i : Fin t, E.card := by
+          exact Finset.sum_congr rfl fun i _ => card_filter_shift_mem E (u i)
+      _ = t * E.card := by
+          rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
+          simp
+      _ ≤ t * E.card := le_rfl
+  omega
+
+/-! ## Probability form -/
+
+/-- An event of probability at most `2 ^ (-k)` has at most `2 ^ (m - k)`
+elements, in the multiplication-only form used below. -/
+theorem card_mul_two_pow_le (E : Finset (Fin m → Bool)) (h : eventProb E ≤ 1 / 2 ^ k) :
+    E.card * 2 ^ k ≤ 2 ^ m := by
+  have h2m : (0 : ℚ) < 2 ^ m := by positivity
+  have h2k : (0 : ℚ) < 2 ^ k := by positivity
+  have hq : (E.card : ℚ) * 2 ^ k ≤ 2 ^ m := by
+    rw [eventProb, div_le_div_iff₀ h2m h2k] at h
+    linarith
+  exact_mod_cast hq
+
+/-- **Lautemann's covering lemma, completeness direction.** If the event `E`
+fails with probability at most `2 ^ (-k)`, and the seed length `m` is below
+`k * t`, then some `t` shifts of `E` cover the whole seed space. Since the
+failure probability enters as its `t`-th power against a union bound over the
+`2 ^ m` seeds, any `k ≥ 2` suffices at `t ≥ m`. -/
+theorem exists_covers_of_eventProb_compl_le (E : Finset (Fin m → Bool))
+    (hmt : m < k * t) (h : eventProb Eᶜ ≤ 1 / 2 ^ k) :
+    ∃ u : Fin t → Fin m → Bool, Covers E u := by
+  have hc : Eᶜ.card = 2 ^ m - E.card := by rw [Finset.card_compl, card_finArrowBool]
+  have hle : Eᶜ.card * 2 ^ k ≤ 2 ^ m := card_mul_two_pow_le Eᶜ h
+  refine exists_covers_of_card E ?_
+  rw [← hc]
+  by_contra hcon
+  simp only [not_lt] at hcon
+  have hpos : 0 < (2 ^ m : ℕ) ^ t := Nat.pow_pos (Nat.two_pow_pos m)
+  have key : (2 ^ m : ℕ) ^ t * 2 ^ (k * t) ≤ (2 ^ m : ℕ) ^ t * 2 ^ m := by
+    calc (2 ^ m : ℕ) ^ t * 2 ^ (k * t)
+        ≤ (2 ^ m * Eᶜ.card ^ t) * 2 ^ (k * t) := Nat.mul_le_mul_right _ hcon
+      _ = 2 ^ m * (Eᶜ.card * 2 ^ k) ^ t := by
+          rw [mul_pow, ← pow_mul]
+          ring
+      _ ≤ 2 ^ m * (2 ^ m) ^ t := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hle t)
+      _ = (2 ^ m : ℕ) ^ t * 2 ^ m := by ring
+  have hexp : (2 : ℕ) ^ (k * t) ≤ 2 ^ m := Nat.le_of_mul_le_mul_left key hpos
+  have hkm : k * t ≤ m := (Nat.pow_le_pow_iff_right (by norm_num)).mp hexp
+  omega
+
+/-- **Lautemann's covering lemma, soundness direction.** If the event `E` holds
+with probability at most `2 ^ (-k)` and the number of shifts `t` is below
+`2 ^ k`, then no `t` shifts of `E` cover the seed space. -/
+theorem not_covers_of_eventProb_le (E : Finset (Fin m → Bool)) (hk : t < 2 ^ k)
+    (h : eventProb E ≤ 1 / 2 ^ k) (u : Fin t → Fin m → Bool) : ¬ Covers E u := by
+  refine not_covers_of_card E ?_ u
+  have hle := card_mul_two_pow_le E h
+  rcases Nat.eq_zero_or_pos E.card with h0 | h0
+  · simp [h0, Nat.two_pow_pos m]
+  · calc t * E.card < 2 ^ k * E.card := (Nat.mul_lt_mul_right h0).mpr hk
+      _ = E.card * 2 ^ k := Nat.mul_comm _ _
+      _ ≤ 2 ^ m := hle
+
+end Lautemann
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann/Encode.lean b/Complexitylib/Classes/PH/SipserLautemann/Encode.lean
new file mode 100644
index 00000000..52758c65
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann/Encode.lean
@@ -0,0 +1,91 @@
+/-
+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.PH.SipserLautemann.Covering
+
+/-!
+# Bitstring codecs for seeds and shift tuples
+
+The Lautemann characterization quantifies over seeds `Fin m → Bool` and over
+tuples of shifts `Fin t → Fin m → Bool`, while the polynomial hierarchy
+quantifies over bitstrings. This file provides the two codecs and their
+round-trip lemmas: `listOfSeed`/`seedOfList` for a single seed, and
+`listOfShifts`/`shiftsOfList` for a tuple, flattened in row-major order.
+
+Decoding is total — out-of-range positions read as `false` — so a decoder is
+available on every bitstring, and the length equations pin down the well-formed
+encodings.
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Lautemann
+
+variable {t m : ℕ}
+
+/-- Encode a seed as a bitstring, one bit per position. -/
+def listOfSeed (s : Fin m → Bool) : List Bool := (List.finRange m).map s
+
+/-- Decode a bitstring as a seed, reading out-of-range positions as `false`. -/
+def seedOfList (m : ℕ) (r : List Bool) : Fin m → Bool := fun j => r.getD j.val false
+
+@[simp] theorem length_listOfSeed (s : Fin m → Bool) : (listOfSeed s).length = m := by
+  simp [listOfSeed]
+
+/-- Reading an encoded seed at an in-range position returns that bit. -/
+theorem getD_listOfSeed (s : Fin m → Bool) (idx : ℕ) (h : idx < m) :
+    (listOfSeed s).getD idx false = s ⟨idx, h⟩ := by
+  have hlen : idx < (listOfSeed s).length := by simpa using h
+  rw [List.getD, List.getElem?_eq_getElem hlen, Option.getD_some]
+  simp [listOfSeed]
+
+@[simp] theorem seedOfList_listOfSeed (s : Fin m → Bool) :
+    seedOfList m (listOfSeed s) = s := by
+  funext j
+  simpa [seedOfList] using getD_listOfSeed s j.val j.isLt
+
+/-- Flatten a tuple of shifts into a single seed of length `t * m`, in
+row-major order. -/
+def flattenShifts (u : Fin t → Fin m → Bool) : Fin (t * m) → Bool := fun kk =>
+  if h : 0 < m then
+    u ⟨kk.val / m, (Nat.div_lt_iff_lt_mul h).mpr kk.isLt⟩ ⟨kk.val % m, Nat.mod_lt _ h⟩
+  else false
+
+/-- Encode a tuple of shifts as a bitstring of length `t * m`. -/
+def listOfShifts (u : Fin t → Fin m → Bool) : List Bool := listOfSeed (flattenShifts u)
+
+/-- Decode a bitstring as a tuple of shifts, reading out-of-range positions as
+`false`. -/
+def shiftsOfList (t m : ℕ) (w : List Bool) : Fin t → Fin m → Bool :=
+  fun i j => w.getD (i.val * m + j.val) false
+
+@[simp] theorem length_listOfShifts (u : Fin t → Fin m → Bool) :
+    (listOfShifts u).length = t * m := by
+  simp [listOfShifts]
+
+@[simp] theorem shiftsOfList_listOfShifts (u : Fin t → Fin m → Bool) :
+    shiftsOfList t m (listOfShifts u) = u := by
+  funext i j
+  have hm : 0 < m := Nat.pos_of_ne_zero (by rintro rfl; exact absurd j.isLt (by omega))
+  have hidx : i.val * m + j.val < t * m := by
+    have hi : i.val + 1 ≤ t := i.isLt
+    calc i.val * m + j.val < i.val * m + m := by omega
+      _ = (i.val + 1) * m := by ring
+      _ ≤ t * m := Nat.mul_le_mul_right _ hi
+  have hdiv : (i.val * m + j.val) / m = i.val := by
+    rw [Nat.mul_comm, Nat.mul_add_div hm, Nat.div_eq_of_lt j.isLt, Nat.add_zero]
+  have hmod : (i.val * m + j.val) % m = j.val := by
+    rw [Nat.mul_comm, Nat.mul_add_mod, Nat.mod_eq_of_lt j.isLt]
+  simp only [shiftsOfList, listOfShifts]
+  rw [getD_listOfSeed _ _ hidx]
+  simp only [flattenShifts, dif_pos hm]
+  congr 1 <;> [exact Fin.ext hdiv; exact Fin.ext hmod]
+
+end Lautemann
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann/Matrix.lean b/Complexitylib/Classes/PH/SipserLautemann/Matrix.lean
new file mode 100644
index 00000000..638ae476
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann/Matrix.lean
@@ -0,0 +1,220 @@
+/-
+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.PH
+public import Complexitylib.Classes.P.Cobham.Internal.BlockScan
+public import Complexitylib.Classes.PH.SipserLautemann.Amplified
+public import Complexitylib.Classes.PH.SipserLautemann.Encode
+public import Complexitylib.Classes.PH.SipserLautemann.TimeBound
+
+/-!
+# The Lautemann matrix language and the `Σ₂` form
+
+The `∃∀` characterization of
+`Complexitylib.Classes.PH.SipserLautemann.Amplified` quantifies over shift
+tuples and seeds; the polynomial hierarchy quantifies over bitstrings. This
+file bridges the two: `matrixLang` is the innermost, quantifier-free predicate
+as a language of encoded triples, and `eq_polyExistsLang_polyForallLang` says
+that a bounded-error language is literally a polynomially bounded `∃∀` over it.
+
+Both the language and the identity are stated for a general time-bound
+function `f`, but the intended instance takes `f` to be the evaluation of a
+polynomial — see `NTM.acceptsWithProb_of_le`, which replaces a machine's
+arbitrary halting bound by a dominating polynomial. That is what makes the
+matrix predicate computable: a decider must recover the per-trial step count
+from the input length, which it can do when the count is a fixed polynomial in
+`|x|`, and cannot do for an arbitrary `f`.
+
+## Main definitions
+
+- `matrixLang tm f b` — on `pair (pair x w) r`: the decoded shifts of the
+  decoded seed contain one whose amplified majority verdict is `b`
+- `boundPoly` — the polynomial bounding the amplified seed length
+
+## Main results
+
+- `mem_matrixLang_pair` — membership on an encoded triple
+- `eq_polyExistsLang_polyForallLang` — the `Σ₂` form of a bounded-error
+  language, and `compl_eq_polyExistsLang_polyForallLang` for its complement
+- `boundPoly_bounds` — the amplified lengths are polynomially bounded
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Lautemann
+
+variable {k : ℕ}
+
+/-! ## The matrix language -/
+
+/-- The quantifier-free predicate of the Lautemann characterization, on the
+three decoded components. -/
+def matrixPred (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) : Prop :=
+  r.length = ampRuns f x.length * f x.length →
+    ∃ i : Fin (ampShifts f x.length),
+      blockMajority (NTM.repeatAcceptEvent tm x (f x.length))
+        (shift (seedOfList (ampRuns f x.length * f x.length) r)
+          (shiftsOfList (ampShifts f x.length)
+            (ampRuns f x.length * f x.length) w i)) = b
+
+/-- The same predicate as a `Bool`-valued verdict. -/
+noncomputable def matrixVerdictOn (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) :
+    Bool :=
+  if r.length = ampRuns f x.length * f x.length then
+    decide (∃ i : Fin (ampShifts f x.length),
+      blockMajority (NTM.repeatAcceptEvent tm x (f x.length))
+        (shift (seedOfList (ampRuns f x.length * f x.length) r)
+          (shiftsOfList (ampShifts f x.length)
+            (ampRuns f x.length * f x.length) w i)) = b)
+  else true
+
+/-- The verdict decides the predicate. -/
+theorem matrixVerdictOn_eq_true_iff (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) :
+    matrixVerdictOn tm f b x w r = true ↔ matrixPred tm f b x w r := by
+  rw [matrixVerdictOn, matrixPred]
+  by_cases h : r.length = ampRuns f x.length * f x.length
+  · rw [if_pos h]
+    simp [h]
+  · rw [if_neg h]
+    simp [h]
+
+/-- The innermost predicate of the Lautemann characterization, as a language of
+encoded triples. The components are decoded with the polynomial-time payload
+scanners `Cobham.fstBlock` and `Cobham.sndBlock`, which recover them from a
+canonical pair; on malformed input the decoders return their partial reads, and
+the language's contents there are irrelevant to the `Σ₂` identity below. -/
+def matrixLang (tm : NTM k) (f : ℕ → ℕ) (b : Bool) : Language :=
+  {z | matrixPred tm f b (Cobham.fstBlock (Cobham.fstBlock z))
+    (Cobham.sndBlock (Cobham.fstBlock z)) (Cobham.sndBlock z)}
+
+/-- Membership of an encoded triple in the matrix language. -/
+theorem mem_matrixLang_pair (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) :
+    pair (pair x w) r ∈ matrixLang tm f b ↔ matrixPred tm f b x w r := by
+  rw [matrixLang]
+  simp
+
+/-- The matrix as a `Bool`-valued verdict function, so that the remaining
+polynomial-time obligation is about a *function*, which
+`Complexitylib.Classes.P.Cobham` can discharge inside Cobham's algebra without
+constructing a machine. -/
+noncomputable def matrixVerdict (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (z : List Bool) : Bool :=
+  matrixVerdictOn tm f b (Cobham.fstBlock (Cobham.fstBlock z))
+    (Cobham.sndBlock (Cobham.fstBlock z)) (Cobham.sndBlock z)
+
+/-- The verdict function on an encoded triple. -/
+@[simp] theorem matrixVerdict_pair (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (x w r : List Bool) :
+    matrixVerdict tm f b (pair (pair x w) r) = matrixVerdictOn tm f b x w r := by
+  rw [matrixVerdict]
+  simp
+
+/-- The verdict function decides the matrix language. -/
+theorem mem_matrixLang_iff_verdict (tm : NTM k) (f : ℕ → ℕ) (b : Bool) (z : List Bool) :
+    z ∈ matrixLang tm f b ↔ matrixVerdict tm f b z = true := by
+  rw [matrixLang, matrixVerdict, matrixVerdictOn_eq_true_iff]
+  rfl
+
+/-! ## The `Σ₂` form -/
+
+/-- **The `Σ₂` form of a covering characterization.** Given a family of events
+whose covering-by-shifts characterizes a language `A`, that language is a
+polynomially bounded existential over a polynomially bounded universal over
+the matrix language. The existential witness encodes a covering tuple of
+shifts, and the universal variable ranges over seeds. -/
+theorem eq_polyExistsLang_polyForallLang {tm : NTM k} {f : ℕ → ℕ} {b : Bool}
+    {A : Language}
+    (E : ∀ x : List Bool, Finset (Fin (ampRuns f x.length * f x.length) → Bool))
+    (hmem : ∀ (x : List Bool) (w : Fin (ampRuns f x.length * f x.length) → Bool),
+      w ∈ E x ↔ blockMajority (NTM.repeatAcceptEvent tm x (f x.length)) w = b)
+    (hA : ∀ x : List Bool, x ∈ A ↔ ∃ u : Fin (ampShifts f x.length) →
+        Fin (ampRuns f x.length * f x.length) → Bool, Covers (E x) u)
+    {p q : Polynomial ℕ}
+    (hp : ∀ n, ampShifts f n * (ampRuns f n * f n) ≤ p.eval n)
+    (hq : ∀ n, ampRuns f n * f n ≤ q.eval n) :
+    A = polyExistsLang p (polyForallLang q (matrixLang tm f b)) := by
+  ext x
+  rw [hA x]
+  simp only [mem_polyExistsLang, mem_polyForallLang]
+  constructor
+  · rintro ⟨u, hu⟩
+    refine ⟨listOfShifts u, ?_, ?_⟩
+    · rw [length_listOfShifts]
+      exact hp x.length
+    · intro r _
+      rw [mem_matrixLang_pair]
+      intro hrlen
+      obtain ⟨i, hi⟩ := hu (seedOfList (ampRuns f x.length * f x.length) r)
+      rw [hmem] at hi
+      exact ⟨i, by simpa using hi⟩
+  · rintro ⟨w, _, hw⟩
+    refine ⟨shiftsOfList (ampShifts f x.length) (ampRuns f x.length * f x.length) w, ?_⟩
+    intro s
+    have hxle : x.length ≤ (pair x w).length := by
+      rw [pair_length]
+      omega
+    have hlen : (listOfSeed s).length ≤ q.eval (pair x w).length := by
+      rw [length_listOfSeed]
+      exact le_trans (hq x.length) (polynomial_eval_mono_nat q hxle)
+    have hmatrix := hw (listOfSeed s) hlen
+    rw [mem_matrixLang_pair] at hmatrix
+    obtain ⟨i, hi⟩ := hmatrix (by simp)
+    refine ⟨i, ?_⟩
+    rw [hmem]
+    simpa using hi
+
+/-- The `Σ₂` form of a bounded-error language: `L` itself. -/
+theorem eq_polyExistsLang_of_boundedError {tm : NTM k} {L : Language} {f : ℕ → ℕ}
+    (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3))
+    {p q : Polynomial ℕ}
+    (hp : ∀ n, ampShifts f n * (ampRuns f n * f n) ≤ p.eval n)
+    (hq : ∀ n, ampRuns f n * f n ≤ q.eval n) :
+    L = polyExistsLang p (polyForallLang q (matrixLang tm f true)) :=
+  eq_polyExistsLang_polyForallLang (fun x => ampEvent tm f x)
+    (fun x w => mem_ampEvent tm f x w) (mem_iff_exists_covers haccept hreject) hp hq
+
+/-- The `Σ₂` form of a bounded-error language: its complement. -/
+theorem compl_eq_polyExistsLang_of_boundedError {tm : NTM k} {L : Language} {f : ℕ → ℕ}
+    (haccept : tm.AcceptsWithProb L f (2 / 3)) (hreject : tm.RejectsWithProb L f (1 / 3))
+    {p q : Polynomial ℕ}
+    (hp : ∀ n, ampShifts f n * (ampRuns f n * f n) ≤ p.eval n)
+    (hq : ∀ n, ampRuns f n * f n ≤ q.eval n) :
+    Lᶜ = polyExistsLang p (polyForallLang q (matrixLang tm f false)) :=
+  eq_polyExistsLang_polyForallLang (fun x => (ampEvent tm f x)ᶜ)
+    (fun x w => mem_compl_ampEvent tm f x w)
+    (fun x => notMem_iff_exists_covers_compl haccept hreject x) hp hq
+
+/-! ## Polynomial bounds -/
+
+/-- The polynomial bounding the amplified seed length, given a polynomial `P`
+dominating the machine's time bound. -/
+noncomputable def boundPoly (P : Polynomial ℕ) : Polynomial ℕ :=
+  (Polynomial.C 12 * P + Polynomial.C 133) * P
+
+@[simp] theorem boundPoly_eval (P : Polynomial ℕ) (n : ℕ) :
+    (boundPoly P).eval n = (12 * P.eval n + 133) * P.eval n := by
+  simp [boundPoly]
+
+/-- The amplified seed length is bounded by `boundPoly P`, and the amplified
+witness length by `(boundPoly P + 1) * boundPoly P`. -/
+theorem boundPoly_bounds {f : ℕ → ℕ} {P : Polynomial ℕ} (hf : ∀ n, f n ≤ P.eval n) :
+    (∀ n, ampRuns f n * f n ≤ (boundPoly P).eval n) ∧
+      (∀ n, ampShifts f n * (ampRuns f n * f n) ≤
+        ((boundPoly P + 1) * boundPoly P).eval n) := by
+  have hseed : ∀ n, ampRuns f n * f n ≤ (boundPoly P).eval n := by
+    intro n
+    rw [boundPoly_eval]
+    have hr : ampRuns f n = 12 * f n + 133 := by simp [ampRuns, ampExp]; ring
+    rw [hr]
+    exact Nat.mul_le_mul (by have := hf n; omega) (hf n)
+  refine ⟨hseed, fun n => ?_⟩
+  have hs : ampShifts f n = ampRuns f n * f n + 1 := rfl
+  rw [hs, Polynomial.eval_mul, Polynomial.eval_add, Polynomial.eval_one]
+  exact Nat.mul_le_mul (by have := hseed n; omega) (hseed n)
+
+end Lautemann
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann/TimeBound.lean b/Complexitylib/Classes/PH/SipserLautemann/TimeBound.lean
new file mode 100644
index 00000000..0d1e50c5
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann/TimeBound.lean
@@ -0,0 +1,99 @@
+/-
+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.EventProb
+public import Complexitylib.Classes.Randomized
+
+/-!
+# Freezing the acceptance probability past the halting time
+
+A probabilistic machine whose paths all halt within `T` steps has the same
+acceptance probability at every later time bound: the extra choice bits are
+read by no transition, so they only refine the sample space uniformly. This
+lets a machine's arbitrary time-bound function be replaced by a polynomial
+that dominates it, which is what makes the Lautemann matrix predicate
+computable — see
+`Complexitylib.Classes.PH.SipserLautemann.Matrix`.
+
+## Main results
+
+- `card_filter_blockFst_eq` — a prefix fiber of the seed space has `2 ^ b`
+  points
+- `NTM.acceptProb_eq_of_allPathsHaltIn` — the acceptance probability is frozen
+  past the halting time
+- `NTM.acceptsWithProb_of_le`, `NTM.rejectsWithProb_of_le` — the bounded-error
+  conditions transfer to any pointwise-larger time bound
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+/-- Every prefix fiber of the seed space has exactly `2 ^ b` points: fixing the
+first `a` bits leaves the last `b` free. -/
+theorem card_filter_blockFst_eq (a b : ℕ) (seed : Fin a → Bool) :
+    (Finset.univ.filter fun w : Fin (a + b) → Bool => blockFst a b w = seed).card
+      = 2 ^ b := by
+  classical
+  have hinj : Function.Injective (fun v : Fin b → Bool => blockAppend a b seed v) := by
+    intro v v' hvv
+    have := congrArg (blockSnd a b) hvv
+    simpa using this
+  have hset : (Finset.univ.filter fun w : Fin (a + b) → Bool => blockFst a b w = seed)
+      = Finset.univ.image (fun v : Fin b → Bool => blockAppend a b seed v) := by
+    ext w
+    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]
+    constructor
+    · intro h
+      exact ⟨blockSnd a b w, by rw [← h, blockAppend_fst_snd]⟩
+    · rintro ⟨v, rfl⟩
+      simp
+  rw [hset, Finset.card_image_of_injective _ hinj, Finset.card_univ, card_finArrowBool]
+
+namespace NTM
+
+variable {n : ℕ}
+
+/-- **The acceptance probability is frozen past the halting time.** If all
+paths halt within `T (|x|)` steps, running the machine for any longer bound
+leaves the acceptance probability unchanged: the surplus choice bits partition
+the enlarged sample space into equal fibers over the original one. -/
+theorem acceptProb_eq_of_allPathsHaltIn {tm : NTM n} {T : ℕ → ℕ}
+    (hN : tm.AllPathsHaltIn T) (x : List Bool) {T' : ℕ} (hle : T x.length ≤ T') :
+    tm.acceptProb x T' = tm.acceptProb x (T x.length) := by
+  classical
+  obtain ⟨i, rfl⟩ := Nat.exists_eq_add_of_le hle
+  rw [acceptProb_eq_eventProb, acceptProb_eq_eventProb]
+  refine eventProb_filter_of_constant_fibers (htotal := rfl)
+    (randomSeed := blockFst (T x.length) i) _ _ ?_ (card_filter_blockFst_eq _ _)
+  intro w
+  have hagree : ∀ j : Fin (T x.length),
+      w ⟨j.val, by omega⟩ = blockFst (T x.length) i w j := by
+    intro j
+    rfl
+  have hhalt : tm.halted (tm.trace (T x.length) (blockFst (T x.length) i w)
+      (tm.initCfg x)) := hN x _
+  rw [tm.trace_mono (Nat.le_add_right _ i) hagree hhalt]
+
+/-- The completeness condition transfers to any pointwise-larger time bound. -/
+theorem acceptsWithProb_of_le {tm : NTM n} {L : Language} {T T' : ℕ → ℕ} {c : ℚ}
+    (hN : tm.AllPathsHaltIn T) (hle : ∀ m, T m ≤ T' m)
+    (h : tm.AcceptsWithProb L T c) : tm.AcceptsWithProb L T' c := by
+  intro x hx
+  rw [acceptProb_eq_of_allPathsHaltIn hN x (hle x.length)]
+  exact h x hx
+
+/-- The soundness condition transfers to any pointwise-larger time bound. -/
+theorem rejectsWithProb_of_le {tm : NTM n} {L : Language} {T T' : ℕ → ℕ} {s : ℚ}
+    (hN : tm.AllPathsHaltIn T) (hle : ∀ m, T m ≤ T' m)
+    (h : tm.RejectsWithProb L T s) : tm.RejectsWithProb L T' s := by
+  intro x hx
+  rw [acceptProb_eq_of_allPathsHaltIn hN x (hle x.length)]
+  exact h x hx
+
+end NTM
+
+end Complexity
diff --git a/Complexitylib/Classes/PH/SipserLautemann/Verdict.lean b/Complexitylib/Classes/PH/SipserLautemann/Verdict.lean
new file mode 100644
index 00000000..fe5a090e
--- /dev/null
+++ b/Complexitylib/Classes/PH/SipserLautemann/Verdict.lean
@@ -0,0 +1,383 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+module
+public import Complexitylib.Classes.P.Cobham
+public import Complexitylib.Classes.P.Cobham.Internal.FstBlock
+public import Complexitylib.Classes.P.Cobham.Internal.SndBlock
+public import Complexitylib.Classes.P.Cobham.Internal.BlockLoop
+public import Complexitylib.Classes.PH.SipserLautemann.Matrix
+
+/-!
+# Bridging the string computation and the counting definitions
+
+The amplified verdict is defined by counting blocks of a seed *function*
+`Fin (k * T) → Bool` inside a `Finset`; the algebra computes with the seed as a
+*string*. This file identifies the two views: a block of the string decodes to
+the corresponding block of the function, so the algebra's unary count is the
+`blockEventCount` of the amplification lemmas.
+
+## Main results
+
+- `Lautemann.getD_take_drop` — reading inside a block of a string
+- `Lautemann.seedOfList_blockAtIdx` — the decoded block is the function's block
+- `Lautemann.blockEventCount_seedOfList` — the two counts agree
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace Lautemann
+
+variable {k : ℕ}
+
+/-- Reading inside a block of a string reads the underlying string. -/
+theorem getD_take_drop (s : List Bool) (a b j : ℕ) (hj : j < b) :
+    ((s.drop a).take b).getD j false = s.getD (a + j) false := by
+  rw [List.getD, List.getD, List.getElem?_take_of_lt hj, List.getElem?_drop]
+
+/-- The block of a decoded seed is the decoding of the block of the string. -/
+theorem seedOfList_blockAtIdx (T : ℕ) (s : List Bool) (i : ℕ) (t : Fin T) :
+    seedOfList T (Cobham.blockAtIdx T s i) t = s.getD (i * T + t.val) false := by
+  rw [seedOfList, Cobham.blockAtIdx]
+  exact getD_take_drop s (i * T) T t.val t.isLt
+
+/-- The blocks of a decoded long seed are the decodings of its string blocks. -/
+theorem blocksEquiv_seedOfList (runs T : ℕ) (s : List Bool) (i : Fin runs) :
+    blocksEquiv runs T (seedOfList (runs * T) s) i
+      = seedOfList T (Cobham.blockAtIdx T s i.val) := by
+  funext t
+  rw [blocksEquiv_apply, seedOfList_blockAtIdx, seedOfList]
+  congr 1
+  show t.val + T * i.val = i.val * T + t.val
+  rw [Nat.mul_comm]
+  omega
+
+/-- Path acceptance is membership of the decoded choice string in the
+single-trial accepting event. -/
+theorem pathAccepts_iff (tm : NTM k) (x c : List Bool) :
+    Cobham.PathAccepts tm x c
+      ↔ seedOfList c.length c ∈ NTM.repeatAcceptEvent tm x c.length := by
+  have hfun : (fun j : Fin c.length => c[j.val]'j.isLt) = seedOfList c.length c := by
+    funext j
+    rw [seedOfList, List.getD, List.getElem?_eq_getElem j.isLt, Option.getD_some]
+  rw [Cobham.PathAccepts, hfun, NTM.repeatAcceptEvent]
+  simp
+
+/-- The block count of a decoded seed is a sum over block indices. -/
+theorem blockEventCount_seedOfList {T : ℕ} (E : Finset (Fin T → Bool)) (runs : ℕ)
+    (s : List Bool) :
+    blockEventCount E (seedOfList (runs * T) s)
+      = ∑ j ∈ Finset.range runs,
+          (if seedOfList T (Cobham.blockAtIdx T s j) ∈ E then 1 else 0) := by
+  rw [blockEventCount, Finset.card_filter, ← Fin.sum_univ_eq_sum_range
+    (fun j => if seedOfList T (Cobham.blockAtIdx T s j) ∈ E then 1 else 0) runs]
+  refine Finset.sum_congr rfl fun i _ => ?_
+  rw [blocksEquiv_seedOfList]
+
+/-- Inside a seed of exactly `runs` blocks, every block is full. -/
+theorem blockAtIdx_length (T : ℕ) (s : List Bool) (j runs : ℕ)
+    (hs : s.length = runs * T) (hj : j < runs) :
+    (Cobham.blockAtIdx T s j).length = T := by
+  have hmul : j * T + T ≤ runs * T := by
+    have h := Nat.mul_le_mul_right T (Nat.succ_le_of_lt hj)
+    rwa [Nat.succ_mul] at h
+  rw [Cobham.blockAtIdx, List.length_take, List.length_drop, hs]
+  omega
+
+/-- **The algebra's count is the amplification lemmas' block count.** -/
+theorem acceptCountAux_length_eq (tm : NTM k) (u x τ s ρ : List Bool) (runs : ℕ)
+    (hρ : ρ.length = runs) (hs : s.length = runs * τ.length)
+    (hu : x.length + τ.length + Fintype.card tm.Q + 3 ≤ u.length) :
+    (Cobham.acceptCountAux tm u x τ s ρ).length
+      = blockEventCount (NTM.repeatAcceptEvent tm x τ.length)
+          (seedOfList (runs * τ.length) s) := by
+  rw [Cobham.acceptCountAux_length, blockEventCount_seedOfList, hρ]
+  refine Finset.sum_congr rfl fun j hj => ?_
+  rw [Finset.mem_range] at hj
+  have hblen : (Cobham.blockAtIdx τ.length s j).length = τ.length :=
+    blockAtIdx_length τ.length s j runs hs hj
+  have hacc : Cobham.acceptChoiceFn tm u x (Cobham.blockAtIdx τ.length s j) = [true]
+      ↔ seedOfList τ.length (Cobham.blockAtIdx τ.length s j)
+          ∈ NTM.repeatAcceptEvent tm x τ.length := by
+    rw [Cobham.acceptChoiceFn_eq_true_iff tm u x (Cobham.blockAtIdx τ.length s j)
+      (by rw [hblen]; omega), pathAccepts_iff, hblen]
+  by_cases h : Cobham.acceptChoiceFn tm u x (Cobham.blockAtIdx τ.length s j) = [true]
+  · rw [if_pos h, if_pos (hacc.mp h)]
+  · rw [if_neg h, if_neg (fun hmem => h (hacc.mpr hmem))]
+
+/-- **The algebra's majority flag is the amplified majority verdict.** -/
+theorem majorityFlag_eq_true_iff' (tm : NTM k) (u x τ s ρ : List Bool) (runs : ℕ)
+    (hρ : ρ.length = runs) (hs : s.length = runs * τ.length)
+    (hu : x.length + τ.length + Fintype.card tm.Q + 3 ≤ u.length) :
+    Cobham.majorityFlag tm u x τ s ρ = [true]
+      ↔ blockMajority (NTM.repeatAcceptEvent tm x τ.length)
+          (seedOfList (runs * τ.length) s) = true := by
+  rw [Cobham.majorityFlag_eq_true_iff, acceptCountAux_length_eq tm u x τ s ρ runs hρ hs hu,
+    hρ, blockMajority]
+  simp only [decide_eq_true_eq]
+
+/-! ## The shift action -/
+
+/-- Reading inside a padded block reads the block. -/
+theorem getD_padTo (σ b : List Bool) (j : ℕ) (hj : j < σ.length) :
+    (padTo σ b).getD j false = b.getD j false := by
+  rcases Nat.lt_or_ge j b.length with hb | hb
+  · rw [padTo, List.getD, List.getD, List.getElem?_take_of_lt hj,
+      List.getElem?_append_left hb]
+  · have h1 : (padTo σ b)[j]? = some false := by
+      rw [padTo, List.getElem?_take_of_lt hj,
+        List.getElem?_append_right hb, List.getElem?_replicate]
+      rw [if_pos (by omega)]
+    rw [List.getD, h1, List.getD, List.getElem?_eq_none hb]
+    rfl
+
+/-- The decoded exclusive-or is the shift action on decoded seeds. -/
+theorem seedOfList_xorSuffix (m : ℕ) (r blk : List Bool) (hr : r.length = m)
+    (hblk : blk.length = m) :
+    seedOfList m (Cobham.xorSuffix r blk) = shift (seedOfList m r) (seedOfList m blk) := by
+  funext j
+  rw [Cobham.xorSuffix_eq_zipWith_of_length r blk (by omega), shift, seedOfList,
+    seedOfList, seedOfList]
+  have hj : j.val < (List.zipWith xor r blk).length := by
+    rw [List.length_zipWith]
+    omega
+  have hjr : j.val < r.length := by omega
+  have hjb : j.val < blk.length := by omega
+  rw [List.getD, List.getElem?_eq_getElem hj, Option.getD_some, List.getElem_zipWith,
+    List.getD, List.getElem?_eq_getElem hjr, Option.getD_some,
+    List.getD, List.getElem?_eq_getElem hjb, Option.getD_some]
+
+/-- The decoded padded block is the decoded shift vector. -/
+theorem seedOfList_padTo_block (t m : ℕ) (σ w : List Bool) (hσ : σ.length = m)
+    (i : Fin t) :
+    seedOfList m (padTo σ (Cobham.blockAtIdx m w i.val))
+      = shiftsOfList t m w i := by
+  funext j
+  rw [seedOfList, shiftsOfList, getD_padTo σ _ j.val (by rw [hσ]; exact j.isLt),
+    Cobham.blockAtIdx, getD_take_drop w (i.val * m) m j.val j.isLt]
+
+/-! ## The rulers -/
+
+/-- The clock string for the path simulations: long enough for every block. -/
+noncomputable def clockStr (pt : Polynomial ℕ) (q : ℕ) (x : List Bool) : List Bool :=
+  x ++ (Cobham.polyLen pt x ++ List.replicate (q + 3) false)
+
+@[simp] theorem clockStr_length (pt : Polynomial ℕ) (q : ℕ) (x : List Bool) :
+    (clockStr pt q x).length = x.length + pt.eval x.length + (q + 3) := by
+  rw [clockStr, List.length_append, List.length_append, Cobham.polyLen_length,
+    List.length_replicate]
+  omega
+
+/-- The ruler whose length is the number of amplification trials. -/
+noncomputable def runsStr (pt : Polynomial ℕ) (x : List Bool) : List Bool :=
+  List.replicate 133 false
+    ++ Complexity.smash (List.replicate 12 false) (Cobham.polyLen pt x)
+
+@[simp] theorem runsStr_length (pt : Polynomial ℕ) (x : List Bool) :
+    (runsStr pt x).length = ampRuns pt.eval x.length := by
+  rw [runsStr, List.length_append, List.length_replicate, smash_length,
+    List.length_replicate, Cobham.polyLen_length, ampRuns, ampExp]
+  ring
+
+/-- The ruler whose length is the amplified seed length. -/
+noncomputable def seedStr (pt : Polynomial ℕ) (x : List Bool) : List Bool :=
+  Complexity.smash (runsStr pt x) (Cobham.polyLen pt x)
+
+@[simp] theorem seedStr_length (pt : Polynomial ℕ) (x : List Bool) :
+    (seedStr pt x).length = ampRuns pt.eval x.length * pt.eval x.length := by
+  rw [seedStr, smash_length, runsStr_length, Cobham.polyLen_length]
+
+/-- The ruler whose length is the number of shifts. -/
+noncomputable def shiftStr (pt : Polynomial ℕ) (x : List Bool) : List Bool :=
+  false :: seedStr pt x
+
+@[simp] theorem shiftStr_length (pt : Polynomial ℕ) (x : List Bool) :
+    (shiftStr pt x).length = ampShifts pt.eval x.length := by
+  rw [shiftStr, List.length_cons, seedStr_length, ampShifts]
+
+/-! ## The verdict as an algebra function -/
+
+/-- The matrix verdict, computed from the decoded components with the rulers
+above: check the seed's length, then take the disjunction over shift blocks of
+the amplified majority verdict. -/
+noncomputable def matrixFn (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) (z : List Bool) :
+    List Bool :=
+  caseBit₀
+    (Cobham.lenEqFlag (Cobham.sndBlock z)
+      (seedStr pt (Cobham.fstBlock (Cobham.fstBlock z))))
+    (Cobham.anyShiftAux tm b
+      (clockStr pt (Fintype.card tm.Q) (Cobham.fstBlock (Cobham.fstBlock z)))
+      (Cobham.fstBlock (Cobham.fstBlock z))
+      (Cobham.polyLen pt (Cobham.fstBlock (Cobham.fstBlock z)))
+      (runsStr pt (Cobham.fstBlock (Cobham.fstBlock z)))
+      (seedStr pt (Cobham.fstBlock (Cobham.fstBlock z)))
+      (Cobham.sndBlock z) (Cobham.sndBlock (Cobham.fstBlock z))
+      (shiftStr pt (Cobham.fstBlock (Cobham.fstBlock z))))
+    [true]
+
+/-- A flag matching a Boolean, in the two polarities. -/
+private theorem flag_iff_bool {fl : List Bool} {c b : Bool}
+    (hflag : fl = [true] ∨ fl = [false]) (h : fl = [true] ↔ c = true) :
+    (bif b then fl else notBit fl) = [true] ↔ c = b := by
+  cases b
+  · rw [Bool.cond_false, Cobham.notBit_eq_true_iff hflag]
+    rcases hflag with hf | hf
+    · have hc : c = true := h.mp hf
+      rw [hf, hc]
+      simp
+    · rw [hf]
+      simp only [true_iff]
+      cases hc : c
+      · rfl
+      · rw [hc] at h
+        exact absurd (h.mpr rfl) (by rw [hf]; simp)
+  · rw [Bool.cond_true]
+    exact h
+
+/-- **The per-shift verdict is the amplified majority at that shift.** -/
+theorem verdictFlag_shift_iff (tm : NTM k) (pt : Polynomial ℕ) (b : Bool)
+    (x w r : List Bool)
+    (hr : r.length = ampRuns pt.eval x.length * pt.eval x.length)
+    (i : Fin (ampShifts pt.eval x.length)) :
+    Cobham.verdictFlag tm b (clockStr pt (Fintype.card tm.Q) x) x (Cobham.polyLen pt x)
+        (Cobham.xorSuffix r (padTo (seedStr pt x)
+          (Cobham.blockAtIdx (seedStr pt x).length w i.val))) (runsStr pt x) = [true]
+      ↔ blockMajority (NTM.repeatAcceptEvent tm x (pt.eval x.length))
+          (shift (seedOfList (ampRuns pt.eval x.length * pt.eval x.length) r)
+            (shiftsOfList (ampShifts pt.eval x.length)
+              (ampRuns pt.eval x.length * pt.eval x.length) w i)) = b := by
+  have hσ : (seedStr pt x).length = ampRuns pt.eval x.length * pt.eval x.length :=
+    seedStr_length pt x
+  have hblk : Cobham.blockAtIdx (seedStr pt x).length w i.val
+      = Cobham.blockAtIdx (ampRuns pt.eval x.length * pt.eval x.length) w i.val := by
+    rw [hσ]
+  have hslen : (Cobham.xorSuffix r (padTo (seedStr pt x)
+      (Cobham.blockAtIdx (seedStr pt x).length w i.val))).length
+      = ampRuns pt.eval x.length * pt.eval x.length := by
+    rw [Cobham.xorSuffix_length, hr]
+  have hseed : seedOfList (ampRuns pt.eval x.length * pt.eval x.length)
+        (Cobham.xorSuffix r (padTo (seedStr pt x)
+          (Cobham.blockAtIdx (seedStr pt x).length w i.val)))
+      = shift (seedOfList (ampRuns pt.eval x.length * pt.eval x.length) r)
+          (shiftsOfList (ampShifts pt.eval x.length)
+            (ampRuns pt.eval x.length * pt.eval x.length) w i) := by
+    rw [hblk, seedOfList_xorSuffix _ r _ hr (by rw [padTo_length, hσ]),
+      seedOfList_padTo_block (ampShifts pt.eval x.length)
+        (ampRuns pt.eval x.length * pt.eval x.length) (seedStr pt x) w hσ i]
+  have hmaj := majorityFlag_eq_true_iff' tm (clockStr pt (Fintype.card tm.Q) x) x
+    (Cobham.polyLen pt x)
+    (Cobham.xorSuffix r (padTo (seedStr pt x)
+      (Cobham.blockAtIdx (seedStr pt x).length w i.val)))
+    (runsStr pt x) (ampRuns pt.eval x.length) (runsStr_length pt x)
+    (by rw [hslen, Cobham.polyLen_length])
+    (by rw [clockStr_length, Cobham.polyLen_length]; omega)
+  rw [Cobham.polyLen_length] at hmaj
+  rw [hseed] at hmaj
+  exact flag_iff_bool (Cobham.majorityFlag_flag _ _ _ _ _ _) hmaj
+
+/-- The verdict computation on the three decoded components. -/
+private theorem matrixFn_aux (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) (x w r : List Bool) :
+    caseBit₀ (Cobham.lenEqFlag r (seedStr pt x))
+      (Cobham.anyShiftAux tm b (clockStr pt (Fintype.card tm.Q) x) x (Cobham.polyLen pt x)
+        (runsStr pt x) (seedStr pt x) r w (shiftStr pt x)) [true]
+      = [matrixVerdictOn tm pt.eval b x w r] := by
+  rw [matrixVerdictOn]
+  by_cases hlen : r.length = ampRuns pt.eval x.length * pt.eval x.length
+  · have hflag : Cobham.lenEqFlag r (seedStr pt x) = [true] := by
+      rw [Cobham.lenEqFlag_eq_true_iff, seedStr_length]
+      exact hlen
+    rw [hflag, if_pos hlen, caseBit₀_cons, cond_true]
+    have hiff : Cobham.anyShiftAux tm b (clockStr pt (Fintype.card tm.Q) x) x
+        (Cobham.polyLen pt x) (runsStr pt x) (seedStr pt x) r w (shiftStr pt x) = [true]
+        ↔ ∃ i : Fin (ampShifts pt.eval x.length),
+            blockMajority (NTM.repeatAcceptEvent tm x (pt.eval x.length))
+              (shift (seedOfList (ampRuns pt.eval x.length * pt.eval x.length) r)
+                (shiftsOfList (ampShifts pt.eval x.length)
+                  (ampRuns pt.eval x.length * pt.eval x.length) w i)) = b := by
+      rw [Cobham.anyShiftAux_eq_true_iff, shiftStr_length]
+      constructor
+      · rintro ⟨i, hi, hv⟩
+        exact ⟨⟨i, hi⟩, (verdictFlag_shift_iff tm pt b x w r hlen ⟨i, hi⟩).mp hv⟩
+      · rintro ⟨i, hb⟩
+        exact ⟨i.val, i.isLt, (verdictFlag_shift_iff tm pt b x w r hlen i).mpr hb⟩
+    rcases Cobham.anyShiftAux_flag tm b (clockStr pt (Fintype.card tm.Q) x) x
+      (Cobham.polyLen pt x) (runsStr pt x) (seedStr pt x) r w (shiftStr pt x) with h | h
+    · rw [h, decide_eq_true (hiff.mp h)]
+    · rw [h, decide_eq_false ?_]
+      intro hex
+      rw [hiff.mpr hex] at h
+      exact absurd h (by simp)
+  · have hflag : Cobham.lenEqFlag r (seedStr pt x) = [false] := by
+      rcases Cobham.lenEqFlag_flag r (seedStr pt x) with h | h
+      · rw [Cobham.lenEqFlag_eq_true_iff, seedStr_length] at h
+        exact absurd h hlen
+      · exact h
+    rw [hflag, if_neg hlen, caseBit₀_cons, cond_false]
+
+/-- **The algebra function computes the matrix verdict.** -/
+theorem matrixFn_eq (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) (z : List Bool) :
+    matrixFn tm pt b z = [matrixVerdict tm pt.eval b z] :=
+  matrixFn_aux tm pt b _ _ _
+
+/-! ## Membership in the algebra -/
+
+/-- The pair decoders are in the algebra, being polynomial-time. -/
+theorem fstBlock_cobham {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => Cobham.fstBlock (g v) :=
+  (Cobham.comp (FP_subset_CobhamFP Cobham.fstBlock_mem_FP)
+    fun _ : Fin 1 => hg).of_eq fun _ => rfl
+
+theorem sndBlock_cobham {n : ℕ} {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => Cobham.sndBlock (g v) :=
+  (Cobham.comp (FP_subset_CobhamFP Cobham.sndBlock_mem_FP)
+    fun _ : Fin 1 => hg).of_eq fun _ => rfl
+
+theorem clockStr_mem {n : ℕ} (pt : Polynomial ℕ) (q : ℕ)
+    {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => clockStr pt q (g v) :=
+  (Cobham.appendFn hg
+    (Cobham.appendFn (Cobham.polyLen_mem pt hg) (Cobham.const _))).of_eq fun _ => rfl
+
+theorem runsStr_mem {n : ℕ} (pt : Polynomial ℕ)
+    {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => runsStr pt (g v) :=
+  (Cobham.appendFn (Cobham.const _)
+    (Cobham.comp₂ Cobham.smash (Cobham.const _) (Cobham.polyLen_mem pt hg))).of_eq fun _ => rfl
+
+theorem seedStr_mem {n : ℕ} (pt : Polynomial ℕ)
+    {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => seedStr pt (g v) :=
+  (Cobham.comp₂ Cobham.smash (runsStr_mem pt hg) (Cobham.polyLen_mem pt hg)).of_eq fun _ => rfl
+
+theorem shiftStr_mem {n : ℕ} (pt : Polynomial ℕ)
+    {g : (Fin n → List Bool) → List Bool} (hg : Cobham g) :
+    Cobham fun v : Fin n → List Bool => shiftStr pt (g v) :=
+  (Cobham.comp (Cobham.bit false) fun _ : Fin 1 => seedStr_mem pt hg).of_eq fun _ => rfl
+
+/-- **The matrix verdict is in the algebra.** -/
+theorem matrixFn_mem (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) :
+    Cobham fun v : Fin 1 → List Bool => matrixFn tm pt b (v 0) := by
+  have hz : Cobham fun v : Fin 1 → List Bool => v 0 := Cobham.proj 0
+  have hx : Cobham fun v : Fin 1 → List Bool =>
+      Cobham.fstBlock (Cobham.fstBlock (v 0)) := fstBlock_cobham (fstBlock_cobham hz)
+  have hw : Cobham fun v : Fin 1 → List Bool =>
+      Cobham.sndBlock (Cobham.fstBlock (v 0)) := sndBlock_cobham (fstBlock_cobham hz)
+  have hr : Cobham fun v : Fin 1 → List Bool => Cobham.sndBlock (v 0) := sndBlock_cobham hz
+  exact (Cobham.iteFn (Cobham.lenEqFlag_mem hr (seedStr_mem pt hx))
+    (Cobham.anyShiftAux_mem tm b (clockStr_mem pt (Fintype.card tm.Q) hx) hx
+      (Cobham.polyLen_mem pt hx) (runsStr_mem pt hx) (seedStr_mem pt hx) hr hw
+      (shiftStr_mem pt hx))
+    (Cobham.const [true])).of_eq fun _ => rfl
+
+/-- **The matrix verdict is polynomial-time computable.** -/
+theorem matrixVerdict_mem_FP (tm : NTM k) (pt : Polynomial ℕ) (b : Bool) :
+    (fun z => [matrixVerdict tm pt.eval b z]) ∈ FP :=
+  CobhamFP_subset_FP ((matrixFn_mem tm pt b).of_eq fun v => matrixFn_eq tm pt b (v 0))
+
+end Lautemann
+
+end Complexity
diff --git a/Complexitylib/Languages/Contains.lean b/Complexitylib/Languages/Contains.lean
index 18dc6191..2e87c9ef 100644
--- a/Complexitylib/Languages/Contains.lean
+++ b/Complexitylib/Languages/Contains.lean
@@ -53,6 +53,14 @@ def containsZero : Language := {x | ∃ b ∈ x, b = false}
 /-- Strings containing at least one `1`-bit. -/
 def containsOne : Language := {x | ∃ b ∈ x, b = true}
 
+/-- Membership in `containsZero` unfolds to the existence of a `0`-bit. -/
+@[simp] theorem mem_containsZero {x : List Bool} :
+    x ∈ containsZero ↔ ∃ b ∈ x, b = false := Iff.rfl
+
+/-- Membership in `containsOne` unfolds to the existence of a `1`-bit. -/
+@[simp] theorem mem_containsOne {x : List Bool} :
+    x ∈ containsOne ↔ ∃ b ∈ x, b = true := Iff.rfl
+
 end Language
 
 -- ════════════════════════════════════════════════════════════════════════
diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean
index 7d808aeb..997a6ac1 100644
--- a/Complexitylib/Models.lean
+++ b/Complexitylib/Models.lean
@@ -9,6 +9,7 @@ public import Complexitylib.Models.TuringMachine
 public import Complexitylib.Models.TuringMachine.Trace
 public import Complexitylib.Models.TuringMachine.Trace.DetPrefix
 public import Complexitylib.Models.TuringMachine.SingleTape
+public import Complexitylib.Models.TuringMachine.ChoiceTape
 public import Complexitylib.Models.TuringMachine.Combinators
 public import Complexitylib.Models.TuringMachine.Combinators.ForBinaryWork
 public import Complexitylib.Models.TuringMachine.Combinators.ForInput
diff --git a/Complexitylib/Models/TuringMachine/ChoiceTape.lean b/Complexitylib/Models/TuringMachine/ChoiceTape.lean
new file mode 100644
index 00000000..644de84e
--- /dev/null
+++ b/Complexitylib/Models/TuringMachine/ChoiceTape.lean
@@ -0,0 +1,177 @@
+/-
+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.Combinators
+
+/-!
+# Running one nondeterministic path deterministically
+
+An `NTM`'s transition function has exactly the shape of a `TM`'s, plus a
+`Bool`. Feeding that `Bool` from a dedicated work tape — one cell per step,
+scanned left to right and written back unchanged — turns the nondeterministic
+machine into a deterministic one whose run is the chosen path.
+
+This is the primitive that lets deterministic machines reason about
+nondeterministic runs: a decider that must evaluate "does `tm` accept `x` along
+choice sequence `c`" places `c` on the choice tape and runs `choiceTM tm`.
+
+## Main definitions
+
+- `NTM.choiceTM` — the deterministic machine with a choice tape appended
+- `NTM.dropChoice` — forget the choice tape from a configuration
+- `NTM.choiceStream` — the choice bits under and to the right of the head
+
+## Main results
+
+- `NTM.choiceTM_step` — one step of `choiceTM` is one step of the path
+- `NTM.choiceTM_simulates` — a `T`-step run of `choiceTM` is `tm.trace T`
+  along the choice bits found on the tape
+-/
+
+@[expose] public section
+
+namespace Complexity
+
+namespace TM
+
+variable {k : ℕ}
+
+/-- The configuration update inlined in `TM.step`. -/
+def stepCfg (tm : TM k) (c : Cfg k tm.Q) : Cfg k tm.Q :=
+  let (q', workWrites, outWrite, inDir, workDirs, outDir) :=
+    tm.δ c.state c.input.read (fun i => (c.work i).read) c.output.read
+  { state := q'
+    input := c.input.move inDir
+    work := fun i => (c.work i).writeAndMove (workWrites i) (workDirs i)
+    output := c.output.writeAndMove outWrite outDir }
+
+/-- A non-halted configuration steps to `stepCfg`. -/
+theorem step_of_not_halted (tm : TM k) {c : Cfg k tm.Q} (h : c.state ≠ tm.qhalt) :
+    tm.step c = some (tm.stepCfg c) := by
+  unfold TM.step
+  rw [if_neg h]
+  rfl
+
+end TM
+
+namespace NTM
+
+variable {k : ℕ}
+
+/-- The deterministic machine that runs one path of `tm`, reading its choice
+bits from the appended last work tape: each step consults the cell under that
+head, writes it back unchanged, and advances the head one cell right. -/
+def choiceTM (tm : NTM k) : TM (k + 1) where
+  Q := tm.Q
+  qstart := tm.qstart
+  qhalt := tm.qhalt
+  δ q iHead wHeads oHead :=
+    let cHead := wHeads (Fin.last k)
+    let r := tm.δ (decide (cHead = Γ.one)) q iHead (fun i => wHeads i.castSucc) oHead
+    (r.1, Fin.snoc r.2.1 (TM.readBackWrite cHead), r.2.2.1,
+      r.2.2.2.1, Fin.snoc r.2.2.2.2.1 Dir3.right, r.2.2.2.2.2)
+  δ_right_of_start := by
+    intro q iHead wHeads oHead
+    have h := tm.δ_right_of_start (decide (wHeads (Fin.last k) = Γ.one)) q iHead
+      (fun i => wHeads i.castSucc) oHead
+    dsimp only at h ⊢
+    refine ⟨h.1, ?_, h.2.2⟩
+    intro i
+    refine Fin.lastCases ?_ ?_ i
+    · intro _
+      simp
+    · intro j hj
+      rw [Fin.snoc_castSucc]
+      exact h.2.1 j (by simpa using hj)
+
+/-- One step of an NTM along a fixed choice bit: the configuration update
+inlined in `NTM.trace`. -/
+def stepCfg (tm : NTM k) (b : Bool) (c : Cfg k tm.Q) : Cfg k tm.Q :=
+  let (q', workWrites, outWrite, inDir, workDirs, outDir) :=
+    tm.δ b c.state c.input.read (fun i => (c.work i).read) c.output.read
+  { state := q'
+    input := c.input.move inDir
+    work := fun i => (c.work i).writeAndMove (workWrites i) (workDirs i)
+    output := c.output.writeAndMove outWrite outDir }
+
+/-- Unfolding one non-halted step of `trace`. -/
+theorem trace_succ_of_not_halted (tm : NTM k) (T : ℕ) (choices : Fin (T + 1) → Bool)
+    {c : Cfg k tm.Q} (h : c.state ≠ tm.qhalt) :
+    tm.trace (T + 1) choices c =
+      tm.trace T (fun i => choices ⟨i.val + 1, by omega⟩)
+        (stepCfg tm (choices ⟨0, Nat.zero_lt_succ T⟩) c) := by
+  rw [NTM.trace]
+  simp [h, stepCfg]
+
+/-- Forget the choice tape from a configuration. -/
+def dropChoice {Q : Type} (c : Cfg (k + 1) Q) : Cfg k Q where
+  state := c.state
+  input := c.input
+  work := fun i => c.work i.castSucc
+  output := c.output
+
+/-- The choice bits under and to the right of the choice head. -/
+def choiceStream {Q : Type} (c : Cfg (k + 1) Q) (j : ℕ) : Bool :=
+  decide ((c.work (Fin.last k)).cells ((c.work (Fin.last k)).head + j) = Γ.one)
+
+/-- **One step of `choiceTM` is one step of the chosen path.** The choice tape
+is written back unchanged and its head advances one cell. -/
+theorem choiceTM_step (tm : NTM k) (c : Cfg (k + 1) tm.Q) (hhalt : c.state ≠ tm.qhalt)
+    (hread : (c.work (Fin.last k)).read ≠ Γ.start) :
+    ∃ c₁, (choiceTM tm).step c = some c₁ ∧
+      dropChoice c₁ = stepCfg tm (choiceStream c 0) (dropChoice c) ∧
+      c₁.work (Fin.last k) = (c.work (Fin.last k)).move Dir3.right := by
+  refine ⟨(choiceTM tm).stepCfg c, TM.step_of_not_halted _ hhalt, ?_, ?_⟩
+  · refine Cfg.ext rfl rfl ?_ rfl
+    funext i
+    simp [TM.stepCfg, choiceTM, stepCfg, dropChoice, choiceStream, Tape.read]
+  · simp only [TM.stepCfg, choiceTM, Fin.snoc_last]
+    exact TM.writeAndMove_readBack _ hread Dir3.right
+
+/-- **A `T`-step run of `choiceTM` is the `T`-step trace of `tm` along the
+choice bits on the tape.** The run stops early exactly when the path halts;
+the choice tape is left untouched apart from its head, which advances one cell
+per step. -/
+theorem choiceTM_simulates (tm : NTM k) (T : ℕ) (c : Cfg (k + 1) tm.Q)
+    (hinv : (c.work (Fin.last k)).StartInvariant)
+    (hhead : 1 ≤ (c.work (Fin.last k)).head) :
+    ∃ (c' : Cfg (k + 1) tm.Q) (t : ℕ), t ≤ T ∧
+      (choiceTM tm).reachesIn t c c' ∧
+      (t < T → (choiceTM tm).halted c') ∧
+      dropChoice c' = tm.trace T (fun j => choiceStream c j.val) (dropChoice c) := by
+  induction T generalizing c with
+  | zero => exact ⟨c, 0, le_rfl, TM.reachesIn.zero, by omega, rfl⟩
+  | succ T ih =>
+    by_cases hhalt : c.state = tm.qhalt
+    · refine ⟨c, 0, Nat.zero_le _, TM.reachesIn.zero, fun _ => hhalt, ?_⟩
+      rw [NTM.trace]
+      simp [dropChoice, hhalt]
+    · have hread : (c.work (Fin.last k)).read ≠ Γ.start := hinv.read_ne_start hhead
+      obtain ⟨c₁, hstep, hdrop, hchoice⟩ := choiceTM_step tm c hhalt hread
+      have hinv₁ : (c₁.work (Fin.last k)).StartInvariant := by
+        rw [hchoice]
+        exact hinv
+      have hhead₁ : 1 ≤ (c₁.work (Fin.last k)).head := by
+        rw [hchoice]
+        show 1 ≤ (c.work (Fin.last k)).head + 1
+        omega
+      obtain ⟨c', t, hle, hreach, hstop, heq⟩ := ih c₁ hinv₁ hhead₁
+      refine ⟨c', t + 1, by omega, TM.reachesIn.step hstep hreach, fun _ => hstop (by omega), ?_⟩
+      rw [trace_succ_of_not_halted tm T _ (by simpa [dropChoice] using hhalt), ← hdrop]
+      rw [heq]
+      congr 1
+      funext j
+      have harg : ((c.work (Fin.last k)).move Dir3.right).head + j.val
+          = (c.work (Fin.last k)).head + (j.val + 1) := by
+        show (c.work (Fin.last k)).head + 1 + j.val = _
+        omega
+      show choiceStream c₁ j.val = choiceStream c (j.val + 1)
+      simp only [choiceStream, hchoice, harg]
+      rfl
+
+end NTM
+
+end Complexity
diff --git a/ROADMAP.md b/ROADMAP.md
index 439b509b..036881ed 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -1971,11 +1971,31 @@ randomness, interaction, and lower bounds.
 
 **Staged directions.**
 
-- [ ] Define the polynomial hierarchy both by alternating quantifiers and oracle
-  levels, then prove equivalence at fixed levels.
-- [~] Define `#P`, `GapP`, and parsimonious reductions using exact accepting-path
-  counts. *(`#P` = `SharpP` and `GapP` (with `GapP.neg_mem`) in
-  `Complexitylib.Classes.SharpP` done; parsimonious reductions remain.)*
+- [~] Define the polynomial hierarchy both by alternating quantifiers and oracle
+  levels, then prove equivalence at fixed levels. *(The certificate-quantifier
+  definition is `Complexitylib.Classes.PH`: `SigmaP`, `PiP`, `PH`, quantifier
+  duality, and the level inclusions relative to the `pairFst ∈ FP` seam. Oracle
+  levels and the equivalence remain.)*
+- [x] Prove the Sipser--Lautemann theorem `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ`
+  (`Complexitylib.Classes.PH.SipserLautemann`: `sipserLautemann`, with
+  `BPP_subset_SigmaP_two`, `BPP_subset_PiP_two` and `BPP_subset_PH`).
+  Unconditional. The development: Lautemann's covering lemma in both
+  directions (`SipserLautemann.Covering`); the freeze of acceptance
+  probability past the halting time, which replaces a machine's arbitrary time
+  bound by a dominating polynomial (`SipserLautemann.TimeBound`); the
+  amplified `∃∀` characterization of `L` and of its complement
+  (`SipserLautemann.Amplified`); the seed/shift codecs
+  (`SipserLautemann.Encode`); the identity exhibiting `L` and `Lᶜ` as
+  polynomially bounded `∃∀` forms over the matrix language
+  (`SipserLautemann.Matrix`); and the matrix verdict as a member of Cobham's
+  algebra (`SipserLautemann.Verdict`), which discharges the polynomial-time
+  obligation with no machine construction. Supporting additions:
+  `NTM.choiceTM` runs one nondeterministic path deterministically from a
+  choice tape (`Complexitylib.Models.TuringMachine.ChoiceTape`), simulated
+  inside the algebra by `Complexitylib.Classes.P.Cobham.Internal.ChoiceSim`
+  and `.BlockLoop`; `mem_P_of_decisionFn_bool`
+  (`Complexitylib.Classes.P.DecisionFn`) turns a verdict function in `FP` into
+  membership in `P`.
 - [ ] Prove elementary closure properties and relate PP to GapP sign.
 - [ ] Formalize `PH subset P^#P`/Toda-style results only after polynomial
   interpolation and modular counting are available.