feat(Machines): zip transducer kernel for linear-time two-operand functions (#608)

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

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

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]

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

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