Frontier-seeking clock machine for the time-bounded universal machine

Clock initialization delivers the canonical register tape regTape V = ⟨1, regCells V⟩ on the clock tape (clkT = work tape 6 of a TM 7): head parked at cell 1. The clocked universal loop (clocked_loop_simulates in SimClocked.lean) instead wants the frontier-parked form of ClockFrontier.lean: cells regCells V, head at max V 1. seekFrontierTM bridges the two: starting at cell 1, it walks right over the unary 1 marks to the last mark (the frontier), or halts immediately at cell 1 when the clock is zero (frontier read □).

Spec: seekFrontierTM_hoareTime (ghost-initial-tapes style), V + 3 steps, every other tape exactly preserved. Behavior from head 1 on regTape V:

• V = 0: cell 1 reads □, halt in 1 step, head stays at 1 = max 0 1.
• V ≥ 1: cell 1 reads 1, step right into walk; walk right while reading 1; at cell V + 1 read □ and step left onto the frontier V = max V 1, halting. Total V + 1 steps.

inductive Complexity.TM.SeekFrontierPhase : Type

Control states of seekFrontierTM.

• first : SeekFrontierPhase
• walk : SeekFrontierPhase
• done : SeekFrontierPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqSeekFrontierPhase : DecidableEq SeekFrontierPhase

Equations

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

@[implicit_reducible]

instance Complexity.TM.instFintypeSeekFrontierPhase : Fintype SeekFrontierPhase

Equations

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

def Complexity.TM.seekFrontierTM : TM 7

Frontier seek: with the clock head at cell 1 of the canonical register tape regTape V, reading □ (V = 0) halts immediately; reading any mark (V ≥ 1) steps right into walk, which walks right over the 1 marks and, on the first □ (cell V + 1), steps left onto the frontier mark at cell V and halts. All other tapes idle throughout.

Equations

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

theorem Complexity.TM.seekFrontierTM_hoareTime (V : ℕ) (inp₀ : Tape) (work₀ : Fin 7 → Tape) (out₀ : Tape) (hclk : work₀ clkT = regTape V) (hinp : inp₀.read ≠ Γ.start) (hothers : ∀ (i : Fin 7), i ≠ clkT → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : seekFrontierTM.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 ∧ (work clkT).head = max V 1 ∧ out = out₀) (V + 3)

seekFrontierTM specification (ghost-initial-tapes style). Starting from qstart with the clock tape (clkT = work tape 6) holding the canonical register tape regTape V (cells regCells V, head at cell 1), and every other tape parked on a non-▷ symbol, seekFrontierTM halts within V + 3 steps having walked the clock head to the frontier (max V 1) with the cells untouched; the input tape, the output tape, and every other work tape are preserved exactly.