Clock infrastructure for the time-bounded universal machine

The generic liftTM frame rules live in Lift.Hoare, re-exported here for compatibility. They preserve arbitrary non-marker extra tapes with the source's unchanged time bound; the clocked UTM uses them to pin tape 6 while running a six-tape phase.

The module also defines two standalone clock machines. They are not part of the clocked universal machine, whose loop uses the frontier-parked variants decFrontierTM and orZeroTM from UTM/Internal/ClockFrontier.lean; nothing in the library uses them. Both are TM 7, acting on work tape 6 (clkT), which holds a unary counter (1s on cells 1..v, head parked at 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).

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

@[instance_reducible]

instance Complexity.TM.instDecidableEqClockPhase : DecidableEq ClockPhase

Equations

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

@[instance_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. Standalone: the clocked universal machine uses decFrontierTM instead.

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

@[instance_reducible]

instance Complexity.TM.instDecidableEqZeroTestPhase : DecidableEq ZeroTestPhase

Equations

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

@[instance_reducible]

instance Complexity.TM.instFintypeZeroTestPhase : Fintype ZeroTestPhase

Equations

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

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. Standalone: the clocked universal machine uses orZeroTM instead.

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.