Universal machine: the clocked (time-bounded) simulate/halt-test loop

The time-bounded variant of utm_loop_simulates: the 7-tape loop clockedLoop = loopTM clockedBody clockedTest runs the interpreted machine for min (halting time, clock budget) steps, where

• clockedBody = seqTM (bodyTM.liftTM 1) decFrontierTM — one body pass of the 6-tape UTM (lifted to 7 tapes, the clock tape pinned by the frame rule liftTM_hoareTime_frame) followed by an O(1) decrement of the frontier-parked unary clock on tape 6 (clkT);
• clockedTest = seqTM (haltTestTM.liftTM 1) orZeroTM — the lifted halt test writes the halt verdict at output cell 1, and orZeroTM overwrites it with the combined loop-exit verdict (halted or clock zero).

Frontier representation: clock value v ⟺ tape-6 cells are regCells v and the head is at max v 1.

Proof structure

Composition strategy (option (i) of the design space): bodyIteration is packaged as a ghost-style HoareTime triple at fixed tapes (clockedBody_hoareTime's inner triple), lifted through liftTM_hoareTime_frame with the clock tape as the pinned extra, and composed with decFrontierTM_hoareTime via seqTM_hoareTime; similarly for the test half with haltTestTM_hoareTime and orZeroTM_hoareTime. The per-iteration lemma clocked_iteration then mirrors SimLoop's loop_iteration at the loop level (body/test phase embeddings plus a local copy of the rewind/check bookkeeping), and two strong inductions on the remaining fuel (clocked_aux_halt / clocked_aux_timeout) deliver the two cases of the headline theorem clocked_loop_simulates.

Statement notes (deviations from the naive statement)

The loop is do-while: even a T = 0 run (initial configuration already halted) executes one full iteration, which decrements the clock. Hence case A leaves the clock at V - max T 1 (equal to V - T for T ≥ 1). Case B requires 1 ≤ V: with a zero budget the do-while loop still simulates one interpreted step before its first exit test, so "exactly V simulated steps" would be false for V = 0. In both cases the exit verdict at output cell 1 is Γ.one; the two exits are distinguished by the state tape (SimInv at the final interpreted configuration makes a subsequent halt test conclusive via simInv_verdict).

def Complexity.TM.UTMBody.clockedBody : TM 7

The clocked loop body: one (lifted) UTM body pass, then one O(1) decrement of the frontier-parked clock on tape 6.

Equations

• Complexity.TM.UTMBody.clockedBody = (Complexity.TM.UTMBody.bodyTM.liftTM 1).seqTM Complexity.TM.decFrontierTM

def Complexity.TM.UTMBody.clockedTest : TM 7

The clocked loop test: the (lifted) halt test writes the halt verdict at output cell 1; orZeroTM replaces it with the combined loop-exit verdict (halted or clock zero).

Equations

• Complexity.TM.UTMBody.clockedTest = (Complexity.TM.haltTestTM.liftTM 1).seqTM Complexity.TM.orZeroTM

def Complexity.TM.UTMBody.clockedLoop : TM 7

The clocked simulate/halt-test loop.

Equations

• Complexity.TM.UTMBody.clockedLoop = Complexity.TM.UTMBody.clockedBody.loopTM Complexity.TM.UTMBody.clockedTest

theorem Complexity.TM.UTMBody.clocked_loop_simulates (α x : List Bool) (hterm : TerminatedRegion α) (V : ℕ) (inp : Tape) (work : Fin 7 → Tape) (out : Tape) (hinv : SimInv α ((decodeDesc α).toTM.initCfg x) inp (fun (k : Fin 6) => work (Fin.castAdd 1 k)) out) (hclk : (work clkT).cells = regCells V) (hclkh : (work clkT).head = max V 1) (hout0 : out.cells 0 = Γ.start) (houtns : ∀ (j : ℕ), 1 ≤ j → out.cells j ≠ Γ.start) (houth : out.head = 1) : (∀ (T : ℕ) (mcF : Cfg 1 (decodeDesc α).toTM.Q), T ≤ V → (decodeDesc α).toTM.reachesIn T ((decodeDesc α).toTM.initCfg x) mcF → (decodeDesc α).toTM.halted mcF → ∃ (c' : Cfg 7 clockedLoop.Q), ∃ t ≤ (T + 1) * (utmStepTime α + 10), clockedLoop.reachesIn t { state := clockedLoop.qstart, input := inp, work := work, output := out } c' ∧ clockedLoop.halted c' ∧ SimInv α mcF c'.input (fun (k : Fin 6) => c'.work (Fin.castAdd 1 k)) c'.output ∧ (c'.work clkT).cells = regCells (V - max T 1) ∧ (c'.work clkT).head = max (V - max T 1) 1 ∧ c'.output.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → c'.output.cells j ≠ Γ.start) ∧ c'.output.head = 1 ∧ c'.output.cells 1 = Γ.one) ∧ ∀ (mcV : Cfg 1 (decodeDesc α).toTM.Q), 1 ≤ V → (decodeDesc α).toTM.reachesIn V ((decodeDesc α).toTM.initCfg x) mcV → ¬(decodeDesc α).toTM.halted mcV → ∃ (c' : Cfg 7 clockedLoop.Q), ∃ t ≤ (V + 1) * (utmStepTime α + 10), clockedLoop.reachesIn t { state := clockedLoop.qstart, input := inp, work := work, output := out } c' ∧ clockedLoop.halted c' ∧ SimInv α mcV c'.input (fun (k : Fin 6) => c'.work (Fin.castAdd 1 k)) c'.output ∧ (c'.work clkT).cells = regCells 0 ∧ (c'.work clkT).head = 1 ∧ c'.output.cells 0 = Γ.start ∧ (∀ (j : ℕ), 1 ≤ j → c'.output.cells j ≠ Γ.start) ∧ c'.output.head = 1 ∧ c'.output.cells 1 = Γ.one

The clocked UTM loop simulates the interpreted machine for min (halting time, clock budget) steps. From any tapes realizing SimInv at the interpreted machine's initial configuration on the six embedded tapes — with the frontier-parked unary clock at V on tape 6 (clkT) and the output tape ▷-clean and parked at cell 1 — the loop clockedLoop = loopTM clockedBody clockedTest halts with the exit verdict Γ.one at output cell 1, and:

• (A: halt within budget) if (decodeDesc α).toTM halts on x at mcF in T ≤ V steps, the loop exits within (T + 1) * (utmStepTime α + 10) steps with SimInv re-established at mcF and the clock at V - max T 1 (i.e. V - T for T ≥ 1; the do-while loop burns one tick even when the machine starts halted);
• (B: timeout) if the machine is still running after V ≥ 1 steps (at mcV), the loop exits within (V + 1) * (utmStepTime α + 10) steps with SimInv at the V-step configuration mcV and the clock at 0.

In both cases the output tape is parked (▷-clean, head at cell 1). The two exits are distinguished by the final state tape: SimInv at the exit configuration makes a subsequent (lifted) halt test conclusive via simInv_verdict. Note that no-halt-before-V in case B is automatic: the prefix configurations of the V-step run all step, and halted configurations cannot step.