From 0ed555f3e90044257ae1d5ce6dcb47c9c1aa15f3 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <sgschlesinger@gmail.com>
Date: Tue, 18 Aug 2026 12:15:55 -0400
Subject: [PATCH] feat: halting-time, output-length, and visited-position
 lemmas for multi-tape TMs

General lemmas independent of any particular construction:
- exists_minimal_halting_config: a padded halting run has a least
  halting time reaching the same configuration
- outputString_length_le / output_length_le_time: the output is no
  longer than the elapsed time
- spaceUsedByTape_le_of_positions: space comparison between two
  machines via inclusion of visited head positions
---
 .../Turing/MultiTape/Deterministic.lean       | 43 +++++++++++++++++++
 .../Machines/Turing/MultiTape/TapeLemmas.lean | 22 ++++++++++
 2 files changed, 65 insertions(+)

diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 625b932b2..68d0ccc63 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
@@ -289,6 +289,26 @@ lemma configs_of_halts (cfg : Cfg k Symbol State input) (h : cfg.state = none) {
   | succ d ih =>
     rw [configs_succ_eq_step', ih, step_of_halt h]
 
+/-- Every padded halting computation has a least halting time, and the configuration there is the
+same as at the padded time. -/
+lemma exists_minimal_halting_config (tm : MultiTapeTM k Symbol State)
+    {input : List Symbol} (start : Cfg k Symbol State input) (t : ℕ)
+    (hhalt : (tm.configs start t).state = none) :
+    ∃ u ≤ t, (tm.configs start u).state = none ∧
+      (∀ m < u, (tm.configs start m).state ≠ none) ∧
+      tm.configs start u = tm.configs start t := by
+  let hex : ∃ n, (tm.configs start n).state.isNone := ⟨t, by simp [hhalt]⟩
+  let u := Nat.find hex
+  have huBool : (tm.configs start u).state.isNone := Nat.find_spec hex
+  have huHalt : (tm.configs start u).state = none := by simpa using huBool
+  have hut : u ≤ t := Nat.find_min' hex (by simp [hhalt])
+  refine ⟨u, hut, huHalt, ?_, ?_⟩
+  · intro m hm hnone
+    exact Nat.find_min hex hm (by simp [hnone])
+  · obtain ⟨d, ht⟩ := Nat.exists_eq_add_of_le hut
+    rw [ht, configs_add]
+    exact (tm.configs_of_halts _ huHalt).symm
+
 @[simp]
 lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) :
     tm.outputSymbol cfg = none := by
@@ -401,6 +421,20 @@ lemma outputString_eq_of_halt
   rw [outputString_add_eq_append, outputString_halt _ _ hhalt]
   simp
 
+/-- The output produced in `t` steps has length at most `t`. -/
+lemma outputString_length_le
+    (tm : MultiTapeTM k Symbol State)
+    (cfg : Cfg k Symbol State input) (t : ℕ) :
+    (tm.outputString cfg t).length ≤ t := by
+  induction t with
+  | zero => simp [outputString]
+  | succ t ih =>
+      rw [outputString_succ]
+      have hone : (tm.outputSymbol (tm.configs cfg t)).toList.length ≤ 1 := by
+        cases tm.outputSymbol (tm.configs cfg t) <;> simp
+      simp only [List.length_append]
+      omega
+
 /-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps
 and uses exactly `s` space.
 Note that this does not require the alphabet or state set to be finite. -/
@@ -412,6 +446,15 @@ def ComputesInTimeAndSpace
   tm.outputString (tm.initCfg input) t = output ∧
   tm.spaceUsed (tm.initCfg input) t = s
 
+/-- The output of a computation is no longer than its running time. -/
+lemma output_length_le_time
+    {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {t s : ℕ}
+    (h : ComputesInTimeAndSpace tm input output t s) :
+    output.length ≤ t := by
+  obtain ⟨-, hout, -⟩ := h
+  rw [← hout]
+  exact outputString_length_le tm (tm.initCfg input) t
+
 /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of
 length `n` it uses at most `t n` steps and `s n` space. It assumes an embedding function
 from the input/output alphabet into the machine alphabet.
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
index 39ec30f56..e90127b61 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean
@@ -132,6 +132,28 @@ lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) :
     _ ≤ ∑ i, (t + 1) := Finset.sum_le_sum (fun i _ => tm.spaceUsedByTape_le cfg t i)
     _ = k * t + k := by simp [Nat.mul_succ]
 
+/--
+The space used by one tape is monotone under inclusion of its visited head positions in the
+trajectory of another tape.
+-/
+lemma spaceUsedByTape_le_of_positions
+    {k' : ℕ} {Symbol' State' : Type*}
+    (tm : MultiTapeTM k Symbol State) (tm' : MultiTapeTM k' Symbol' State')
+    {input : List Symbol} {input' : List Symbol'}
+    (cfg : Cfg k Symbol State input) (cfg' : Cfg k' Symbol' State' input')
+    (t t' : ℕ) (i : Fin k) (i' : Fin k')
+    (hpos : ∀ r ≤ t, ∃ r' ≤ t',
+      (tm.configs cfg r).workTapePos i =
+        (tm'.configs cfg' r').workTapePos i') :
+    tm.spaceUsedByTape cfg t i ≤ tm'.spaceUsedByTape cfg' t' i' := by
+  unfold spaceUsedByTape visitedByTapeHead
+  apply Finset.card_le_card
+  intro p hp
+  simp only [Finset.mem_image, Finset.mem_range] at hp ⊢
+  obtain ⟨r, hr, rfl⟩ := hp
+  obtain ⟨r', hr', hpos'⟩ := hpos r (by omega)
+  exact ⟨r', by omega, hpos'.symm⟩
+
 /-- The space used by a single tape is monotone in the number of steps. -/
 lemma spaceUsedByTape_mono
     (tm : MultiTapeTM k Symbol State)