Frontier-parked clock machines for the time-bounded universal machine

Frontier variants of decClockTM / zeroTestTM (see Clock.lean): to make each clock tick O(1), the clock head stays parked at the frontier (the last unary mark) between ticks, rather than rewinding to cell 1.

Frontier representation: clock value v ⟺ tape-6 (clkT) cells are regCells v and the head is at max v 1. At v = 0 the head sits at cell 1 reading □; at v ≥ 1 it sits at cell v reading 1.

Two TM 7 machines, both with ghost-initial-tapes HoareTime specs:

• decFrontierTM — one O(1) decrement: blank the mark under the head, move left, then settle (when the head lands on ▷, i.e. v = 1 → 0, the settle step is forced right onto cell 1; otherwise it stays on the new frontier mark). The zero clock is left unchanged in one idle step. Spec: decFrontierTM_hoareTime, 3 steps, every other tape exactly preserved.
• orZeroTM — the combined loop-exit test, run right after the (lifted) halt test has left its verdict at output cell 1 with the output head at 1: overwrite output cell 1 with 1 if the verdict is 1 or the clock is zero (frontier read □), else 0, keeping the output head at 1. Spec: orZeroTM_hoareTime, 2 steps. The verdict must be a non-▷ symbol (hverdns): reading ▷ at the output head would force a right move via δ_right_of_start, making out.head = 1 unachievable.

inductive Complexity.TM.DecFrontierPhase : Type

Control states of decFrontierTM.

• dec : DecFrontierPhase
• settle : DecFrontierPhase
• done : DecFrontierPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqDecFrontierPhase : DecidableEq DecFrontierPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeDecFrontierPhase : Fintype DecFrontierPhase

Equations

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

def Complexity.TM.decFrontierTM : TM 7

Frontier decrement: with the clock head parked at the frontier (max v 1), reading 1 (v ≥ 1) blanks the mark and moves left; the settle step then either steps right off ▷ (was at cell 1, v = 1 → 0) or stays on the new frontier mark (v ≥ 2). Reading □ (v = 0) halts immediately — decrement of zero is a no-op. All other tapes idle throughout.

Equations

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

theorem Complexity.TM.decFrontierTM_hoareTime (v : ℕ) (inp₀ : Tape) (work₀ : Fin 7 → Tape) (out₀ : Tape) (hclk : (work₀ clkT).cells = regCells v) (hclkh : (work₀ clkT).head = max v 1) (hinp : inp₀.read ≠ Γ.start) (hwork : ∀ (i : Fin 7), i ≠ clkT → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : decFrontierTM.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).cells = regCells (v - 1) ∧ (work clkT).head = max (v - 1) 1 ∧ out = out₀) 3

decFrontierTM specification (ghost-initial-tapes style). Starting from qstart with the clock tape (clkT = work tape 6) holding regCells v with its head parked at the frontier (max v 1), and every other tape parked on a non-▷ symbol, decFrontierTM halts within 3 steps having decremented the clock to regCells (v - 1) with the head parked at the new frontier (max (v - 1) 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.OrZeroPhase : Type

Control states of orZeroTM.

• test : OrZeroPhase
• done : OrZeroPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqOrZeroPhase : DecidableEq OrZeroPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeOrZeroPhase : Fintype OrZeroPhase

Equations

• Complexity.TM.instFintypeOrZeroPhase = { elems := {Complexity.TM.OrZeroPhase.test, Complexity.TM.OrZeroPhase.done}, complete := Complexity.TM.instFintypeOrZeroPhase._proof_1 }

def Complexity.TM.orZeroTM : TM 7

Combined loop-exit test: read output cell 1 (the halt-test verdict, head parked at 1) and the frontier-parked clock tape; overwrite output cell 1 with 1 if the verdict is 1 or the clock reads □ (i.e. is zero), else 0, keeping 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.orZeroTM_hoareTime (v : ℕ) (verdict : Γ) (inp₀ : Tape) (work₀ : Fin 7 → Tape) (out₀ : Tape) (hclk : (work₀ clkT).cells = regCells v) (hclkh : (work₀ clkT).head = max v 1) (hverd : out₀.cells 1 = verdict) (hverdns : verdict ≠ Γ.start) (houth : out₀.head = 1) (hout0 : out₀.cells 0 = Γ.start) (hinp : inp₀.read ≠ Γ.start) (hwork : ∀ (i : Fin 7), i ≠ clkT → (work₀ i).read ≠ Γ.start) : orZeroTM.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 verdict = Γ.one ∨ v = 0 then Γ.one else Γ.zero) ∧ out.head = 1) 2

orZeroTM specification (ghost-initial-tapes style). Starting from qstart with the clock tape (clkT = work tape 6) holding regCells v with its head parked at the frontier (max v 1), the output head resting at cell 1 on the halt-test verdict (a non-▷ symbol), and every other tape parked on a non-▷ symbol, orZeroTM halts within 2 steps having

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