diff --git a/Complexity.lean b/Complexity.lean
index 312878daa..1c4a9384d 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1433,6 +1433,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Str
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyZeroSpace
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Transducer
+public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.ZipTransducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Bounds
@@ -1641,6 +1642,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.Kernel
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelOnWords
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZeroSpace
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZipTransducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.LinearCodecPrimitives
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.LinearPairPrimitives
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.LinearPrimitives
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Combinators/ZipTransducer.lean b/Complexity/Computability/Machines/Turing/MultiTape/Combinators/ZipTransducer.lean
new file mode 100644
index 000000000..929f38b40
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Combinators/ZipTransducer.lean
@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZipTransducer
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds
+
+/-!
+# Zip transducers
+
+A zip transducer (`Turing.MultiTapeTM.ZipTransducer`) reads two binary words in lockstep, least
+significant digit first, padding the shorter word with `none`. In state `q`, on the pair `(x, y)`
+of next digits, it moves to state `(τ.step q (x, y)).1` and emits `(τ.step q (x, y)).2`; when both
+words are exhausted it emits `τ.final q`. Every emitted word has length at most two.
+
+On a pair `(a, b)` encoded as `frame (enc₁ a) ++ enc₂ b`, the machine `τ.toTM` copies `enc₁ a` to
+its work tape and then reads both words simultaneously. Every two-operand function whose encoded
+value is the output of a zip transducer on the encoded operands is therefore computable in time
+linear in the encoded pair and in work space linear in the first operand.
+
+## Main results
+
+* `Turing.MultiTapeTM.ZipTransducer.computableInTimeAndSpace`: a function computed by a zip
+  transducer with finitely many states on the encoded components of a pair is computable within
+  `3 * (encPair enc₁ enc₂ p).length + 1` steps and `(enc₁ p.1).length + 2` work-tape cells.
+* `Turing.MultiTapeTM.ZipTransducer.computableInTimeAndSpace_run`: the same on raw words.
+* `Turing.MultiTapeTM.ZipTransducer.computableInLinearTimeAndSpace`,
+  `Turing.MultiTapeTM.ZipTransducer.computableInDegree`: its linear and degree-one forms.
+-/
+
+namespace Turing.MultiTapeTM
+
+namespace ZipTransducer
+
+universe u
+
+variable {Q : Type} [Finite Q] (τ : ZipTransducer Q) {α β γ : Type u}
+  {enc₁ : α ↪ List Bool} {enc₂ : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : α × β → γ}
+
+/-- **Two-operand functions computed by a zip transducer.** If the encoded value of `f p` is what
+`τ` emits on the encoded components of `p`, then `f` is computable within
+`3 * (encPair enc₁ enc₂ p).length + 1` steps and `(enc₁ p.1).length + 2` work-tape cells. -/
+public theorem computableInTimeAndSpace
+    (hf : ∀ p, encOut (f p) = τ.run τ.q₀ (enc₁ p.1) (enc₂ p.2)) :
+    ComputableInTimeAndSpace f (encPair enc₁ enc₂) encOut
+      (fun p => 3 * (encPair enc₁ enc₂ p).length + 1) (fun p => (enc₁ p.1).length + 2) :=
+  ⟨1, State Q, inferInstance, τ.toTM, fun p => by
+    rw [hf p, encPair_apply]
+    exact τ.computesInTimeAndSpace_toTM (enc₁ p.1) (enc₂ p.2)⟩
+
+/-- `τ` on raw words: on `frame u ++ v` it emits `τ.run τ.q₀ u v` within
+`3 * (frame u ++ v).length + 1` steps and `u.length + 2` work-tape cells. -/
+public theorem computableInTimeAndSpace_run :
+    ComputableInTimeAndSpace (fun p : List Bool × List Bool => τ.run τ.q₀ p.1 p.2)
+      (encPair encBits encBits) encBits
+      (fun p => 3 * (encPair encBits encBits p).length + 1) (fun p => p.1.length + 2) :=
+  τ.computableInTimeAndSpace fun _ => rfl
+
+/-- A function computed by a zip transducer is computable in linear time and work space. -/
+public theorem computableInLinearTimeAndSpace
+    (hf : ∀ p, encOut (f p) = τ.run τ.q₀ (enc₁ p.1) (enc₂ p.2)) :
+    ComputableInLinearTimeAndSpace f (encPair enc₁ enc₂) encOut :=
+  ⟨3, (τ.computableInTimeAndSpace hf).mono (fun _ => by omega) fun p => by
+    have := length_le_encPair_left enc₁ enc₂ p
+    omega⟩
+
+/-- A function computed by a zip transducer has cost and output degree one. -/
+public theorem computableInDegree
+    (hf : ∀ p, encOut (f p) = τ.run τ.q₀ (enc₁ p.1) (enc₂ p.2)) :
+    ComputableInDegree f (encPair enc₁ enc₂) encOut 1 1 :=
+  let ⟨c, hc⟩ := τ.computableInLinearTimeAndSpace hf
+  ComputableInDegree.of_bounds ⟨c, fun _ => by simp⟩ ⟨c, fun _ => by simp⟩ hc
+
+end ZipTransducer
+
+end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean
index c50c101e5..a9dfc7aef 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Nat/Binary.lean
@@ -34,9 +34,8 @@ multiplication are Christian Reitwiessner's degree-bounded
 machines (`Turing.MultiTapeTM.computableTidilyInDegree_add`,
 `Turing.MultiTapeTM.computableTidilyInDegree_mul`). A list is summed by a left fold whose
 accumulator grows by at most one digit more than the length of the element added. Powers of two are
-computed from a unary exponent by repeated doubling. Strict comparison scans bit positions: `m < n`
-exactly when some position holds a one in `n` and a zero in `m` and all higher positions agree
-(`Nat.lt_of_testBit`); the scan is quadratic in the number of digits. The verifiers and reductions
+computed from a unary exponent by repeated doubling. Strict comparison is the linear-time zip
+transducer of `Turing.MultiTapeTM.computableInTimeAndSpace_natLt`. The verifiers and reductions
 of the number problems (`Cslib.Complexity.SubsetSum` and its relatives) are built from these.
 
 Truncated subtraction is schoolbook subtraction: a left fold over the digit pairs of both operands
@@ -240,31 +239,11 @@ theorem binary_two_pow : ComputableTidilyInPolyTime (fun k : ℕ => 2 ^ k) encUn
       lia)
   simpa only [hfold] using h
 
-/-- Strict comparison of binary naturals by scanning bit positions. -/
+/-- Strict comparison of binary naturals, from the linear zip-transducer certificate. -/
 @[fun_prop]
 theorem binary_lt : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => decide (p.1 < p.2))
-    (encPair encNat encNat) encBool := by
-  have hscan : ComputableTidilyInPolyTime (fun p : ℕ × ℕ =>
-      (List.range p.2.bits.length).any fun i =>
-        !p.1.bits.getD i false && p.2.bits.getD i false &&
-          (List.range (p.1.bits.length + p.2.bits.length)).all fun j =>
-            decide (j ≤ i) || p.1.bits.getD j false == p.2.bits.getD j false)
-      (encPair encNat encNat) encBool := by
-    apply anyWithInput (by fun_prop)
-    refine bool_and' (by fun_prop) ?_
-    apply allWithInput (by fun_prop)
-    fun_prop
-  refine hscan.of_enc_eq fun p => congrArg encBool ?_
-  have hbit (k i : ℕ) : k.bits.getD i false = k.testBit i := by
-    rw [Nat.testBit_eq_inth, ← List.getD_default_eq_getI]
-    rfl
-  rw [Bool.eq_iff_iff, decide_eq_true_iff, Nat.lt_iff_exists_testBit]
-  simp only [hbit, Nat.size_eq_bits_len, List.any_eq_true, List.mem_range, Bool.and_eq_true,
-    Bool.not_eq_true', List.all_eq_true, Bool.or_eq_true, decide_eq_true_eq, beq_iff_eq]
-  refine exists_congr fun i => and_congr_right fun _ => ?_
-  rw [and_assoc]
-  refine and_congr_right fun _ => and_congr_right fun _ => forall₂_congr fun j _ => ?_
-  rw [← Nat.not_le, imp_iff_not_or, not_not]
+    (encPair encNat encNat) encBool :=
+  ComputableInPolyTime.binary_lt.tidy
 
 /-- Comparison of binary naturals. -/
 @[fun_prop]
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryComparison.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryComparison.lean
index 674063f40..2901bb2b8 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryComparison.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryComparison.lean
@@ -15,22 +15,86 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeComposi
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Subtraction
 import Mathlib.Tactic.Linarith
+import Complexity.Computability.Machines.Turing.MultiTape.Combinators.ZipTransducer
 
-/-! # Quadratic schoolbook binary subtraction and comparison
+/-! # Binary subtraction and comparison
 
 The existing borrow algorithm runs through consuming input-word cursors, so every round costs
 only a linear amount and there are at most as many rounds as input digits. The plain machine
 certificate retains quadratic time and linear output-charged workspace, independently of the
-numeric operands. Comparison tests that same result; no qualitative polynomial-time bridge is
-used to establish either resource bound.
+numeric operands.
+
+Comparison is computed by one zip transducer (`Turing.MultiTapeTM.ZipTransducer`) that reads both
+operands in lockstep, least significant digit first, and remembers whether the digits read so far
+compare as less than. It runs in linear time and in work space linear in the first operand.
 
 ## Main results
 
 * `ComputableInO.natSub`: truncated subtraction in quadratic time and linear charged space.
-* `ComputableInO.natLt`: strict comparison with the same independent resource bounds.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_natLt`: strict comparison within
+  `3 * (encPair encNat encNat p).length + 1` steps and `(encNat p.1).length + 2` work-tape cells.
+* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natLt`: its linear form.
+* `ComputableInO.natLt`: strict comparison with the bounds of `ComputableInO.natSub`.
 -/
 
 @[expose] public section
+namespace Turing.MultiTapeTM
+
+/-- Strict comparison as a zip transducer. The state records whether the digits read so far,
+which are the low-order digits, compare as less than; a differing digit overrides it. -/
+private def ltZip : ZipTransducer Bool where
+  q₀ := false
+  step c x := (if x.1.getD false = x.2.getD false then c else x.2.getD false, [])
+  final c := [c]
+  length_step_le _ _ := by simp
+  length_final_le _ := by simp
+
+private lemma run_ltZip (c : Bool) (u v : List Bool) :
+    ltZip.run c u v = [decide (ofBits u < ofBits v ∨ ofBits u = ofBits v ∧ c = true)] := by
+  induction u generalizing v c with
+  | nil =>
+    induction v generalizing c with
+    | nil => cases c <;> simp [ltZip, ofBits]
+    | cons b v ih =>
+      rw [ZipTransducer.run_nil_cons, ih]
+      simp only [ltZip, ofBits, List.foldr_cons, List.foldr_nil, Nat.bit_val, List.nil_append,
+        List.cons.injEq, and_true, decide_eq_decide]
+      cases b <;> cases c <;> simp <;> omega
+  | cons a u ih =>
+    cases v with
+    | nil =>
+      rw [ZipTransducer.run_cons_nil, ih]
+      simp only [ltZip, ofBits, List.foldr_cons, List.foldr_nil, Nat.bit_val, List.nil_append,
+        List.cons.injEq, and_true, decide_eq_decide]
+      cases a <;> cases c <;> simp
+    | cons b v =>
+      rw [ZipTransducer.run_cons_cons, ih]
+      simp only [ltZip, ofBits, List.foldr_cons, Nat.bit_val, List.nil_append,
+        List.cons.injEq, and_true, decide_eq_decide]
+      cases a <;> cases b <;> cases c <;> simp <;> omega
+
+private lemma encBool_natLt (p : ℕ × ℕ) :
+    encBool (decide (p.1 < p.2)) = ltZip.run ltZip.q₀ (encNat p.1) (encNat p.2) := by
+  have h (n : ℕ) : ofBits n.bits = n := Nat.foldr_bit_bits n
+  rw [encBool_apply, encNat_apply, encNat_apply, run_ltZip, h, h]
+  simp [ltZip]
+
+/-- **Binary comparison in linear time.** One zip transducer decides `a < b` from
+`encPair encNat encNat (a, b)` within `3 * (encPair encNat encNat p).length + 1` steps and
+`(encNat p.1).length + 2` work-tape cells. -/
+public theorem computableInTimeAndSpace_natLt :
+    ComputableInTimeAndSpace (fun p : ℕ × ℕ => decide (p.1 < p.2)) (encPair encNat encNat) encBool
+      (fun p => 3 * (encPair encNat encNat p).length + 1) (fun p => (encNat p.1).length + 2) :=
+  ltZip.computableInTimeAndSpace encBool_natLt
+
+/-- Binary comparison in linear time and work space, from `computableInTimeAndSpace_natLt`. -/
+public theorem ComputableInLinearTimeAndSpace.natLt :
+    ComputableInLinearTimeAndSpace (fun p : ℕ × ℕ => decide (p.1 < p.2))
+      (encPair encNat encNat) encBool :=
+  ltZip.computableInLinearTimeAndSpace encBool_natLt
+
+end Turing.MultiTapeTM
+
 namespace Turing.MultiTapeTM.ComputableInO
 
 private abbrev encCursor :=
@@ -124,18 +188,14 @@ public theorem natSub :
     rw [heq]
     exact congrArg encNat (BinarySub.sub_eq (p.2, p.1))
 
-/-- **The strict order in binary.** -/
+/-- **The strict order in binary**, from the linear zip-transducer certificate
+`Turing.MultiTapeTM.computableInTimeAndSpace_natLt`. -/
 public theorem natLt :
     ComputableInO (fun p : ℕ × ℕ => decide (p.1 < p.2)) (encPair encNat encNat) encBool
       (fun p => ((encPair encNat encNat p).length + 1) ^ 2)
-      fun p => (encPair encNat encNat p).length + 1 := by
-  have hnot : ComputableInO (fun b : Bool => !b) encBool encBool
-      (fun b => (encBool b).length) fun b => (encBool b).length :=
-    (ComputableInDegree.of_finite (encIn := encBool) (encMid := encBool) _).inO_one
-  refine (hnot.comp_linear (natIsZero.comp_linear natSub)).of_enc_eq fun p => ?_
-  simp only [Function.comp_apply]
-  congr 1
-  by_cases h : p.1 < p.2 <;> simp [h] <;> omega
-
+      fun p => (encPair encNat encNat p).length + 1 :=
+  (of_linear ComputableInLinearTimeAndSpace.natLt).mono 1
+    (fun p => by have := Nat.le_self_pow two_ne_zero ((encPair encNat encNat p).length + 1); omega)
+    (fun _ => by omega)
 
 end Turing.MultiTapeTM.ComputableInO
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
index 6b969c3a0..4b8c5588b 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
@@ -70,7 +70,7 @@ public def toTM : MultiTapeTM 0 Symbol (Q × Option Symbol × Bool) :=
           state := some (q, (τ.final q).tail.head?, true) }
 
 /-- A word of length at most two is its head followed by the head of its tail. -/
-lemma toList_head?_append {w : List Symbol} (h : w.length ≤ 2) :
+public lemma toList_head?_append {w : List Symbol} (h : w.length ≤ 2) :
     w.head?.toList ++ w.tail.head?.toList = w := by
   match w, h with
   | [], _ => rfl
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean
new file mode 100644
index 000000000..5cd4d841c
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean
@@ -0,0 +1,598 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Run
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic
+public import Mathlib.Data.Fintype.Option
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
+import Mathlib.Basic.Finite.Prod
+import Mathlib.Basic.Finite.Sum
+
+/-! # Zip transducers and their machine semantics
+
+A zip transducer reads two binary words in lockstep, least significant digit first, padding the
+shorter one with `none`. Its machine `ZipTransducer.toTM` reads `frame u ++ v` from the input
+tape: it copies `u` to its single work tape, rewinds that tape and then reads `v` on the input
+tape and `u` on the work tape simultaneously. It runs in time linear in the input and uses
+`u.length + 2` work-tape cells.
+
+## Main definitions
+
+* `Turing.MultiTapeTM.ZipTransducer`: finite-state transducers on pairs of optional bits.
+* `Turing.MultiTapeTM.ZipTransducer.run`: the word a zip transducer emits on two words.
+* `Turing.MultiTapeTM.ZipTransducer.toTM`: the zip transducer as a machine with one work tape.
+
+## Main results
+
+* `Turing.MultiTapeTM.ZipTransducer.computesInTimeAndSpace_toTM`: on `frame u ++ v`, `τ.toTM`
+  emits `τ.run τ.q₀ u v` within `3 * (frame u ++ v).length + 1` steps and `u.length + 2` cells.
+-/
+
+namespace Turing.MultiTapeTM
+
+/-- A finite-state transducer reading two words in lockstep. In state `q`, on the pair `(x, y)` of
+the next digits of the two words, where `none` pads the shorter word, it moves to
+`(step q (x, y)).1` and emits `(step q (x, y)).2`; when both words are exhausted it emits
+`final q`. The value of `step` on `(none, none)` is never used. -/
+public structure ZipTransducer (Q : Type*) where
+  /-- The initial state. -/
+  q₀ : Q
+  /-- The successor state and the emitted word on reading a pair of digits. -/
+  step : Q → Option Bool × Option Bool → Q × List Bool
+  /-- The word emitted when both words are exhausted. -/
+  final : Q → List Bool
+  /-- At most two symbols are emitted per pair of digits. -/
+  length_step_le : ∀ q x, (step q x).2.length ≤ 2
+  /-- At most two symbols are emitted at the end. -/
+  length_final_le : ∀ q, (final q).length ≤ 2
+
+namespace ZipTransducer
+
+variable {Q : Type*} (τ : ZipTransducer Q)
+
+/-- The word `τ` emits on the words `u` and `v`, started in state `q`. -/
+public def run (q : Q) : List Bool → List Bool → List Bool
+  | [], [] => τ.final q
+  | a :: u, [] => (τ.step q (some a, none)).2 ++ run (τ.step q (some a, none)).1 u []
+  | [], b :: v => (τ.step q (none, some b)).2 ++ run (τ.step q (none, some b)).1 [] v
+  | a :: u, b :: v => (τ.step q (some a, some b)).2 ++ run (τ.step q (some a, some b)).1 u v
+
+@[simp]
+public lemma run_nil_nil (q : Q) : τ.run q [] [] = τ.final q := by
+  simp [run]
+
+@[simp]
+public lemma run_cons_nil (q : Q) (a : Bool) (u : List Bool) :
+    τ.run q (a :: u) [] =
+      (τ.step q (some a, none)).2 ++ τ.run (τ.step q (some a, none)).1 u [] := by
+  simp [run]
+
+@[simp]
+public lemma run_nil_cons (q : Q) (b : Bool) (v : List Bool) :
+    τ.run q [] (b :: v) =
+      (τ.step q (none, some b)).2 ++ τ.run (τ.step q (none, some b)).1 [] v := by
+  simp [run]
+
+@[simp]
+public lemma run_cons_cons (q : Q) (a b : Bool) (u v : List Bool) :
+    τ.run q (a :: u) (b :: v) =
+      (τ.step q (some a, some b)).2 ++ τ.run (τ.step q (some a, some b)).1 u v := by
+  simp [run]
+
+/-- Unless both words are exhausted, `τ` reads their first digits and continues on the rest. -/
+public lemma run_of_ne {q : Q} {u v : List Bool} (h : ¬(u = [] ∧ v = [])) :
+    τ.run q u v = (τ.step q (u.head?, v.head?)).2 ++
+      τ.run (τ.step q (u.head?, v.head?)).1 u.tail v.tail := by
+  cases u <;> cases v <;> simp_all
+
+/-- The control states of `ZipTransducer.toTM`. -/
+public inductive State (Q : Type*) where
+  /-- Expecting the next frame marker of the first word. -/
+  | copy
+  /-- Expecting the next digit of the first word, to be copied to the work tape. -/
+  | copyBit
+  /-- Moving the work head back to the start of the copied word. -/
+  | rewind
+  /-- Running `τ` in state `q`, with a pending output symbol. -/
+  | zip (q : Q) (pending : Option Bool)
+  /-- Emitting the last output symbol before halting. -/
+  | flush (b : Bool)
+
+/-- An encoding of the control states into a finite type. -/
+private def State.toSum {Q : Type*} : State Q → Fin 3 ⊕ (Q × Option Bool) ⊕ Bool
+  | .copy => .inl 0
+  | .copyBit => .inl 1
+  | .rewind => .inl 2
+  | .zip q p => .inr (.inl (q, p))
+  | .flush b => .inr (.inr b)
+
+/-- With finitely many states of the transducer, the machine has finitely many states. -/
+public instance State.instFinite {Q : Type*} [Finite Q] : Finite (State Q) :=
+  Finite.of_injective State.toSum fun a b h => by
+    cases a <;> cases b <;> simp_all [State.toSum]
+
+/-- The action that halts without moving or writing. -/
+private def haltAction {Q : Type*} : Action 1 Bool (State Q) :=
+  { inputTape := 0, workTapes := fun _ => (none, 0), output := none, state := none }
+
+/-- The transition function of `ZipTransducer.toTM`. -/
+private def tr : State Q → Option Bool → Option Bool → Action 1 Bool (State Q)
+  | .copy, some true, _ =>
+    { inputTape := 1, workTapes := fun _ => (none, 0), output := none, state := some .copyBit }
+  | .copy, some false, _ =>
+    { inputTape := 1, workTapes := fun _ => (none, -1), output := none, state := some .rewind }
+  | .copy, none, _ => haltAction
+  | .copyBit, some b, _ =>
+    { inputTape := 1, workTapes := fun _ => (some (some b), 1), output := none,
+      state := some .copy }
+  | .copyBit, none, _ => haltAction
+  | .rewind, _, some _ =>
+    { inputTape := 0, workTapes := fun _ => (none, -1), output := none, state := some .rewind }
+  | .rewind, _, none =>
+    { inputTape := 0, workTapes := fun _ => (none, 1), output := none,
+      state := some (.zip τ.q₀ none) }
+  | .zip q (some b), _, _ =>
+    { inputTape := 0, workTapes := fun _ => (none, 0), output := some b,
+      state := some (.zip q none) }
+  | .zip q none, none, none =>
+    { inputTape := 0, workTapes := fun _ => (none, 0), output := (τ.final q).head?,
+      state := (τ.final q).tail.head?.map .flush }
+  | .zip q none, x, y =>
+    { inputTape := if x.isSome then 1 else 0,
+      workTapes := fun _ => (none, if y.isSome then 1 else 0),
+      output := (τ.step q (y, x)).2.head?,
+      state := some (.zip (τ.step q (y, x)).1 (τ.step q (y, x)).2.tail.head?) }
+  | .flush b, _, _ =>
+    { inputTape := 0, workTapes := fun _ => (none, 0), output := some b, state := none }
+
+/-- `τ` as a machine with one work tape. On `frame u ++ v` it copies `u` to the work tape,
+rewinds the work tape, and then runs `τ` on `u` from the work tape and `v` from the input tape. -/
+public def toTM : MultiTapeTM 1 Bool (State Q) :=
+  ofTr .copy fun s x ys => τ.tr s x (ys 0)
+
+/-! ### Configurations -/
+
+variable {w : List Bool}
+
+/-- The configuration in state `st` with the input head at `p` (clamped to the input), the work
+tape `tape` with its head at `h`, and the output `o`. -/
+private def cfgAt (w : List Bool) (st : Option (State Q)) (p : ℕ) (tape : ℤ → Option Bool) (h : ℤ)
+    (o : List Bool) : Cfg 1 Bool (State Q) w :=
+  ⟨st, ⟨min p (w.length + 1), by omega⟩, fun _ => tape, fun _ => h, o⟩
+
+private lemma moveInputPosNat_le (n j : ℕ) (d : SignType) (hj : j < n + 2) :
+    moveInputPosNat n j d ≤ n + 1 := by
+  have := (moveInputPos (⟨j, hj⟩ : Fin (n + 2)) d).isLt
+  rw [val_moveInputPos_eq_moveInputPosNat] at this
+  exact Nat.lt_succ_iff.mp this
+
+/-- One step of `τ.toTM`, read off its transition function. -/
+private lemma step_cfgAt (s : State Q) (p : ℕ) (tape : ℤ → Option Bool) (h : ℤ) (o : List Bool) :
+    τ.toTM.step (cfgAt w (some s) p tape h o) =
+      cfgAt w (τ.tr s (inputAt w (min p (w.length + 1))) (tape h)).state
+        (moveInputPosNat w.length (min p (w.length + 1))
+          (τ.tr s (inputAt w (min p (w.length + 1))) (tape h)).inputTape)
+        (match ((τ.tr s (inputAt w (min p (w.length + 1))) (tape h)).workTapes 0).1 with
+          | none => tape
+          | some x => Function.update tape h x)
+        (h + (((τ.tr s (inputAt w (min p (w.length + 1))) (tape h)).workTapes 0).2 : ℤ))
+        (o ++ (τ.tr s (inputAt w (min p (w.length + 1))) (tape h)).output.toList) := by
+  have hw : (cfgAt w (some s) p tape h o).workTapeSymbols = fun _ => tape h := rfl
+  have hp : ((cfgAt w (some s) p tape h o).inputPos : ℕ) = min p (w.length + 1) := rfl
+  rw [step_of_state rfl, Cfg.inputSymbol_eq_inputAt, hw, hp]
+  simp only [toTM, tr_ofTr]
+  refine Cfg.ext rfl (Fin.ext ?_) (funext fun i => ?_) (funext fun i => ?_) rfl
+  · rw [Action.apply_inputPos, val_moveInputPos_eq_moveInputPosNat, hp]
+    exact (min_eq_left (moveInputPosNat_le _ _ _ (by omega))).symm
+  · obtain rfl : i = 0 := Subsingleton.elim _ _
+    simp only [cfgAt, Action.apply_workTapes]
+    rcases ((τ.tr s (inputAt w (min p (w.length + 1))) (tape h)).workTapes 0).1 with _ | _ <;> rfl
+  · obtain rfl : i = 0 := Subsingleton.elim _ _
+    simp only [cfgAt, Action.apply_workTapePos]
+
+private lemma cfgAt_congr {st : Option (State Q)} {p p' : ℕ} {tape : ℤ → Option Bool} {h h' : ℤ}
+    {o : List Bool} (hp : min p (w.length + 1) = min p' (w.length + 1)) (hh : h = h') :
+    cfgAt w st p tape h o = cfgAt w st p' tape h' o := by
+  subst hh
+  simp only [cfgAt, hp]
+
+private lemma moveInputPosNat_one {n j : ℕ} (hj : j ≤ n) : moveInputPosNat n j 1 = j + 1 := by
+  simp only [moveInputPosNat, SignType.coe_one]
+  omega
+
+private lemma moveInputPosNat_zero {n j : ℕ} (hj : j ≤ n + 1) : moveInputPosNat n j 0 = j := by
+  simp only [moveInputPosNat, SignType.coe_zero]
+  omega
+
+/-! ### Runs through a set of work-head positions -/
+
+/-- From `c`, `τ.toTM` reaches `c'` within `t` steps, its work head staying in `S`. -/
+private def Seg (S : Finset ℤ) (c c' : Cfg 1 Bool (State Q) w) (t : ℕ) : Prop :=
+  ∃ n ≤ t, τ.toTM.runFrom c n = c' ∧ ∀ j ≤ n, (τ.toTM.runFrom c j).workTapePos 0 ∈ S
+
+variable {τ} {S : Finset ℤ} {c c' c'' : Cfg 1 Bool (State Q) w} {t t' : ℕ}
+
+private lemma Seg.refl (hc : c.workTapePos 0 ∈ S) : τ.Seg S c c 0 :=
+  ⟨0, le_rfl, rfl, fun j hj => by
+    obtain rfl : j = 0 := by omega
+    exact hc⟩
+
+private lemma Seg.single (hc : c.workTapePos 0 ∈ S) (h : τ.toTM.step c = c')
+    (hc' : c'.workTapePos 0 ∈ S) : τ.Seg S c c' 1 :=
+  ⟨1, le_rfl, h, fun j hj => by
+    rcases Nat.le_one_iff_eq_zero_or_eq_one.mp hj with rfl | rfl
+    · exact hc
+    · rw [runFrom_one, h]
+      exact hc'⟩
+
+private lemma Seg.trans (h₁ : τ.Seg S c c' t) (h₂ : τ.Seg S c' c'' t') :
+    τ.Seg S c c'' (t + t') := by
+  obtain ⟨n₁, hn₁, hr₁, hs₁⟩ := h₁
+  obtain ⟨n₂, hn₂, hr₂, hs₂⟩ := h₂
+  refine ⟨n₁ + n₂, by omega, by rw [runFrom_add, hr₁, hr₂], fun j hj => ?_⟩
+  rcases Nat.lt_or_ge n₁ j with h | h
+  · obtain ⟨d, rfl⟩ : ∃ d, j = n₁ + d := ⟨j - n₁, by omega⟩
+    rw [runFrom_add, hr₁]
+    exact hs₂ d (by omega)
+  · exact hs₁ j h
+
+private lemma Seg.mono (h : τ.Seg S c c' t) (ht : t ≤ t') : τ.Seg S c c' t' :=
+  let ⟨n, hn, hr, hs⟩ := h
+  ⟨n, hn.trans ht, hr, hs⟩
+
+/-! ### The framed input -/
+
+private lemma getElem?_frame_append (u v : List Bool) {i : ℕ} (hi : i < u.length) :
+    (frame u ++ v)[2 * i]? = some true ∧ (frame u ++ v)[2 * i + 1]? = some u[i] := by
+  induction u generalizing i with
+  | nil => simp at hi
+  | cons b u ih =>
+    rcases i with _ | i
+    · simp [frame_cons]
+    · obtain ⟨h₁, h₂⟩ := ih (i := i) (by simpa using hi)
+      have e₁ : 2 * (i + 1) = 2 * i + 1 + 1 := by omega
+      simp only [frame_cons, List.cons_append, e₁, List.getElem?_cons_succ,
+        List.getElem_cons_succ]
+      exact ⟨h₁, h₂⟩
+
+private lemma getElem?_frame_append_length (u v : List Bool) (j : ℕ) :
+    (frame u ++ v)[2 * u.length]? = some false ∧
+      (frame u ++ v)[2 * u.length + 1 + j]? = v[j]? := by
+  have hfl : frame u ++ v = u.flatMap (fun b => [true, b]) ++ false :: v := by simp [frame]
+  have hlen : (u.flatMap (fun b => [true, b])).length = 2 * u.length := by
+    have := length_frame u
+    simp only [frame, List.length_append, List.length_singleton] at this
+    omega
+  rw [hfl, List.getElem?_append_right (by omega), List.getElem?_append_right (by omega), hlen,
+    Nat.sub_self, (by omega : 2 * u.length + 1 + j - 2 * u.length = j + 1)]
+  exact ⟨rfl, rfl⟩
+
+/-! ### The phases of the machine -/
+
+variable {u v : List Bool}
+
+/-- The work head stays within the cells `-1, …, u.length`. -/
+private abbrev cells (u : List Bool) : Finset ℤ := Finset.Icc (-1) u.length
+
+@[simp]
+private lemma cfgAt_workTapePos (st : Option (State Q)) (p : ℕ) (tape : ℤ → Option Bool) (h : ℤ)
+    (o : List Bool) : (cfgAt w st p tape h o).workTapePos 0 = h :=
+  rfl
+
+private lemma cfgAt_mem_cells {st : Option (State Q)} {p : ℕ} {tape : ℤ → Option Bool} {h : ℤ}
+    {o : List Bool} (h₀ : -1 ≤ h) (h₁ : h ≤ u.length) :
+    (cfgAt w st p tape h o).workTapePos 0 ∈ cells u :=
+  Finset.mem_Icc.mpr ⟨h₀, h₁⟩
+
+private lemma length_frame_append (u v : List Bool) :
+    (frame u ++ v).length = 2 * u.length + 1 + v.length := by
+  rw [List.length_append, length_frame]
+
+/-- Copying the first word to the work tape, digit by digit. -/
+private lemma seg_copy {i : ℕ} (hi : i ≤ u.length) :
+    τ.Seg (cells u)
+      (cfgAt (frame u ++ v) (some .copy) (2 * i + 1) (tapeOfList (u.take i)) i [])
+      (cfgAt (frame u ++ v) (some .copy) (2 * u.length + 1) (tapeOfList u) u.length [])
+      (2 * (u.length - i)) := by
+  obtain ⟨d, hd⟩ : ∃ d, u.length - i = d := ⟨_, rfl⟩
+  have hn := length_frame_append u v
+  induction d generalizing i with
+  | zero =>
+    obtain rfl : i = u.length := by omega
+    rw [List.take_length]
+    exact (Seg.refl (cfgAt_mem_cells (by omega) le_rfl)).mono (Nat.zero_le _)
+  | succ d ih =>
+    have hi' : i < u.length := by omega
+    obtain ⟨h₁, h₂⟩ := getElem?_frame_append u v hi'
+    have s₁ : τ.toTM.step
+        (cfgAt (frame u ++ v) (some .copy) (2 * i + 1) (tapeOfList (u.take i)) i []) =
+        cfgAt (frame u ++ v) (some .copyBit) (2 * i + 2) (tapeOfList (u.take i)) i [] := by
+      rw [step_cfgAt]
+      have hp : min (2 * i + 1) ((frame u ++ v).length + 1) = 2 * i + 1 := by omega
+      have hx : inputAt (frame u ++ v) (2 * i + 1) = some true := by simpa [inputAt] using h₁
+      simp only [hp, hx, tr, moveInputPosNat_one (by omega : 2 * i + 1 ≤ (frame u ++ v).length),
+        SignType.coe_zero, add_zero, List.append_nil, Option.toList_none]
+    have s₂ : τ.toTM.step
+        (cfgAt (frame u ++ v) (some .copyBit) (2 * i + 2) (tapeOfList (u.take i)) i []) =
+        cfgAt (frame u ++ v) (some .copy) (2 * (i + 1) + 1) (tapeOfList (u.take (i + 1)))
+          ((i + 1 : ℕ) : ℤ) [] := by
+      rw [step_cfgAt]
+      have hp : min (2 * i + 2) ((frame u ++ v).length + 1) = 2 * i + 2 := by omega
+      have hx : inputAt (frame u ++ v) (2 * i + 2) = some u[i] := by simpa [inputAt] using h₂
+      have ht : Function.update (tapeOfList (u.take i)) (i : ℤ) (some u[i]) =
+          tapeOfList (u.take (i + 1)) := by
+        rw [List.take_add_one, List.getElem?_eq_getElem hi', Option.toList_some,
+          tapeOfList_append_single, List.length_take, min_eq_left hi'.le]
+      simp only [hp, hx, tr, moveInputPosNat_one (by omega : 2 * i + 2 ≤ (frame u ++ v).length),
+        SignType.coe_one, List.append_nil, Option.toList_none, ht]
+      exact cfgAt_congr (by omega) (by push_cast; rfl)
+    refine ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₁
+      (cfgAt_mem_cells (by omega) (by omega))).trans
+      ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₂
+        (cfgAt_mem_cells (by omega) (by omega))).trans
+        (ih (i := i + 1) (by omega) (by omega)))).mono (by omega)
+
+/-! The transitions used outside the copy phase, for arbitrary read symbols. -/
+
+private lemma tr_rewind_some (x : Option Bool) (b : Bool) :
+    τ.tr .rewind x (some b) =
+      { inputTape := 0, workTapes := fun _ => (none, -1), output := none,
+        state := some .rewind } := by
+  cases x <;> rfl
+
+private lemma tr_rewind_none (x : Option Bool) :
+    τ.tr .rewind x none =
+      { inputTape := 0, workTapes := fun _ => (none, 1), output := none,
+        state := some (.zip τ.q₀ none) } := by
+  cases x <;> rfl
+
+private lemma tr_zip_some (q : Q) (b : Bool) (x y : Option Bool) :
+    τ.tr (.zip q (some b)) x y =
+      { inputTape := 0, workTapes := fun _ => (none, 0), output := some b,
+        state := some (.zip q none) } := by
+  cases x <;> cases y <;> rfl
+
+private lemma tr_zip_step (q : Q) {x y : Option Bool} (h : ¬(x = none ∧ y = none)) :
+    τ.tr (.zip q none) x y =
+      { inputTape := if x.isSome then 1 else 0,
+        workTapes := fun _ => (none, if y.isSome then 1 else 0),
+        output := (τ.step q (y, x)).2.head?,
+        state := some (.zip (τ.step q (y, x)).1 (τ.step q (y, x)).2.tail.head?) } := by
+  rcases x with _ | _ <;> rcases y with _ | _
+  · simp at h
+  all_goals rfl
+
+private lemma tr_flush (b : Bool) (x y : Option Bool) :
+    τ.tr (.flush b) x y =
+      { inputTape := 0, workTapes := fun _ => (none, 0), output := some b, state := none } := by
+  cases x <;> cases y <;> rfl
+
+/-- The end of the frame: the input head moves to the second word and the work head starts
+moving back. -/
+private lemma step_endFrame :
+    τ.toTM.step (cfgAt (frame u ++ v) (some .copy) (2 * u.length + 1) (tapeOfList u)
+      u.length []) =
+      cfgAt (frame u ++ v) (some .rewind) (2 * u.length + 2) (tapeOfList u)
+        ((u.length : ℤ) - 1) [] := by
+  have hn := length_frame_append u v
+  rw [step_cfgAt]
+  have hp : min (2 * u.length + 1) ((frame u ++ v).length + 1) = 2 * u.length + 1 := by omega
+  have hx : inputAt (frame u ++ v) (2 * u.length + 1) = some false := by
+    simpa [inputAt] using (getElem?_frame_append_length u v 0).1
+  simp only [hp, hx, tr, moveInputPosNat_one (by omega : 2 * u.length + 1 ≤ (frame u ++ v).length),
+    SignType.coe_neg_one, List.append_nil, Option.toList_none]
+  exact cfgAt_congr (by omega) (by omega)
+
+/-- Rewinding the work tape. -/
+private lemma seg_rewind {i : ℕ} (hi : i ≤ u.length) :
+    τ.Seg (cells u)
+      (cfgAt (frame u ++ v) (some .rewind) (2 * u.length + 2) (tapeOfList u) ((i : ℤ) - 1) [])
+      (cfgAt (frame u ++ v) (some (.zip τ.q₀ none)) (2 * u.length + 2) (tapeOfList u) 0 [])
+      (i + 1) := by
+  have hn := length_frame_append u v
+  have hp : min (2 * u.length + 2) ((frame u ++ v).length + 1) = 2 * u.length + 2 := by omega
+  induction i with
+  | zero =>
+    refine Seg.single (cfgAt_mem_cells (by omega) (by omega)) ?_
+      (cfgAt_mem_cells (by omega) (by omega))
+    rw [step_cfgAt, hp, (by simp : ((0 : ℕ) : ℤ) - 1 = Int.negSucc 0), tapeOfList_negSucc,
+      tr_rewind_none, moveInputPosNat_zero (by omega)]
+    simp only [SignType.coe_one, List.append_nil, Option.toList_none]
+    exact cfgAt_congr rfl (by omega)
+  | succ i ih =>
+    have hi' : i < u.length := by omega
+    have hs : τ.toTM.step (cfgAt (frame u ++ v) (some .rewind) (2 * u.length + 2) (tapeOfList u)
+        (((i + 1 : ℕ) : ℤ) - 1) []) =
+        cfgAt (frame u ++ v) (some .rewind) (2 * u.length + 2) (tapeOfList u) ((i : ℤ) - 1) [] := by
+      rw [step_cfgAt, hp, (by omega : ((i + 1 : ℕ) : ℤ) - 1 = ((i : ℕ) : ℤ)),
+        tapeOfList_ofNat, List.getElem?_eq_getElem hi', tr_rewind_some,
+        moveInputPosNat_zero (by omega)]
+      simp only [SignType.coe_neg_one, List.append_nil, Option.toList_none]
+      exact cfgAt_congr rfl (by omega)
+    exact ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) hs
+      (cfgAt_mem_cells (by omega) (by omega))).trans (ih (by omega))).mono (by omega)
+
+/-- Emitting a pending output symbol. -/
+private lemma seg_flush {q : Q} (pend : Option Bool) {p : ℕ} (hp : p ≤ (frame u ++ v).length + 1)
+    {tape : ℤ → Option Bool} {h : ℤ} (h₀ : -1 ≤ h) (h₁ : h ≤ u.length) (o : List Bool) :
+    τ.Seg (cells u) (cfgAt (frame u ++ v) (some (.zip q pend)) p tape h o)
+      (cfgAt (frame u ++ v) (some (.zip q none)) p tape h (o ++ pend.toList)) 1 := by
+  rcases pend with _ | b
+  · rw [Option.toList_none, List.append_nil]
+    exact (Seg.refl (cfgAt_mem_cells h₀ h₁)).mono (Nat.zero_le _)
+  · refine Seg.single (cfgAt_mem_cells h₀ h₁) ?_ (cfgAt_mem_cells h₀ h₁)
+    rw [step_cfgAt, tr_zip_some, min_eq_left hp, moveInputPosNat_zero hp]
+    simp only [SignType.coe_zero, add_zero, Option.toList_some]
+
+private lemma getElem?_min_length {α : Type*} (l : List α) (r : ℕ) :
+    l[min r l.length]? = (l.drop r).head? := by
+  rw [List.head?_drop]
+  rcases Nat.le_total r l.length with h | h
+  · rw [min_eq_left h]
+  · rw [min_eq_right h, List.getElem?_eq_none le_rfl, List.getElem?_eq_none h]
+
+/-- Running `τ` on both words in lockstep, from round `r` on. -/
+private lemma seg_zip (q : Q) {r : ℕ} (hr : r ≤ max u.length v.length) (o : List Bool) :
+    τ.Seg (cells u)
+      (cfgAt (frame u ++ v) (some (.zip q none)) (2 * u.length + 2 + min r v.length)
+        (tapeOfList u) (min r u.length : ℕ) o)
+      (cfgAt (frame u ++ v) none (2 * u.length + 2 + v.length) (tapeOfList u) u.length
+        (o ++ τ.run q (u.drop r) (v.drop r)))
+      (2 * (max u.length v.length - r) + 2) := by
+  obtain ⟨d, hd⟩ : ∃ d, max u.length v.length - r = d := ⟨_, rfl⟩
+  have hn := length_frame_append u v
+  induction d generalizing r q o with
+  | zero =>
+    have hu : u.drop r = [] := List.drop_eq_nil_of_le (by omega)
+    have hv : v.drop r = [] := List.drop_eq_nil_of_le (by omega)
+    have hp : min (2 * u.length + 2 + min r v.length) ((frame u ++ v).length + 1) =
+        2 * u.length + 2 + v.length := by omega
+    have hx : inputAt (frame u ++ v) (2 * u.length + 2 + v.length) = none := by
+      unfold inputAt
+      split_ifs
+      · rfl
+      · exact List.getElem?_eq_none (by omega)
+    have hy : tapeOfList u ((min r u.length : ℕ) : ℤ) = none := by
+      rw [tapeOfList_ofNat, List.getElem?_eq_none (by omega)]
+    have s₁ : τ.toTM.step (cfgAt (frame u ++ v) (some (.zip q none))
+        (2 * u.length + 2 + min r v.length) (tapeOfList u) (min r u.length : ℕ) o) =
+        cfgAt (frame u ++ v) ((τ.final q).tail.head?.map .flush) (2 * u.length + 2 + v.length)
+          (tapeOfList u) u.length (o ++ (τ.final q).head?.toList) := by
+      rw [step_cfgAt, hp, hx, hy]
+      simp only [tr, SignType.coe_zero, add_zero,
+        moveInputPosNat_zero (by omega : 2 * u.length + 2 + v.length ≤ (frame u ++ v).length + 1)]
+      exact cfgAt_congr rfl (by omega)
+    rw [hu, hv, run_nil_nil]
+    have hfin := Transducer.toList_head?_append (τ.length_final_le q)
+    rcases hb : (τ.final q).tail.head? with _ | b
+    · rw [hb, Option.toList_none, List.append_nil] at hfin
+      rw [hb, Option.map_none] at s₁
+      rw [hfin] at s₁
+      exact (Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₁
+        (cfgAt_mem_cells (by omega) (by omega))).mono (by omega)
+    · rw [hb, Option.map_some] at s₁
+      have s₂ : τ.toTM.step (cfgAt (frame u ++ v) (some (.flush b)) (2 * u.length + 2 + v.length)
+          (tapeOfList u) u.length (o ++ (τ.final q).head?.toList)) =
+          cfgAt (frame u ++ v) none (2 * u.length + 2 + v.length) (tapeOfList u) u.length
+            (o ++ τ.final q) := by
+        rw [step_cfgAt, tr_flush, moveInputPosNat_zero (by omega)]
+        rw [hb, Option.toList_some] at hfin
+        simp only [SignType.coe_zero, add_zero, Option.toList_some, List.append_assoc, hfin]
+        exact cfgAt_congr (by omega) rfl
+      exact ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₁
+        (cfgAt_mem_cells (by omega) (by omega))).trans
+        (Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₂
+          (cfgAt_mem_cells (by omega) (by omega)))).mono (by omega)
+  | succ d ih =>
+    have hne : ¬((v.drop r).head? = none ∧ (u.drop r).head? = none) := by
+      simp only [List.head?_eq_none_iff, List.drop_eq_nil_iff]
+      omega
+    have hp : min (2 * u.length + 2 + min r v.length) ((frame u ++ v).length + 1) =
+        2 * u.length + 2 + min r v.length := by omega
+    have hx : inputAt (frame u ++ v) (2 * u.length + 2 + min r v.length) = (v.drop r).head? := by
+      rw [← getElem?_min_length]
+      simpa [inputAt,
+        (by omega : 2 * u.length + 2 + min r v.length - 1 = 2 * u.length + 1 + min r v.length)]
+        using (getElem?_frame_append_length u v (min r v.length)).2
+    have hy : tapeOfList u ((min r u.length : ℕ) : ℤ) = (u.drop r).head? := by
+      rw [tapeOfList_ofNat, getElem?_min_length]
+    set x := (v.drop r).head? with hxdef
+    set y := (u.drop r).head? with hydef
+    have hxs : x.isSome = decide (r < v.length) := by
+      rw [hxdef, List.head?_drop]
+      rcases Nat.lt_or_ge r v.length with h | h
+      · simp [h]
+      · simp [Nat.not_lt.mpr h]
+    have hys : y.isSome = decide (r < u.length) := by
+      rw [hydef, List.head?_drop]
+      rcases Nat.lt_or_ge r u.length with h | h
+      · simp [h]
+      · simp [Nat.not_lt.mpr h]
+    have hmove : moveInputPosNat (frame u ++ v).length (2 * u.length + 2 + min r v.length)
+        (if x.isSome then 1 else 0) = 2 * u.length + 2 + min (r + 1) v.length := by
+      rw [hxs]
+      rcases Nat.lt_or_ge r v.length with h | h
+      · simp only [decide_eq_true h, ↓reduceIte]
+        rw [moveInputPosNat_one (by omega)]
+        omega
+      · simp only [decide_eq_false (Nat.not_lt.mpr h), Bool.false_eq_true, ↓reduceIte]
+        rw [moveInputPosNat_zero (by omega)]
+        omega
+    have hhead : ((min r u.length : ℕ) : ℤ) + ((if y.isSome then 1 else 0 : SignType) : ℤ) =
+        ((min (r + 1) u.length : ℕ) : ℤ) := by
+      rw [hys]
+      rcases Nat.lt_or_ge r u.length with h | h
+      · simp only [decide_eq_true h, ↓reduceIte, SignType.coe_one]
+        omega
+      · simp only [decide_eq_false (Nat.not_lt.mpr h), Bool.false_eq_true, ↓reduceIte,
+          SignType.coe_zero]
+        omega
+    have s₁ : τ.toTM.step (cfgAt (frame u ++ v) (some (.zip q none))
+        (2 * u.length + 2 + min r v.length) (tapeOfList u) (min r u.length : ℕ) o) =
+        cfgAt (frame u ++ v) (some (.zip (τ.step q (y, x)).1 (τ.step q (y, x)).2.tail.head?))
+          (2 * u.length + 2 + min (r + 1) v.length) (tapeOfList u) (min (r + 1) u.length : ℕ)
+          (o ++ (τ.step q (y, x)).2.head?.toList) := by
+      rw [step_cfgAt, hp, hx, hy, tr_zip_step q hne]
+      simp only [hmove, hhead]
+    have hrun : o ++ τ.run q (u.drop r) (v.drop r) =
+        o ++ (τ.step q (y, x)).2.head?.toList ++ (τ.step q (y, x)).2.tail.head?.toList ++
+          τ.run (τ.step q (y, x)).1 (u.drop (r + 1)) (v.drop (r + 1)) := by
+      rw [τ.run_of_ne (by simpa [hxdef, hydef, and_comm] using hne), List.tail_drop,
+        List.tail_drop, List.append_assoc, List.append_assoc,
+        ← List.append_assoc ((τ.step q (y, x)).2.head?.toList),
+        Transducer.toList_head?_append (τ.length_step_le _ _)]
+    rw [hrun]
+    exact ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₁
+      (cfgAt_mem_cells (by omega) (by omega))).trans
+      ((seg_flush _ (by omega) (by omega) (by omega) _).trans
+        (ih _ (by omega) _ (by omega)))).mono (by omega)
+
+/-- The complete run on `frame u ++ v`. -/
+private lemma seg_run (u v : List Bool) :
+    τ.Seg (cells u) (τ.toTM.initCfg (frame u ++ v))
+      (cfgAt (frame u ++ v) none (2 * u.length + 2 + v.length) (tapeOfList u) u.length
+        (τ.run τ.q₀ u v))
+      (3 * (frame u ++ v).length + 1) := by
+  have hn := length_frame_append u v
+  have hinit : τ.toTM.initCfg (frame u ++ v) =
+      cfgAt (frame u ++ v) (some .copy) (2 * 0 + 1) (tapeOfList (u.take 0)) ((0 : ℕ) : ℤ) [] := by
+    refine Cfg.ext rfl (Fin.ext ?_) (funext fun _ => ?_) rfl rfl
+    · simp [MultiTapeNTM.initCfg, Cfg.init, cfgAt]
+    · simp [MultiTapeNTM.initCfg, Cfg.init, cfgAt]
+  have hzip := seg_zip (τ := τ) (u := u) (v := v) τ.q₀ (r := 0) (Nat.zero_le _) []
+  simp only [Nat.zero_min, Nat.add_zero, Nat.cast_zero, List.drop_zero, List.nil_append,
+    Nat.sub_zero] at hzip
+  rw [hinit]
+  refine (((seg_copy (Nat.zero_le _)).trans ((Seg.single (cfgAt_mem_cells (by omega) le_rfl)
+    step_endFrame (cfgAt_mem_cells (by omega) (by omega))).trans
+    ((seg_rewind le_rfl).trans hzip))).mono ?_)
+  have := Nat.max_le.mpr ⟨(le_rfl : u.length ≤ u.length), le_rfl⟩
+  omega
+
+/-- On `frame u ++ v`, `τ.toTM` emits `τ.run τ.q₀ u v` within `3 * (frame u ++ v).length + 1`
+steps, visiting the `u.length + 2` work-tape cells `-1, …, u.length`. -/
+public theorem computesInTimeAndSpace_toTM (u v : List Bool) :
+    τ.toTM.ComputesInTimeAndSpace (frame u ++ v) (τ.run τ.q₀ u v)
+      (3 * (frame u ++ v).length + 1) (u.length + 2) := by
+  obtain ⟨n, hn, hrun, hcells⟩ := τ.seg_run u v
+  have hhalt : (τ.toTM.runFrom (τ.toTM.initCfg (frame u ++ v)) n).Halted := by
+    rw [hrun]
+    rfl
+  refine ⟨⟨n, hhalt, by rw [hrun]; rfl⟩, runsInTime_of_halted ?_, runsInSpace_of_halted hhalt ?_⟩
+  · rw [runFrom_eq_of_halt _ _ hn hhalt]
+    exact hhalt
+  · simp only [MultiTapeNTM.RunPath.space, Finset.univ_unique, Fin.default_eq_zero,
+      Finset.sum_singleton]
+    refine (spaceUsedByTape_le_card _ hcells).trans_eq ?_
+    simp only [cells, Int.card_Icc]
+    omega
+
+end ZipTransducer
+
+end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean
index 4bd891c3e..3eee7125e 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeBinaryPrimitives.lean
@@ -11,14 +11,14 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTi
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeClosure
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition
-import Mathlib.Data.Nat.Bitwise
-import Mathlib.Data.List.GetD
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryComparison
 
 /-!
 # Direct polynomial-time binary arithmetic
 
-The existing carry folds and bit-position scan are certified using plain machine closure.
+The existing carry folds are certified using plain machine closure.
 Reachable word states are bounded by the encoded input length, not the numeric operands.
+Strict comparison is the linear zip-transducer certificate of `BinaryComparison`.
 Captured multiplication uses the original shift-and-add fold over the first operand's bits,
 with the unchanged full-prefix state bound; its pair certificate remains private.
 -/
@@ -39,54 +39,14 @@ theorem binary_add : ComputableInPolyTime (fun p : ℕ × ℕ => p.1 + p.2)
     (PolyBounded.of_forall_le 1 2 (fun _ => by simp))
     (PolyBounded.of_forall_le 1 1 (fun _ => by simp))
 
-/-- Strict comparison by scanning binary bit positions, never the numeric operand range. -/
+/-- Strict comparison of binary naturals, from the linear zip-transducer certificate
+`Turing.MultiTapeTM.computableInTimeAndSpace_natLt`. -/
 @[fun_prop]
 theorem binary_lt : ComputableInPolyTime (fun p : ℕ × ℕ => decide (p.1 < p.2))
-    (encPair encNat encNat) encBool := by
-  have hbits : ComputableInPolyTime Nat.bits encNat encBits := of_eq fun _ => rfl
-  have hlen : ComputableInPolyTime (fun n : ℕ => n.bits.length) encNat encUnary :=
-    Internal.DecoderWords.unary_degree.computableInPolyTime.comp hbits
-  have hwords : ComputableInDegree (fun p : ℕ × ℕ => p.1.bits ++ p.2.bits)
-      (encPair encNat encNat) encBits 1 1 :=
-    (ComputableInDegree.fst encNat encNat).append (ComputableInDegree.snd encNat encNat)
-      (fun _ => rfl)
-  have hsum : ComputableInPolyTime (fun p : ℕ × ℕ => p.1.bits.length + p.2.bits.length)
-      (encPair encNat encNat) encUnary := by
-    simpa only [Function.comp_def, List.length_append] using
-      Internal.DecoderWords.unary_degree.computableInPolyTime.comp hwords.computableInPolyTime
-  have hscan : ComputableInPolyTime (fun p : ℕ × ℕ =>
-      (List.range p.2.bits.length).any fun i =>
-        !p.1.bits.getD i false && p.2.bits.getD i false &&
-          (List.range (p.1.bits.length + p.2.bits.length)).all fun j =>
-            decide (j ≤ i) || p.1.bits.getD j false == p.2.bits.getD j false)
-      (encPair encNat encNat) encBool := by
-    simp only [List.any_eq_not_all_not]
-    apply bool_not.comp
-    apply allWithInput (range.comp (hlen.comp (snd encNat encNat)))
-    apply bool_not.comp
-    let input := encPair (encPair encNat encNat) encUnary
-    have hlist := range.comp (hsum.comp (fst (encPair encNat encNat) encUnary))
-    have hhigh : ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ =>
-        (List.range (p.1.1.bits.length + p.1.2.bits.length)).all fun j =>
-          decide (j ≤ p.2) || p.1.1.bits.getD j false == p.1.2.bits.getD j false)
-        input encBool := by
-      apply allWithInput hlist
-      fun_prop
-    have hflags : ComputableInPolyTime (fun p : (ℕ × ℕ) × ℕ =>
-        !p.1.1.bits.getD p.2 false && p.1.2.bits.getD p.2 false) input encBool := by
-      fun_prop
-    exact bool_and.comp (hflags.prod hhigh)
-  refine hscan.of_enc_eq fun p => congrArg encBool ?_
-  have hbit (k i : ℕ) : k.bits.getD i false = k.testBit i := by
-    rw [Nat.testBit_eq_inth, ← List.getD_default_eq_getI]
-    rfl
-  rw [Bool.eq_iff_iff, decide_eq_true_iff, Nat.lt_iff_exists_testBit]
-  simp only [hbit, Nat.size_eq_bits_len, List.any_eq_true, List.mem_range, Bool.and_eq_true,
-    Bool.not_eq_true', List.all_eq_true, Bool.or_eq_true, decide_eq_true_eq, beq_iff_eq]
-  refine exists_congr fun i => and_congr_right fun _ => ?_
-  rw [and_assoc]
-  refine and_congr_right fun _ => and_congr_right fun _ => forall₂_congr fun j _ => ?_
-  rw [← Nat.not_le, imp_iff_not_or, not_not]
+    (encPair encNat encNat) encBool :=
+  (ComputableInO.of_linear ComputableInLinearTimeAndSpace.natLt).computableInPolyTime
+    (PolyBounded.of_forall_le 1 1 (fun _ => by simp))
+    (PolyBounded.of_forall_le 1 1 (fun _ => by simp))
 
 private theorem binaryMulPair :
     ComputableInPolyTime (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat := by
diff --git a/ComplexityTests/Machines/Turing/MultiTape/ZipTransducer.lean b/ComplexityTests/Machines/Turing/MultiTape/ZipTransducer.lean
new file mode 100644
index 000000000..2b2dc6954
--- /dev/null
+++ b/ComplexityTests/Machines/Turing/MultiTape/ZipTransducer.lean
@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+module
+-- upstream: local-only (test driver)
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.ZipTransducer
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryComparison
+
+/-! Zip transducers: semantics on concrete words, the machine bound on a concrete input, and the
+linear comparison certificate instantiated on concrete numbers. -/
+
+@[expose] public section
+namespace ComplexityTests.ZipTransducer
+open Turing.MultiTapeTM
+
+/-- Bitwise disjunction of two words, padding the shorter one with zeros. -/
+def orZip : ZipTransducer Unit where
+  q₀ := ()
+  step _ x := ((), [x.1.getD false || x.2.getD false])
+  final _ := []
+  length_step_le _ _ := by simp
+  length_final_le _ := by simp
+
+/-- Emits the number of digits by which the first word is longer, in unary, then a marker; it
+exercises a state that changes when only one word has digits left. -/
+def longerZip : ZipTransducer Bool where
+  q₀ := false
+  step _ x := (x.2.isNone, if x.2.isNone then [true] else [])
+  final b := [b, false]
+  length_step_le _ x := by cases x.2 <;> simp
+  length_final_le _ := by simp
+
+-- The semantics pads the shorter word and runs in lockstep, in both directions.
+example : orZip.run () [true, false] [false, false, true] = [true, false, true] := by
+  simp [orZip]
+
+example : orZip.run () [false, false, true] [] = [false, false, true] := by
+  simp [orZip]
+
+example : longerZip.run false [true, true, true] [false] = [true, true, true, false] := by
+  simp [longerZip]
+
+example : longerZip.run false [] [false, true] = [false, false] := by
+  simp [longerZip]
+
+-- The machine on `frame [true, false] ++ [false, false, true]`: the input has length `8`, so the
+-- run takes at most `25` steps, and the work head visits the four cells `-1, 0, 1, 2`.
+example : orZip.toTM.ComputesInTimeAndSpace (frame [true, false] ++ [false, false, true])
+    [true, false, true] 25 4 := by
+  have h := orZip.computesInTimeAndSpace_toTM [true, false] [false, false, true]
+  simp only [List.length_append, length_frame, List.length_cons, List.length_nil] at h
+  simpa [orZip] using h
+
+-- The linear comparison certificate on `(5, 6)`: `encPair encNat encNat (5, 6)` has length
+-- `2 * 3 + 1 + 3 = 10`, so some machine outputs `[true]` within `31` steps and `5` cells.
+example : ∃ (k : ℕ) (Q : Type) (_ : Finite Q) (tm : Turing.MultiTapeTM k Bool Q),
+    tm.ComputesInTimeAndSpace (encPair encNat encNat (5, 6)) [true] 31 5 := by
+  obtain ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_natLt
+  have hb5 : Nat.bits 5 = [true, false, true] := by
+    rw [show 5 = Nat.bit true 2 from rfl, Nat.bits_append_bit _ _ (by simp),
+      show 2 = Nat.bit false 1 from rfl, Nat.bits_append_bit _ _ (by simp), Nat.one_bits]
+  have hb6 : Nat.bits 6 = [false, true, true] := by
+    rw [show 6 = Nat.bit false 3 from rfl, Nat.bits_append_bit _ _ (by simp),
+      show 3 = Nat.bit true 1 from rfl, Nat.bits_append_bit _ _ (by simp), Nat.one_bits]
+  refine ⟨k, Q, hQ, tm, ?_⟩
+  simpa [encNat_apply, encBool_apply, hb5, hb6, length_frame] using h (5, 6)
+
+-- The comparison is correct on both sides, including equal operands.
+example : ∃ (k : ℕ) (Q : Type) (_ : Finite Q) (tm : Turing.MultiTapeTM k Bool Q),
+    tm.Computes (encPair encNat encNat (6, 5)) [false] ∧
+      tm.Computes (encPair encNat encNat (6, 6)) [false] ∧
+      tm.Computes (encPair encNat encNat (0, 1)) [true] := by
+  obtain ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_natLt
+  exact ⟨k, Q, hQ, tm, (h (6, 5)).1, (h (6, 6)).1, (h (0, 1)).1⟩
+
+end ComplexityTests.ZipTransducer