The clocked universal machine

clockedUtmTM — the 7-tape time-bounded universal machine that the time-hierarchy diagonalizer runs under retargetInput. On input pair α x with the unary clock V preloaded on the clock tape (clkT):

• the lifted initTM parses the input onto the six UTM tapes (the frame rule pins the clock tape);
• seekFrontierTM walks the clock head from cell 1 to the frontier (max V 1), the representation expected by the clocked loop;
• clockedLoop simulates the interpreted machine (decodeDesc α).toTM for min (halting time, clock budget) steps;
• a lifted haltTestTM, as the test of an ifTM, re-derives whether the simulation halted: verdict Γ.one routes to the lifted extractTM (copy the simulated output to the real output tape), verdict Γ.zero (timeout) routes to writeTM Γw.one (the timeout sentinel at output cell 1).

Main results

• clockedUtmTM_hoareTime_halt — if the interpreted machine halts at mcF within T ≤ V steps, the real output tape agrees with mcF's output tape through the latter's first blank;
• clockedUtmTM_hoareTime_timeout — if the interpreted machine is still running after V ≥ 1 steps, output cell 1 holds the sentinel Γ.one;

both within clockedUtmTime α x V steps from the started tapes clockedUtmPre α x V (the shape delivered by the diagonalizer's retargetInput mid-sequence).

theorem Complexity.TM.HoareTime.with_output_wf {n : ℕ} {tm : TM n} {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → out.cells 0 = Γ.start ∧ ∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) : tm.HoareTime pre (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => post inp work out ∧ out.cells 0 = Γ.start ∧ ∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) b

Output-WF strengthening for Hoare triples. If the precondition puts a well-formed output tape at the start (cell 0 = ▷ and nowhere else), the postcondition may be strengthened with the same well-formedness of the final output tape — writes are Γw and cell 0 is immutable, so the shape survives any run. This is what lets branch postconditions survive the combinators' final transitionTape (which preserves cells only on ▷-clean tapes).

def Complexity.TM.UTMBody.clockedUtmTM : TM 7

The clocked universal machine: initialize the six UTM tapes (the lifted initTM, clock tape pinned), park the clock head at the frontier, run the clocked simulate/decrement loop, then test whether the simulation halted: extract its output on verdict Γ.one, write the timeout sentinel Γw.one on verdict Γ.zero.

Equations

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

def Complexity.TM.UTMBody.clockedUtmPre (α x : List Bool) (V : ℕ) : TapePred 7

The clocked universal machine's precondition, in started form (the machine runs under retargetInput mid-sequence): input pair α x with the head parked at cell 1, the six UTM tapes blank and parked, the clock tape holding the canonical unary register regTape V, and the output tape blank and parked.

Equations

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

def Complexity.TM.UTMBody.clockedUtmTime (α x : List Bool) (V : ℕ) : ℕ

The clocked universal machine's time bound, covering both the halt-within-budget and timeout cases: initialization, the frontier seek, the clocked loop (at most V + 1 iterations), and the final halt-test/extract-or-write branch.

Equations

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

theorem Complexity.TM.UTMBody.clockedUtmTM_hoareTime_halt (α x : List Bool) (hterm : TerminatedRegion α) (V T : ℕ) (mcF : Cfg 1 (decodeDesc α).toTM.Q) (hTV : T ≤ V) (hrun : (decodeDesc α).toTM.reachesIn T ((decodeDesc α).toTM.initCfg x) mcF) (hhalt : (decodeDesc α).toTM.halted mcF) : clockedUtmTM.HoareTime (clockedUtmPre α x V) (fun (x : Tape) (x_1 : Fin 7 → Tape) (out : Tape) => ∃ m ≤ T, mcF.output.cells (m + 1) = Γ.blank ∧ (∀ j < m, mcF.output.cells (j + 1) ≠ Γ.blank) ∧ ∀ j ≤ m, out.cells (j + 1) = mcF.output.cells (j + 1)) (clockedUtmTime α x V)

The clocked universal machine, halting case. On the started tapes clockedUtmPre α x V, if the interpreted machine (decodeDesc α).toTM halts on x at mcF within T ≤ V steps, then clockedUtmTM halts within clockedUtmTime α x V steps with its real output tape agreeing with mcF's output tape through the latter's first blank — i.e. the clocked UTM computes exactly the simulated machine's output.

theorem Complexity.TM.UTMBody.clockedUtmTM_hoareTime_timeout (α x : List Bool) (hterm : TerminatedRegion α) (V : ℕ) (hV : 1 ≤ V) (mcV : Cfg 1 (decodeDesc α).toTM.Q) (hrun : (decodeDesc α).toTM.reachesIn V ((decodeDesc α).toTM.initCfg x) mcV) (hnh : ¬(decodeDesc α).toTM.halted mcV) : clockedUtmTM.HoareTime (clockedUtmPre α x V) (fun (x : Tape) (x_1 : Fin 7 → Tape) (out : Tape) => out.cells 1 = Γ.one) (clockedUtmTime α x V)

The clocked universal machine, timeout case. On the started tapes clockedUtmPre α x V, if the interpreted machine (decodeDesc α).toTM is still running after V ≥ 1 steps on x, then clockedUtmTM halts within clockedUtmTime α x V steps with the timeout sentinel Γ.one at output cell 1.