A constructible time bound yields a uniformly clocked simulator

On input $x$, the machine ${\mathrm{Clock}}_{e,t}$ first scans the whole input once to learn $\mathrm{\mid }x\mathrm{\mid }$. The lower bound hypothesis $n\le t(n)$ together with [L4] ensures that this preliminary scan fits inside the intended asymptotic budget. It then runs the constructor from [L1] on unary input $1^{\mathrm{\mid }x\mathrm{\mid }}$ to obtain the binary numeral of $t(\mathrm{\mid }x\mathrm{\mid })$ and writes a counter of that size on a work tape.

Next, using the fixed code $e$ from [L3], the machine initializes the simulated configuration of $M$ on $x$. It first checks whether that configuration is already halting. Otherwise, while the counter is positive it simulates one transition, decrements the counter, and checks whether the new configuration is halting. If so, it outputs exactly what $M$ outputs, including when this was the $t(\mathrm{\mid }x\mathrm{\mid })$-th transition. If the counter is zero and the simulated configuration is still nonhalting, it rejects. This is the standard clocked simulation built from the effective transition table [L3] and universal behavior in [L2].

Step 2.1 proves the two clauses of the statement: runs of $M$ halting in at most $t(\mathrm{\mid }x\mathrm{\mid })$ transitions are preserved, and overlong runs are cut off by a halting reject state.