Let \(a, b, u, n, \tau , w \in \mathbb {N}\) satisfy \(n \le u\), \(\tau \le b\, (u+1)\), and \(w \le b\, (u+1)\). Then

The left-hand side gathers, as abstract summands, the costs of a clock run of length \(\tau \), an input reset over \(n\) cells, the fixed overheads, \(u+1\) budget rounds over a word of width \(w\), and the allocation and sweep stages measured in the unary budget \((a+1)(u+1)\); the inequality itself is a statement of pure natural-number arithmetic.

Let \(W\) be a machine over the Boolean alphabet, let \(a, b \in \mathbb {N}\), and let \(T \colon \mathbb {N}\to \mathbb {N}\) satisfy \(n \le T(n)\) for every \(n\). Suppose that on every Boolean input \(x\) the machine \(W\) halts within \(b\, (T(\left\lvert x\right\rvert )+1)\) steps with output exactly the list of (little-endian) binary digits of \(T(\left\lvert x\right\rvert )\). Then for every Boolean input \(x\), the length-only schedule machine built from \(W\) and the padding parameter \(a\), started on the embedding of \(x\) into the schedule alphabet (each bit sent to its tagged bit symbol), halts — through its clock capture, input reset, copy, fixed-width budget conversion, guide allocation, all macrosteps, and the final counter test — within a uniform quadratic budget: there exists a time

after which its control state is the halting state.

Let \(W\) and \(M\) be machines over the Boolean alphabet, let \(a, b \in \mathbb {N}\), and let \(T \colon \mathbb {N}\to \mathbb {N}\) satisfy \(n \le T(n)\) for every \(n\). Suppose that on every Boolean input \(x\) the machine \(W\) halts within \(b\, (T(\left\lvert x\right\rvert )+1)\) steps with output exactly the list of (little-endian) binary digits of \(T(\left\lvert x\right\rvert )\). Then for every Boolean input \(x\), the candidate oblivious simulator built from \(W\), \(M\), and \(a\) — the length-only schedule decorated by the data transducer for \(M\) and realized over the binary alphabet by transverse binary blocks — halts on \(x\) within the same uniform quadratic budget: there exists a time

after which its control state is the halting state. No hypothesis on the computation of the source machine \(M\) is needed, and the bound does not depend on \(M\).

Let \(P\) be a machine over an alphabet \(A\), decorated by a data transducer with \(l\) extra tapes, designated head index \(h\), a finite data-state set with initial element \(d_0\), and a visit function. For every input word \(x\), the initial configuration of the decorated machine on \(x\) equals the decorated configuration built from the initial configuration of \(P\) on \(x\), the initial data state \(d_0\), entirely blank extra tapes, and the empty output: the data tapes begin blank and aligned with the schedule’s origin.

Let \(P\) be a machine over an alphabet \(A\), decorated by a data transducer with \(l\) extra tapes, designated head index \(h\), initial data state, and visit function. Let \(c\) be a configuration of \(P\) on an input word \(x\) whose control state is a live state \(q\), let \(d\) be a data state, and fix contents for the \(l\) data tapes and an output word. Write \(v\) for the value of the visit function on \(q\), \(d\), the input symbol scanned by \(c\), the \(k\) work-tape reads of \(c\), and the data-tape symbols at the position of the designated head \(h\); thus \(v\) consists of a new data state, one optional write per data tape, and an optional emitted symbol. Then one step of the decorated machine from the decorated configuration equals the decorated configuration built from one step of \(P\) from \(c\), the new data state, each data tape updated by its optional write at the position of the designated head, and the output word extended by the emitted symbol when one is present. In particular the decorated transition consists of exactly the prescribed schedule step together with the local data visit.