diff --git a/Cslib/Computability/Languages/ComplexityClass.lean b/Cslib/Computability/Languages/ComplexityClass.lean
new file mode 100644
index 000000000..ae06b365b
--- /dev/null
+++ b/Cslib/Computability/Languages/ComplexityClass.lean
@@ -0,0 +1,445 @@
+
+import Cslib.Foundations.Data.BitstringEncoding
+-- import Cslib.Computability.Automata.Acceptor
+import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime
+
+/-!
+# Complexity Classes
+
+This file contains the definition of `ComplexityClass`es over bitstring decision problems.
+
+## Main Definitions
+
+We define
+
+- `BitstringDecisionProblem` as a type alias for `List Bool → Bool`,
+  the type of decision problems over bitstrings.
+- `ComplexityClass` as a type alias for `Set BitstringDecisionProblem`,
+  the type of complexity classes over bitstring decision problems.
+
+And from these we define the following complexity classes:
+
+- `P` as the set of decision problems decidable in polynomial time by a deterministic
+  Turing machine.
+- `∃ᴾ C`, the set of decision problems that can be decided using polynomially long
+  membership witnesses over `C`.
+- `∀ᴾ C`, the set of decision problems that can be decided using polynomially long
+  non-membership witnesses over `C`.
+- `NP` as `∃ᴾ P`, the set of decision problems decidable in polynomial time by a
+  nondeterministic Turing machine.
+- `coNP` as `∀ᴾ P`, the set of decision problems whose complements are in `NP`.
+- `Σᴾ n` and `Πᴾ n` as the `n`th levels of the polynomial time hierarchy, defined inductively as
+  `Σᴾ 0 = P`, `Σᴾ (n + 1) = ∃ᴾ (Πᴾ n)`, and `Πᴾ n = (Σᴾ n).complement`.
+- `PH` as the union of all levels of the polynomial time hierarchy.
+
+
+as well as several standard complexity classes such as P, NP, and the polynomial time hierarchy.
+
+## TODO
+
+- Define other complexity classes such as
+  - Easy
+    - BPP, RP, coRP, ZPP, Δ n
+  - PSPACE.
+
+- Make every complexity class have a long name under the `ComplexityClass` namespace,
+  as well as a short notation?
+
+- Prove basic inclusions between these classes.
+-/
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+
+/--
+The type of decision problems on bitstrings.
+
+We define these as functions from lists of booleans to booleans,
+implicitly assuming the usual encodings.
+
+TODO: An Decision Problem type over arbitrary types.
+-/
+abbrev BitstringDecisionProblem : Type := List Bool → Bool
+
+/--
+The list of all bitstrings of exactly length `n`, in lexicographic order.
+-/
+def bitstringsOfLength : ℕ → List (List Bool)
+  | 0     => [[]]
+  | n + 1 => (bitstringsOfLength n) >>= fun bs ↦ [bs ++ [false], bs ++ [true]]
+
+/--
+The list of all bitstrings of length `n` or less.
+
+Ordered first by length, then lexicographically.
+-/
+def bitstringsUpToLength (n : ℕ) : List (List Bool) :=
+  (List.range (n + 1)) >>= bitstringsOfLength
+
+@[simp]
+lemma bitstringsUpToLength_zero :
+    bitstringsUpToLength 0 = [[]] := by
+  rfl
+
+/--
+Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
+defines a new decision problem to determine, for an input string `x`,
+whether all strings `w` of length at most `p (|x|)` satisfy `L (x, w)`.
+
+Reference:
+- https://en.wikipedia.org/wiki/Polynomial_hierarchy#Quantified_Boolean_formulae_definition
+-/
+def BitstringDecisionProblem.universallyQuantifyOverPolynomial
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    BitstringDecisionProblem :=
+  fun x ↦
+    List.all (bitstringsUpToLength (p.eval x.length)) fun w ↦
+      L (BitstringEncoding.encode (α := Bitstring × Bitstring) (x, w))
+
+/--
+Given a polynomial `p` and a bitstring decision problem `L` that operates on pairs of bitstrings,
+defines a new decision problem to determine, for an input string `x`,
+whether there exists a string `w` of length at most `p (|x|)` such that `L (x, w)` holds.
+
+Reference:
+- https://en.wikipedia.org/wiki/Polynomial_hierarchy#Quantified_Boolean_formulae_definition
+-/
+def BitstringDecisionProblem.existentiallyQuantifyOverPolynomial
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    BitstringDecisionProblem :=
+  fun x ↦ List.any (bitstringsUpToLength (p.eval x.length)) fun w ↦
+    L (BitstringEncoding.encode (α := Bitstring × Bitstring) (x, w))
+
+@[simp]
+lemma BitstringDecisionProblem.universallyQuantifyOverPolynomial_complement
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    (L.universallyQuantifyOverPolynomial p)ᶜ =
+      (Lᶜ).existentiallyQuantifyOverPolynomial p := by
+  unfold universallyQuantifyOverPolynomial
+  unfold existentiallyQuantifyOverPolynomial
+  ext x
+  simp [List.not_any_eq_all_not] -- Add to push Bool.not
+
+@[simp]
+lemma BitstringDecisionProblem.existentiallyQuantifyOverPolynomial_complement
+    (p : Polynomial ℕ) (L : BitstringDecisionProblem) :
+    (L.existentiallyQuantifyOverPolynomial p)ᶜ =
+      (Lᶜ).universallyQuantifyOverPolynomial p := by
+  unfold universallyQuantifyOverPolynomial
+  unfold existentiallyQuantifyOverPolynomial
+  ext x
+  simp [List.not_all_eq_any_not] -- Add to push Bool.not
+
+
+
+/--
+The type of complexity classes over bitstrings.
+We define these as sets of `BitstringDecisionProblem`s.
+-/
+abbrev ComplexityClass : Type := Set BitstringDecisionProblem
+
+namespace ComplexityClass
+
+/--
+The class P is the set of decision problems
+decidable in polynomial time by a deterministic Turing machine.
+
+The input is treated as a raw bitstring (the identity encoding on `Bitstring`).
+-/
+def P : ComplexityClass :=
+  { L | IsComputableInPolyTime (α := Bitstring) L }
+
+/--
+The complement of a complexity class `C` is the set of decision problems
+whose complements are in `C`.
+
+Note that this is distinct from the complement of `C` as a set, which would be
+the set of decision problems not in `C`.
+-/
+def complement (C : ComplexityClass) : ComplexityClass :=
+  { L | (Lᶜ ∈ C) }
+
+@[simp]
+lemma complement_complement (C : ComplexityClass) :
+    C.complement.complement = C := by
+  ext L
+  simp [complement, Set.mem_setOf_eq, compl_compl]
+
+@[simp]
+lemma P_complement : P.complement = P := by
+  ext L
+  simp_rw [complement, P, Set.mem_setOf_eq, compl]
+  constructor
+  · intro h
+    rw [show (fun i => !L i) = Bool.not ∘ L by grind] at h
+    rw [show L = Bool.not ∘ (Bool.not ∘ L) by grind]
+    exact IsComputableInPolyTime.comp h (IsComputableInPolyTime.finite not)
+  · intro h
+    rw [show (fun i => !L i) = Bool.not ∘ L by grind]
+    exact IsComputableInPolyTime.comp h (IsComputableInPolyTime.finite not)
+
+def polyUniversallyQuantify (C : ComplexityClass) :
+    ComplexityClass :=
+  { BitstringDecisionProblem.universallyQuantifyOverPolynomial p L | (p : Polynomial ℕ) (L ∈ C) }
+
+notation "∀ᴾ " C => polyUniversallyQuantify C
+
+def polyExistentiallyQuantify (C : ComplexityClass) :
+    ComplexityClass :=
+  { BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L | (p : Polynomial ℕ) (L ∈ C) }
+
+notation "∃ᴾ " C => polyExistentiallyQuantify C
+
+/--
+The class NP is the set of decision problems
+such that there exists a polynomial `p` over ℕ and a poly-time Turing machine
+where for all `x`, `L x = true` iff there exists a `w` of length at most `p (|x|)`
+such that the Turing machine accepts the pair `(x,w)`.
+
+See Definition 2.1 in Arora-Barak (2009).
+-/
+def NP : ComplexityClass := ∃ᴾ P
+
+/--
+The class coNP is the set of decision problems
+whose complements are in NP.
+-/
+def coNP : ComplexityClass := ∀ᴾ P
+
+@[simp]
+lemma polyUniversallyQuantify_complement
+    (C : ComplexityClass) :
+    (∀ᴾ C).complement = ∃ᴾ (C.complement) := by
+  unfold complement polyExistentiallyQuantify polyUniversallyQuantify
+  ext L
+  simp only [Set.mem_setOf_eq]
+  refine exists_congr ?_
+  intro p
+  constructor
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L'ᶜ = Lᶜᶜ := by
+      rw [← h_eq]
+      simp only [BitstringDecisionProblem.universallyQuantifyOverPolynomial_complement]
+    use L'ᶜ
+    simp only [compl_compl] at *
+    exact And.symm ⟨h_eq, hL'⟩
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : BitstringDecisionProblem.universallyQuantifyOverPolynomial p L'ᶜ = Lᶜ := by
+      rw [← h_eq]
+      simp only [BitstringDecisionProblem.existentiallyQuantifyOverPolynomial_complement]
+    use L'ᶜ
+
+@[simp]
+lemma polyExistentiallyQuantify_complement
+    (C : ComplexityClass) :
+    (∃ᴾ C).complement = ∀ᴾ (C.complement) := by
+  unfold complement polyExistentiallyQuantify polyUniversallyQuantify
+  ext L
+  simp only [Set.mem_setOf_eq]
+  refine exists_congr ?_
+  intro p
+  constructor
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : BitstringDecisionProblem.universallyQuantifyOverPolynomial p L'ᶜ = Lᶜᶜ := by
+      rw [← h_eq]
+      simp only [BitstringDecisionProblem.existentiallyQuantifyOverPolynomial_complement]
+    use L'ᶜ
+    simp only [compl_compl] at *
+    exact And.symm ⟨h_eq, hL'⟩
+  · intro ⟨L', hL', h_eq⟩
+    replace h_eq : BitstringDecisionProblem.existentiallyQuantifyOverPolynomial p L'ᶜ = Lᶜ := by
+      rw [← h_eq]
+      simp only [BitstringDecisionProblem.universallyQuantifyOverPolynomial_complement]
+    use L'ᶜ
+
+lemma complement_mono
+    {C D : ComplexityClass} (h : C ⊆ D) :
+    C.complement ⊆ D.complement := by
+  unfold complement
+  simp only [Set.subset_def]
+  intro L hL
+  simp only [Set.mem_setOf_eq] at hL ⊢
+  exact h hL
+
+lemma complement_mono_iff
+    {C D : ComplexityClass} :
+    C ⊆ D ↔ C.complement ⊆ D.complement := by
+  constructor
+  · exact complement_mono
+  · intro h
+    have h' := complement_mono h
+    rw [complement_complement C, complement_complement D] at h'
+    exact h'
+
+lemma polyUniversallyQuantify_mono
+    {C D : ComplexityClass} (h : C ⊆ D) :
+    (∀ᴾ C) ⊆ (∀ᴾ D) := by
+  unfold polyUniversallyQuantify
+  simp only [Set.subset_def]
+  intro L hL
+  rcases hL with ⟨p, L', hL', h_eq⟩
+  exact ⟨p, L', h hL', h_eq⟩
+
+lemma polyExistentiallyQuantify_mono
+    {C D : ComplexityClass} (h : C ⊆ D) :
+    (∃ᴾ C) ⊆ (∃ᴾ D) := by
+  unfold polyExistentiallyQuantify
+  simp only [Set.subset_def]
+  intro L hL
+  rcases hL with ⟨p, L', hL', h_eq⟩
+  exact ⟨p, L', h hL', h_eq⟩
+
+def extract_statement (input : List Bool) : Option Bitstring :=
+  match BitstringEncoding.decode (α := Bitstring × Bitstring) input with
+    | none => none
+    | some (x', _) => some x'
+
+/--
+The bitstring decision problem that decodes the input as a pair of lists,
+then tests if the first list satisfies L.
+Returns false if decoding failure.
+-/
+def ignore_witness (L : BitstringDecisionProblem) : BitstringDecisionProblem :=
+  (fun x ↦ x |>.map (fun x' ↦ L x') |>.getD false) ∘ extract_statement
+
+lemma P_subset_NP : P ⊆ NP := by
+  unfold NP
+  unfold polyExistentiallyQuantify
+  simp_rw [P, Set.mem_setOf_eq]
+  intro L hL
+  use 0
+  simp_all only [Set.mem_setOf_eq]
+  use ignore_witness L
+  constructor
+  · simp only [ignore_witness]
+    apply IsComputableInPolyTime.comp
+    · -- `extract_statement = Option.map Prod.fst ∘ decode`
+      have h : extract_statement
+          = Option.map Prod.fst
+            ∘ (BitstringEncoding.decode : Bitstring → Option (Bitstring × Bitstring)) := by
+        funext input
+        change extract_statement input = Option.map Prod.fst (BitstringEncoding.decode input)
+        unfold extract_statement
+        cases BitstringEncoding.decode (α := Bitstring × Bitstring) input with
+        | none => rfl
+        | some p => rfl
+      rw [h]
+      exact IsComputableInPolyTime.comp IsComputableInPolyTime_decode
+        IsComputableInPolyTime_fst.optionMap
+    · exact IsComputableInPolyTime.comp hL.optionMap
+        (IsComputableInPolyTime.finite fun o : Option Bool => o.getD false)
+  · ext x
+    simp [BitstringDecisionProblem.existentiallyQuantifyOverPolynomial, ignore_witness,
+      extract_statement]
+    rfl
+
+
+
+lemma P_subset_coNP : P ⊆ coNP := by
+  unfold coNP
+  rw [complement_mono_iff]
+  simp only [P_complement, polyUniversallyQuantify_complement]
+  exact P_subset_NP
+
+/--
+The Sigma levels of the polynomial time hierarchy.
+
+Σᴾ 0 = P
+Σᴾ n+1 = ∃ᴾ (Σᴾ n).complement
+-/
+def SigmaPolyTimeHierarchy : ℕ → ComplexityClass
+  | 0     => P
+  | n + 1 => (SigmaPolyTimeHierarchy n).complement.polyExistentiallyQuantify
+
+/--
+The Pi levels of the polynomial time hierarchy, defined as the complement of the Sigma levels.
+
+Πᴾ n = (Σᴾ n).complement
+-/
+def PiPolyTimeHierarchy (n : ℕ) : ComplexityClass :=
+  (SigmaPolyTimeHierarchy n).complement
+
+-- TODO bind more tightly
+scoped notation "Σᴾ" => SigmaPolyTimeHierarchy
+scoped notation "Πᴾ" => PiPolyTimeHierarchy
+
+def PH : ComplexityClass :=
+  { L | ∃ n : ℕ, L ∈ Σᴾ n }
+
+@[simp]
+lemma SigmaPolyTimeHierarchy_zero : Σᴾ 0 = P := rfl
+
+@[simp]
+lemma PiPolyTimeHierarchy_zero : Πᴾ 0 = P.complement := rfl
+
+@[simp]
+lemma SigmaPolyTimeHierarchy_one : Σᴾ 1 = NP := by
+  simp [SigmaPolyTimeHierarchy, NP]
+
+@[simp]
+lemma PiPolyTimeHierarchy_one : Πᴾ 1 = coNP := by
+  simp [PiPolyTimeHierarchy, coNP, NP]
+
+lemma SigmaPolyTimeHierarchy_succ
+    (n : ℕ) : Σᴾ (n + 1) = ∃ᴾ (Πᴾ n) := by
+  simp only [SigmaPolyTimeHierarchy, PiPolyTimeHierarchy]
+
+lemma PiPolyTimeHierarchy_succ
+    (n : ℕ) : Πᴾ (n + 1) = ∀ᴾ (Σᴾ n) := by
+  simp only [PiPolyTimeHierarchy, SigmaPolyTimeHierarchy,
+    complement_complement,
+    polyExistentiallyQuantify_complement]
+
+@[simp]
+lemma PiPolyTimeHierarchy_complement
+    (n : ℕ) : (Πᴾ n).complement = Σᴾ n := by
+  simp [PiPolyTimeHierarchy, complement_complement]
+
+@[simp]
+lemma SigmaPolyTimeHierarchy_complement
+    (n : ℕ) : (Σᴾ n).complement = Πᴾ n := by
+  simp [PiPolyTimeHierarchy]
+
+private lemma PolyTimeHierarchy_subset_aux (n : ℕ) :
+    (Πᴾ n) ⊆ (Πᴾ (n + 1)) ∧ (Σᴾ n) ⊆ Σᴾ (n + 1) := by
+  induction n with
+  | zero =>
+    simp only [SigmaPolyTimeHierarchy_succ, PiPolyTimeHierarchy_succ]
+    simp only [PiPolyTimeHierarchy_zero, P_complement, SigmaPolyTimeHierarchy_zero]
+    constructor
+    · exact P_subset_coNP
+    · exact P_subset_NP
+  | succ n ih =>
+    simp only [SigmaPolyTimeHierarchy_succ, PiPolyTimeHierarchy_succ] at *
+    obtain ⟨ih_pi, ih_sigma⟩ := ih
+    constructor
+    · apply polyUniversallyQuantify_mono
+      exact ih_sigma
+    · apply polyExistentiallyQuantify_mono
+      exact ih_pi
+
+/--
+Pi n contained in Pi n+1
+-/
+lemma PiPolyTimeHierarchy_subset_PiPolyTimeHierarchy_succ
+    (n : ℕ) : (Πᴾ n) ⊆ Πᴾ (n + 1) := by
+  exact (PolyTimeHierarchy_subset_aux n).1
+
+/--
+Sigma n contained in Sigma n+1
+-/
+lemma SigmaPolyTimeHierarchy_subset_SigmaPolyTimeHierarchy_succ
+    (n : ℕ) : (Σᴾ n) ⊆ Σᴾ (n + 1) := by
+  exact (PolyTimeHierarchy_subset_aux n).2
+
+lemma PH_eq_union_sigma :
+  PH = ⋃ n : ℕ, Σᴾ n := by
+  ext L
+  simp [PH]
+
+end ComplexityClass
+
+end ComplexityTheory
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
index 79c4ae530..5c168a229 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
@@ -48,10 +48,12 @@ We define a number of structures related to Turing machine computation:
 * `TimeComputable f`: a TM for computing `f`, packaged with a bound on runtime.
 * `PolyTimeComputable f`: `TimeComputable f` packaged with a polynomial bound on runtime.
 
-We also provide ways of constructing polynomial-runtime TMs
+We also provide the `PolyTimeComputable.normalize` operation, which renormalizes a machine's time
+bound to the (automatically monotone) evaluation of its bounding polynomial.
 
-* `PolyTimeComputable.id`: computes the identity function
-* `PolyTimeComputable.comp`: computes the composition of polynomial time machines
+The concrete machine constructions witnessing computability of the identity and of composition
+(`idComputer`/`PolyTimeComputable.id`, `compComputer`/`PolyTimeComputable.comp`) live in the
+`PolyTime/Id` and `PolyTime/Comp` files of this directory.
 
 ## TODOs
 
@@ -219,164 +221,6 @@ lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' :
   grind [hevals.apply_le_apply_add (Cfg.spaceUsed tm)
       fun a b hstep ↦ Cfg.spaceUsed_step a b (Option.mem_def.mp hstep)]
 
-section Computers
-
-/-- A Turing machine computing the identity. -/
-def idComputer : SingleTapeTM Symbol where
-  State := PUnit
-  q₀ := PUnit.unit
-  tr _ b := ⟨⟨b, none⟩, none⟩
-
-/--
-A Turing machine computing the composition of two other Turing machines.
-
-If f and g are computed by Turing machines `tm1` and `tm2`
-then we can construct a Turing machine which computes g ∘ f by first running `tm1`
-and then, when `tm1` halts, transitioning to the start state of `tm2` and running `tm2`.
--/
-def compComputer (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol where
-  -- The states of the composed machine are the disjoint union of the states of the input machines.
-  State := tm1.State ⊕ tm2.State
-  -- The start state is the start state of the first input machine.
-  q₀ := .inl tm1.q₀
-  tr q h :=
-    match q with
-    -- If we are in the first input machine's states, run that machine ...
-    | .inl ql => match tm1.tr ql h with
-      | (stmt, state) =>
-        -- ... taking the same tape action as the first input machine would.
-        (stmt,
-          match state with
-          -- If it halts, transition to the start state of the second input machine
-          | none => some (.inr tm2.q₀)
-          -- Otherwise continue as normal
-          | _ => Option.map .inl state)
-    -- If we are in the second input machine's states, run that machine ...
-    | .inr qr =>
-      match tm2.tr qr h with
-      | (stmt, state) =>
-        -- ... taking the same tape action as the second input machine would.
-        (stmt,
-          match state with
-          -- If it halts, transition to the halting state
-          | none => none
-          -- Otherwise continue as normal
-          | _ => Option.map .inr state)
-
-section compComputerLemmas
-
-/-! ### Composition Computer Lemmas -/
-
-variable (tm1 tm2 : SingleTapeTM Symbol) (cfg1 : tm1.Cfg) (cfg2 : tm2.Cfg)
-
-lemma compComputer_q₀_eq : (compComputer tm1 tm2).q₀ = Sum.inl tm1.q₀ := rfl
-
-/--
-Convert a `Cfg` over the first input machine to a config over the composed machine.
-Note it may transition to the start state of the second machine if the first machine halts.
--/
-private def toCompCfg_left : (compComputer tm1 tm2).Cfg :=
-  match cfg1.state with
-  | some q => ⟨some (Sum.inl q), cfg1.BiTape⟩
-  | none => ⟨some (Sum.inr tm2.q₀), cfg1.BiTape⟩
-
-/-- Convert a `Cfg` over the second input machine to a config over the composed machine -/
-private def toCompCfg_right : (compComputer tm1 tm2).Cfg :=
-  ⟨Option.map Sum.inr cfg2.state, cfg2.BiTape⟩
-
-/-- The initial configuration for the composed machine, with the first machine starting. -/
-private def initialCfg (input : List Symbol) : (compComputer tm1 tm2).Cfg :=
-  ⟨some (Sum.inl tm1.q₀), BiTape.mk₁ input⟩
-
-/-- The intermediate configuration for the composed machine,
-after the first machine halts and the second machine starts. -/
-private def intermediateCfg (intermediate : List Symbol) : (compComputer tm1 tm2).Cfg :=
-  ⟨some (Sum.inr tm2.q₀), BiTape.mk₁ intermediate⟩
-
-/-- The final configuration for the composed machine, after the second machine halts. -/
-private def finalCfg (output : List Symbol) : (compComputer tm1 tm2).Cfg :=
-  ⟨none, BiTape.mk₁ output⟩
-
-/-- The left converting function commutes with steps of the machines. -/
-private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) :
-    Option.map (toCompCfg_left tm1 tm2) (tm1.step cfg1) =
-      (compComputer tm1 tm2).step (toCompCfg_left tm1 tm2 cfg1) := by
-  cases cfg1 with | mk state BiTape => cases state with
-    | none => grind
-    | some q =>
-      simp only [step, toCompCfg_left, compComputer]
-      generalize hM : tm1.tr q BiTape.head = result
-      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
-      #adaptation_note
-      /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-      cases nextState <;> (simp_all; rfl)
-
-/-- The right converting function commutes with steps of the machines. -/
-private theorem map_toCompCfg_right_step :
-    Option.map (toCompCfg_right tm1 tm2) (tm2.step cfg2) =
-      (compComputer tm1 tm2).step (toCompCfg_right tm1 tm2 cfg2) := by
-  cases cfg2 with
-  | mk state BiTape =>
-    cases state with
-    | none =>
-      simp only [step, toCompCfg_right, Option.map_none, compComputer]
-    | some q =>
-      generalize hM : tm2.tr q BiTape.head = result
-      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
-      simp only [compComputer]
-      grind [toCompCfg_right, step, compComputer]
-
-/--
-Simulation for the first phase of the composed computer.
-When the first machine runs from start to halt, the composed machine
-runs from start (with Sum.inl state) to Sum.inr tm2.q₀ (the start of the second phase).
-This takes the same number of steps because the halt transition becomes a transition to the
-second machine.
--/
-private theorem comp_left_relatesWithinSteps (input intermediate : List Symbol) (t : ℕ)
-    (htm1 :
-      RelatesWithinSteps tm1.TransitionRelation
-        (tm1.initCfg input)
-        (tm1.haltCfg intermediate)
-        t) :
-    RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation
-      (initialCfg tm1 tm2 input)
-      (intermediateCfg tm1 tm2 intermediate)
-      t := by
-  simp only [initialCfg, intermediateCfg, initCfg, haltCfg] at htm1 ⊢
-  refine RelatesWithinSteps.map (toCompCfg_left tm1 tm2) ?_ htm1
-  intro a b hab
-  have ha : a.state.isSome := by
-    simp only [TransitionRelation, step] at hab
-    cases a with | mk state _ => cases state <;> simp_all
-  have h1 := map_toCompCfg_left_step tm1 tm2 a ha
-  rw [hab, Option.map_some] at h1
-  exact h1.symm
-
-/--
-Simulation for the second phase of the composed computer.
-When the second machine runs from start to halt, the composed machine
-runs from Sum.inr tm2.q₀ to halt.
--/
-private theorem comp_right_relatesWithinSteps (intermediate output : List Symbol) (t : ℕ)
-    (htm2 :
-      RelatesWithinSteps tm2.TransitionRelation
-        (tm2.initCfg intermediate)
-        (tm2.haltCfg output)
-        t) :
-    RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation
-      (intermediateCfg tm1 tm2 intermediate)
-      (finalCfg tm1 tm2 output)
-      t := by
-  simp only [intermediateCfg, finalCfg, initCfg, haltCfg] at htm2 ⊢
-  refine RelatesWithinSteps.map (toCompCfg_right tm1 tm2) ?_ htm2
-  intro a b hab
-  grind [map_toCompCfg_right_step tm1 tm2 a]
-
-end compComputerLemmas
-
-end Computers
-
 /-!
 ## Time Computability
 
@@ -395,63 +239,6 @@ structure TimeComputable (f : List Symbol → List Symbol) where
   /-- proof this machine outputs `f` in at most `timeBound(input.length)` steps -/
   outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (timeBound a.length)
 
-
-/-- The identity map on Symbol is computable in constant time. -/
-def TimeComputable.id : TimeComputable (Symbol := Symbol) id where
-  tm := idComputer
-  timeBound _ := 1
-  outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩
-
-/--
-Time bounds for `compComputer`.
-
-The `compComputer` of two machines which have time bounds is bounded by
-
-* The time taken by the first machine on the input size
-* added to the time taken by the second machine on the output size of the first machine
-  (which is itself bounded by the time taken by the first machine)
-
-Note that we require the time function of the second machine to be monotone;
-this is to ensure that if the first machine returns an output
-which is shorter than the maximum possible length of output for that input size,
-then the time bound for the second machine still holds for that shorter input to the second machine.
--/
-def TimeComputable.comp {f g : List Symbol → List Symbol}
-    (hf : TimeComputable f) (hg : TimeComputable g)
-    (h_mono : Monotone hg.timeBound) :
-    (TimeComputable (g ∘ f)) where
-  tm := compComputer hf.tm hg.tm
-  -- perhaps it would be good to track the blow up separately?
-  timeBound l := (hf.timeBound l) + hg.timeBound (max 1 l + hf.timeBound l)
-  outputsFunInTime a := by
-    have hf_outputsFun := hf.outputsFunInTime a
-    have hg_outputsFun := hg.outputsFunInTime (f a)
-    simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply,
-      haltCfg] at hg_outputsFun hf_outputsFun ⊢
-    -- The computer reduces a to f a in time hf.timeBound a.length
-    have h_a_reducesTo_f_a :
-        RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
-          (initialCfg hf.tm hg.tm a)
-          (intermediateCfg hf.tm hg.tm (f a))
-          (hf.timeBound a.length) :=
-      comp_left_relatesWithinSteps hf.tm hg.tm a (f a)
-        (hf.timeBound a.length) hf_outputsFun
-    -- The computer reduces f a to g (f a) in time hg.timeBound (f a).length
-    have h_f_a_reducesTo_g_f_a :
-        RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
-          (intermediateCfg hf.tm hg.tm (f a))
-          (finalCfg hf.tm hg.tm (g (f a)))
-          (hg.timeBound (f a).length) :=
-      comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a))
-        (hg.timeBound (f a).length) hg_outputsFun
-    -- Therefore, the computer reduces a to g (f a) in the sum of those times.
-    have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
-    apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
-    refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
-    · apply h_mono
-      -- Use the lemma about output length being bounded by input length + time
-      exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a)
-
 end TimeComputable
 
 /-!
@@ -477,30 +264,500 @@ structure PolyTimeComputable (f : List Symbol → List Symbol) extends TimeCompu
   /-- proof that this machine outputs `f` in at most `time(input.length)` steps -/
   bounds : ∀ n, timeBound n ≤ poly.eval n
 
-/-- A proof that the identity map on Symbol is computable in polytime. -/
-noncomputable def PolyTimeComputable.id : PolyTimeComputable (Symbol := Symbol) id where
-  toTimeComputable := TimeComputable.id
-  poly := 1
-  bounds _ := by simp [TimeComputable.id]
+/-- Evaluation of a polynomial with natural-number coefficients is monotone in its argument. -/
+lemma monotone_poly_eval (p : Polynomial ℕ) : Monotone fun n => p.eval n := by
+  intro a b hab
+  induction p using Polynomial.induction_on' with
+  | add p q hp hq => simpa only [eval_add] using Nat.add_le_add hp hq
+  | monomial n c =>
+    simpa only [eval_monomial] using Nat.mul_le_mul le_rfl (Nat.pow_le_pow_left hab n)
+
+/-- Renormalize a polynomial-time machine so that its time bound is the (automatically monotone)
+evaluation of its bounding polynomial. This drops the monotonicity side-condition from `comp`. -/
+noncomputable def PolyTimeComputable.normalize {f : List Symbol → List Symbol}
+    (h : PolyTimeComputable f) : PolyTimeComputable f where
+  toTimeComputable :=
+    { tm := h.tm
+      timeBound := fun n => h.poly.eval n
+      outputsFunInTime := fun a =>
+        RelatesWithinSteps.of_le (h.outputsFunInTime a) (h.bounds a.length) }
+  poly := h.poly
+  bounds _ := le_rfl
+
+lemma PolyTimeComputable.monotone_normalize {f : List Symbol → List Symbol}
+    (h : PolyTimeComputable f) : Monotone h.normalize.timeBound :=
+  monotone_poly_eval h.poly
 
--- TODO remove `h_mono` assumption
--- by developing function to convert PolyTimeComputable into one with monotone time bound
-/--
-A proof that the composition of two polytime computable functions is polytime computable.
+end PolyTimeComputable
+
+/-!
+## Functions with finite domain of interest
+
+Given a target function `g : List Symbol → List Symbol` and a finite set `S` of "inputs of
+interest", we construct a `SingleTapeTM` computing a function that agrees with `g` on every
+element of `S` (and outputs `[]` elsewhere), and show it runs in linear (hence polynomial) time.
+
+The machine works in two phases:
+
+* **Read phase.** It scans the input left to right, erasing each symbol as it goes and tracking,
+  in its (finite) state, the prefix read so far — as long as that prefix is still a prefix of some
+  element of `S`; otherwise it enters a "dead" state. Writing a blank before every rightward move
+  keeps the left half of the tape normalized to the empty tape.
+* **Write phase.** On reaching the end of the input it knows exactly which element of `S` (if any)
+  was the input, hence which fixed output string to produce. It writes that string onto the (now
+  blank) tape in reverse, moving left after each symbol, landing exactly on the halting
+  configuration.
+
+Since the read phase takes `input.length` steps and the write phase is bounded by a constant
+(the longest possible output), the runtime is linear.
 -/
-noncomputable def PolyTimeComputable.comp {f g : List Symbol → List Symbol}
-    (hf : PolyTimeComputable f) (hg : PolyTimeComputable g)
-    (h_mono : Monotone hg.timeBound) :
-    PolyTimeComputable (g ∘ f) where
-  toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono
-  poly := hf.poly + hg.poly.comp (1 + X + hf.poly)
-  bounds n := by
-    simp only [TimeComputable.comp, eval_add, eval_comp, eval_X, eval_one]
-    apply add_le_add
-    · exact hf.bounds n
-    · exact (h_mono (add_le_add (by omega) (hf.bounds n))).trans (hg.bounds _)
 
-end PolyTimeComputable
+section FinsetDomain
+
+open Polynomial
+
+variable [DecidableEq Symbol]
+
+/-- The finite set of all prefixes of elements of `S`. -/
+def prefixesFinset (S : Finset (List Symbol)) : Finset (List Symbol) :=
+  S.biUnion fun s => s.inits.toFinset
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+@[simp]
+lemma mem_prefixesFinset {S : Finset (List Symbol)} {p : List Symbol} :
+    p ∈ prefixesFinset S ↔ ∃ s ∈ S, p <+: s := by
+  simp [prefixesFinset, List.mem_inits]
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma mem_prefixesFinset_self {S : Finset (List Symbol)} {s : List Symbol} (hs : s ∈ S) :
+    s ∈ prefixesFinset S :=
+  mem_prefixesFinset.2 ⟨s, hs, List.prefix_rfl⟩
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma prefixesFinset_closed {S : Finset (List Symbol)} {p : List Symbol} {a : Symbol}
+    (h : p ++ [a] ∈ prefixesFinset S) : p ∈ prefixesFinset S := by
+  rw [mem_prefixesFinset] at *
+  obtain ⟨s, hs, hp⟩ := h
+  exact ⟨s, hs, (List.prefix_append p [a]).trans hp⟩
+
+/-- The possible output strings: `g s` for `s ∈ S`, together with `[]`. -/
+def outputsFinset (g : List Symbol → List Symbol) (S : Finset (List Symbol)) :
+    Finset (List Symbol) :=
+  insert [] (S.image g)
+
+/-- The reachable "remaining to write" states: suffixes of the reverses of possible outputs. -/
+def writeStatesFinset (g : List Symbol → List Symbol) (S : Finset (List Symbol)) :
+    Finset (List Symbol) :=
+  (outputsFinset g S).biUnion fun c => c.reverse.tails.toFinset
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma mem_writeStatesFinset {g : List Symbol → List Symbol} {S : Finset (List Symbol)}
+    {w : List Symbol} :
+    w ∈ writeStatesFinset g S ↔ ∃ c ∈ outputsFinset g S, w <:+ c.reverse := by
+  simp [writeStatesFinset, List.mem_tails]
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma nil_mem_writeStatesFinset {g : List Symbol → List Symbol} {S : Finset (List Symbol)} :
+    ([] : List Symbol) ∈ writeStatesFinset g S :=
+  mem_writeStatesFinset.2 ⟨[], Finset.mem_insert_self _ _, List.nil_suffix⟩
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma writeStatesFinset_closed {g : List Symbol → List Symbol} {S : Finset (List Symbol)}
+    {a : Symbol} {w : List Symbol} (h : a :: w ∈ writeStatesFinset g S) :
+    w ∈ writeStatesFinset g S := by
+  rw [mem_writeStatesFinset] at *
+  obtain ⟨c, hc, hw⟩ := h
+  exact ⟨c, hc, (List.suffix_cons a w).trans hw⟩
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma reverse_output_mem_writeStatesFinset {g : List Symbol → List Symbol}
+    {S : Finset (List Symbol)} {input : List Symbol} :
+    (if input ∈ S then g input else ([] : List Symbol)).reverse ∈ writeStatesFinset g S := by
+  rw [mem_writeStatesFinset]
+  refine ⟨_, ?_, List.suffix_rfl⟩
+  unfold outputsFinset
+  split
+  · exact Finset.mem_insert_of_mem (Finset.mem_image_of_mem g ‹_›)
+  · exact Finset.mem_insert_self _ _
+
+/-- States of the lookup machine: either a read-phase state (an optional prefix, `none` being the
+"dead" state after diverging from every element of `S`), or a write-phase state (the reversed
+suffix of the output still to be written). -/
+abbrev LookupState (g : List Symbol → List Symbol) (S : Finset (List Symbol)) : Type :=
+  Option {p : List Symbol // p ∈ prefixesFinset S} ⊕ {w : List Symbol // w ∈ writeStatesFinset g S}
+
+variable (g : List Symbol → List Symbol) (S : Finset (List Symbol))
+
+/-- The read-phase state after having consumed prefix `p` of the input: the viable prefix `p`
+itself if it is still a prefix of some element of `S`, otherwise the dead state. -/
+def readState (p : List Symbol) : LookupState g S :=
+  Sum.inl (if h : p ∈ prefixesFinset S then some ⟨p, h⟩ else none)
+
+/-- The lookup machine for `g` and `S`. See the module docstring above for the construction. -/
+def lookupTM : SingleTapeTM Symbol where
+  State := LookupState g S
+  q₀ := readState g S []
+  tr q sym :=
+    match q with
+    | Sum.inl (some ⟨p, _⟩) =>
+      match sym with
+      | some a => (⟨none, some .right⟩, some (readState g S (p ++ [a])))
+      | none =>
+        (⟨none, none⟩,
+          some (Sum.inr ⟨(if p ∈ S then g p else []).reverse,
+            reverse_output_mem_writeStatesFinset⟩))
+    | Sum.inl none =>
+      match sym with
+      | some _ => (⟨none, some .right⟩, some (Sum.inl none))
+      | none => (⟨none, none⟩, some (Sum.inr ⟨[], nil_mem_writeStatesFinset⟩))
+    | Sum.inr ⟨w, hw⟩ =>
+      match w, hw with
+      | [], _ => (⟨none, none⟩, none)
+      | [a], _ => (⟨some a, none⟩, none)
+      | a :: b :: rest, hw =>
+        (⟨some a, some .left⟩, some (Sum.inr ⟨b :: rest, writeStatesFinset_closed hw⟩))
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+/-- Erasing the head of a nonempty tape and moving right yields the tape of the remaining input.
+This is the tape action performed on each step of the read phase; writing a blank before the move
+keeps the left half of the tape empty. -/
+private lemma mk₁_erase_moveRight (a : Symbol) (s : List Symbol) :
+    ((BiTape.mk₁ (a :: s)).write none).optionMove (some .right) = BiTape.mk₁ s := by
+  cases s <;> rfl
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+private lemma mk₁_cons_head (a : Symbol) (s : List Symbol) :
+    (BiTape.mk₁ (a :: s)).head = some a := rfl
+
+/-- The tape configuration during the write phase: blank head, empty left half, and the
+already-written suffix `r` of the output in the right half. -/
+private def writeTape (r : List Symbol) : BiTape Symbol := ⟨none, ∅, StackTape.mapSome r⟩
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+private lemma writeTape_nil : writeTape ([] : List Symbol) = (∅ : BiTape Symbol) := rfl
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+/-- Writing the final output symbol on the blank head (without moving) completes the output tape. -/
+private lemma writeTape_lastWrite (a : Symbol) (r : List Symbol) :
+    ((writeTape r).write (some a)).optionMove none = BiTape.mk₁ (a :: r) := rfl
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+/-- Writing a symbol on the blank head and moving left prepends it to the written suffix. -/
+private lemma writeTape_step (a : Symbol) (r : List Symbol) :
+    ((writeTape r).write (some a)).optionMove (some .left) = writeTape (a :: r) := rfl
+
+/-- A single step of the read phase: reading a symbol advances the tracked prefix and erases the
+symbol from the tape. -/
+private lemma readState_step (p : List Symbol) (a : Symbol) (s : List Symbol) :
+    (lookupTM g S).TransitionRelation
+      ⟨some (readState g S p), BiTape.mk₁ (a :: s)⟩
+      ⟨some (readState g S (p ++ [a])), BiTape.mk₁ s⟩ := by
+  simp only [TransitionRelation]
+  by_cases hp : p ∈ prefixesFinset S
+  · simp only [readState, dif_pos hp, SingleTapeTM.step, lookupTM, mk₁_cons_head,
+      mk₁_erase_moveRight]
+  · have hp' : p ++ [a] ∉ prefixesFinset S := fun h => hp (prefixesFinset_closed h)
+    simp only [readState, dif_neg hp, dif_neg hp', SingleTapeTM.step, lookupTM, mk₁_cons_head,
+      mk₁_erase_moveRight]
+
+/-- The full read phase: starting from a tracked prefix `p` and the input on the tape, the machine
+consumes the whole input (erasing it), advancing the prefix to `p ++ input`, in `input.length`
+steps. -/
+private lemma read_phase (input p : List Symbol) :
+    RelatesInSteps (lookupTM g S).TransitionRelation
+      ⟨some (readState g S p), BiTape.mk₁ input⟩
+      ⟨some (readState g S (p ++ input)), BiTape.mk₁ []⟩
+      input.length := by
+  induction input generalizing p with
+  | nil => simp only [List.append_nil, List.length_nil]; exact RelatesInSteps.refl _
+  | cons a rest ih =>
+    have hstep := readState_step g S p a rest
+    have hrest := ih (p ++ [a])
+    rw [List.append_assoc] at hrest
+    simp only [List.singleton_append] at hrest
+    exact RelatesInSteps.head _ _ _ _ hstep hrest
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+private lemma mk₁_nil_head : (BiTape.mk₁ ([] : List Symbol)).head = none := rfl
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+private lemma mk₁_nil_noop :
+    ((BiTape.mk₁ ([] : List Symbol)).write none).optionMove none = BiTape.mk₁ [] := rfl
+
+omit [Inhabited Symbol] [Fintype Symbol] [DecidableEq Symbol] in
+private lemma nil_noop : ((∅ : BiTape Symbol).write none).optionMove none = ∅ := rfl
+
+/-- The write-phase state entered on reaching the end of the input: it carries the reversed output
+string `(if input ∈ S then g input else []).reverse` still to be written. -/
+def writeStartState (input : List Symbol) : LookupState g S :=
+  Sum.inr ⟨(if input ∈ S then g input else []).reverse, reverse_output_mem_writeStatesFinset⟩
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+lemma writeStartState_of_not_mem (input : List Symbol) (h : input ∉ S) :
+    writeStartState g S input = Sum.inr ⟨[], nil_mem_writeStatesFinset⟩ := by
+  unfold writeStartState
+  congr 1
+  exact Subtype.ext (by simp [if_neg h])
+
+/-- The handoff step from the read phase to the write phase: on reaching the end of the input, the
+machine switches to the write-phase state without moving. -/
+private lemma handoff (input : List Symbol) :
+    (lookupTM g S).TransitionRelation
+      ⟨some (readState g S input), BiTape.mk₁ []⟩
+      ⟨some (writeStartState g S input), BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation]
+  by_cases hp : input ∈ prefixesFinset S
+  · simp only [readState, dif_pos hp, writeStartState, SingleTapeTM.step, lookupTM, mk₁_nil_head,
+      mk₁_nil_noop]
+  · have hs : input ∉ S := fun h => hp (mem_prefixesFinset_self h)
+    have hstep : (lookupTM g S).step ⟨some (readState g S input), BiTape.mk₁ []⟩
+        = some ⟨some (Sum.inr ⟨[], nil_mem_writeStatesFinset⟩), BiTape.mk₁ []⟩ := by
+      simp only [readState, dif_neg hp, SingleTapeTM.step, lookupTM, mk₁_nil_head, mk₁_nil_noop]
+    rw [hstep, writeStartState_of_not_mem g S input hs]
+
+/-- A single non-terminal step of the write phase: write the head symbol and move left, prepending
+it to the already-written output suffix. -/
+private lemma write_step (a b : Symbol) (rest r : List Symbol)
+    (hw : a :: b :: rest ∈ writeStatesFinset g S) :
+    (lookupTM g S).TransitionRelation
+      ⟨some (Sum.inr ⟨a :: b :: rest, hw⟩), writeTape r⟩
+      ⟨some (Sum.inr ⟨b :: rest, writeStatesFinset_closed hw⟩), writeTape (a :: r)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, lookupTM, writeTape_step]
+
+/-- The terminal step of the write phase: write the last (leftmost) output symbol and halt. -/
+private lemma write_step_last (a : Symbol) (r : List Symbol)
+    (hw : [a] ∈ writeStatesFinset g S) :
+    (lookupTM g S).TransitionRelation
+      ⟨some (Sum.inr ⟨[a], hw⟩), writeTape r⟩
+      ⟨none, BiTape.mk₁ (a :: r)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, lookupTM, writeTape_lastWrite]
+
+/-- The degenerate write phase for the empty output: halt immediately, leaving the tape blank. -/
+private lemma write_step_nil (hw : ([] : List Symbol) ∈ writeStatesFinset g S) :
+    (lookupTM g S).TransitionRelation
+      ⟨some (Sum.inr ⟨[], hw⟩), (∅ : BiTape Symbol)⟩
+      ⟨none, (∅ : BiTape Symbol)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, lookupTM, nil_noop]
+
+/-- The full write phase for a nonempty reversed output `w`: writes the output into the right half
+of the tape, landing on the halting configuration, in `w.length` steps. -/
+private lemma write_phase (w r : List Symbol) (hw : w ∈ writeStatesFinset g S) (hne : w ≠ []) :
+    RelatesInSteps (lookupTM g S).TransitionRelation
+      ⟨some (Sum.inr ⟨w, hw⟩), writeTape r⟩
+      ⟨none, BiTape.mk₁ (w.reverse ++ r)⟩
+      w.length := by
+  induction w generalizing r with
+  | nil => exact absurd rfl hne
+  | cons a tl ih =>
+    cases tl with
+    | nil => simpa using RelatesInSteps.single (write_step_last g S a r hw)
+    | cons b rest =>
+      have hstep := write_step g S a b rest r hw
+      have hrest := ih (a :: r) (writeStatesFinset_closed hw) (by simp)
+      rw [show (a :: b :: rest).reverse ++ r = (b :: rest).reverse ++ (a :: r) by simp]
+      exact RelatesInSteps.head _ _ _ _ hstep hrest
+
+/-- The complete write phase (from a blank tape): writes output `c` and halts, within `c.length + 1`
+steps. -/
+private lemma write_run (c : List Symbol) (hw : c.reverse ∈ writeStatesFinset g S) :
+    RelatesWithinSteps (lookupTM g S).TransitionRelation
+      ⟨some (Sum.inr ⟨c.reverse, hw⟩), (∅ : BiTape Symbol)⟩
+      ⟨none, BiTape.mk₁ c⟩
+      (c.length + 1) := by
+  cases c with
+  | nil => exact RelatesWithinSteps.single (write_step_nil g S hw)
+  | cons a tl =>
+    have hwp := write_phase g S (a :: tl).reverse [] hw (by simp)
+    rw [writeTape_nil, List.reverse_reverse, List.append_nil, List.length_reverse] at hwp
+    exact (RelatesWithinSteps.of_relatesInSteps hwp).of_le (Nat.le_succ _)
+
+/-- A uniform bound on the length of any output the machine can produce. -/
+def maxOutputLen (g : List Symbol → List Symbol) (S : Finset (List Symbol)) : ℕ :=
+  S.sup fun s => (g s).length
+
+open Polynomial in
+/-- The lookup machine runs in linear (hence polynomial) time and agrees with `g` on `S`:
+any function of the form `fun s => if s ∈ S then g s else []` is polynomial-time computable. -/
+noncomputable def PolyTimeComputable.ofFinsetDomain :
+    PolyTimeComputable (fun s => if s ∈ S then g s else []) where
+  tm := lookupTM g S
+  timeBound n := n + maxOutputLen g S + 2
+  poly := X + C (maxOutputLen g S + 2)
+  bounds n := by simp only [eval_add, eval_X, eval_C]; omega
+  outputsFunInTime a := by
+    simp only [OutputsWithinTime]
+    set c := (if a ∈ S then g a else []) with hc
+    have hc_len : c.length ≤ maxOutputLen g S := by
+      rw [hc]
+      unfold maxOutputLen
+      split
+      · exact Finset.le_sup (f := fun s => (g s).length) ‹a ∈ S›
+      · exact Nat.zero_le _
+    have hread := read_phase g S a []
+    rw [List.nil_append] at hread
+    have hchain :
+        RelatesWithinSteps (lookupTM g S).TransitionRelation
+          (initCfg (lookupTM g S) a)
+          (haltCfg (lookupTM g S) c)
+          (a.length + (1 + (c.length + 1))) :=
+      (RelatesWithinSteps.of_relatesInSteps hread).trans
+        ((RelatesWithinSteps.single (handoff g S a)).trans
+          (write_run g S c reverse_output_mem_writeStatesFinset))
+    exact hchain.of_le (by omega)
+
+end FinsetDomain
+
+/-!
+## Running a machine on the tail of the input
+
+Given a machine for `f`, we build a machine computing
+`fun input => match input with | [] => [] | b :: rest => b :: f rest`,
+i.e. one that preserves the leading symbol and applies `f` to the remaining input. This is the
+key ingredient for lifting polynomial-time computability along `Option.map` (the leading symbol
+being the `some`/`none` tag of the `Option` encoding).
+
+The machine erases the head (remembering it in its finite state), runs the underlying machine on
+the tail — the erased cell reads as blank, so the simulation is faithful — and finally re-inserts
+the remembered symbol to the left of the produced output.
+-/
+
+section OnTail
+
+open Polynomial
+
+/-- The function computed by `onTailComputer tm`: preserve the head symbol and apply the underlying
+function to the tail (the empty input maps to the empty output). -/
+def onTailFun (f : List Symbol → List Symbol) : List Symbol → List Symbol
+  | [] => []
+  | b :: rest => b :: f rest
+
+/-- A Turing machine that runs `tm` on the tail of the input while preserving the leading symbol.
+Its states are: a start state, the states of `tm` paired with the remembered leading symbol, and
+two finishing states (also carrying the remembered symbol). -/
+def onTailComputer (tm : SingleTapeTM Symbol) : SingleTapeTM Symbol where
+  State := Unit ⊕ (tm.State × Symbol) ⊕ Symbol ⊕ Symbol
+  q₀ := Sum.inl ()
+  tr q sym :=
+    match q with
+    | Sum.inl () =>
+      match sym with
+      -- empty input: halt immediately with empty output
+      | none => (⟨none, none⟩, none)
+      -- erase the head, remember it, and start the underlying machine
+      | some b => (⟨none, some .right⟩, some (Sum.inr (Sum.inl (tm.q₀, b))))
+    | Sum.inr (Sum.inl (q, b)) =>
+      match tm.tr q sym with
+      | (stmt, some q') => (stmt, some (Sum.inr (Sum.inl (q', b))))
+      -- underlying machine halts: move to the finishing phase
+      | (stmt, none) => (stmt, some (Sum.inr (Sum.inr (Sum.inl b))))
+    -- finish (read): write the head back unchanged and step left onto the blank cell
+    | Sum.inr (Sum.inr (Sum.inl b)) => (⟨sym, some .left⟩, some (Sum.inr (Sum.inr (Sum.inr b))))
+    -- finish (write): write the remembered symbol and halt
+    | Sum.inr (Sum.inr (Sum.inr b)) => (⟨some b, none⟩, none)
+
+omit [Inhabited Symbol] [Fintype Symbol] in
+/-- Writing the head symbol back unchanged and moving left turns `mk₁ out` into `writeTape out`,
+placing a blank under the head ready to receive the preserved symbol. -/
+private lemma mk₁_writeHead_moveLeft (out : List Symbol) :
+    ((BiTape.mk₁ out).write (BiTape.mk₁ out).head).optionMove (some .left) = writeTape out := by
+  cases out <;> rfl
+
+variable (tm : SingleTapeTM Symbol)
+
+/-- Embedding of a `tm`-configuration into an `onTailComputer tm`-configuration during the run
+phase, carrying the preserved leading symbol `b`. -/
+private def toRunCfg (b : Symbol) (cfg : tm.Cfg) : (onTailComputer tm).Cfg :=
+  match cfg.state with
+  | some q => ⟨some (Sum.inr (Sum.inl (q, b))), cfg.BiTape⟩
+  | none => ⟨some (Sum.inr (Sum.inr (Sum.inl b))), cfg.BiTape⟩
+
+/-- The embedding commutes with a step of the underlying machine. -/
+private theorem map_toRunCfg_step (b : Symbol) (cfg : tm.Cfg) (hcfg : cfg.state.isSome) :
+    Option.map (toRunCfg tm b) (tm.step cfg) = (onTailComputer tm).step (toRunCfg tm b cfg) := by
+  cases cfg with | mk state BiTape => cases state with
+    | none => simp at hcfg
+    | some q =>
+      simp only [step, toRunCfg, onTailComputer]
+      generalize hM : tm.tr q BiTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      cases nextState <;> (simp_all; rfl)
+
+/-- The run phase: while `tm` runs from its initial to its halting configuration, the composed
+machine runs from the (remembered-symbol) run state to the finishing state, in the same time. -/
+private theorem run_relatesWithinSteps (b : Symbol) (rest out : List Symbol) (t : ℕ)
+    (h : RelatesWithinSteps tm.TransitionRelation (tm.initCfg rest) (tm.haltCfg out) t) :
+    RelatesWithinSteps (onTailComputer tm).TransitionRelation
+      ⟨some (Sum.inr (Sum.inl (tm.q₀, b))), BiTape.mk₁ rest⟩
+      ⟨some (Sum.inr (Sum.inr (Sum.inl b))), BiTape.mk₁ out⟩
+      t := by
+  have hhom : ∀ x y : tm.Cfg, tm.TransitionRelation x y →
+      (onTailComputer tm).TransitionRelation (toRunCfg tm b x) (toRunCfg tm b y) := by
+    intro x y hxy
+    have hx : x.state.isSome := by
+      simp only [TransitionRelation, step] at hxy
+      cases x with | mk st _ => cases st <;> simp_all
+    have h1 := map_toRunCfg_step tm b x hx
+    rw [hxy, Option.map_some] at h1
+    exact h1.symm
+  have hmap := RelatesWithinSteps.map (toRunCfg tm b) hhom h
+  simpa only [toRunCfg, initCfg, haltCfg] using hmap
+
+/-- The start step on a nonempty input: erase and remember the head, positioning to run `tm`. -/
+private lemma onTail_start (b : Symbol) (rest : List Symbol) :
+    (onTailComputer tm).TransitionRelation
+      (initCfg (onTailComputer tm) (b :: rest))
+      ⟨some (Sum.inr (Sum.inl (tm.q₀, b))), BiTape.mk₁ rest⟩ := by
+  simp only [TransitionRelation, initCfg, onTailComputer, SingleTapeTM.step, mk₁_cons_head,
+    mk₁_erase_moveRight]
+
+/-- The start step on the empty input: halt immediately with empty output. -/
+private lemma onTail_start_nil :
+    (onTailComputer tm).TransitionRelation
+      (initCfg (onTailComputer tm) [])
+      (haltCfg (onTailComputer tm) []) := by
+  simp only [TransitionRelation, initCfg, haltCfg, onTailComputer, SingleTapeTM.step, mk₁_nil_head,
+    mk₁_nil_noop]
+
+/-- The first finishing step: rewrite the head and move left onto the blank cell. -/
+private lemma onTail_finishRead (b : Symbol) (out : List Symbol) :
+    (onTailComputer tm).TransitionRelation
+      ⟨some (Sum.inr (Sum.inr (Sum.inl b))), BiTape.mk₁ out⟩
+      ⟨some (Sum.inr (Sum.inr (Sum.inr b))), writeTape out⟩ := by
+  simp only [TransitionRelation, onTailComputer, SingleTapeTM.step, mk₁_writeHead_moveLeft]
+
+/-- The second finishing step: write the remembered symbol and halt, prepending it to the output. -/
+private lemma onTail_finishWrite (b : Symbol) (out : List Symbol) :
+    (onTailComputer tm).TransitionRelation
+      ⟨some (Sum.inr (Sum.inr (Sum.inr b))), writeTape out⟩
+      (haltCfg (onTailComputer tm) (b :: out)) := by
+  simp only [TransitionRelation, haltCfg, onTailComputer, SingleTapeTM.step, writeTape_lastWrite]
+
+/-- Running a polynomial-time machine on the tail of the input is polynomial-time. -/
+noncomputable def PolyTimeComputable.onTail {f : List Symbol → List Symbol}
+    (h : PolyTimeComputable f) : PolyTimeComputable (onTailFun f) where
+  tm := onTailComputer h.normalize.tm
+  timeBound n := h.normalize.timeBound n + 3
+  poly := h.normalize.poly + C 3
+  bounds n := by
+    simp only [eval_add, eval_C]
+    exact Nat.add_le_add_right (h.normalize.bounds n) 3
+  outputsFunInTime a := by
+    simp only [OutputsWithinTime]
+    cases a with
+    | nil =>
+      exact (RelatesWithinSteps.single (onTail_start_nil h.normalize.tm)).of_le (by omega)
+    | cons b rest =>
+      have hrun := run_relatesWithinSteps h.normalize.tm b rest (f rest) _
+        (h.normalize.outputsFunInTime rest)
+      have hchain := (RelatesWithinSteps.single (onTail_start h.normalize.tm b rest)).trans
+        (hrun.trans ((RelatesWithinSteps.single (onTail_finishRead h.normalize.tm b (f rest))).trans
+          (RelatesWithinSteps.single (onTail_finishWrite h.normalize.tm b (f rest)))))
+      refine hchain.of_le ?_
+      have hmono := h.monotone_normalize (Nat.le_succ rest.length)
+      simp only [List.length_cons, Nat.succ_eq_add_one] at *
+      omega
+
+end OnTail
 
 end SingleTapeTM
 
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime.lean
new file mode 100644
index 000000000..622b544ae
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Id
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Comp
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Basic
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TapeHelpers
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TakeFirstBlock
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.UndelimitBlock
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TagBlock
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Prod
+
+/-!
+# Polynomial-time computable functions between encoded types
+
+This is the aggregator for the `PolyTime` development: the predicate `IsComputableInPolyTime` on
+functions between `BitstringEncoding` types, its generic closure properties, and the concrete
+single-tape Turing machines witnessing computability of the operations on encoded pairs
+(`takeFirstBlock`, `undelimitBlock`, `tagBlock`) and the symmetric monoidal structure maps.
+-/
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Basic.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Basic.lean
new file mode 100644
index 000000000..daf633282
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Basic.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
+-/
+import Cslib.Foundations.Data.BitstringEncoding
+import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Id
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Comp
+
+/-!
+# Polynomial-time computable functions between encoded types
+
+This file abstracts the low-level `SingleTapeTM.PolyTimeComputable` predicate (about functions
+`List Bool → List Bool`) into `IsComputableInPolyTime`, a predicate on functions `f : α → β`
+between arbitrary types carrying a `BitstringEncoding`, and establishes the generic closure
+properties that do not require building a specific Turing machine.
+
+## Main results
+
+* `IsComputableInPolyTime.id`: the identity function is polynomial-time computable.
+* `IsComputableInPolyTime.comp`: closure under composition.
+* `IsComputableInPolyTime.finite`: any function out of a finite type is polynomial-time computable.
+* `IsComputableInPolyTime.optionMap`: `Option.map` preserves polynomial-time computability.
+
+The concrete machine constructions witnessing computability of specific operations on encoded
+pairs live in the sibling files of this directory (`TakeFirstBlock`, `UndelimitBlock`, `TagBlock`,
+`Prod`).
+-/
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+/--
+A simple definition to abstract the notion of a poly-time Turing machine into a predicate.
+-/
+def IsComputableInPolyTime {α β : Type} [BitstringEncoding α] [BitstringEncoding β]
+    (f : α → β) : Prop :=
+  ∃ f' : List Bool → List Bool,
+    Nonempty (Cslib.Turing.SingleTapeTM.PolyTimeComputable f') ∧
+    ∀ x, f' (BitstringEncoding.encode x) = BitstringEncoding.encode (f x)
+
+/-- The identity function is polynomial-time computable. -/
+lemma IsComputableInPolyTime.id {α : Type} [BitstringEncoding α] :
+    IsComputableInPolyTime (id : α → α) :=
+  ⟨_root_.id, ⟨Cslib.Turing.SingleTapeTM.PolyTimeComputable.id⟩, fun _ => rfl⟩
+
+lemma IsComputableInPolyTime.comp {α β γ : Type}
+    [BitstringEncoding α] [BitstringEncoding β] [BitstringEncoding γ]
+    {f : α → β} {g : β → γ}
+    (hf : IsComputableInPolyTime f) (hg : IsComputableInPolyTime g) :
+    IsComputableInPolyTime (g ∘ f) := by
+  rcases hf with ⟨f', ⟨hft, hfe⟩⟩
+  rcases hg with ⟨g', ⟨hgt, hge⟩⟩
+  use g' ∘ f'
+  constructor
+  · exact Nonempty.intro ((Classical.choice hft).comp' (Classical.choice hgt))
+  · intro x
+    simp only [Function.comp_apply, hfe, hge]
+
+/--
+A function with a finite domain is always computable in polynomial time, since we can just
+hardcode the output for each input.
+-/
+lemma IsComputableInPolyTime.finite {α β : Type}
+    [Finite α] [BitstringEncoding α] [BitstringEncoding β]
+    (f : α → β) : IsComputableInPolyTime f := by
+  -- We hardcode the output for each input into a lookup table: over the finite set of encodings
+  -- of `α`, the function `g` below decodes the input and re-encodes `f` of it. Any function with a
+  -- finite domain of interest is polynomial-time computable via `ofFinsetDomain`.
+  have : Fintype α := Fintype.ofFinite α
+  set S : Finset (List Bool) := Finset.univ.image (BitstringEncoding.encode : α → List Bool)
+    with hS
+  set g : List Bool → List Bool :=
+    fun s => (BitstringEncoding.decode s).elim [] fun x => BitstringEncoding.encode (f x) with hg
+  refine ⟨fun s => if s ∈ S then g s else [],
+    ⟨Cslib.Turing.SingleTapeTM.PolyTimeComputable.ofFinsetDomain g S⟩, ?_⟩
+  intro x
+  have hx : BitstringEncoding.encode x ∈ S := by
+    rw [hS]; exact Finset.mem_image_of_mem _ (Finset.mem_univ x)
+  simp only [hg, if_pos hx]
+  simp
+
+/--
+If `f` is polynomial-time computable, then so is `Option.map f`. The underlying machine preserves
+the leading `some`/`none` tag of the encoding and runs the machine for `f` on the payload.
+-/
+lemma IsComputableInPolyTime.optionMap {α β : Type} [BitstringEncoding α] [BitstringEncoding β]
+    {f : α → β} (hf : IsComputableInPolyTime f) :
+    IsComputableInPolyTime (Option.map f) := by
+  obtain ⟨f', ⟨hft, hfe⟩⟩ := hf
+  refine ⟨Cslib.Turing.SingleTapeTM.onTailFun f', ⟨(Classical.choice hft).onTail⟩, ?_⟩
+  intro o
+  cases o with
+  | none => rfl
+  | some a =>
+    change true :: f' (BitstringEncoding.encode a) = true :: BitstringEncoding.encode (f a)
+    rw [hfe a]
+
+end ComplexityTheory
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Comp.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Comp.lean
new file mode 100644
index 000000000..8735c392e
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Comp.lean
@@ -0,0 +1,263 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey, Pim Spelier, Daan van Gent
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+
+/-!
+# The composition machine
+
+The Turing machine `compComputer tm1 tm2` running `tm1` and then `tm2`, together with the witnesses
+that the composition of `TimeComputable`/`PolyTimeComputable` functions is again computable in the
+respective sense.
+
+* `TimeComputable.comp`, `PolyTimeComputable.comp`: composition with a monotonicity side-condition
+  on the second machine's time bound.
+* `PolyTimeComputable.comp'`: composition with no side-condition, obtained by first `normalize`-ing
+  the second machine (defined in `Deterministic`).
+-/
+
+@[expose] public section
+
+open Relation
+
+namespace Cslib.Turing
+
+open BiTape StackTape
+open _root_.Turing
+
+namespace SingleTapeTM
+
+variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol]
+
+/--
+A Turing machine computing the composition of two other Turing machines.
+
+If f and g are computed by Turing machines `tm1` and `tm2`
+then we can construct a Turing machine which computes g ∘ f by first running `tm1`
+and then, when `tm1` halts, transitioning to the start state of `tm2` and running `tm2`.
+-/
+def compComputer (tm1 tm2 : SingleTapeTM Symbol) : SingleTapeTM Symbol where
+  -- The states of the composed machine are the disjoint union of the states of the input machines.
+  State := tm1.State ⊕ tm2.State
+  -- The start state is the start state of the first input machine.
+  q₀ := .inl tm1.q₀
+  tr q h :=
+    match q with
+    -- If we are in the first input machine's states, run that machine ...
+    | .inl ql => match tm1.tr ql h with
+      | (stmt, state) =>
+        -- ... taking the same tape action as the first input machine would.
+        (stmt,
+          match state with
+          -- If it halts, transition to the start state of the second input machine
+          | none => some (.inr tm2.q₀)
+          -- Otherwise continue as normal
+          | _ => Option.map .inl state)
+    -- If we are in the second input machine's states, run that machine ...
+    | .inr qr =>
+      match tm2.tr qr h with
+      | (stmt, state) =>
+        -- ... taking the same tape action as the second input machine would.
+        (stmt,
+          match state with
+          -- If it halts, transition to the halting state
+          | none => none
+          -- Otherwise continue as normal
+          | _ => Option.map .inr state)
+
+section compComputerLemmas
+
+/-! ### Composition Computer Lemmas -/
+
+variable (tm1 tm2 : SingleTapeTM Symbol) (cfg1 : tm1.Cfg) (cfg2 : tm2.Cfg)
+
+lemma compComputer_q₀_eq : (compComputer tm1 tm2).q₀ = Sum.inl tm1.q₀ := rfl
+
+/--
+Convert a `Cfg` over the first input machine to a config over the composed machine.
+Note it may transition to the start state of the second machine if the first machine halts.
+-/
+private def toCompCfg_left : (compComputer tm1 tm2).Cfg :=
+  match cfg1.state with
+  | some q => ⟨some (Sum.inl q), cfg1.BiTape⟩
+  | none => ⟨some (Sum.inr tm2.q₀), cfg1.BiTape⟩
+
+/-- Convert a `Cfg` over the second input machine to a config over the composed machine -/
+private def toCompCfg_right : (compComputer tm1 tm2).Cfg :=
+  ⟨Option.map Sum.inr cfg2.state, cfg2.BiTape⟩
+
+/-- The initial configuration for the composed machine, with the first machine starting. -/
+private def initialCfg (input : List Symbol) : (compComputer tm1 tm2).Cfg :=
+  ⟨some (Sum.inl tm1.q₀), BiTape.mk₁ input⟩
+
+/-- The intermediate configuration for the composed machine,
+after the first machine halts and the second machine starts. -/
+private def intermediateCfg (intermediate : List Symbol) : (compComputer tm1 tm2).Cfg :=
+  ⟨some (Sum.inr tm2.q₀), BiTape.mk₁ intermediate⟩
+
+/-- The final configuration for the composed machine, after the second machine halts. -/
+private def finalCfg (output : List Symbol) : (compComputer tm1 tm2).Cfg :=
+  ⟨none, BiTape.mk₁ output⟩
+
+/-- The left converting function commutes with steps of the machines. -/
+private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) :
+    Option.map (toCompCfg_left tm1 tm2) (tm1.step cfg1) =
+      (compComputer tm1 tm2).step (toCompCfg_left tm1 tm2 cfg1) := by
+  cases cfg1 with | mk state BiTape => cases state with
+    | none => grind
+    | some q =>
+      simp only [step, toCompCfg_left, compComputer]
+      generalize hM : tm1.tr q BiTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      #adaptation_note
+      /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+      cases nextState <;> (simp_all; rfl)
+
+/-- The right converting function commutes with steps of the machines. -/
+private theorem map_toCompCfg_right_step :
+    Option.map (toCompCfg_right tm1 tm2) (tm2.step cfg2) =
+      (compComputer tm1 tm2).step (toCompCfg_right tm1 tm2 cfg2) := by
+  cases cfg2 with
+  | mk state BiTape =>
+    cases state with
+    | none =>
+      simp only [step, toCompCfg_right, Option.map_none, compComputer]
+    | some q =>
+      generalize hM : tm2.tr q BiTape.head = result
+      obtain ⟨⟨wr, dir⟩, nextState⟩ := result
+      simp only [compComputer]
+      grind [toCompCfg_right, step, compComputer]
+
+/--
+Simulation for the first phase of the composed computer.
+When the first machine runs from start to halt, the composed machine
+runs from start (with Sum.inl state) to Sum.inr tm2.q₀ (the start of the second phase).
+This takes the same number of steps because the halt transition becomes a transition to the
+second machine.
+-/
+private theorem comp_left_relatesWithinSteps (input intermediate : List Symbol) (t : ℕ)
+    (htm1 :
+      RelatesWithinSteps tm1.TransitionRelation
+        (tm1.initCfg input)
+        (tm1.haltCfg intermediate)
+        t) :
+    RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation
+      (initialCfg tm1 tm2 input)
+      (intermediateCfg tm1 tm2 intermediate)
+      t := by
+  simp only [initialCfg, intermediateCfg, initCfg, haltCfg] at htm1 ⊢
+  refine RelatesWithinSteps.map (toCompCfg_left tm1 tm2) ?_ htm1
+  intro a b hab
+  have ha : a.state.isSome := by
+    simp only [TransitionRelation, step] at hab
+    cases a with | mk state _ => cases state <;> simp_all
+  have h1 := map_toCompCfg_left_step tm1 tm2 a ha
+  rw [hab, Option.map_some] at h1
+  exact h1.symm
+
+/--
+Simulation for the second phase of the composed computer.
+When the second machine runs from start to halt, the composed machine
+runs from Sum.inr tm2.q₀ to halt.
+-/
+private theorem comp_right_relatesWithinSteps (intermediate output : List Symbol) (t : ℕ)
+    (htm2 :
+      RelatesWithinSteps tm2.TransitionRelation
+        (tm2.initCfg intermediate)
+        (tm2.haltCfg output)
+        t) :
+    RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation
+      (intermediateCfg tm1 tm2 intermediate)
+      (finalCfg tm1 tm2 output)
+      t := by
+  simp only [intermediateCfg, finalCfg, initCfg, haltCfg] at htm2 ⊢
+  refine RelatesWithinSteps.map (toCompCfg_right tm1 tm2) ?_ htm2
+  intro a b hab
+  grind [map_toCompCfg_right_step tm1 tm2 a]
+
+end compComputerLemmas
+
+/--
+Time bounds for `compComputer`.
+
+The `compComputer` of two machines which have time bounds is bounded by
+
+* The time taken by the first machine on the input size
+* added to the time taken by the second machine on the output size of the first machine
+  (which is itself bounded by the time taken by the first machine)
+
+Note that we require the time function of the second machine to be monotone;
+this is to ensure that if the first machine returns an output
+which is shorter than the maximum possible length of output for that input size,
+then the time bound for the second machine still holds for that shorter input to the second machine.
+-/
+def TimeComputable.comp {f g : List Symbol → List Symbol}
+    (hf : TimeComputable f) (hg : TimeComputable g)
+    (h_mono : Monotone hg.timeBound) :
+    (TimeComputable (g ∘ f)) where
+  tm := compComputer hf.tm hg.tm
+  -- perhaps it would be good to track the blow up separately?
+  timeBound l := (hf.timeBound l) + hg.timeBound (max 1 l + hf.timeBound l)
+  outputsFunInTime a := by
+    have hf_outputsFun := hf.outputsFunInTime a
+    have hg_outputsFun := hg.outputsFunInTime (f a)
+    simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply,
+      haltCfg] at hg_outputsFun hf_outputsFun ⊢
+    -- The computer reduces a to f a in time hf.timeBound a.length
+    have h_a_reducesTo_f_a :
+        RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
+          (initialCfg hf.tm hg.tm a)
+          (intermediateCfg hf.tm hg.tm (f a))
+          (hf.timeBound a.length) :=
+      comp_left_relatesWithinSteps hf.tm hg.tm a (f a)
+        (hf.timeBound a.length) hf_outputsFun
+    -- The computer reduces f a to g (f a) in time hg.timeBound (f a).length
+    have h_f_a_reducesTo_g_f_a :
+        RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation
+          (intermediateCfg hf.tm hg.tm (f a))
+          (finalCfg hf.tm hg.tm (g (f a)))
+          (hg.timeBound (f a).length) :=
+      comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a))
+        (hg.timeBound (f a).length) hg_outputsFun
+    -- Therefore, the computer reduces a to g (f a) in the sum of those times.
+    have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
+    apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
+    refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
+    · apply h_mono
+      -- Use the lemma about output length being bounded by input length + time
+      exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a)
+
+open Polynomial
+
+-- TODO remove `h_mono` assumption
+-- by developing function to convert PolyTimeComputable into one with monotone time bound
+/--
+A proof that the composition of two polytime computable functions is polytime computable.
+-/
+noncomputable def PolyTimeComputable.comp {f g : List Symbol → List Symbol}
+    (hf : PolyTimeComputable f) (hg : PolyTimeComputable g)
+    (h_mono : Monotone hg.timeBound) :
+    PolyTimeComputable (g ∘ f) where
+  toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono
+  poly := hf.poly + hg.poly.comp (1 + X + hf.poly)
+  bounds n := by
+    simp only [TimeComputable.comp, eval_add, eval_comp, eval_X, eval_one]
+    apply add_le_add
+    · exact hf.bounds n
+    · exact (h_mono (add_le_add (by omega) (hf.bounds n))).trans (hg.bounds _)
+
+/-- The composition of two polynomial-time computable functions is polynomial-time computable,
+with no monotonicity side-condition (unlike `comp`, which this specializes via `normalize`). -/
+noncomputable def PolyTimeComputable.comp' {f g : List Symbol → List Symbol}
+    (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) :
+    PolyTimeComputable (g ∘ f) :=
+  hf.comp hg.normalize hg.monotone_normalize
+
+end SingleTapeTM
+
+end Cslib.Turing
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Id.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Id.lean
new file mode 100644
index 000000000..2c76c8bec
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Id.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey, Pim Spelier, Daan van Gent
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+
+/-!
+# The identity machine
+
+The Turing machine `idComputer` computing the identity function, together with the witnesses that
+the identity is `TimeComputable` (in constant time) and `PolyTimeComputable`.
+-/
+
+@[expose] public section
+
+open Relation
+
+namespace Cslib.Turing
+
+open BiTape StackTape
+open _root_.Turing
+
+namespace SingleTapeTM
+
+variable {Symbol : Type} [Inhabited Symbol] [Fintype Symbol]
+
+/-- A Turing machine computing the identity. -/
+def idComputer : SingleTapeTM Symbol where
+  State := PUnit
+  q₀ := PUnit.unit
+  tr _ b := ⟨⟨b, none⟩, none⟩
+
+/-- The identity map on Symbol is computable in constant time. -/
+def TimeComputable.id : TimeComputable (Symbol := Symbol) id where
+  tm := idComputer
+  timeBound _ := 1
+  outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩
+
+/-- A proof that the identity map on Symbol is computable in polytime. -/
+noncomputable def PolyTimeComputable.id : PolyTimeComputable (Symbol := Symbol) id where
+  toTimeComputable := TimeComputable.id
+  poly := 1
+  bounds _ := by simp [TimeComputable.id]
+
+end SingleTapeTM
+
+end Cslib.Turing
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Prod.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Prod.lean
new file mode 100644
index 000000000..ac7388b03
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/Prod.lean
@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Basic
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TakeFirstBlock
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.UndelimitBlock
+
+/-!
+# Symmetric monoidal structure on encoded types
+
+Types carrying a `BitstringEncoding`, with polynomial-time computable functions as morphisms, form
+a symmetric monoidal category: the tensor product of objects is `α × β` (with the block-based pair
+encoding) and the tensor unit is `Unit` (encoded as the empty bitstring). Together with
+`IsComputableInPolyTime.id` and `IsComputableInPolyTime.comp`, this file states the remaining
+structure maps: the first projection, the tensor product of morphisms, the braiding, the
+associator, and the unitors.
+
+## Main results
+
+* `IsComputableInPolyTime_fst`: the first projection on encoded pairs is polynomial-time computable.
+* The `SymmetricMonoidal` section states the remaining structure maps; those whose machines are not
+  yet built are `sorry`ed.
+-/
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+open BitstringEncoding (undelimitBlock undelimitBlock_delimit)
+
+/-- The first projection on encoded pairs is polynomial-time computable, by composing
+`takeFirstBlock` (drop everything after the first block) and `undelimitBlock` (strip framing). -/
+lemma IsComputableInPolyTime_fst {α β : Type} [BitstringEncoding α] [BitstringEncoding β] :
+    IsComputableInPolyTime (Prod.fst : α × β → α) := by
+  obtain ⟨m1⟩ := PolyTimeComputable_takeFirstBlock
+  obtain ⟨m2⟩ := PolyTimeComputable_undelimitBlock
+  refine ⟨undelimitBlock ∘ takeFirstBlock, ⟨m1.comp' m2⟩, ?_⟩
+  rintro ⟨x, w⟩
+  change undelimitBlock (takeFirstBlock (BitstringEncoding.encode (x, w)))
+    = BitstringEncoding.encode x
+  have h : BitstringEncoding.encode (x, w)
+      = BitstringEncoding.delimit (BitstringEncoding.encode x) ++ BitstringEncoding.encode w := rfl
+  rw [h, takeFirstBlock_delimit_append, undelimitBlock_delimit]
+
+/-!
+### Symmetric monoidal structure
+
+Types carrying a `BitstringEncoding`, with polynomial-time computable functions as morphisms, form
+a symmetric monoidal category: the tensor product of objects is `α × β` (with the block-based pair
+encoding) and the tensor unit is `Unit` (encoded as the empty bitstring). Together with
+`IsComputableInPolyTime.id` and `IsComputableInPolyTime.comp` above, this section states the
+remaining operations: the tensor product of morphisms, the braiding, the associator, and the
+unitors, each with its inverse where the structure map is an isomorphism. The coherence laws hold
+on the nose, since they are equalities of the underlying functions.
+
+At the level of encodings, `encode (x, y) = delimit (encode x) ++ encode y` and `encode () = []`,
+so each structure map is a concrete rearrangement of self-delimiting blocks; the docstrings record
+the bitstring-level function the witnessing machine must compute.
+-/
+
+section SymmetricMonoidal
+
+variable {α β γ δ : Type}
+variable [BitstringEncoding α] [BitstringEncoding β] [BitstringEncoding γ] [BitstringEncoding δ]
+
+/-- Tensor product of morphisms: if `f` and `g` are polynomial-time computable, so is
+`Prod.map f g : α × β → γ × δ`. The underlying machine must run the machine for `f` on the payload
+of the leading self-delimiting block (re-delimiting its output) and the machine for `g` on the
+remainder of the input.
+
+TODO: construct the machine. -/
+lemma IsComputableInPolyTime.prodMap {f : α → γ} {g : β → δ}
+    (hf : IsComputableInPolyTime f) (hg : IsComputableInPolyTime g) :
+    IsComputableInPolyTime (Prod.map f g) := by
+  sorry
+
+/-- The braiding: swapping the components of a pair is polynomial-time computable. On encodings
+this exchanges the leading block with the trailing remainder, moving the framing:
+`delimit P ++ Q ↦ delimit Q ++ P`.
+
+TODO: construct the machine. -/
+lemma IsComputableInPolyTime_swap :
+    IsComputableInPolyTime (Prod.swap : α × β → β × α) := by
+  sorry
+
+/-- The associator: `((x, y), z) ↦ (x, (y, z))` is polynomial-time computable. On encodings this
+reframes `delimit (delimit P ++ Q) ++ R` as `delimit P ++ delimit Q ++ R`.
+
+TODO: construct the machine. -/
+lemma IsComputableInPolyTime_prodAssoc :
+    IsComputableInPolyTime (fun p : (α × β) × γ => (p.1.1, (p.1.2, p.2))) := by
+  sorry
+
+/-- The inverse associator: `(x, (y, z)) ↦ ((x, y), z)` is polynomial-time computable. On
+encodings this reframes `delimit P ++ delimit Q ++ R` as `delimit (delimit P ++ Q) ++ R`.
+
+TODO: construct the machine. -/
+lemma IsComputableInPolyTime_prodAssoc_symm :
+    IsComputableInPolyTime (fun p : α × (β × γ) => ((p.1, p.2.1), p.2.2)) := by
+  sorry
+
+/-- The left unitor: `((), x) ↦ x` is polynomial-time computable. Since `encode () = []`, on
+encodings this drops the leading `false` (the delimiter of the empty block):
+`false :: P ↦ P`.
+
+TODO: construct the machine (a leftward shift by one cell; alternatively derive this from a
+general `Prod.snd` lemma once a drop-first-block machine exists). -/
+lemma IsComputableInPolyTime_leftUnitor :
+    IsComputableInPolyTime (Prod.snd : Unit × α → α) := by
+  sorry
+
+/-- The inverse left unitor: `x ↦ ((), x)` is polynomial-time computable. On encodings this
+prepends `false`: `P ↦ false :: P`.
+
+TODO: construct the machine (a rightward shift by one cell, like the accepting branch of
+`tagBlockComputer`). -/
+lemma IsComputableInPolyTime_leftUnitor_inv :
+    IsComputableInPolyTime (fun x : α => ((), x)) := by
+  sorry
+
+/-- The right unitor: `(x, ()) ↦ x` is polynomial-time computable. Since `encode () = []`, the
+encoding of `(x, ())` is exactly `delimit (encode x)`, and this is the first projection, already
+witnessed by `takeFirstBlockComputer` and `undelimitBlockComputer`. -/
+lemma IsComputableInPolyTime_rightUnitor :
+    IsComputableInPolyTime (Prod.fst : α × Unit → α) :=
+  IsComputableInPolyTime_fst
+
+/-- The inverse right unitor: `x ↦ (x, ())` is polynomial-time computable. On encodings this is
+`delimit`: `P ↦ delimit P`.
+
+TODO: construct the machine (an expansion shuttle mirroring `undelimitBlockComputer`). -/
+lemma IsComputableInPolyTime_rightUnitor_inv :
+    IsComputableInPolyTime (fun x : α => (x, ())) := by
+  sorry
+
+end SymmetricMonoidal
+
+end ComplexityTheory
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TagBlock.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TagBlock.lean
new file mode 100644
index 000000000..633966cd1
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TagBlock.lean
@@ -0,0 +1,476 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.Basic
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TapeHelpers
+
+/-!
+# The `tagBlock` machine and decoding of encoded pairs
+
+Since `Bitstring` carries the identity encoding, `decode` for pairs of bitstrings sends `l` to
+`some (x, w)` exactly when `l` begins with a well-formed self-delimiting block. At the level of
+encodings this is the function `tagBlock`, which prepends `true` (the `some` tag) to well-formed
+inputs and erases ill-formed ones — a validating parser, computable in linear time by a single
+left-to-right scan followed by a shift-right-by-one (accept) or a leftward erase (reject).
+
+## Main results
+
+* `PolyTimeComputable_tagBlock`: `tagBlock` is computable in linear time by `tagBlockComputer`.
+* `IsComputableInPolyTime_decode`: decoding a bitstring as a pair of bitstrings is
+  polynomial-time computable.
+-/
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+section TagBlockMachine
+
+open Cslib.Turing Cslib.Turing.SingleTapeTM Cslib.Turing.StackTape
+
+/-- Does the bitstring begin with a well-formed self-delimiting block? -/
+def hasBlock : List Bool → Bool
+  | [] => false
+  | false :: _ => true
+  | true :: _ :: rest => hasBlock rest
+  | [true] => false
+
+/-- Tag a bitstring with a leading `true` if it begins with a well-formed self-delimiting block,
+and return the empty bitstring otherwise. On pair encodings this computes `encode ∘ decode`. -/
+def tagBlock (l : List Bool) : List Bool :=
+  bif hasBlock l then true :: l else []
+
+private lemma hasBlock_eq_isSome_undelimit : ∀ (n : ℕ) (l : List Bool), l.length = n →
+    hasBlock l = (BitstringEncoding.undelimit l).isSome := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro l hlen
+    match l with
+    | [] => rfl
+    | false :: rest => rfl
+    | true :: [] => rfl
+    | true :: b :: rest =>
+      have hrec := ih rest.length (by simp only [List.length_cons] at hlen; omega) rest rfl
+      simp only [hasBlock, BitstringEncoding.undelimit, hrec]
+      cases BitstringEncoding.undelimit rest <;> rfl
+
+private lemma undelimit_eq_some : ∀ (n : ℕ) (l : List Bool), l.length = n →
+    ∀ x w, BitstringEncoding.undelimit l = some (x, w) →
+      l = BitstringEncoding.delimit x ++ w := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro l hlen x w h
+    match l with
+    | [] => simp [BitstringEncoding.undelimit] at h
+    | false :: rest =>
+      simp only [BitstringEncoding.undelimit, Option.some.injEq, Prod.mk.injEq] at h
+      obtain ⟨rfl, rfl⟩ := h
+      rfl
+    | true :: [] => simp [BitstringEncoding.undelimit] at h
+    | true :: b :: rest =>
+      simp only [BitstringEncoding.undelimit, Option.map_eq_some_iff] at h
+      obtain ⟨⟨p₁, p₂⟩, hp, heq⟩ := h
+      have hrec := ih rest.length (by simp only [List.length_cons] at hlen; omega) rest rfl
+        p₁ p₂ hp
+      obtain ⟨rfl, rfl⟩ : b :: p₁ = x ∧ p₂ = w := by simpa [Prod.ext_iff] using heq
+      simp only [hrec, BitstringEncoding.delimit, List.cons_append]
+
+/-- States of the `tagBlock` machine. -/
+inductive TBState
+  /-- Parsing: expecting a pair marker `true` or the block terminator `false`. -/
+  | pTF
+  /-- Parsing: expecting the payload bit after a marker. -/
+  | pB
+  /-- Terminator seen (input valid): scan to the end of the input. -/
+  | pOk
+  /-- Accept phase: reading the rightmost unshifted cell. -/
+  | shRead
+  /-- Accept phase: writing the carried bit one cell to the right. -/
+  | shWrite (b : Bool)
+  /-- Accept phase: stepping back over the moving blank gap. -/
+  | shBack
+  /-- Accept phase: writing the leading `true` tag and halting. -/
+  | shTag
+  /-- Reject phase: erasing the input leftward. -/
+  | erL
+  deriving DecidableEq, Fintype
+
+/-- The validating parser: scan the input checking that it begins with a well-formed
+self-delimiting block; if so, shift the input one cell to the right (right to left, carrying one
+bit at a time) and write a leading `true`; otherwise erase the input. Computes `tagBlock` in
+linear time. -/
+def tagBlockComputer : SingleTapeTM Bool where
+  State := TBState
+  q₀ := .pTF
+  tr q sym :=
+    match q, sym with
+    -- parse phase
+    | .pTF, some true => (⟨some true, some .right⟩, some .pB)
+    | .pTF, some false => (⟨some false, some .right⟩, some .pOk)
+    | .pTF, none => (⟨none, some .left⟩, some .erL)          -- no terminator: reject
+    | .pB, some b => (⟨some b, some .right⟩, some .pTF)
+    | .pB, none => (⟨none, some .left⟩, some .erL)           -- lone marker: reject
+    | .pOk, some b => (⟨some b, some .right⟩, some .pOk)
+    | .pOk, none => (⟨none, some .left⟩, some .shRead)       -- accept: shift and tag
+    -- accept phase: shift the input right one cell, working right to left
+    | .shRead, some b => (⟨none, some .right⟩, some (.shWrite b))
+    | .shRead, none => (⟨none, some .right⟩, some .shTag)    -- everything shifted
+    | .shWrite b, _ => (⟨some b, some .left⟩, some .shBack)
+    | .shBack, _ => (⟨none, some .left⟩, some .shRead)
+    | .shTag, _ => (⟨some true, none⟩, none)
+    -- reject phase
+    | .erL, some _ => (⟨none, some .left⟩, some .erL)
+    | .erL, none => (⟨none, none⟩, none)
+
+/-! #### Parse phase -/
+
+private lemma tb_pTF_true (done rest : List Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pTF, splitTape done (true :: rest)⟩
+      ⟨some .pB, splitTape (done ++ [true]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma tb_pTF_false (done rest : List Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pTF, splitTape done (false :: rest)⟩
+      ⟨some .pOk, splitTape (done ++ [false]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma tb_pB_step (done : List Bool) (b : Bool) (rest : List Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pB, splitTape done (b :: rest)⟩
+      ⟨some .pTF, splitTape (done ++ [b]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma tb_pOk_step (done : List Bool) (b : Bool) (rest : List Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pOk, splitTape done (b :: rest)⟩
+      ⟨some .pOk, splitTape (done ++ [b]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+open Relation in
+private lemma tb_pOk_scan : ∀ (rest done : List Bool),
+    RelatesWithinSteps tagBlockComputer.TransitionRelation
+      ⟨some .pOk, splitTape done rest⟩ ⟨some .pOk, splitTape (done ++ rest) []⟩ rest.length := by
+  intro rest
+  induction rest with
+  | nil =>
+    intro done
+    rw [List.append_nil]
+    simp only [List.length_nil]
+    exact RelatesWithinSteps.refl _
+  | cons b r ih =>
+    intro done
+    have h1 := RelatesWithinSteps.single (tb_pOk_step done b r)
+    have h2 := ih (done ++ [b])
+    rw [show done ++ [b] ++ r = done ++ b :: r by simp] at h2
+    exact (h1.trans h2).of_le (by simp only [List.length_cons]; omega)
+
+open Relation in
+/-- The scan on inputs beginning with a well-formed block ends at the right end in `pOk`. -/
+private lemma tb_scan_accept : ∀ (n : ℕ) (rest done : List Bool), rest.length = n →
+    hasBlock rest = true →
+    RelatesWithinSteps tagBlockComputer.TransitionRelation
+      ⟨some .pTF, splitTape done rest⟩ ⟨some .pOk, splitTape (done ++ rest) []⟩ rest.length := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro rest done hlen hblock
+    match rest with
+    | [] => simp [hasBlock] at hblock
+    | false :: r =>
+      have h1 := RelatesWithinSteps.single (tb_pTF_false done r)
+      have h2 := tb_pOk_scan r (done ++ [false])
+      rw [show done ++ [false] ++ r = done ++ false :: r by simp] at h2
+      exact (h1.trans h2).of_le (by simp only [List.length_cons]; omega)
+    | true :: [] => simp [hasBlock] at hblock
+    | true :: b :: r =>
+      have h1 := RelatesWithinSteps.single (tb_pTF_true done (b :: r))
+      have h2 := RelatesWithinSteps.single (tb_pB_step (done ++ [true]) b r)
+      have h3 := ih r.length (by simp only [List.length_cons] at hlen; omega) r
+        (done ++ [true] ++ [b]) rfl (by simpa [hasBlock] using hblock)
+      rw [show done ++ [true] ++ [b] ++ r = done ++ true :: b :: r by simp] at h3
+      refine (h1.trans (h2.trans h3)).of_le ?_
+      simp only [List.length_cons]
+      omega
+
+/-! #### Accept phase: shift right by one and tag -/
+
+/-- Tape during the accept-phase shift: `done ++ [c]` is still unshifted (head on `c`), and
+`shifted` has been moved one cell to the right, separated by a single blank. -/
+private def shiftTape (done : List Bool) (c : Bool) (shifted : List Bool) : BiTape Bool :=
+  ⟨some c, StackTape.mapSome done.reverse, StackTape.cons none (StackTape.mapSome shifted)⟩
+
+private lemma tb_pOk_exit (l' : List Bool) (c : Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pOk, splitTape (l' ++ [c]) []⟩
+      ⟨some .shRead, shiftTape l' c []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape, shiftTape,
+    List.head?_nil, List.tail_nil, mapSome_nil, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
+    List.singleton_append, mapSome_head, mapSome_tail, List.head?_cons, List.tail_cons,
+    cons_none_empty]
+
+private lemma tb_shift_read (L : StackTape Bool) (c : Bool) (shifted : List Bool) :
+    tagBlockComputer.TransitionRelation
+      ⟨some .shRead, ⟨some c, L, StackTape.cons none (StackTape.mapSome shifted)⟩⟩
+      ⟨some (.shWrite c), ⟨none, StackTape.cons none L, StackTape.mapSome shifted⟩⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, StackTape.head_cons, StackTape.tail_cons]
+
+private lemma tb_shift_write (L : StackTape Bool) (c : Bool) (shifted : List Bool) :
+    tagBlockComputer.TransitionRelation
+      ⟨some (.shWrite c), ⟨none, StackTape.cons none L, StackTape.mapSome shifted⟩⟩
+      ⟨some .shBack, ⟨none, L, StackTape.mapSome (c :: shifted)⟩⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveLeft, StackTape.head_cons, StackTape.tail_cons,
+    cons_some_mapSome]
+
+private lemma tb_shift_back (D : List Bool) (c' : Bool) (rest : List Bool) :
+    tagBlockComputer.TransitionRelation
+      ⟨some .shBack, ⟨none, StackTape.mapSome (D ++ [c']).reverse, StackTape.mapSome rest⟩⟩
+      ⟨some .shRead, shiftTape D c' rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, shiftTape,
+    List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
+    List.singleton_append, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    mapSome_head, mapSome_tail, List.head?_cons, List.tail_cons]
+
+private lemma tb_shift_back_nil (rest : List Bool) :
+    tagBlockComputer.TransitionRelation
+      ⟨some .shBack, ⟨none, ∅, StackTape.mapSome rest⟩⟩
+      ⟨some .shRead, ⟨none, ∅, StackTape.cons none (StackTape.mapSome rest)⟩⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveLeft, empty_head, empty_tail]
+
+private lemma tb_shift_read_nil (rest : List Bool) :
+    tagBlockComputer.TransitionRelation
+      ⟨some .shRead, ⟨none, ∅, StackTape.cons none (StackTape.mapSome rest)⟩⟩
+      ⟨some .shTag, ⟨none, ∅, StackTape.mapSome rest⟩⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, StackTape.head_cons, StackTape.tail_cons,
+    cons_none_empty]
+
+private lemma tb_shift_tag (rest : List Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .shTag, ⟨none, ∅, StackTape.mapSome rest⟩⟩
+      ⟨none, BiTape.mk₁ (true :: rest)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, BiTape.mk₁, BiTape.write,
+    BiTape.optionMove]
+
+open Relation in
+/-- The full shift-and-tag: from the rightmost cell, halt on `true :: input`. -/
+private lemma tb_shift : ∀ (done : List Bool) (c : Bool) (shifted : List Bool),
+    RelatesWithinSteps tagBlockComputer.TransitionRelation
+      ⟨some .shRead, shiftTape done c shifted⟩
+      ⟨none, BiTape.mk₁ (true :: (done ++ c :: shifted))⟩ (3 * done.length + 5) := by
+  intro done
+  induction done using List.reverseRecOn with
+  | nil =>
+    intro c shifted
+    simp only [shiftTape, List.reverse_nil, mapSome_nil, List.nil_append, List.length_nil,
+      Nat.mul_zero, Nat.zero_add]
+    have h1 := RelatesWithinSteps.single (tb_shift_read ∅ c shifted)
+    have h2 := RelatesWithinSteps.single (tb_shift_write ∅ c shifted)
+    have h3 := RelatesWithinSteps.single (tb_shift_back_nil (c :: shifted))
+    have h4 := RelatesWithinSteps.single (tb_shift_read_nil (c :: shifted))
+    have h5 := RelatesWithinSteps.single (tb_shift_tag (c :: shifted))
+    exact (h1.trans (h2.trans (h3.trans (h4.trans h5)))).of_le (by omega)
+  | append_singleton D d ih =>
+    intro c shifted
+    have h1 := RelatesWithinSteps.single
+      (tb_shift_read (StackTape.mapSome (D ++ [d]).reverse) c shifted)
+    have h2 := RelatesWithinSteps.single
+      (tb_shift_write (StackTape.mapSome (D ++ [d]).reverse) c shifted)
+    have h3 := RelatesWithinSteps.single (tb_shift_back D d (c :: shifted))
+    have h4 := ih d (c :: shifted)
+    rw [show D ++ d :: c :: shifted = (D ++ [d]) ++ c :: shifted by simp] at h4
+    have hchain := h1.trans (h2.trans (h3.trans h4))
+    refine hchain.of_le ?_
+    simp only [List.length_append, List.length_cons, List.length_nil]
+    omega
+
+/-! #### Reject phase: erase the input -/
+
+private lemma tb_pTF_reject (D : List Bool) (c : Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pTF, splitTape (D ++ [c]) []⟩
+      ⟨some .erL, splitTape D [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape, List.head?_nil,
+    List.tail_nil, List.head?_cons, List.tail_cons, mapSome_nil, BiTape.write, BiTape.optionMove,
+    BiTape.move, BiTape.moveLeft, List.reverse_append, List.reverse_cons, List.reverse_nil,
+    List.nil_append, List.singleton_append, mapSome_head, mapSome_tail, cons_none_empty]
+
+private lemma tb_pB_reject (D : List Bool) (c : Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .pB, splitTape (D ++ [c]) []⟩
+      ⟨some .erL, splitTape D [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape, List.head?_nil,
+    List.tail_nil, List.head?_cons, List.tail_cons, mapSome_nil, BiTape.write, BiTape.optionMove,
+    BiTape.move, BiTape.moveLeft, List.reverse_append, List.reverse_cons, List.reverse_nil,
+    List.nil_append, List.singleton_append, mapSome_head, mapSome_tail, cons_none_empty]
+
+private lemma tb_pTF_reject_nil :
+    tagBlockComputer.TransitionRelation ⟨some .pTF, splitTape [] []⟩
+      ⟨some .erL, BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape, List.head?_nil,
+    List.tail_nil, List.reverse_nil, mapSome_nil, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, empty_head, empty_tail, cons_none_empty, BiTape.mk₁, BiTape.empty_eq_nil,
+    BiTape.nil]
+
+private lemma tb_erL_step (D : List Bool) (c' c : Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .erL, splitTape (D ++ [c']) [c]⟩
+      ⟨some .erL, splitTape D [c']⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape, List.head?_cons,
+    List.tail_cons, mapSome_nil, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
+    List.singleton_append, mapSome_head, mapSome_tail, cons_none_empty]
+
+private lemma tb_erL_last (c : Bool) :
+    tagBlockComputer.TransitionRelation ⟨some .erL, splitTape [] [c]⟩
+      ⟨some .erL, BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, splitTape, List.head?_cons,
+    List.tail_cons, mapSome_nil, List.reverse_nil, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, empty_head, empty_tail, cons_none_empty, BiTape.mk₁, BiTape.empty_eq_nil,
+    BiTape.nil]
+
+private lemma tb_erL_halt :
+    tagBlockComputer.TransitionRelation ⟨some .erL, BiTape.mk₁ []⟩ ⟨none, BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, tagBlockComputer, BiTape.mk₁, BiTape.write,
+    BiTape.optionMove, BiTape.empty_eq_nil, BiTape.nil]
+
+open Relation in
+private lemma tb_erase : ∀ (D : List Bool) (c : Bool),
+    RelatesWithinSteps tagBlockComputer.TransitionRelation
+      ⟨some .erL, splitTape D [c]⟩ ⟨none, BiTape.mk₁ []⟩ (D.length + 2) := by
+  intro D
+  induction D using List.reverseRecOn with
+  | nil =>
+    intro c
+    exact ((RelatesWithinSteps.single (tb_erL_last c)).trans
+      (RelatesWithinSteps.single tb_erL_halt)).of_le (by simp)
+  | append_singleton D' c' ih =>
+    intro c
+    have hchain := (RelatesWithinSteps.single (tb_erL_step D' c' c)).trans (ih c')
+    refine hchain.of_le ?_
+    simp only [List.length_append, List.length_cons, List.length_nil]
+    omega
+
+open Relation in
+/-- The scan on inputs not beginning with a well-formed block ends by erasing everything. -/
+private lemma tb_scan_reject : ∀ (n : ℕ) (rest done : List Bool), rest.length = n →
+    hasBlock rest = false →
+    RelatesWithinSteps tagBlockComputer.TransitionRelation
+      ⟨some .pTF, splitTape done rest⟩ ⟨none, BiTape.mk₁ []⟩
+      (2 * rest.length + done.length + 4) := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro rest done hlen hblock
+    match rest with
+    | [] =>
+      rcases List.eq_nil_or_concat done with rfl | ⟨D, c, rfl⟩
+      · exact ((RelatesWithinSteps.single tb_pTF_reject_nil).trans
+          (RelatesWithinSteps.single tb_erL_halt)).of_le (by simp)
+      · rw [List.concat_eq_append]
+        have hchain := (RelatesWithinSteps.single (tb_pTF_reject D c)).trans (tb_erase D c)
+        refine hchain.of_le ?_
+        simp only [List.length_nil, List.length_append, List.length_cons]
+        omega
+    | false :: r => simp [hasBlock] at hblock
+    | true :: [] =>
+      have h1 := RelatesWithinSteps.single (tb_pTF_true done [])
+      have h2 := RelatesWithinSteps.single (tb_pB_reject done true)
+      have h3 := tb_erase done true
+      refine (h1.trans (h2.trans h3)).of_le ?_
+      simp only [List.length_cons, List.length_nil]
+      omega
+    | true :: b :: r =>
+      have h1 := RelatesWithinSteps.single (tb_pTF_true done (b :: r))
+      have h2 := RelatesWithinSteps.single (tb_pB_step (done ++ [true]) b r)
+      have h3 := ih r.length (by simp only [List.length_cons] at hlen; omega) r
+        (done ++ [true] ++ [b]) rfl (by simpa [hasBlock] using hblock)
+      refine (h1.trans (h2.trans h3)).of_le ?_
+      simp only [List.length_cons, List.length_append, List.length_nil]
+      omega
+
+open Relation Polynomial in
+/-- `tagBlock` is computable in linear time by `tagBlockComputer`. -/
+theorem PolyTimeComputable_tagBlock :
+    Nonempty (Cslib.Turing.SingleTapeTM.PolyTimeComputable tagBlock) :=
+  ⟨{ tm := tagBlockComputer
+     timeBound := fun n => 4 * n + 4
+     poly := C 4 * X + C 4
+     bounds := fun n => by simp only [eval_add, eval_mul, eval_C, eval_X]; omega
+     outputsFunInTime := fun a => by
+       simp only [OutputsWithinTime, initCfg, haltCfg]
+       cases hb : hasBlock a with
+       | false =>
+         have h := tb_scan_reject a.length a [] rfl hb
+         rw [splitTape_nil_left] at h
+         rw [show tagBlock a = [] by simp [tagBlock, hb]]
+         refine h.of_le ?_
+         simp only [List.length_nil]
+         omega
+       | true =>
+         have hne : a ≠ [] := by rintro rfl; simp [hasBlock] at hb
+         obtain ⟨l', c, rfl⟩ := (List.eq_nil_or_concat a).resolve_left hne
+         rw [List.concat_eq_append] at hb ⊢
+         have h1 := tb_scan_accept (l' ++ [c]).length (l' ++ [c]) [] rfl hb
+         rw [splitTape_nil_left, List.nil_append] at h1
+         have h2 := RelatesWithinSteps.single (tb_pOk_exit l' c)
+         have h3 := tb_shift l' c []
+         rw [show tagBlock (l' ++ [c]) = true :: (l' ++ [c]) by simp [tagBlock, hb]]
+         refine (h1.trans (h2.trans h3)).of_le ?_
+         simp only [List.length_append, List.length_cons, List.length_nil]
+         omega } ⟩
+
+private lemma encode_option_none :
+    BitstringEncoding.encode (none : Option (Bitstring × Bitstring)) = ([] : List Bool) := rfl
+
+private lemma encode_option_some (x w : List Bool) :
+    BitstringEncoding.encode (some (Bitstring.ofList x, Bitstring.ofList w))
+      = true :: (BitstringEncoding.delimit x ++ w) := rfl
+
+/-- The `tagBlock` function computes `encode ∘ decode` for pairs of bitstrings, at the level of
+raw `List Bool` inputs. -/
+private lemma tagBlock_eq_encode_decodePair (l : List Bool) :
+    tagBlock l
+      = BitstringEncoding.encode
+          (BitstringEncoding.decodePair (α := Bitstring) (β := Bitstring) l) := by
+  cases h : BitstringEncoding.undelimit l with
+  | none =>
+    have hd : BitstringEncoding.decodePair (α := Bitstring) (β := Bitstring) l = none := by
+      simp [BitstringEncoding.decodePair, h]
+    have hb : hasBlock l = false := by
+      rw [hasBlock_eq_isSome_undelimit l.length l rfl, h]; rfl
+    rw [hd, encode_option_none]
+    simp [tagBlock, hb]
+  | some p =>
+    obtain ⟨x, w⟩ := p
+    have hd : BitstringEncoding.decodePair (α := Bitstring) (β := Bitstring) l
+        = some (Bitstring.ofList x, Bitstring.ofList w) := by
+      simp [BitstringEncoding.decodePair, h, BitstringEncoding.decode_bitstring]
+    have hb : hasBlock l = true := by
+      rw [hasBlock_eq_isSome_undelimit l.length l rfl, h]; rfl
+    have hl : l = BitstringEncoding.delimit x ++ w :=
+      undelimit_eq_some l.length l rfl x w h
+    rw [hd, encode_option_some, ← hl]
+    simp [tagBlock, hb]
+
+end TagBlockMachine
+
+/-- Decoding a bitstring as a pair of bitstrings is polynomial-time computable: the machine
+validates that the input begins with a well-formed self-delimiting block, tagging it with a
+leading `true` (the `some` tag) if so and erasing it otherwise. -/
+lemma IsComputableInPolyTime_decode :
+    IsComputableInPolyTime (α := Bitstring)
+      (BitstringEncoding.decode (α := Bitstring × Bitstring)) := by
+  obtain ⟨m⟩ := PolyTimeComputable_tagBlock
+  refine ⟨tagBlock, ⟨m⟩, fun l =>
+    (tagBlock_eq_encode_decodePair (BitstringEncoding.encode l)).trans ?_⟩
+  -- `decodePair (encode l)` and `decode l` agree definitionally: `encode` on a `Bitstring` is
+  -- the identity and `decode` on pairs is `decodePair`.
+  rfl
+
+
+end ComplexityTheory
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TakeFirstBlock.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TakeFirstBlock.lean
new file mode 100644
index 000000000..72562740c
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TakeFirstBlock.lean
@@ -0,0 +1,389 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Cslib.Foundations.Data.BitstringEncoding
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TapeHelpers
+
+/-!
+# The `takeFirstBlock` machine
+
+`takeFirstBlock` keeps the leading self-delimiting block of a bitstring, dropping everything after
+it: on a pair encoding `delimit (encode x) ++ encode w` it returns `delimit (encode x)`. On a tape
+this is a scan to the end of the first block followed by erasing the suffix — no compaction, since
+the kept prefix stays in place.
+
+The main result is `PolyTimeComputable_takeFirstBlock`, witnessed by `takeFirstBlockComputer`.
+-/
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+open Cslib.Turing Cslib.Turing.SingleTapeTM Cslib.Turing.StackTape
+
+/-- Keep the leading self-delimiting block of a bitstring, dropping everything after it. On a pair
+encoding `delimit (encode x) ++ encode w` this returns `delimit (encode x)`. -/
+def takeFirstBlock : List Bool → List Bool
+  | [] => []
+  | false :: _ => [false]
+  | true :: b :: rest => true :: b :: takeFirstBlock rest
+  | [true] => [true]
+
+@[simp]
+lemma takeFirstBlock_delimit_append (P Q : List Bool) :
+    takeFirstBlock (BitstringEncoding.delimit P ++ Q) = BitstringEncoding.delimit P := by
+  induction P with
+  | nil => rfl
+  | cons b P ih => simp only [BitstringEncoding.delimit, List.cons_append, takeFirstBlock, ih]
+
+/-- States of the `takeFirstBlock` machine. -/
+inductive TFBState
+  /-- Initial state (needed to distinguish empty input, which halts, from a full-input block). -/
+  | scanStart
+  /-- Scanning, expecting `true`/`false` at the start of a block cell pair. -/
+  | scanTF
+  /-- Scanning, expecting the payload bit after a `true`. -/
+  | scanB
+  /-- Erasing the suffix after the block-terminating `false`. -/
+  | eraseQ
+  /-- Rewinding leftward, skipping the erased (blank) suffix cells. -/
+  | rewindSkipQ
+  /-- Rewinding leftward through the block back to its start. -/
+  | rewindBlock
+  deriving DecidableEq, Fintype
+
+/-- The machine keeping the leading self-delimiting block: scan to the end of the first block,
+erase the suffix, and rewind to the start. No compaction is involved. -/
+def takeFirstBlockComputer : SingleTapeTM Bool where
+  State := TFBState
+  q₀ := .scanStart
+  tr q sym :=
+    match q, sym with
+    -- empty input: halt immediately with empty output
+    | .scanStart, none => (⟨none, none⟩, none)
+    | .scanStart, some true => (⟨some true, some .right⟩, some .scanB)
+    | .scanStart, some false => (⟨some false, some .right⟩, some .eraseQ)
+    -- end of input with the block spanning the whole input: rewind
+    | .scanTF, none => (⟨none, none⟩, some .rewindSkipQ)
+    | .scanTF, some true => (⟨some true, some .right⟩, some .scanB)
+    | .scanTF, some false => (⟨some false, some .right⟩, some .eraseQ)
+    -- end of input just after a lone `true`: rewind
+    | .scanB, none => (⟨none, none⟩, some .rewindSkipQ)
+    | .scanB, some b => (⟨some b, some .right⟩, some .scanTF)
+    | .eraseQ, none => (⟨none, none⟩, some .rewindSkipQ)
+    | .eraseQ, some _ => (⟨none, some .right⟩, some .eraseQ)
+    | .rewindSkipQ, none => (⟨none, some .left⟩, some .rewindSkipQ)
+    -- found the block's rightmost cell: switch to rewinding through the block (no move)
+    | .rewindSkipQ, some b => (⟨some b, none⟩, some .rewindBlock)
+    | .rewindBlock, some b => (⟨some b, some .left⟩, some .rewindBlock)
+    -- reached the blank just left of the block: step back onto its first cell and halt
+    | .rewindBlock, none => (⟨none, some .right⟩, none)
+
+/-! ### Scan phase single steps -/
+
+private lemma tfb_scanStart_true (rest : List Bool) :
+    takeFirstBlockComputer.TransitionRelation
+      ⟨some .scanStart, BiTape.mk₁ (true :: rest)⟩ ⟨some .scanB, splitTape [true] rest⟩ := by
+  rw [← splitTape_nil_left]; simp only [TransitionRelation, SingleTapeTM.step,
+    takeFirstBlockComputer, splitTape_head_cons, splitTape_scan, List.nil_append]
+
+private lemma tfb_scanStart_false (rest : List Bool) :
+    takeFirstBlockComputer.TransitionRelation
+      ⟨some .scanStart, BiTape.mk₁ (false :: rest)⟩ ⟨some .eraseQ, splitTape [false] rest⟩ := by
+  rw [← splitTape_nil_left]; simp only [TransitionRelation, SingleTapeTM.step,
+    takeFirstBlockComputer, splitTape_head_cons, splitTape_scan, List.nil_append]
+
+private lemma tfb_scanTF_true (done rest : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .scanTF, splitTape done (true :: rest)⟩
+      ⟨some .scanB, splitTape (done ++ [true]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma tfb_scanTF_false (done rest : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .scanTF, splitTape done (false :: rest)⟩
+      ⟨some .eraseQ, splitTape (done ++ [false]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma tfb_scanB_step (done : List Bool) (b : Bool) (rest : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .scanB, splitTape done (b :: rest)⟩
+      ⟨some .scanTF, splitTape (done ++ [b]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma tfb_scanTF_nil (done : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .scanTF, splitTape done []⟩
+      ⟨some .rewindSkipQ, splitTape done []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape,
+    List.head?_nil, List.tail_nil, BiTape.write, BiTape.optionMove]
+
+private lemma tfb_scanB_nil (done : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .scanB, splitTape done []⟩
+      ⟨some .rewindSkipQ, splitTape done []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape,
+    List.head?_nil, List.tail_nil, BiTape.write, BiTape.optionMove]
+
+/-! ### Erase phase -/
+
+private lemma tfb_eraseQ_step (n : ℕ) (block : List Bool) (s : Bool) (suffix : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .eraseQ, eraseTape n block (s :: suffix)⟩
+      ⟨some .eraseQ, eraseTape (n + 1) block suffix⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, eraseTape,
+    List.head?_cons, List.tail_cons, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveRight,
+    mapSome_head, mapSome_tail, blanksLeft_succ]
+
+/-- Erasing the whole suffix, ending in the `eraseQ` state on an all-blank right half. -/
+private lemma tfb_erase_phase (block suffix : List Bool) (n : ℕ) :
+    Relation.RelatesInSteps takeFirstBlockComputer.TransitionRelation
+      ⟨some .eraseQ, eraseTape n block suffix⟩
+      ⟨some .eraseQ, eraseTape (n + suffix.length) block []⟩ suffix.length := by
+  induction suffix generalizing n with
+  | nil => simp only [List.length_nil, Nat.add_zero]; exact Relation.RelatesInSteps.refl _
+  | cons s suffix ih =>
+    have hstep := tfb_eraseQ_step n block s suffix
+    have hrest := ih (n + 1)
+    rw [show n + (s :: suffix).length = (n + 1) + suffix.length by simp; omega]
+    exact Relation.RelatesInSteps.head _ _ _ _ hstep hrest
+
+/-! ### Rewind phase -/
+
+/-- On reaching the end of the erased suffix, switch from erasing to rewinding. -/
+private lemma tfb_eraseQ_nil (n : ℕ) (block : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .eraseQ, rewindTape n block⟩
+      ⟨some .rewindSkipQ, rewindTape n block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, rewindTape,
+    BiTape.write, BiTape.optionMove]
+
+/-- Rewinding one blank of the erased suffix. -/
+private lemma tfb_rewindSkipQ_step (n : ℕ) (block : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .rewindSkipQ, rewindTape (n + 1) block⟩
+      ⟨some .rewindSkipQ, rewindTape n block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, rewindTape,
+    blanksLeft_succ, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    StackTape.head_cons, StackTape.tail_cons, cons_none_empty]
+
+/-- Rewinding past all erased blanks. -/
+private lemma tfb_rewindSkipQ_phase (n : ℕ) (block : List Bool) :
+    Relation.RelatesInSteps takeFirstBlockComputer.TransitionRelation
+      ⟨some .rewindSkipQ, rewindTape n block⟩ ⟨some .rewindSkipQ, rewindTape 0 block⟩ n := by
+  induction n with
+  | zero => exact Relation.RelatesInSteps.refl _
+  | succ n ih =>
+    exact Relation.RelatesInSteps.head _ _ _ _ (tfb_rewindSkipQ_step n block) ih
+
+/-- On reaching the block's rightmost cell, step onto it (rewinding no further blanks). -/
+private lemma tfb_rewindSkipQ_last (block' : List Bool) (c : Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .rewindSkipQ, rewindTape 0 (block' ++ [c])⟩
+      ⟨some .rewindSkipQ, splitTape block' [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, rewindTape, blanksLeft,
+    Function.iterate_zero, id_eq, List.reverse_append, List.reverse_cons, List.reverse_nil,
+    List.nil_append, List.singleton_append, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, mapSome_head, mapSome_tail, List.head?_cons, List.tail_cons, cons_none_empty,
+    mapSome_nil, splitTape]
+
+/-- Switch from skipping blanks to rewinding the block. -/
+private lemma tfb_rewindSkipQ_to_block (block' : List Bool) (c : Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .rewindSkipQ, splitTape block' [c]⟩
+      ⟨some .rewindBlock, splitTape block' [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape_head_cons,
+    splitTape_write_head, BiTape.optionMove]
+
+/-- Rewinding one block cell leftward (moving it back into the right half). -/
+private lemma tfb_rewindBlock_step (D : List Bool) (d e : Bool) (rest : List Bool) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .rewindBlock, splitTape (D ++ [d]) (e :: rest)⟩
+      ⟨some .rewindBlock, splitTape D (d :: e :: rest)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, splitTape_head_cons,
+    splitTape_write_head, splitTape_rewind]
+
+/-- Rewinding the whole block back to the leftmost cell. -/
+private lemma tfb_rewindBlock_phase :
+    ∀ (done rest : List Bool), rest ≠ [] →
+      Relation.RelatesInSteps takeFirstBlockComputer.TransitionRelation
+        ⟨some .rewindBlock, splitTape done rest⟩
+        ⟨some .rewindBlock, BiTape.mk₁ (done ++ rest)⟩ done.length := by
+  intro done
+  induction done using List.reverseRecOn with
+  | nil => intro rest _; simp only [List.nil_append, splitTape_nil_left, List.length_nil]
+           exact Relation.RelatesInSteps.refl _
+  | append_singleton D d ih =>
+    intro rest hrest
+    obtain ⟨e, rest', rfl⟩ := List.exists_cons_of_ne_nil hrest
+    have hstep := tfb_rewindBlock_step D d e rest'
+    have hIH := ih (d :: e :: rest') (by simp)
+    rw [List.length_append, List.length_singleton,
+      show (D ++ [d]) ++ (e :: rest') = D ++ (d :: e :: rest') by simp]
+    exact Relation.RelatesInSteps.head _ _ _ _ hstep hIH
+
+/-- Final leftward step: step off the block onto the blank to its left. -/
+private lemma tfb_rewindBlock_mk1 (block : List Bool) (hb : block ≠ []) :
+    takeFirstBlockComputer.TransitionRelation ⟨some .rewindBlock, BiTape.mk₁ block⟩
+      ⟨some .rewindBlock, ⟨none, ∅, StackTape.mapSome block⟩⟩ := by
+  obtain ⟨e, block', rfl⟩ := List.exists_cons_of_ne_nil hb
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, BiTape.mk₁,
+    BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft, empty_head, empty_tail,
+    cons_some_mapSome]
+
+/-- Final rightward step onto the first block cell, halting. -/
+private lemma tfb_rewindBlock_final (block : List Bool) :
+    takeFirstBlockComputer.TransitionRelation
+      ⟨some .rewindBlock, ⟨none, ∅, StackTape.mapSome block⟩⟩ ⟨none, BiTape.mk₁ block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, mapSome_head, mapSome_tail, cons_none_empty,
+    mk₁_eq]
+
+/-- The full rewind: from the start of the rewind, reach the halting configuration on `block`. -/
+private lemma tfb_rewind (n : ℕ) (block : List Bool) (hb : block ≠ []) :
+    Relation.RelatesWithinSteps takeFirstBlockComputer.TransitionRelation
+      ⟨some .rewindSkipQ, rewindTape n block⟩ ⟨none, BiTape.mk₁ block⟩ (n + block.length + 3) := by
+  obtain ⟨block', c, rfl⟩ := (List.eq_nil_or_concat block).resolve_left hb
+  rw [List.concat_eq_append]
+  have h1 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (tfb_rewindSkipQ_phase n (block' ++ [c]))
+  have h2 := Relation.RelatesWithinSteps.single (tfb_rewindSkipQ_last block' c)
+  have h3 := Relation.RelatesWithinSteps.single (tfb_rewindSkipQ_to_block block' c)
+  have h4 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (tfb_rewindBlock_phase block' [c] (by simp))
+  have h5 := Relation.RelatesWithinSteps.single (tfb_rewindBlock_mk1 (block' ++ [c]) (by simp))
+  have h6 := Relation.RelatesWithinSteps.single (tfb_rewindBlock_final (block' ++ [c]))
+  have := (h1.trans (h2.trans (h3.trans (h4.trans (h5.trans h6)))))
+  refine this.of_le ?_
+  simp only [List.length_append, List.length_singleton]
+  omega
+
+/-! ### Scan phase -/
+
+open Relation in
+/-- The scan/erase phase: from the `scanTF` state, scan the leading block of `rest`, erase whatever
+follows, and end poised to rewind the block `done ++ takeFirstBlock rest`. -/
+private lemma tfb_scan_loop : ∀ (n : ℕ) (rest done : List Bool), rest.length = n →
+    RelatesWithinSteps takeFirstBlockComputer.TransitionRelation
+      ⟨some .scanTF, splitTape done rest⟩
+      ⟨some .rewindSkipQ,
+        rewindTape (rest.length - (takeFirstBlock rest).length) (done ++ takeFirstBlock rest)⟩
+      (2 * rest.length + 1) := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro rest done hlen
+    match rest with
+    | [] =>
+      simp only [takeFirstBlock, List.length_nil, Nat.sub_zero, List.append_nil, Nat.mul_zero,
+        Nat.zero_add]
+      exact RelatesWithinSteps.single (tfb_scanTF_nil done)
+    | false :: rest' =>
+      have hs := RelatesWithinSteps.single (tfb_scanTF_false done rest')
+      have he := RelatesWithinSteps.of_relatesInSteps
+        (tfb_erase_phase (done ++ [false]) rest' 0)
+      have hn := RelatesWithinSteps.single (tfb_eraseQ_nil rest'.length (done ++ [false]))
+      rw [eraseTape_zero, Nat.zero_add, eraseTape_nil] at he
+      have hchain := hs.trans (he.trans hn)
+      simp only [takeFirstBlock, List.length_cons]
+      refine hchain.of_le ?_
+      omega
+    | true :: [] =>
+      have h1 := RelatesWithinSteps.single (tfb_scanTF_true done [])
+      have h2 := RelatesWithinSteps.single (tfb_scanB_nil (done ++ [true]))
+      have hchain := h1.trans h2
+      simp only [takeFirstBlock, List.length_cons, List.length_nil, Nat.sub_self]
+      refine hchain.of_le ?_
+      omega
+    | true :: b :: rest'' =>
+      have h1 := RelatesWithinSteps.single (tfb_scanTF_true done (b :: rest''))
+      have h2 := RelatesWithinSteps.single (tfb_scanB_step (done ++ [true]) b rest'')
+      have h3 := ih rest''.length (by simp only [List.length_cons] at hlen; omega)
+        rest'' (done ++ [true] ++ [b]) rfl
+      have hchain := h1.trans (h2.trans h3)
+      simp only [takeFirstBlock, List.length_cons, List.append_assoc, List.singleton_append,
+        Nat.add_sub_add_right] at hchain ⊢
+      refine hchain.of_le ?_
+      omega
+
+private lemma tfb_scanStart_nil :
+    takeFirstBlockComputer.TransitionRelation ⟨some .scanStart, BiTape.mk₁ []⟩
+      ⟨none, BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, takeFirstBlockComputer, mk₁_eq, List.head?_nil,
+    List.tail_nil, mapSome_nil, BiTape.write, BiTape.optionMove]
+
+private lemma takeFirstBlock_ne_nil : ∀ {a : List Bool}, a ≠ [] → takeFirstBlock a ≠ [] := by
+  intro a ha
+  match a with
+  | [] => exact absurd rfl ha
+  | false :: _ => simp [takeFirstBlock]
+  | true :: [] => simp [takeFirstBlock]
+  | true :: _ :: _ => simp [takeFirstBlock]
+
+private lemma takeFirstBlock_length_le : ∀ (n : ℕ) (a : List Bool), a.length = n →
+    (takeFirstBlock a).length ≤ a.length := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro a hlen
+    match a with
+    | [] => simp [takeFirstBlock]
+    | false :: rest => simp [takeFirstBlock]
+    | true :: [] => simp [takeFirstBlock]
+    | true :: b :: rest'' =>
+      have := ih rest''.length (by simp only [List.length_cons] at hlen; omega) rest'' rfl
+      simp only [takeFirstBlock, List.length_cons]
+      omega
+
+open Relation in
+/-- The scan/erase phase from the initial state (differing from `scanTF` only on empty input). -/
+private lemma tfb_scan_start : ∀ (input : List Bool), input ≠ [] →
+    RelatesWithinSteps takeFirstBlockComputer.TransitionRelation
+      ⟨some .scanStart, BiTape.mk₁ input⟩
+      ⟨some .rewindSkipQ,
+        rewindTape (input.length - (takeFirstBlock input).length) (takeFirstBlock input)⟩
+      (2 * input.length + 1) := by
+  intro input hne
+  match input with
+  | [] => exact absurd rfl hne
+  | false :: rest =>
+    have hs := RelatesWithinSteps.single (tfb_scanStart_false rest)
+    have he := RelatesWithinSteps.of_relatesInSteps (tfb_erase_phase [false] rest 0)
+    have hn := RelatesWithinSteps.single (tfb_eraseQ_nil rest.length [false])
+    rw [eraseTape_zero, Nat.zero_add, eraseTape_nil] at he
+    have hchain := hs.trans (he.trans hn)
+    simp only [takeFirstBlock, List.length_cons]
+    refine hchain.of_le ?_
+    omega
+  | true :: [] =>
+    have hchain := (RelatesWithinSteps.single (tfb_scanStart_true [])).trans
+      (RelatesWithinSteps.single (tfb_scanB_nil [true]))
+    simp only [takeFirstBlock, List.length_cons, List.length_nil, Nat.sub_self]
+    refine hchain.of_le ?_
+    omega
+  | true :: b :: rest' =>
+    have h3 := tfb_scan_loop rest'.length rest' ([true] ++ [b]) rfl
+    have hchain := (RelatesWithinSteps.single (tfb_scanStart_true (b :: rest'))).trans
+      ((RelatesWithinSteps.single (tfb_scanB_step [true] b rest')).trans h3)
+    simp only [takeFirstBlock, List.length_cons, List.singleton_append,
+      Nat.add_sub_add_right] at hchain ⊢
+    refine hchain.of_le ?_
+    omega
+
+open Relation Polynomial in
+/-- The machine keeping the leading self-delimiting block: scan to the end of the first block, erase
+the suffix, and rewind. No compaction is involved. -/
+theorem PolyTimeComputable_takeFirstBlock :
+    Nonempty (Cslib.Turing.SingleTapeTM.PolyTimeComputable takeFirstBlock) :=
+  ⟨{ tm := takeFirstBlockComputer
+     timeBound := fun n => 3 * n + 4
+     poly := C 3 * X + C 4
+     bounds := fun n => by simp only [eval_add, eval_mul, eval_C, eval_X]; omega
+     outputsFunInTime := fun a => by
+       simp only [OutputsWithinTime, initCfg, haltCfg]
+       rcases eq_or_ne a [] with rfl | hne
+       · exact (RelatesWithinSteps.single tfb_scanStart_nil).of_le (by simp)
+       · have hblock : takeFirstBlock a ≠ [] := takeFirstBlock_ne_nil hne
+         have hlen : (takeFirstBlock a).length ≤ a.length :=
+           takeFirstBlock_length_le a.length a rfl
+         have h1 := tfb_scan_start a hne
+         have h2 := tfb_rewind (a.length - (takeFirstBlock a).length) (takeFirstBlock a) hblock
+         refine (h1.trans h2).of_le ?_
+         omega } ⟩
+
+
+end ComplexityTheory
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TapeHelpers.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TapeHelpers.lean
new file mode 100644
index 000000000..06dcd5d61
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/TapeHelpers.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+
+/-!
+# Tape configurations for single-tape scan/erase/rewind machines
+
+This file collects the low-level `StackTape`/`BiTape` helpers shared by the polynomial-time machine
+constructions in this directory (`takeFirstBlockComputer`, `undelimitBlockComputer`,
+`tagBlockComputer`). They describe the tape configurations of a left-to-right scan and the
+subsequent erase and rewind phases, together with the single-step rewrite lemmas that move between
+adjacent configurations.
+
+* `splitTape done rest`: mid-scan, with `rest` under and to the right of the head and `done`
+  already scanned (in the reversed left half).
+* `eraseTape n block suffix`: erasing the suffix after a block, `n` cells already blanked.
+* `rewindTape n block`: rewinding leftward over the `n` blanks left by the erase phase.
+-/
+
+namespace ComplexityTheory
+
+open Cslib.Turing Cslib.Turing.SingleTapeTM Cslib.Turing.StackTape
+
+/-! ### The scan configuration `splitTape` -/
+
+/-- Tape configuration during a left-to-right scan: `done` has already been scanned (it sits in the
+left half, reversed) and `rest` lies under and to the right of the head. -/
+def splitTape (done rest : List Bool) : BiTape Bool :=
+  ⟨rest.head?, StackTape.mapSome done.reverse, StackTape.mapSome rest.tail⟩
+
+@[simp] lemma splitTape_nil_left (rest : List Bool) : splitTape [] rest = BiTape.mk₁ rest := by
+  cases rest <;> rfl
+
+/-- Scanning one cell to the right (keeping it) moves it into the scanned prefix. -/
+lemma splitTape_scan (done : List Bool) (c : Bool) (rest : List Bool) :
+    ((splitTape done (c :: rest)).write (some c)).optionMove (some .right)
+      = splitTape (done ++ [c]) rest := by
+  simp only [splitTape, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveRight,
+    List.head?_cons, List.tail_cons, mapSome_head, mapSome_tail, List.reverse_append,
+    List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append, cons_some_mapSome]
+
+/-- Rewinding one cell to the left undoes one scan step. -/
+lemma splitTape_rewind (done : List Bool) (c : Bool) (rest : List Bool) :
+    (splitTape (done ++ [c]) rest).optionMove (some .left) = splitTape done (c :: rest) := by
+  simp only [splitTape, BiTape.optionMove, BiTape.move, BiTape.moveLeft, List.reverse_append,
+    List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append, mapSome_head,
+    mapSome_tail, List.head?_cons, List.tail_cons, cons_head?_mapSome]
+
+lemma splitTape_head_cons (done : List Bool) (c : Bool) (rest : List Bool) :
+    (splitTape done (c :: rest)).head = some c := rfl
+
+lemma splitTape_write_head (done : List Bool) (c : Bool) (rest : List Bool) :
+    (splitTape done (c :: rest)).write (some c) = splitTape done (c :: rest) := rfl
+
+lemma mk₁_eq (l : List Bool) :
+    BiTape.mk₁ l = ⟨l.head?, ∅, StackTape.mapSome l.tail⟩ := by cases l <;> rfl
+
+/-! ### The erase and rewind configurations -/
+
+/-- The left half of the tape during the erase/rewind phases: `block` reversed, buried under `n`
+blanks (the erased suffix cells). -/
+def blanksLeft (n : ℕ) (block : List Bool) : StackTape Bool :=
+  (StackTape.cons none)^[n] (StackTape.mapSome block.reverse)
+
+lemma blanksLeft_succ (n : ℕ) (block : List Bool) :
+    blanksLeft (n + 1) block = StackTape.cons none (blanksLeft n block) := by
+  simp only [blanksLeft, Function.iterate_succ_apply']
+
+/-- Tape while erasing the suffix: `block` (with `n` erased blanks) sits in the left half, `suffix`
+lies under and to the right of the head. -/
+def eraseTape (n : ℕ) (block suffix : List Bool) : BiTape Bool :=
+  ⟨suffix.head?, blanksLeft n block, StackTape.mapSome suffix.tail⟩
+
+/-- Tape while rewinding leftward: `block` reversed under `n` blanks, head on the blanks. -/
+def rewindTape (n : ℕ) (block : List Bool) : BiTape Bool :=
+  ⟨none, blanksLeft n block, ∅⟩
+
+lemma eraseTape_nil (n : ℕ) (block : List Bool) :
+    eraseTape n block [] = rewindTape n block := rfl
+
+lemma eraseTape_zero (block suffix : List Bool) :
+    eraseTape 0 block suffix = splitTape block suffix := rfl
+
+lemma splitTape_nil_eq_rewind (done : List Bool) :
+    splitTape done [] = rewindTape 0 done := rfl
+
+end ComplexityTheory
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/UndelimitBlock.lean b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/UndelimitBlock.lean
new file mode 100644
index 000000000..4b69a8183
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/PolyTime/UndelimitBlock.lean
@@ -0,0 +1,799 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import Cslib.Foundations.Data.BitstringEncoding
+import Cslib.Computability.Machines.Turing.SingleTape.PolyTime.TapeHelpers
+
+/-!
+# The `undelimitBlock` machine
+
+`undelimitBlock` turns a single self-delimiting block `delimit P` into its payload `P`, i.e. strips
+the framing bits. This is the genuine compaction of the pair-projection pipeline: the machine first
+normalizes the input to a well-formed terminated block, then compacts the payload bits to the front
+of the tape, a quadratic-time single-tape shuttle.
+
+The main result is `PolyTimeComputable_undelimitBlock`, witnessed by `undelimitBlockComputer`.
+-/
+
+open Computability Turing
+
+namespace ComplexityTheory
+
+open Cslib.Turing Cslib.Turing.SingleTapeTM Cslib.Turing.StackTape
+open BitstringEncoding (undelimitBlock)
+
+/-- States of the `undelimitBlock` machine. The machine works in two phases.
+
+**Normalization** (`norm*` states): a left-to-right scan through the pair structure that rewrites
+the input into an equivalent *well-formed* block `true b₁ … true bₖ false` with nothing after it —
+appending the missing `false` terminator if the input ends mid-structure, turning a lone trailing
+`true` into the terminator, and erasing any garbage after the terminator — then rewinds to the
+start. During this scan the unread input is a contiguous run of non-blank cells, so the end of the
+input is detectable as the first blank.
+
+**Shuttle** (remaining states): builds the output (payload bits) at the front of the tape; a
+growing region of blanks separates the finished output from the input still to be scanned, and the
+head shuttles across this gap to carry each payload bit to the output frontier. The shuttle relies
+on normalization: while seeking rightward across the gap it cannot tell gap blanks from the blanks
+past the end of the input, so it only halts because a `false` terminator is guaranteed to be
+present (and it leaves no garbage behind only because normalization already erased it). -/
+inductive UBState
+  /-- Normalizing: expecting `true` (pair marker) or `false` (terminator); on a blank the input
+  ended mid-structure, so write the missing terminator and rewind. -/
+  | normTF
+  /-- Normalizing: expecting the payload bit after a `true`; a blank here means a lone trailing
+  `true`, which is removed by turning it into the terminator. -/
+  | normB
+  /-- On the lone trailing `true`: overwrite it with the terminator `false`. -/
+  | normFixLone
+  /-- Erasing everything after the terminator. -/
+  | normErase
+  /-- Rewinding leftward over the blanks left by `normErase`. -/
+  | normRewindSkip
+  /-- Rewinding leftward through the normalized block; on the blank left of it, step right and
+  start the shuttle. -/
+  | normRewind
+  /-- Shuttle start: at the first `true` of the first block cell pair (special-cased: the output
+  is still empty). -/
+  | initTrue
+  /-- At the first payload bit (to be placed at the very front). -/
+  | initBit
+  /-- Depositing the carried bit `b` at the output frontier. -/
+  | deposit (b : Bool)
+  /-- Seeking rightward across the gap to the next input cell. -/
+  | seekInput
+  /-- Just consumed a `true`; at the payload bit to grab. -/
+  | grabBit
+  /-- Carrying payload bit `b` leftward across the gap to the frontier. -/
+  | carry (b : Bool)
+  /-- Erasing the rest of the input (used when the block is empty, i.e. starts with `false`). -/
+  | eraseAll
+  /-- Rewinding leftward, skipping the gap blanks. -/
+  | rewindSkip
+  /-- Rewinding leftward through the finished output block. -/
+  | rewindBlock
+  deriving DecidableEq, Fintype
+
+/-- The machine stripping a single block's framing: it first normalizes the input to a well-formed
+terminated block (see `UBState`), then compacts the payload bits to the front of the tape, a
+quadratic-time single-tape shuttle. -/
+def undelimitBlockComputer : SingleTapeTM Bool where
+  State := UBState
+  q₀ := .normTF
+  tr q sym :=
+    match q, sym with
+    -- Phase 1: normalize the input to a well-formed block with nothing after it.
+    | .normTF, some true => (⟨some true, some .right⟩, some .normB)   -- keep pair marker
+    | .normTF, some false => (⟨some false, some .right⟩, some .normErase) -- keep terminator
+    | .normTF, none => (⟨some false, none⟩, some .normRewind)        -- write missing terminator
+    | .normB, some b => (⟨some b, some .right⟩, some .normTF)        -- keep payload bit
+    | .normB, none => (⟨none, some .left⟩, some .normFixLone)        -- lone trailing `true`
+    | .normFixLone, some _ => (⟨some false, none⟩, some .normRewind) -- lone `true` → terminator
+    | .normFixLone, none => (⟨none, none⟩, none)                     -- unreachable
+    | .normErase, some _ => (⟨none, some .right⟩, some .normErase)   -- erase garbage
+    | .normErase, none => (⟨none, none⟩, some .normRewindSkip)       -- garbage done: rewind
+    | .normRewindSkip, none => (⟨none, some .left⟩, some .normRewindSkip)
+    | .normRewindSkip, some b => (⟨some b, none⟩, some .normRewind)  -- found the block's end
+    | .normRewind, some b => (⟨some b, some .left⟩, some .normRewind)
+    | .normRewind, none => (⟨none, some .right⟩, some .initTrue)     -- at the start: shuttle
+    -- Phase 2: shuttle the payload bits to the front of the tape.
+    | .initTrue, none => (⟨none, none⟩, none)                        -- empty input
+    | .initTrue, some true => (⟨none, some .right⟩, some .initBit)   -- erase the first `true`
+    | .initTrue, some false => (⟨none, some .right⟩, some .eraseAll) -- empty block: erase all
+    | .initBit, none => (⟨none, none⟩, none)                         -- unreachable (normalized)
+    | .initBit, some b => (⟨none, some .left⟩, some (.deposit b))    -- grab first bit, go to front
+    | .deposit b, _ => (⟨some b, some .right⟩, some .seekInput)      -- write bit, advance to gap
+    | .seekInput, none => (⟨none, some .right⟩, some .seekInput)     -- skip a gap blank
+    | .seekInput, some true => (⟨none, some .right⟩, some .grabBit)  -- erase a `true`
+    | .seekInput, some false => (⟨none, none⟩, some .rewindSkip)     -- terminator: finish
+    | .grabBit, none => (⟨none, none⟩, some .rewindSkip)             -- unreachable (normalized)
+    | .grabBit, some b => (⟨none, some .left⟩, some (.carry b))      -- grab bit, carry left
+    | .carry b, none => (⟨none, some .left⟩, some (.carry b))        -- skip a gap blank
+    | .carry b, some c => (⟨some c, some .right⟩, some (.deposit b)) -- reached output frontier
+    | .eraseAll, none => (⟨none, none⟩, none)                        -- done erasing
+    | .eraseAll, some _ => (⟨none, some .right⟩, some .eraseAll)     -- erase a cell
+    | .rewindSkip, none => (⟨none, some .left⟩, some .rewindSkip)
+    | .rewindSkip, some b => (⟨some b, none⟩, some .rewindBlock)
+    | .rewindBlock, some b => (⟨some b, some .left⟩, some .rewindBlock)
+    | .rewindBlock, none => (⟨none, some .right⟩, none)
+
+/-! #### Facts about `undelimitBlock` and `delimit` -/
+
+private lemma undelimitBlock_length_le : ∀ (n : ℕ) (a : List Bool), a.length = n →
+    2 * (undelimitBlock a).length ≤ a.length := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro a hlen
+    match a with
+    | [] => simp [undelimitBlock]
+    | false :: rest => simp [undelimitBlock]
+    | true :: [] => simp [undelimitBlock]
+    | true :: b :: rest'' =>
+      have := ih rest''.length (by simp only [List.length_cons] at hlen; omega) rest'' rfl
+      simp only [undelimitBlock, List.length_cons]
+      omega
+
+private lemma delimit_nil : BitstringEncoding.delimit [] = [false] := rfl
+
+private lemma delimit_cons (b : Bool) (l : List Bool) :
+    BitstringEncoding.delimit (b :: l) = true :: b :: BitstringEncoding.delimit l := rfl
+
+private lemma delimit_undelimitBlock_nil :
+    BitstringEncoding.delimit (undelimitBlock []) = [false] := rfl
+
+private lemma delimit_undelimitBlock_false (rest : List Bool) :
+    BitstringEncoding.delimit (undelimitBlock (false :: rest)) = [false] := rfl
+
+private lemma delimit_undelimitBlock_singleton :
+    BitstringEncoding.delimit (undelimitBlock [true]) = [false] := rfl
+
+private lemma delimit_undelimitBlock_cons (b : Bool) (rest : List Bool) :
+    BitstringEncoding.delimit (undelimitBlock (true :: b :: rest))
+      = true :: b :: BitstringEncoding.delimit (undelimitBlock rest) := rfl
+
+/-! #### Normalization phase: single steps
+
+The scan steps mirror the `takeFirstBlock` machine's scan exactly (the same `splitTape`
+configurations), with different endings: reaching the end of the input mid-structure writes the
+missing terminator in place. -/
+
+private lemma nm_scanTF_true (done rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normTF, splitTape done (true :: rest)⟩
+      ⟨some .normB, splitTape (done ++ [true]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma nm_scanTF_false (done rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normTF, splitTape done (false :: rest)⟩
+      ⟨some .normErase, splitTape (done ++ [false]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+private lemma nm_scanB_step (done : List Bool) (b : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normB, splitTape done (b :: rest)⟩
+      ⟨some .normTF, splitTape (done ++ [b]) rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_scan]
+
+/-- End of input while expecting a pair marker: write the missing terminator in place. -/
+private lemma nm_scanTF_nil (done : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normTF, splitTape done []⟩
+      ⟨some .normRewind, splitTape done [false]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape,
+    List.head?_nil, List.tail_nil, List.head?_cons, List.tail_cons, mapSome_nil, BiTape.write,
+    BiTape.optionMove]
+
+/-- End of input just after a pair marker (a lone trailing `true`): step back onto it. -/
+private lemma nm_scanB_nil (done : List Bool) (c : Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normB, splitTape (done ++ [c]) []⟩
+      ⟨some .normFixLone, splitTape done [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape,
+    List.head?_nil, List.tail_nil, List.head?_cons, List.tail_cons, BiTape.write, BiTape.optionMove,
+    BiTape.move, BiTape.moveLeft, List.reverse_append, List.reverse_cons, List.reverse_nil,
+    List.nil_append, List.singleton_append, mapSome_head, mapSome_tail, mapSome_nil,
+    cons_none_empty]
+
+/-- Overwrite the lone trailing `true` with the terminator. -/
+private lemma nm_fixLone (done : List Bool) (c : Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normFixLone, splitTape done [c]⟩
+      ⟨some .normRewind, splitTape done [false]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape,
+    List.head?_cons, List.tail_cons, BiTape.write, BiTape.optionMove, mapSome_nil]
+
+/-! #### Normalization phase: erasing the garbage after the terminator -/
+
+private lemma nm_erase_step (n : ℕ) (block : List Bool) (s : Bool) (suffix : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normErase, eraseTape n block (s :: suffix)⟩
+      ⟨some .normErase, eraseTape (n + 1) block suffix⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, eraseTape,
+    List.head?_cons, List.tail_cons, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveRight,
+    mapSome_head, mapSome_tail, blanksLeft_succ]
+
+private lemma nm_erase_phase (block suffix : List Bool) (n : ℕ) :
+    Relation.RelatesInSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .normErase, eraseTape n block suffix⟩
+      ⟨some .normErase, eraseTape (n + suffix.length) block []⟩ suffix.length := by
+  induction suffix generalizing n with
+  | nil => simp only [List.length_nil, Nat.add_zero]; exact Relation.RelatesInSteps.refl _
+  | cons s suffix ih =>
+    have hstep := nm_erase_step n block s suffix
+    have hrest := ih (n + 1)
+    rw [show n + (s :: suffix).length = (n + 1) + suffix.length by simp; omega]
+    exact Relation.RelatesInSteps.head _ _ _ _ hstep hrest
+
+private lemma nm_erase_nil (n : ℕ) (block : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normErase, rewindTape n block⟩
+      ⟨some .normRewindSkip, rewindTape n block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, rewindTape,
+    BiTape.write, BiTape.optionMove]
+
+/-! #### Normalization phase: rewinding to the start (mirrors the `takeFirstBlock` rewind, but
+hands off to the shuttle's `initTrue` state instead of halting) -/
+
+private lemma nm_rewindSkip_step (n : ℕ) (block : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normRewindSkip, rewindTape (n + 1) block⟩
+      ⟨some .normRewindSkip, rewindTape n block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, rewindTape,
+    blanksLeft_succ, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    StackTape.head_cons, StackTape.tail_cons, cons_none_empty]
+
+private lemma nm_rewindSkip_phase (n : ℕ) (block : List Bool) :
+    Relation.RelatesInSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .normRewindSkip, rewindTape n block⟩ ⟨some .normRewindSkip, rewindTape 0 block⟩ n := by
+  induction n with
+  | zero => exact Relation.RelatesInSteps.refl _
+  | succ n ih =>
+    exact Relation.RelatesInSteps.head _ _ _ _ (nm_rewindSkip_step n block) ih
+
+private lemma nm_rewindSkip_last (block' : List Bool) (c : Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .normRewindSkip, rewindTape 0 (block' ++ [c])⟩
+      ⟨some .normRewindSkip, splitTape block' [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, rewindTape, blanksLeft,
+    Function.iterate_zero, id_eq, List.reverse_append, List.reverse_cons, List.reverse_nil,
+    List.nil_append, List.singleton_append, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, mapSome_head, mapSome_tail, List.head?_cons, List.tail_cons, cons_none_empty,
+    mapSome_nil, splitTape]
+
+private lemma nm_rewindSkip_to_block (block' : List Bool) (c : Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normRewindSkip, splitTape block' [c]⟩
+      ⟨some .normRewind, splitTape block' [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_write_head, BiTape.optionMove]
+
+private lemma nm_rewindBlock_step (D : List Bool) (d e : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .normRewind, splitTape (D ++ [d]) (e :: rest)⟩
+      ⟨some .normRewind, splitTape D (d :: e :: rest)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_write_head, splitTape_rewind]
+
+private lemma nm_rewindBlock_phase :
+    ∀ (done rest : List Bool), rest ≠ [] →
+      Relation.RelatesInSteps undelimitBlockComputer.TransitionRelation
+        ⟨some .normRewind, splitTape done rest⟩
+        ⟨some .normRewind, BiTape.mk₁ (done ++ rest)⟩ done.length := by
+  intro done
+  induction done using List.reverseRecOn with
+  | nil => intro rest _; simp only [List.nil_append, splitTape_nil_left, List.length_nil]
+           exact Relation.RelatesInSteps.refl _
+  | append_singleton D d ih =>
+    intro rest hrest
+    obtain ⟨e, rest', rfl⟩ := List.exists_cons_of_ne_nil hrest
+    have hstep := nm_rewindBlock_step D d e rest'
+    have hIH := ih (d :: e :: rest') (by simp)
+    rw [List.length_append, List.length_singleton,
+      show (D ++ [d]) ++ (e :: rest') = D ++ (d :: e :: rest') by simp]
+    exact Relation.RelatesInSteps.head _ _ _ _ hstep hIH
+
+private lemma nm_rewind_mk1 (block : List Bool) (hb : block ≠ []) :
+    undelimitBlockComputer.TransitionRelation ⟨some .normRewind, BiTape.mk₁ block⟩
+      ⟨some .normRewind, ⟨none, ∅, StackTape.mapSome block⟩⟩ := by
+  obtain ⟨e, block', rfl⟩ := List.exists_cons_of_ne_nil hb
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.mk₁,
+    BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft, empty_head, empty_tail,
+    cons_some_mapSome]
+
+/-- The final rightward step onto the first block cell, entering the shuttle phase. -/
+private lemma nm_rewind_final (block : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .normRewind, ⟨none, ∅, StackTape.mapSome block⟩⟩
+      ⟨some .initTrue, BiTape.mk₁ block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, mapSome_head, mapSome_tail, cons_none_empty,
+    mk₁_eq]
+
+/-- The full rewind from the skip state: reach the start of the block in state `initTrue`. -/
+private lemma nm_rewind (n : ℕ) (block : List Bool) (hb : block ≠ []) :
+    Relation.RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .normRewindSkip, rewindTape n block⟩ ⟨some .initTrue, BiTape.mk₁ block⟩
+      (n + block.length + 3) := by
+  obtain ⟨block', c, rfl⟩ := (List.eq_nil_or_concat block).resolve_left hb
+  rw [List.concat_eq_append]
+  have h1 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (nm_rewindSkip_phase n (block' ++ [c]))
+  have h2 := Relation.RelatesWithinSteps.single (nm_rewindSkip_last block' c)
+  have h3 := Relation.RelatesWithinSteps.single (nm_rewindSkip_to_block block' c)
+  have h4 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (nm_rewindBlock_phase block' [c] (by simp))
+  have h5 := Relation.RelatesWithinSteps.single (nm_rewind_mk1 (block' ++ [c]) (by simp))
+  have h6 := Relation.RelatesWithinSteps.single (nm_rewind_final (block' ++ [c]))
+  have := h1.trans (h2.trans (h3.trans (h4.trans (h5.trans h6))))
+  refine this.of_le ?_
+  simp only [List.length_append, List.length_singleton]
+  omega
+
+/-- Rewind starting on the last cell of the block itself (no erased blanks to skip). -/
+private lemma nm_rewind_from_block (done : List Bool) :
+    Relation.RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .normRewind, splitTape done [false]⟩
+      ⟨some .initTrue, BiTape.mk₁ (done ++ [false])⟩ (done.length + 2) := by
+  have h4 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (nm_rewindBlock_phase done [false] (by simp))
+  have h5 := Relation.RelatesWithinSteps.single (nm_rewind_mk1 (done ++ [false]) (by simp))
+  have h6 := Relation.RelatesWithinSteps.single (nm_rewind_final (done ++ [false]))
+  exact (h4.trans (h5.trans h6)).of_le (by omega)
+
+/-! #### Normalization phase: the full scan -/
+
+open Relation in
+/-- The normalization scan: from `normTF`, scanning the pair structure of `rest` (with `done`
+already scanned), the machine reaches the shuttle start on the well-formed block
+`done ++ delimit (undelimitBlock rest)`. -/
+private lemma nm_scan_loop : ∀ (n : ℕ) (rest done : List Bool), rest.length = n →
+    RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .normTF, splitTape done rest⟩
+      ⟨some .initTrue,
+        BiTape.mk₁ (done ++ BitstringEncoding.delimit (undelimitBlock rest))⟩
+      (2 * rest.length + done.length + 6) := by
+  intro n
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    intro rest done hlen
+    match rest with
+    | [] =>
+      rw [delimit_undelimitBlock_nil]
+      have hchain := (RelatesWithinSteps.single (nm_scanTF_nil done)).trans
+        (nm_rewind_from_block done)
+      refine hchain.of_le ?_
+      simp only [List.length_nil]
+      omega
+    | false :: rest' =>
+      rw [delimit_undelimitBlock_false]
+      have hs := RelatesWithinSteps.single (nm_scanTF_false done rest')
+      have he := RelatesWithinSteps.of_relatesInSteps
+        (nm_erase_phase (done ++ [false]) rest' 0)
+      rw [eraseTape_zero, Nat.zero_add, eraseTape_nil] at he
+      have hn := RelatesWithinSteps.single (nm_erase_nil rest'.length (done ++ [false]))
+      have hr := nm_rewind rest'.length (done ++ [false]) (by simp)
+      have hchain := hs.trans (he.trans (hn.trans hr))
+      refine hchain.of_le ?_
+      simp only [List.length_cons, List.length_append, List.length_nil]
+      omega
+    | true :: [] =>
+      rw [delimit_undelimitBlock_singleton]
+      have hchain := (RelatesWithinSteps.single (nm_scanTF_true done [])).trans
+        ((RelatesWithinSteps.single (nm_scanB_nil done true)).trans
+          ((RelatesWithinSteps.single (nm_fixLone done true)).trans
+            (nm_rewind_from_block done)))
+      refine hchain.of_le ?_
+      simp only [List.length_cons, List.length_nil]
+      omega
+    | true :: b :: rest'' =>
+      rw [delimit_undelimitBlock_cons]
+      have h1 := RelatesWithinSteps.single (nm_scanTF_true done (b :: rest''))
+      have h2 := RelatesWithinSteps.single (nm_scanB_step (done ++ [true]) b rest'')
+      have h3 := ih rest''.length (by simp only [List.length_cons] at hlen; omega)
+        rest'' (done ++ [true] ++ [b]) rfl
+      have hchain := h1.trans (h2.trans h3)
+      rw [show done ++ [true] ++ [b] ++ BitstringEncoding.delimit (undelimitBlock rest'')
+        = done ++ true :: b :: BitstringEncoding.delimit (undelimitBlock rest'') by simp]
+        at hchain
+      refine hchain.of_le ?_
+      simp only [List.length_cons, List.length_append, List.length_nil]
+      omega
+
+/-- The normalization phase: on any input `a`, reach the shuttle start with the tape holding the
+well-formed block `delimit (undelimitBlock a)`. -/
+private lemma nm_phase (a : List Bool) :
+    Relation.RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .normTF, BiTape.mk₁ a⟩
+      ⟨some .initTrue, BiTape.mk₁ (BitstringEncoding.delimit (undelimitBlock a))⟩
+      (2 * a.length + 6) := by
+  have h := nm_scan_loop a.length a [] rfl
+  rw [splitTape_nil_left, List.nil_append, List.length_nil, Nat.add_zero] at h
+  exact h
+
+/-! #### Shuttle phase: tape configurations -/
+
+/-- The right half of the tape during the shuttle: the unconsumed input `rem` buried under `k`
+blanks (part of the gap). -/
+private def blanksRight (k : ℕ) (rem : List Bool) : StackTape Bool :=
+  (StackTape.cons none)^[k] (StackTape.mapSome rem)
+
+private lemma blanksRight_succ (k : ℕ) (rem : List Bool) :
+    blanksRight (k + 1) rem = StackTape.cons none (blanksRight k rem) := by
+  simp only [blanksRight, Function.iterate_succ_apply']
+
+private lemma blanksRight_zero (rem : List Bool) :
+    blanksRight 0 rem = StackTape.mapSome rem := rfl
+
+/-- Tape while shuttling with the head on a gap blank: `i` blanks (then the output `out`) to the
+left, `k` blanks (then the unconsumed input `rem`) to the right. -/
+private def shuttleTape (i k : ℕ) (out rem : List Bool) : BiTape Bool :=
+  ⟨none, blanksLeft i out, blanksRight k rem⟩
+
+/-- Tape with the head on the first cell of the unconsumed input `rem`, the whole gap of `g`
+blanks (then the output `out`) to the left. -/
+private def inputEdgeTape (g : ℕ) (out rem : List Bool) : BiTape Bool :=
+  ⟨rem.head?, blanksLeft g out, StackTape.mapSome rem.tail⟩
+
+/-! #### Shuttle phase: single steps -/
+
+private lemma ub_seek_blank (i k : ℕ) (out rem : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .seekInput, shuttleTape i (k + 1) out rem⟩
+      ⟨some .seekInput, shuttleTape (i + 1) k out rem⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, shuttleTape,
+    blanksRight_succ, blanksLeft_succ, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveRight, StackTape.head_cons, StackTape.tail_cons]
+
+private lemma ub_seek_onto (i : ℕ) (out rem : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .seekInput, shuttleTape i 0 out rem⟩
+      ⟨some .seekInput, inputEdgeTape (i + 1) out rem⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, shuttleTape,
+    inputEdgeTape, blanksRight_zero, blanksLeft_succ, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveRight, mapSome_head, mapSome_tail]
+
+open Relation in
+/-- Seeking rightward across the whole gap, ending on the first cell of the unconsumed input. -/
+private lemma ub_seek_phase (k : ℕ) : ∀ (i : ℕ) (out rem : List Bool),
+    RelatesInSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .seekInput, shuttleTape i k out rem⟩
+      ⟨some .seekInput, inputEdgeTape (i + k + 1) out rem⟩ (k + 1) := by
+  induction k with
+  | zero =>
+    intro i out rem
+    rw [Nat.add_zero]
+    exact RelatesInSteps.single (ub_seek_onto i out rem)
+  | succ k ihk =>
+    intro i out rem
+    have h1 := ub_seek_blank i k out rem
+    have h2 := ihk (i + 1) out rem
+    rw [show i + 1 + k + 1 = i + (k + 1) + 1 by omega] at h2
+    exact RelatesInSteps.head _ _ _ _ h1 h2
+
+private lemma ub_seek_true (g : ℕ) (out : List Bool) (b : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .seekInput, inputEdgeTape g out (true :: b :: rest)⟩
+      ⟨some .grabBit, inputEdgeTape (g + 1) out (b :: rest)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, inputEdgeTape,
+    List.head?_cons, List.tail_cons, blanksLeft_succ, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveRight, mapSome_head, mapSome_tail]
+
+private lemma ub_grab (g : ℕ) (out : List Bool) (b : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .grabBit, inputEdgeTape (g + 1) out (b :: rest)⟩
+      ⟨some (.carry b), shuttleTape g 1 out rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, inputEdgeTape,
+    shuttleTape, List.head?_cons, List.tail_cons, blanksLeft_succ, blanksRight_succ,
+    blanksRight_zero, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    StackTape.head_cons, StackTape.tail_cons]
+
+private lemma ub_carry_blank (b : Bool) (i k : ℕ) (out rem : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some (.carry b), shuttleTape (i + 1) k out rem⟩
+      ⟨some (.carry b), shuttleTape i (k + 1) out rem⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, shuttleTape,
+    blanksLeft_succ, blanksRight_succ, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, StackTape.head_cons, StackTape.tail_cons]
+
+open Relation in
+/-- Carrying the grabbed bit leftward across the gap to the output frontier. -/
+private lemma ub_carry_phase (i : ℕ) : ∀ (k : ℕ) (b : Bool) (out rem : List Bool),
+    RelatesInSteps undelimitBlockComputer.TransitionRelation
+      ⟨some (.carry b), shuttleTape i k out rem⟩
+      ⟨some (.carry b), shuttleTape 0 (i + k) out rem⟩ i := by
+  induction i with
+  | zero =>
+    intro k b out rem
+    rw [Nat.zero_add]
+    exact RelatesInSteps.refl _
+  | succ i ihi =>
+    intro k b out rem
+    have h1 := ub_carry_blank b i k out rem
+    have h2 := ihi (k + 1) b out rem
+    rw [show i + (k + 1) = i + 1 + k by omega] at h2
+    exact RelatesInSteps.head _ _ _ _ h1 h2
+
+private lemma ub_carry_edge (b : Bool) (k : ℕ) (out' : List Bool) (c : Bool) (rem : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some (.carry b), shuttleTape 0 k (out' ++ [c]) rem⟩
+      ⟨some (.carry b), ⟨some c, StackTape.mapSome out'.reverse, blanksRight (k + 1) rem⟩⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, shuttleTape,
+    blanksLeft, Function.iterate_zero, id_eq, List.reverse_append, List.reverse_cons,
+    List.reverse_nil, List.nil_append, List.singleton_append, blanksRight_succ, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveLeft, mapSome_head, mapSome_tail, List.head?_cons,
+    List.tail_cons]
+
+private lemma ub_carry_deposit (b : Bool) (k : ℕ) (out' : List Bool) (c : Bool)
+    (rem : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some (.carry b), ⟨some c, StackTape.mapSome out'.reverse, blanksRight (k + 1) rem⟩⟩
+      ⟨some (.deposit b), shuttleTape 0 k (out' ++ [c]) rem⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, shuttleTape,
+    blanksLeft, Function.iterate_zero, id_eq, List.reverse_append, List.reverse_cons,
+    List.reverse_nil, List.nil_append, List.singleton_append, blanksRight_succ, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, StackTape.head_cons, StackTape.tail_cons,
+    cons_some_mapSome]
+
+/-- Turning around at the output frontier: one step onto the last output bit, one step back. -/
+private lemma ub_carry_turn (b : Bool) (k : ℕ) (out rem : List Bool) (hout : out ≠ []) :
+    Relation.RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some (.carry b), shuttleTape 0 k out rem⟩
+      ⟨some (.deposit b), shuttleTape 0 k out rem⟩ 2 := by
+  obtain ⟨out', c, rfl⟩ := (List.eq_nil_or_concat out).resolve_left hout
+  rw [List.concat_eq_append]
+  exact (Relation.RelatesWithinSteps.single (ub_carry_edge b k out' c rem)).trans
+    (Relation.RelatesWithinSteps.single (ub_carry_deposit b k out' c rem))
+
+private lemma ub_deposit (b : Bool) (k : ℕ) (out rem : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some (.deposit b), shuttleTape 0 (k + 1) out rem⟩
+      ⟨some .seekInput, shuttleTape 0 k (out ++ [b]) rem⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, shuttleTape,
+    blanksLeft, Function.iterate_zero, id_eq, blanksRight_succ, List.reverse_append,
+    List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, StackTape.head_cons, StackTape.tail_cons,
+    cons_some_mapSome]
+
+/-! #### Shuttle phase: entry and exit steps -/
+
+private lemma ub_init_true (p : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .initTrue, BiTape.mk₁ (true :: p :: rest)⟩
+      ⟨some .initBit, BiTape.mk₁ (p :: rest)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.mk₁,
+    BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveRight, mapSome_head, mapSome_tail,
+    List.head?_cons, List.tail_cons, cons_none_empty]
+
+private lemma ub_init_bit (p : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .initBit, BiTape.mk₁ (p :: rest)⟩
+      ⟨some (.deposit p), shuttleTape 0 1 [] rest⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.mk₁,
+    shuttleTape, blanksLeft, blanksRight_succ, blanksRight_zero, Function.iterate_zero, id_eq,
+    List.reverse_nil, mapSome_nil, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    empty_head, empty_tail]
+
+private lemma ub_initTrue_false :
+    undelimitBlockComputer.TransitionRelation ⟨some .initTrue, BiTape.mk₁ [false]⟩
+      ⟨some .eraseAll, BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.mk₁,
+    BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveRight, empty_head, empty_tail,
+    cons_none_empty, mapSome_nil, BiTape.empty_eq_nil, BiTape.nil]
+
+private lemma ub_eraseAll_halt :
+    undelimitBlockComputer.TransitionRelation ⟨some .eraseAll, BiTape.mk₁ []⟩
+      ⟨none, BiTape.mk₁ []⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.mk₁,
+    BiTape.write, BiTape.optionMove, BiTape.empty_eq_nil, BiTape.nil]
+
+/-- Reaching the terminator: erase it and start the final rewind. -/
+private lemma ub_seek_false (g : ℕ) (out : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .seekInput, inputEdgeTape g out [false]⟩
+      ⟨some .rewindSkip, rewindTape g out⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, inputEdgeTape,
+    rewindTape, List.head?_cons, List.tail_cons, mapSome_nil, BiTape.write, BiTape.optionMove]
+
+/-! #### Shuttle phase: the final rewind (mirrors the `takeFirstBlock` rewind) -/
+
+private lemma ub_rewindSkip_step (n : ℕ) (block : List Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .rewindSkip, rewindTape (n + 1) block⟩
+      ⟨some .rewindSkip, rewindTape n block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, rewindTape,
+    blanksLeft_succ, BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft,
+    StackTape.head_cons, StackTape.tail_cons, cons_none_empty]
+
+private lemma ub_rewindSkip_phase (n : ℕ) (block : List Bool) :
+    Relation.RelatesInSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .rewindSkip, rewindTape n block⟩ ⟨some .rewindSkip, rewindTape 0 block⟩ n := by
+  induction n with
+  | zero => exact Relation.RelatesInSteps.refl _
+  | succ n ih =>
+    exact Relation.RelatesInSteps.head _ _ _ _ (ub_rewindSkip_step n block) ih
+
+private lemma ub_rewindSkip_last (block' : List Bool) (c : Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .rewindSkip, rewindTape 0 (block' ++ [c])⟩
+      ⟨some .rewindSkip, splitTape block' [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, rewindTape, blanksLeft,
+    Function.iterate_zero, id_eq, List.reverse_append, List.reverse_cons, List.reverse_nil,
+    List.nil_append, List.singleton_append, BiTape.write, BiTape.optionMove, BiTape.move,
+    BiTape.moveLeft, mapSome_head, mapSome_tail, List.head?_cons, List.tail_cons, cons_none_empty,
+    mapSome_nil, splitTape]
+
+private lemma ub_rewindSkip_to_block (block' : List Bool) (c : Bool) :
+    undelimitBlockComputer.TransitionRelation ⟨some .rewindSkip, splitTape block' [c]⟩
+      ⟨some .rewindBlock, splitTape block' [c]⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_write_head, BiTape.optionMove]
+
+private lemma ub_rewindBlock_step (D : List Bool) (d e : Bool) (rest : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .rewindBlock, splitTape (D ++ [d]) (e :: rest)⟩
+      ⟨some .rewindBlock, splitTape D (d :: e :: rest)⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, splitTape_head_cons,
+    splitTape_write_head, splitTape_rewind]
+
+private lemma ub_rewindBlock_phase :
+    ∀ (done rest : List Bool), rest ≠ [] →
+      Relation.RelatesInSteps undelimitBlockComputer.TransitionRelation
+        ⟨some .rewindBlock, splitTape done rest⟩
+        ⟨some .rewindBlock, BiTape.mk₁ (done ++ rest)⟩ done.length := by
+  intro done
+  induction done using List.reverseRecOn with
+  | nil => intro rest _; simp only [List.nil_append, splitTape_nil_left, List.length_nil]
+           exact Relation.RelatesInSteps.refl _
+  | append_singleton D d ih =>
+    intro rest hrest
+    obtain ⟨e, rest', rfl⟩ := List.exists_cons_of_ne_nil hrest
+    have hstep := ub_rewindBlock_step D d e rest'
+    have hIH := ih (d :: e :: rest') (by simp)
+    rw [List.length_append, List.length_singleton,
+      show (D ++ [d]) ++ (e :: rest') = D ++ (d :: e :: rest') by simp]
+    exact Relation.RelatesInSteps.head _ _ _ _ hstep hIH
+
+private lemma ub_rewindBlock_mk1 (block : List Bool) (hb : block ≠ []) :
+    undelimitBlockComputer.TransitionRelation ⟨some .rewindBlock, BiTape.mk₁ block⟩
+      ⟨some .rewindBlock, ⟨none, ∅, StackTape.mapSome block⟩⟩ := by
+  obtain ⟨e, block', rfl⟩ := List.exists_cons_of_ne_nil hb
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.mk₁,
+    BiTape.write, BiTape.optionMove, BiTape.move, BiTape.moveLeft, empty_head, empty_tail,
+    cons_some_mapSome]
+
+private lemma ub_rewindBlock_final (block : List Bool) :
+    undelimitBlockComputer.TransitionRelation
+      ⟨some .rewindBlock, ⟨none, ∅, StackTape.mapSome block⟩⟩ ⟨none, BiTape.mk₁ block⟩ := by
+  simp only [TransitionRelation, SingleTapeTM.step, undelimitBlockComputer, BiTape.write,
+    BiTape.optionMove, BiTape.move, BiTape.moveRight, mapSome_head, mapSome_tail, cons_none_empty,
+    mk₁_eq]
+
+/-- The shuttle's full rewind: from the start of the rewind, reach the halting configuration. -/
+private lemma ub_rewind (n : ℕ) (block : List Bool) (hb : block ≠ []) :
+    Relation.RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .rewindSkip, rewindTape n block⟩ ⟨none, BiTape.mk₁ block⟩
+      (n + block.length + 3) := by
+  obtain ⟨block', c, rfl⟩ := (List.eq_nil_or_concat block).resolve_left hb
+  rw [List.concat_eq_append]
+  have h1 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (ub_rewindSkip_phase n (block' ++ [c]))
+  have h2 := Relation.RelatesWithinSteps.single (ub_rewindSkip_last block' c)
+  have h3 := Relation.RelatesWithinSteps.single (ub_rewindSkip_to_block block' c)
+  have h4 := Relation.RelatesWithinSteps.of_relatesInSteps
+    (ub_rewindBlock_phase block' [c] (by simp))
+  have h5 := Relation.RelatesWithinSteps.single (ub_rewindBlock_mk1 (block' ++ [c]) (by simp))
+  have h6 := Relation.RelatesWithinSteps.single (ub_rewindBlock_final (block' ++ [c]))
+  have := h1.trans (h2.trans (h3.trans (h4.trans (h5.trans h6))))
+  refine this.of_le ?_
+  simp only [List.length_append, List.length_singleton]
+  omega
+
+/-! #### Shuttle phase: the main loop -/
+
+/-- Step-count bound for the shuttle loop: with `j` output bits already deposited and `m` payload
+bits remaining, each round trip costs `2 * j + 5` steps and the final rewind `3 * j + 4`. -/
+private def ubLoopBound : ℕ → ℕ → ℕ
+  | j, 0 => 3 * j + 4
+  | j, m + 1 => (2 * j + 5) + ubLoopBound (j + 1) m
+
+private lemma ubLoopBound_closed : ∀ (m j : ℕ),
+    ubLoopBound j m = 2 * j * m + m * m + 7 * m + 3 * j + 4 := by
+  intro m
+  induction m with
+  | zero => intro j; simp [ubLoopBound]
+  | succ m ih =>
+    intro j
+    simp only [ubLoopBound, ih (j + 1)]
+    ring
+
+open Relation in
+/-- The shuttle loop: with nonempty output `out` deposited and the gap sized `out.length`,
+process the remaining well-formed input `delimit P` and halt on `out ++ P`. -/
+private lemma ub_loop : ∀ (P out : List Bool), out ≠ [] →
+    RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .seekInput, shuttleTape 0 (out.length - 1) out (BitstringEncoding.delimit P)⟩
+      ⟨none, BiTape.mk₁ (out ++ P)⟩ (ubLoopBound out.length P.length) := by
+  intro P
+  induction P with
+  | nil =>
+    intro out hout
+    have hjpos : 1 ≤ out.length := List.length_pos_of_ne_nil hout
+    rw [delimit_nil, List.append_nil]
+    have h1 := RelatesWithinSteps.of_relatesInSteps
+      (ub_seek_phase (out.length - 1) 0 out [false])
+    rw [show 0 + (out.length - 1) + 1 = out.length by omega] at h1
+    have h2 := RelatesWithinSteps.single (ub_seek_false out.length out)
+    have h3 := ub_rewind out.length out hout
+    have hchain := h1.trans (h2.trans h3)
+    refine hchain.of_le ?_
+    simp only [ubLoopBound, List.length_nil]
+    omega
+  | cons b P'' ih =>
+    intro out hout
+    have hjpos : 1 ≤ out.length := List.length_pos_of_ne_nil hout
+    rw [delimit_cons]
+    have h1 := RelatesWithinSteps.of_relatesInSteps
+      (ub_seek_phase (out.length - 1) 0 out (true :: b :: BitstringEncoding.delimit P''))
+    rw [show 0 + (out.length - 1) + 1 = out.length by omega] at h1
+    have h2 := RelatesWithinSteps.single
+      (ub_seek_true out.length out b (BitstringEncoding.delimit P''))
+    have h3 := RelatesWithinSteps.single
+      (ub_grab out.length out b (BitstringEncoding.delimit P''))
+    have h4 := RelatesWithinSteps.of_relatesInSteps
+      (ub_carry_phase out.length 1 b out (BitstringEncoding.delimit P''))
+    have h5 := ub_carry_turn b (out.length + 1) out (BitstringEncoding.delimit P'') hout
+    have h6 := RelatesWithinSteps.single
+      (ub_deposit b out.length out (BitstringEncoding.delimit P''))
+    have h7 := ih (out ++ [b]) (by simp)
+    rw [show (out ++ [b]).length - 1 = out.length by simp] at h7
+    have hchain := h1.trans (h2.trans (h3.trans (h4.trans (h5.trans (h6.trans h7)))))
+    rw [show out ++ [b] ++ P'' = out ++ b :: P'' by simp] at hchain
+    refine hchain.of_le ?_
+    simp only [ubLoopBound, List.length_cons, List.length_append, List.length_nil, Nat.zero_add]
+    omega
+
+open Relation in
+/-- The full shuttle phase: on a well-formed block `delimit P`, halt on `P`. -/
+private lemma ub_shuttle (P : List Bool) :
+    RelatesWithinSteps undelimitBlockComputer.TransitionRelation
+      ⟨some .initTrue, BiTape.mk₁ (BitstringEncoding.delimit P)⟩
+      ⟨none, BiTape.mk₁ P⟩ (P.length * P.length + 7 * P.length + 2) := by
+  match P with
+  | [] =>
+    rw [delimit_nil]
+    have hchain := (RelatesWithinSteps.single ub_initTrue_false).trans
+      (RelatesWithinSteps.single ub_eraseAll_halt)
+    refine hchain.of_le ?_
+    simp
+  | p :: P' =>
+    rw [delimit_cons]
+    have h0 := RelatesWithinSteps.single (ub_init_true p (BitstringEncoding.delimit P'))
+    have h1 := RelatesWithinSteps.single (ub_init_bit p (BitstringEncoding.delimit P'))
+    have h2 := RelatesWithinSteps.single (ub_deposit p 0 [] (BitstringEncoding.delimit P'))
+    rw [List.nil_append] at h2
+    have h3 := ub_loop P' [p] (by simp)
+    rw [show ([p] : List Bool).length - 1 = 0 from rfl] at h3
+    have hchain := h0.trans (h1.trans (h2.trans h3))
+    rw [List.singleton_append] at hchain
+    refine hchain.of_le (le_of_eq ?_)
+    rw [ubLoopBound_closed]
+    simp only [List.length_cons, List.length_nil]
+    ring
+
+open Relation Polynomial in
+/-- `undelimitBlock` is computable in polynomial time: `undelimitBlockComputer` computes it
+within `2 * n ^ 2 + 10 * n + 16` steps. -/
+theorem PolyTimeComputable_undelimitBlock :
+    Nonempty (Cslib.Turing.SingleTapeTM.PolyTimeComputable undelimitBlock) :=
+  ⟨{ tm := undelimitBlockComputer
+     timeBound := fun n => 2 * (n * n) + 10 * n + 16
+     poly := C 2 * X ^ 2 + C 10 * X + C 16
+     bounds := fun n => by
+       simp only [eval_add, eval_mul, eval_C, eval_X, pow_two]
+       omega
+     outputsFunInTime := fun a => by
+       simp only [OutputsWithinTime, initCfg, haltCfg]
+       have h1 := nm_phase a
+       have h2 := ub_shuttle (undelimitBlock a)
+       have hlen := undelimitBlock_length_le a.length a rfl
+       refine (h1.trans h2).of_le ?_
+       have hsq : 4 * ((undelimitBlock a).length * (undelimitBlock a).length)
+           ≤ a.length * a.length := by
+         calc 4 * ((undelimitBlock a).length * (undelimitBlock a).length)
+             = (2 * (undelimitBlock a).length) * (2 * (undelimitBlock a).length) := by ring
+           _ ≤ a.length * a.length := Nat.mul_le_mul hlen hlen
+       have key : ∀ s n A B : ℕ, 2 * s ≤ n → 4 * A ≤ B →
+           2 * n + 6 + (A + 7 * s + 2) ≤ 2 * B + 10 * n + 16 := by
+         intro s n A B hsn hAB
+         omega
+       exact key _ _ _ _ hlen hsq } ⟩
+
+end ComplexityTheory
diff --git a/Cslib/Foundations/Data/BitstringEncoding.lean b/Cslib/Foundations/Data/BitstringEncoding.lean
new file mode 100644
index 000000000..8aafd1bf3
--- /dev/null
+++ b/Cslib/Foundations/Data/BitstringEncoding.lean
@@ -0,0 +1,312 @@
+/-
+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 Mathlib.Computability.Encoding
+public import Mathlib.Data.List.SplitOn
+public import Mathlib.Algebra.Field.Rat
+
+/-!
+# Bitstring Encodings
+
+This section provides a type`class`-inferrable version of Mathlib's `Computability.Encoding`,
+specialized to the alphabet `Bool`.
+(Note that `Computability.Encoding` itself has undergone a rewrite recently.)
+
+Making it a `class` makes it easier to quickly ask if a function is computable in polynomial time,
+without having to explicitly pass around the encoding.
+
+The idea of this class is to set up instances for common types like Bool, ℕ, ℤ, ℚ,
+and instance derivations for product and list types,
+so that the resulting instance for any common type will be polytime-transcodable
+with any other reasonable binary encoding of that type.
+
+Thus, while it may not be obvious without looking carefully
+which of several essentially equivalent encodings of a type is being used,
+we can at least be sure that for functions between types with `BitstringEncoding` instances,
+questions of polynomial-time computability are well-defined, in the sense that
+the formalization will capture the intended meaning.
+-/
+
+@[expose] public section
+
+open Computability
+
+/-- A canonical encoding of a type as bitstrings (`List Bool`).
+
+This is a class version of Mathlib's (bundled) `Computability.Encoding`, specialized to the
+alphabet `Bool`. -/
+class BitstringEncoding (α : Type*) where
+  /-- The encoding function. -/
+  encode : α → List Bool
+  /-- The decoding function; `none` on bitstrings that encode nothing. -/
+  decode : List Bool → Option α
+  /-- Decoding is a left inverse of encoding. -/
+  decode_encode : ∀ x, decode (encode x) = some x
+
+attribute [simp] BitstringEncoding.decode_encode
+
+namespace BitstringEncoding
+
+variable {α β : Type*}
+
+theorem encode_injective [BitstringEncoding α] :
+    Function.Injective (encode : α → List Bool) := fun _ _ h =>
+  Option.some_injective _ (by rw [← decode_encode, ← decode_encode, h])
+
+/-- Transport a `BitstringEncoding` along an injection `f` with partial inverse `g`. -/
+@[reducible]
+def ofLeftInverse [BitstringEncoding β] (f : α → β) (g : β → Option α)
+    (h : ∀ x, g (f x) = some x) : BitstringEncoding α where
+  encode a := encode (f a)
+  decode l := (decode l).bind g
+  decode_encode a := by simp [h]
+
+/- ## Ground instances -/
+
+/-- `ℕ` is encoded by its (little-endian) binary representation, as in
+`Computability.encodeNat`. -/
+instance : BitstringEncoding ℕ where
+  encode := Computability.encodeNat
+  decode l := some (Computability.decodeNat l)
+  decode_encode n := congrArg some (Computability.decode_encodeNat n)
+
+/-- `Bool` is encoded as a singleton bitstring. -/
+instance : BitstringEncoding Bool where
+  encode b := [b]
+  decode l := match l with
+    | [b] => some b
+    | _ => none
+  decode_encode _ := rfl
+
+/-- `Unit` is encoded as the empty bitstring. This is the tensor unit for the pair encoding:
+`encode ((), x) = false :: encode x` and `encode (x, ()) = delimit (encode x)`. -/
+instance : BitstringEncoding Unit where
+  encode _ := []
+  decode l := match l with
+    | [] => some ()
+    | _ => none
+  decode_encode _ := rfl
+
+/- ## Self-delimiting blocks
+
+To concatenate encodings of multipartite data structures,
+we need each piece to announce its own end.
+`delimit` writes each payload bit `b` as `true :: b :: ·` and terminates with `false`;
+`undelimit` parses one such block off the front of the input. -/
+
+/-- Make a bitstring self-delimiting: each payload bit `b` becomes the two bits
+`[true, b]`, and the block is terminated by `false`. -/
+def delimit : List Bool → List Bool
+  | [] => [false]
+  | b :: l => true :: b :: delimit l
+
+/-- Parse one self-delimiting block from the front of the input, returning the payload
+and the remaining input. -/
+def undelimit : List Bool → Option (List Bool × List Bool)
+  | false :: rest => some ([], rest)
+  | true :: b :: input => (undelimit input).map fun p => (b :: p.1, p.2)
+  | _ => none
+
+@[simp]
+theorem undelimit_delimit (l rest : List Bool) :
+    undelimit (delimit l ++ rest) = some (l, rest) := by
+  induction l with
+  | nil => rfl
+  | cons b l ih => simp [delimit, undelimit, ih]
+
+@[simp]
+theorem delimit_length (l : List Bool) : (delimit l).length = 2 * l.length + 1 := by
+  induction l with
+  | nil => rfl
+  | cons b l ih => simp [delimit, ih]; omega
+
+/-- Strip the framing of a single self-delimiting block, returning its payload. On `delimit P`
+this returns `P`. Unlike `undelimit`, this is total: it ignores any data trailing the first block
+and maps malformed input to `[]`. -/
+def undelimitBlock : List Bool → List Bool
+  | [] => []
+  | false :: _ => []
+  | true :: b :: rest => b :: undelimitBlock rest
+  | [true] => []
+
+@[simp]
+theorem undelimitBlock_delimit (P : List Bool) :
+    undelimitBlock (delimit P) = P := by
+  induction P with
+  | nil => rfl
+  | cons b P ih => simp only [delimit, undelimitBlock, ih]
+
+/-- Parse a sequence of self-delimiting blocks, using `fuel` to bound the number of blocks.
+
+This is the auxiliary, fuel-carrying implementation of `undelimitBlocks`; since every block
+is nonempty, `input.length` is always enough fuel. -/
+def undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))
+  | _, [] => some []
+  | 0, _ :: _ => none
+  | fuel + 1, input => do
+    let (block, rest) ← undelimit input
+    let blocks ← undelimitBlocksAux fuel rest
+    return block :: blocks
+
+/-- Parse a sequence of self-delimiting blocks off the front of the input.
+
+Since every block is nonempty, `input.length` bounds the number of blocks, so it always
+suffices as fuel for `undelimitBlocksAux`. -/
+def undelimitBlocks (input : List Bool) : Option (List (List Bool)) :=
+  undelimitBlocksAux input.length input
+
+theorem length_le_length_flatten_delimit (l : List (List Bool)) :
+    l.length ≤ ((l.map delimit).flatten).length := by
+  induction l with
+  | nil => simp
+  | cons b t ih =>
+    simp only [List.map_cons, List.flatten_cons, List.length_append, List.length_cons,
+      delimit_length]
+    omega
+
+private theorem undelimitBlocksAux_flatten_delimit (l : List (List Bool)) :
+    ∀ fuel, l.length ≤ fuel → undelimitBlocksAux fuel ((l.map delimit).flatten) = some l := by
+  induction l with
+  | nil => intro fuel _; cases fuel <;> rfl
+  | cons b t ih =>
+    intro fuel hfuel
+    rw [List.length_cons] at hfuel
+    obtain ⟨fuel, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩
+    obtain ⟨hd, tl, hcons⟩ : ∃ hd tl, delimit b ++ (t.map delimit).flatten = hd :: tl := by
+      cases b <;> exact ⟨_, _, rfl⟩
+    simp only [List.map_cons, List.flatten_cons, hcons, undelimitBlocksAux]
+    rw [← hcons, undelimit_delimit]
+    simp [ih fuel (by omega)]
+
+theorem undelimitBlocks_flatten_delimit (l : List (List Bool)) :
+    undelimitBlocks ((l.map delimit).flatten) = some l :=
+  undelimitBlocksAux_flatten_delimit l _ (length_le_length_flatten_delimit l)
+
+/-- Decode every block in a list of bitstrings, failing if any block fails to decode.
+
+(This is `List.mapM decode` in the `Option` monad, written out by hand so that it works
+for `α` in any universe.) -/
+def decodeAll [BitstringEncoding α] : List (List Bool) → Option (List α)
+  | [] => some []
+  | b :: t =>
+    match decode b, decodeAll t with
+    | some a, some l => some (a :: l)
+    | _, _ => none
+
+@[simp]
+theorem decodeAll_map_encode [BitstringEncoding α] (l : List α) :
+    decodeAll (l.map encode) = some l := by
+  induction l with
+  | nil => rfl
+  | cons a t ih => simp [decodeAll, ih]
+
+/- ## Derived instances -/
+
+/--
+An encoding of `Option α` is obtained encoding `none` as the empty bitstring
+and `some a` as the encoding of `a` prefixed by a `true`.
+-/
+instance [BitstringEncoding α] : BitstringEncoding (Option α) where
+  encode
+    | none => []
+    | some a => true :: encode a
+  decode input :=
+    match input with
+    | [] => some none
+    | true :: rest => (decode rest).map some
+    | false :: _ => none
+  decode_encode
+    | none => rfl
+    | some a => by simp
+
+/-- Decode a bitstring as a pair: parse one self-delimiting block off the front for the first
+component, and decode the remainder as the second. This is the `decode` of the `α × β` instance,
+given as a standalone definition so that it can be unfolded and reasoned about by name. -/
+def decodePair [BitstringEncoding α] [BitstringEncoding β] (input : List Bool) : Option (α × β) :=
+  match undelimit input with
+  | none => none
+  | some (block, rest) =>
+    match decode block, decode rest with
+    | some a, some b => some (a, b)
+    | _, _ => none
+
+/-- A pair is encoded as a self-delimiting block for the first component followed by the
+encoding of the second. -/
+instance [BitstringEncoding α] [BitstringEncoding β] : BitstringEncoding (α × β) where
+  encode p := delimit (encode p.1) ++ encode p.2
+  decode := decodePair
+  decode_encode p := by simp [decodePair]
+
+theorem decode_prod_eq_decodePair [BitstringEncoding α] [BitstringEncoding β] :
+    (decode : List Bool → Option (α × β)) = decodePair := rfl
+
+/-- A list is encoded as the concatenation of self-delimiting blocks for its elements. -/
+instance [BitstringEncoding α] : BitstringEncoding (List α) where
+  encode l := ((l.map encode).map delimit).flatten
+  decode input :=
+    match undelimitBlocks input with
+    | none => none
+    | some blocks => decodeAll blocks
+  decode_encode l := by
+    rw [undelimitBlocks_flatten_delimit (l.map encode)]
+    exact decodeAll_map_encode l
+
+/-- A bitstring: definitionally `List Bool`, but kept as a distinct (semireducible) type-level
+name so that it can carry the identity `BitstringEncoding` without overlapping the generic
+`List α` instance.
+
+Data that is conceptually a raw bitstring should be typed as `Bitstring`, and is encoded as
+itself; a `List Bool` that is conceptually a list which happens to contain booleans keeps the
+generic self-delimiting list encoding (three bits per element). Because `Bitstring` is not
+reducible, instance search never sees through it, so the two encodings cannot be confused: a
+lemma about the generic `List α` encoding instantiated at `α := Bool` and a lemma about
+`Bitstring` can never silently disagree about which encoding is meant. -/
+def _root_.Bitstring : Type := List Bool
+
+/-- A bitstring is encoded as itself. -/
+instance : BitstringEncoding Bitstring where
+  encode := id
+  decode := some
+  decode_encode _ := rfl
+
+/-- Convert a `List Bool` to a `Bitstring`. Definitionally the identity; useful for stating
+lemmas that mix the two types without relying on definitional unfolding. -/
+def _root_.Bitstring.ofList (l : List Bool) : Bitstring := l
+
+/-- Convert a `Bitstring` to a `List Bool`. Definitionally the identity. -/
+def _root_.Bitstring.toList (l : Bitstring) : List Bool := l
+
+@[simp]
+theorem encode_ofList (l : List Bool) : encode (Bitstring.ofList l) = l := rfl
+
+theorem decode_bitstring (l : List Bool) :
+    (decode l : Option Bitstring) = some (Bitstring.ofList l) := rfl
+
+/-- A subtype inherits the encoding of the ambient type; decoding additionally checks the
+defining predicate. This yields encodings for `ℕ+` and friends for free. -/
+instance {p : α → Prop} [BitstringEncoding α] [DecidablePred p] :
+    BitstringEncoding (Subtype p) where
+  encode x := encode x.val
+  decode input := (decode input).bind fun a => if h : p a then some ⟨a, h⟩ else none
+  decode_encode x := by simp [x.property]
+
+/-- `ℕ+` is encoded as the subtype `{n : ℕ // 0 < n}` it is defined to be. -/
+instance : BitstringEncoding ℕ+ :=
+  inferInstanceAs (BitstringEncoding {n : ℕ // 0 < n})
+
+/-- `ℤ` is encoded via the pair `(n.toNat, (-n).toNat)` (one component is always `0`). -/
+instance : BitstringEncoding ℤ :=
+  ofLeftInverse (fun n : ℤ => (n.toNat, (-n).toNat))
+    (fun p => some ((p.1 : ℤ) - (p.2 : ℤ))) (fun n => congrArg some (by dsimp only; omega))
+
+/-- `ℚ` is encoded as its (reduced) numerator-denominator pair. -/
+instance : BitstringEncoding ℚ :=
+  ofLeftInverse (fun q : ℚ => (q.num, q.den))
+    (fun p => some ((p.1 : ℚ) / (p.2 : ℚ))) (fun q => by simp [Rat.num_div_den])
+
+end BitstringEncoding
diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean
index 2cd556ecf..254f23249 100644
--- a/Cslib/Foundations/Data/StackTape.lean
+++ b/Cslib/Foundations/Data/StackTape.lean
@@ -141,6 +141,35 @@ lemma cons_head_tail (l : StackTape Symbol) :
 @[scoped grind]
 def mapSome (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩
 
+@[simp]
+lemma mapSome_head (l : List Symbol) : (mapSome l).head = l.head? := by
+  cases l <;> rfl
+
+@[simp]
+lemma mapSome_tail (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by
+  cases l <;> rfl
+
+@[simp]
+lemma cons_some_mapSome (a : Symbol) (l : List Symbol) :
+    cons (some a) (mapSome l) = mapSome (a :: l) := rfl
+
+@[simp]
+lemma cons_head?_mapSome (l : List Symbol) :
+    cons l.head? (mapSome l.tail) = mapSome l := by
+  cases l <;> rfl
+
+@[simp]
+lemma cons_none_empty : cons none (∅ : StackTape Symbol) = ∅ := rfl
+
+@[simp]
+lemma mapSome_nil : mapSome ([] : List Symbol) = ∅ := rfl
+
+@[simp]
+lemma empty_head : (∅ : StackTape Symbol).head = none := rfl
+
+@[simp]
+lemma empty_tail : (∅ : StackTape Symbol).tail = ∅ := rfl
+
 section Length
 
 /-- The length of the `StackTape` is the number of elements up to the last non-`none` element -/