Clock infrastructure for the time-bounded universal machine

Everything lives in namespace TM (the machines here are generic TM-building blocks in the style of Subroutines.lean / DecReg.lean, not bodyTM phase states, so they sit beside liftTM rather than in TM.UTMBody). Two pieces:

1. HoareTime lifting through liftTM: a Hoare-style spec for tm : TM n transfers to tm.liftTM m with the same time bound, with the m extra work tapes exactly preserved.

   • liftTM_hoareTime_frame is the ghost-pinned frame version: the extras hold arbitrary parked content (head ≥ 1, reading a non-▷ symbol) — needed to run lifted 6-tape UTM phases while tape 6 holds the clock.
   • liftTM_hoareTime is the special case where the extras hold the canonical parked blank tape (Tape.init []).move Dir3.right (the tape liftCfg pins them to).

   The key observation: liftTM's extra-tape action is readBackWrite/idleDir — exactly transitionTape, which is the identity on any tape reading a non-▷ symbol (transitionTape_eq_self). So the extras are preserved exactly at every step, for any parked content, not just the blank tape hard-wired into liftCfg. Since Lift.lean's step commutation is specialized to blank extras (and its internals are private), we redo the small step lemma here against the generalized embedding liftCfgWith.

2. The clock machines, both TM 7, acting on work tape 6 (clkT), which holds a unary counter (1s on cells 1..v, head parked at 1 — i.e. HoldsExact (List.replicate v Γw.one) with head 1):

   • decClockTM — scan right to the last mark, blank it, rewind to cell 1; a zero counter is left unchanged. Spec: decClockTM_hoareTime (ghost style: 2*v + 6 steps, every other tape exactly unchanged).
   • zeroTestTM — read clock cell 1 and write the verdict to the real output cell 1 (1 iff the counter is zero), leaving the output head at cell 1 and every work tape exactly unchanged. Spec: zeroTestTM_hoareTime (4 steps).

theorem Complexity.TM.reachesIn_map' {n n' : ℕ} {tm : TM n} {tm' : TM n'} (wrap : Cfg n tm.Q → Cfg n' tm'.Q) (h_step : ∀ (c c' : Cfg n tm.Q), tm.step c = some c' → tm'.step (wrap c) = some (wrap c')) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') : tm'.reachesIn t (wrap c) (wrap c')

Cross-arity generalization of reachesIn_map: the simulating machine may have a different number of work tapes. If wrap commutes with step, then reachesIn lifts through the embedding.

def Complexity.TM.extraIdx {n m : ℕ} (i : Fin (n + m)) (h : n ≤ ↑i) : Fin m

The extra-tape index of a lifted tape index i with n ≤ i.val.

Equations

• Complexity.TM.extraIdx i h = ⟨↑i - n, ⋯⟩

def Complexity.TM.liftCfgWith {n : ℕ} (tm : TM n) (m : ℕ) (extras : Fin m → Tape) (c : Cfg n tm.Q) : Cfg (n + m) tm.Q

Embed a configuration of tm : TM n into one of tm.liftTM m with the extra work tapes pinned to the fixed tapes extras. Generalizes liftCfg, which is the special case extras = fun _ => (Tape.init []).move Dir3.right.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.TM.liftCfgWith_state {n : ℕ} (tm : TM n) (m : ℕ) (extras : Fin m → Tape) (c : Cfg n tm.Q) : (tm.liftCfgWith m extras c).state = c.state

liftCfgWith leaves the state unchanged.

@[simp]

theorem Complexity.TM.liftCfgWith_input {n : ℕ} (tm : TM n) (m : ℕ) (extras : Fin m → Tape) (c : Cfg n tm.Q) : (tm.liftCfgWith m extras c).input = c.input

liftCfgWith leaves the input tape unchanged.

@[simp]

theorem Complexity.TM.liftCfgWith_output {n : ℕ} (tm : TM n) (m : ℕ) (extras : Fin m → Tape) (c : Cfg n tm.Q) : (tm.liftCfgWith m extras c).output = c.output

liftCfgWith leaves the output tape unchanged.

theorem Complexity.TM.liftCfgWith_work_lt {n : ℕ} (tm : TM n) (m : ℕ) (extras : Fin m → Tape) (c : Cfg n tm.Q) (i : Fin (n + m)) (h : ↑i < n) : (tm.liftCfgWith m extras c).work i = c.work ⟨↑i, h⟩

liftCfgWith maps the first n work tapes to c's work tapes.

theorem Complexity.TM.liftCfgWith_work_ge {n : ℕ} (tm : TM n) (m : ℕ) (extras : Fin m → Tape) (c : Cfg n tm.Q) (i : Fin (n + m)) (h : n ≤ ↑i) : (tm.liftCfgWith m extras c).work i = extras (extraIdx i h)

liftCfgWith maps the extra work tapes to the pinned tapes.

theorem Complexity.TM.liftTM_hoareTime_frame {n m : ℕ} (tm : TM n) {pre post : TapePred n} {b : ℕ} (extras : Fin m → Tape) (hex : ∀ (j : Fin m), 1 ≤ (extras j).head ∧ (extras j).read ≠ Γ.start) (h : tm.HoareTime pre post b) : (tm.liftTM m).HoareTime (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => pre inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = extras j) (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => post inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = extras j) b

Frame rule for liftTM Hoare specs (ghost-pinned extras). If tm : TM n satisfies {pre} tm {post} [≤ b], then tm.liftTM m satisfies the same triple on its first n work tapes while the m extra tapes — holding arbitrary parked content extras (head ≥ 1, reading a non-▷ symbol) — are preserved exactly, with the same time bound. This is what lets lifted 6-tape UTM phases run while tape 6 holds the clock.

theorem Complexity.TM.liftTM_hoareTime {n m : ℕ} (tm : TM n) {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) : (tm.liftTM m).HoareTime (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => pre inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => post inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = (Tape.init []).move Dir3.right) b

liftTM preserves Hoare specs (blank extras). Special case of liftTM_hoareTime_frame: the extra tapes start and end as the canonical parked blank tape (Tape.init []).move Dir3.right.

def Complexity.TM.clkT : Fin 7

The clock tape: work tape 6 of the 7-tape layout (6 UTM body tapes plus the clock).

Equations

• Complexity.TM.clkT = 6

inductive Complexity.TM.ClockPhase : Type

Control states of decClockTM.

• scan : ClockPhase
• erase : ClockPhase
• back : ClockPhase
• park : ClockPhase
• done : ClockPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqClockPhase : DecidableEq ClockPhase

Equations

• Complexity.TM.instDecidableEqClockPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeClockPhase : Fintype ClockPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.decClockTM : TM 7

Decrement the clock: scan right over the marks on tape clkT, erase the last one, rewind to cell 1. From v marks to v - 1 marks in at most 2v + 6 steps; every other tape idles throughout (and is exactly preserved while parked). The zero clock is left unchanged.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.decClockTM_hoareTime (v : ℕ) (inp₀ : Tape) (work₀ : Fin 7 → Tape) (out₀ : Tape) (hclk : (work₀ clkT).HoldsExact (List.replicate v Γw.one)) (hclkh : (work₀ clkT).head = 1) (hinp : inp₀.read ≠ Γ.start) (hwork : ∀ (i : Fin 7), i ≠ clkT → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : decClockTM.HoareTime (fun (inp : Tape) (work : Fin 7 → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin 7 → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (i : Fin 7), i ≠ clkT → work i = work₀ i) ∧ (work clkT).HoldsExact (List.replicate (v - 1) Γw.one) ∧ (work clkT).head = 1 ∧ out = out₀) (2 * v + 6)

decClockTM specification (ghost-initial-tapes style). Starting from qstart with the clock tape (clkT = work tape 6) holding v unary marks with its head at cell 1, and every other tape parked on a non-▷ symbol, decClockTM halts within 2v + 6 steps having decremented the clock to v - 1 marks (head back at cell 1); the input tape, the output tape, and every other work tape are preserved exactly. The zero clock is left unchanged (0 - 1 = 0).

inductive Complexity.TM.ZeroTestPhase : Type

Control states of zeroTestTM.

• test : ZeroTestPhase
• done : ZeroTestPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqZeroTestPhase : DecidableEq ZeroTestPhase

Equations

• Complexity.TM.instDecidableEqZeroTestPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeZeroTestPhase : Fintype ZeroTestPhase

Equations

• Complexity.TM.instFintypeZeroTestPhase = { elems := {Complexity.TM.ZeroTestPhase.test, Complexity.TM.ZeroTestPhase.done}, complete := Complexity.TM.instFintypeZeroTestPhase._proof_1 }

def Complexity.TM.zeroTestTM : TM 7

Clock zero test: read clock cell 1 (head parked at 1) and write the verdict to the real output cell 1 — 1 if it is blank (the counter is zero), else 0 — leaving the output head at cell 1; then halt. Every work tape and the input tape idle.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.zeroTestTM_hoareTime (v : ℕ) (inp₀ : Tape) (work₀ : Fin 7 → Tape) (out₀ : Tape) (hclk : (work₀ clkT).HoldsExact (List.replicate v Γw.one)) (hclkh : (work₀ clkT).head = 1) (hinp : inp₀.read ≠ Γ.start) (hwork : ∀ (i : Fin 7), i ≠ clkT → (work₀ i).read ≠ Γ.start) (houth : out₀.head = 1) (hout1 : out₀.cells 1 ≠ Γ.start) : zeroTestTM.HoareTime (fun (inp : Tape) (work : Fin 7 → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin 7 → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out.cells = Function.update out₀.cells 1 (if v = 0 then Γ.one else Γ.zero) ∧ out.head = 1) 4

zeroTestTM specification (ghost-initial-tapes style). Starting from qstart with the clock tape (clkT = work tape 6) holding v unary marks with its head at cell 1, the output head resting at cell 1 on a non-▷ symbol, and every other tape parked on a non-▷ symbol, zeroTestTM halts within 4 steps having

• written the verdict at output cell 1: Γ.one iff v = 0, else Γ.zero (all other output cells unchanged, head back at cell 1);
• left the input tape and every work tape exactly unchanged.