For all binary machines \(W\) and \(M\) and every padding constant \(a\), the candidate simulator built from \(W\), \(M\), and \(a\) is oblivious: its head positions at every time step depend only on the length of the input. This holds on all binary inputs of every length, including the empty input, and uses no assumption about the computations of \(W\) or \(M\).

For every binary machine \(M\) and every vector of payload reads, the action selected in the halted state is the identity action: it performs no writes, emits no output, moves no head, and keeps the halted successor state.

For every binary machine \(M\) and every vector of payload reads, each of the \(k+1\) virtual head directions selected in the halted state is stationary.

For every natural number \(n\), the little-endian value of the canonical binary representation of \(n\) equals \(n\).

For every bit word, the borrow pass entered with a cleared borrow flag returns a cleared flag and leaves every bit of the word unchanged.

For every borrow flag and every bit word, the word produced by the borrow pass has exactly the length of the input word.

For every bit word \(w\), the borrow pass entered with a set borrow flag ends with a set flag if and only if the little-endian value of \(w\) is \(0\); this holds also for words padded with high zero bits.

For every bit word \(w\) whose little-endian value is positive, the word produced by the borrow pass entered with a set flag has little-endian value exactly one less than the value of \(w\).

In every single-lane configuration, the symbol read on the active lane is the first entry of the unprocessed list, or blank if that list is empty.

Let a single-lane configuration be given whose unprocessed list begins with an entry \(s\). Applying the single-lane action that writes an entry \(s'\) on the lane, moves right, and enters a state \(q\) yields again a single-lane configuration: the state becomes \(q\), the coordinate advances by one, \(s'\) is pushed onto the processed list, \(s\) is removed from the unprocessed list, and all other tapes and heads are unchanged.

Let a \(k\)-tape machine, a designated lane, an encoding of transducer states into machine states, an encoding of transducer letters into tape symbols, and a local transducer step be given. Suppose that from every encoded transducer state, whenever the lane reads an encoded letter, the machine performs exactly the single-lane action that writes the encoded output letter of the local step, moves right, and enters the encoded updated transducer state. Then running the machine for exactly \(\ell \) steps from a single-lane configuration whose unprocessed list begins with an encoded word of length \(\ell \) yields the single-lane configuration in which the transducer has been folded over the whole word: the state is the encoded final transducer state, the coordinate has advanced by \(\ell \), the encoded output word has been moved in reverse onto the processed list, and no inactive tape has changed.

For every carry flag and every bit word, folding the one-bit borrow transducer over the word is precisely the fixed-width borrow pass on that word.

Consider a machine with \(k\) leading work tapes followed by three administrative tapes, of which the first is the budget tape. For every state \(q\), optional symbol \(s\), and direction \(d\), the schedule action that enters \(q\), keeps the input head fixed, writes \(s\) with direction \(d\) on the budget tape, and leaves the two remaining administrative tapes and all \(k\) leading tapes untouched equals the single-lane action on the budget tape writing \(s\), moving in direction \(d\), and entering \(q\).

Let \(W\) be a binary machine and \(a\) a padding constant, and consider the length-only schedule controller built from them, whose first administrative tape is the budget tape. If the budget tape currently reads a bit symbol \(b\), then the transition out of the borrow control phase with carry \(c\) is the single-lane action on the budget tape that writes the bit \(b \oplus c\), moves right, and enters the borrow phase with carry \(c \wedge \lnot b\).

Let \(W\) be a binary machine, \(a\) a padding constant, and let a bit word \(w\) be laid out as bit symbols on the budget lane of the schedule controller, starting in the borrow phase with carry \(c\). Running the controller for exactly \(|w|\) steps carries out the fixed-width borrow pass on \(w\): the phase becomes borrow with the resulting borrow flag, the rewritten word is moved in reverse into the processed zone, the head has advanced by \(|w|\), and every other tape content and head position, including copied input data in later decorations, is unchanged.

For every configuration of a binary machine on an input \(x\) with input head at position \(p\), the virtual input payload of \(x\) at coordinate \(p - 1\) is exactly the pair of the symbol read by the native input head and the boundary tag of that configuration; on the empty input both boundary tags are produced correctly.

For every input head position \(p \in \{ 0, 1, \dots , n+1\} \) and every direction \(d\), the position reached by the native clamped input move of \(p\) in direction \(d\), shifted down by one, equals \(p - 1\) plus the clipped direction viewed as an integer.

For every configuration of a binary machine, the head-centered payload vector at offset \(0\) equals the read vector at the macrostep origin; reading the marked origin therefore obtains all source reads simultaneously.

For every binary machine \(M\) and every configuration \(c\) of \(M\) on an input \(x\), the action selected by the data controller from the control state of \(c\) and the head-centered payloads at offset \(0\) equals the totalized action of \(M\) at \(c\).

For every binary machine \(M\) and every configuration \(c\) of \(M\), applying the totalized action of \(M\) at \(c\) to \(c\) yields exactly one machine step of \(M\) from \(c\), including the idle step performed after \(M\) has halted.

For every binary machine \(M\) and every configuration \(c\) of \(M\) on an input \(x\), the vector of virtual head directions selected by the controller from the control state of \(c\) and the head-centered payloads at offset \(0\) equals the shift vector of the totalized action of \(M\) at \(c\); in particular native input clamping and source work head movement are reproduced exactly.

Let \(c\) be a configuration of a binary machine with \(k\) work tapes, let \(\alpha \) be an action, let \(z\) be an integer offset, and let \(i\) be one of the \(k+1\) virtual tape coordinates. Then the head-centered payload of the configuration obtained by applying \(\alpha \) to \(c\), at offset \(z\) and coordinate \(i\), equals the written payload of \(c\) and \(\alpha \) at offset \(z\) plus the shift direction of coordinate \(i\): writing at the old origin and then shifting each virtual tape by its displacement produces exactly the payloads of the successor configuration, including stationary moves, boundary attempts, and blank writes.

For every payload family and every coordinate \(z\), applying the forward transducer with register the payloads at \(z - 1\) to the uncached row at \(z\) produces the payloads at \(z\) as the new register together with the cached row at \(z\).

For every payload family \(f\), every vector of directions \(d\), and every coordinate \(z\), applying the backward transducer with directions \(d\) and register the payloads at \(z + 1\) to the cached row at \(z\) produces the payloads at \(z\) as the new register together with the uncached row at \(z\) of the shifted family sending coordinate \(z\) and tape \(i\) to the value of \(f\) at \(z\) plus the direction of \(i\).

For every payload family, starting coordinate, caching flag, and length \(n\), the zone of \(n\) rows is a list of length exactly \(n\); every guide cell thus contributes exactly one parallel data row.

For every payload family, coordinate \(z\), and length \(n\), folding the forward transducer with initial register the payloads at \(z - 1\) over the uncached zone of \(n\) rows starting at \(z\) ends with register the payloads at \(z + n - 1\) and produces the cached zone of the same \(n\) rows; all left-neighbor caches are installed.

For every payload family \(f\), every vector of directions \(d\), every coordinate \(z\), and every length \(n\), folding the backward transducer with directions \(d\) and initial register the payloads at \(z + n\) over the reversed cached zone of \(n\) rows starting at \(z\) ends with register the payloads at \(z\) and produces the reversed uncached zone of the family shifted per tape by \(d\); every row is shifted as prescribed.

Let \(c\) be a configuration of a binary machine, \(\alpha \) an action, \(z\) a coordinate, and \(n\) a width. Folding the backward transducer with the shift directions of \(\alpha \), seeded with the written payloads of \(c\) and \(\alpha \) at \(z + n\), over the reversed cached zone of written payloads starting at \(z\) yields the written payloads at \(z\) together with the reversed uncached zone of the head-centered payloads of the configuration obtained by applying \(\alpha \) to \(c\); the two finite transductions thus realize one source action on the whole fixed layout.

For every binary word \(x\) and every integer coordinate \(z\) with \(z \lt -1\) or \(z \gt |x|\), the virtual input payload of \(x\) at \(z\) is the blank payload; outside both virtual boundaries the head-centered input tape is blank.

Let \(M\) be a binary machine, \(x\) an input, and \(t, B\) natural numbers with \(t \le B\) and \(|x| + 1 \le B\). Then for every integer coordinate \(z\) with \(z \lt -3B\) or \(z \gt 3B\) and every virtual tape coordinate, the head-centered payload of the configuration reached by running \(M\) for \(t\) steps from its initial configuration on \(x\) is the blank payload. This bound uses the initialized run, not arbitrary starting configurations.

For every bit list \(w\) and every optional bit \(b\), the last entry, defaulting to false, of \(w\) extended by the zero- or one-element list determined by \(b\) equals \(b\) when \(b\) is present, and the last entry of \(w\) defaulting to false otherwise; a one-bit last-output register can therefore be maintained in finite control.

Let \(M\) be a binary machine that decides a language \(L\) over the binary alphabet within time \(a \cdot T(n)\) on inputs of length \(n\). Then for every input \(x\), after running \(M\) for \((a + 1)(T(|x|) + 1)\) steps from its initial configuration on \(x\), the last bit of the output word, defaulting to false, equals the indicator of the membership of \(x\) in \(L\).

The captured clock tape of the empty word is blank everywhere except for the origin sentinel at coordinate \(0\).

For every bit word \(w\) and every bit \(b\), the captured clock tape of \(w\) extended by \(b\) differs from the captured tape of \(w\) in exactly one cell: the cell at coordinate \(|w| + 1\), which becomes the bit symbol of \(b\).

Let \(W\) be a binary machine, \(a\) a padding constant, and \(c\) a configuration of \(W\) on an input \(x\). After forgetting the bit values (retaining only whether a symbol is present), the symbol read by the input head of the clock-stage configuration of \(c\) agrees with the correspondingly masked native read of \(c\).

Let \(W\) be a binary machine, \(a\) a padding constant, and \(c\) a configuration of \(W\). Decoding the bit symbols read on the \(k\) leading work tapes of the clock-stage configuration of \(c\) recovers exactly the work-tape reads of \(c\).

Let \(W\) be a binary machine, \(a\) a padding constant, and \(c\) a live configuration of \(W\) on an input \(x\) (its control state is some state \(q\)). Then one step of the schedule controller from the clock-stage configuration of \(c\) equals the clock-stage configuration of one step, from \(c\), of the masked clock machine obtained from \(W\) by ignoring the input bit values; in particular any bit emitted by that step, including a final emission, is captured on the budget tape, and administrative work begins only after this transition.

Every element of the canonical three-element index type equals \(0\), \(1\), or \(2\).

Let \(W\) be a binary machine, \(a\) a padding constant, and \(x\) a binary input. One step of the schedule controller from its initial configuration on the block-encoded input equals the clock-stage configuration of the initial configuration on \(x\) of the masked clock machine obtained from \(W\); this single transition installs both sentinels and starts the clock.

Let \(W\) be a binary machine, \(a\) a padding constant, \(x\) a binary input, and \(\tau \) a time bound such that the masked clock machine obtained from \(W\), started on \(x\), is still live at every time strictly before \(\tau \). Then for every \(t \le \tau \), running the schedule controller for \(t + 1\) steps from its initial configuration on the block-encoded input equals the clock-stage configuration of the masked clock run for \(t\) steps from its initial configuration on \(x\); every emitted budget bit is thereby represented.

Let \(W\) be a binary machine, let \(a\) and \(b\) be constants, and let a time bound \(T\) be such that on every input \(x\), the machine \(W\) outputs the binary representation of \(T(|x|)\) within \(b\, (T(|x|)+1)\) steps. Then for every input \(x\) there exist a time \(\tau \le b\, (T(|x|)+1)\) and a halted configuration \(c\) of \(W\) on \(x\) whose output is the binary representation of \(T(|x|)\), such that running the schedule controller for \(\tau + 1\) steps from its initial configuration on the block-encoded input equals the clock-stage configuration of \(c\). No assumption that \(W\) is oblivious is used.

For every radius \(R\) and every integer coordinate \(z\), the guide tape of radius \(R\) carries the left edge marker at \(z\) if and only if \(z = -R - 1\).

For every radius \(R\) and every integer coordinate \(z\), the guide tape of radius \(R\) carries the right edge marker at \(z\) if and only if \(z = R + 1\).

For every radius \(R\) and every integer coordinate \(z\), the guide tape of radius \(R\) carries the origin marker at \(z\) if and only if \(z = 0\).

In every macrostep configuration with unary head at \(u\), the symbol read on the unary tape is the base configuration’s unary tape content at coordinate \(u\).

In every macrostep configuration with guide head at \(g\), the symbol read on the guide tape is the base configuration’s guide tape content at coordinate \(g\).

Let a macrostep configuration with phase \(q\), unary head \(u\), and guide head \(g\) be given. Applying the read-only schedule action that enters a phase \(q'\), keeps the input and budget heads fixed, writes nothing, and moves the unary and guide heads in directions \(d_u\) and \(d_g\) yields the macrostep configuration with phase \(q'\), unary head \(u + d_u\), and guide head \(g + d_g\).

For every macrostep configuration in the counter-test phase with unary head \(u\) and guide head \(g\): if the base’s unary tape holds a unit marker at \(u\), one step of the schedule controller enters the leftward-seek phase; otherwise it halts. In both cases every head stays in place.

Suppose the base’s guide tape is the fixed guide of radius \(R\). From the leftward-seek phase with guide head at \(g\), one step of the schedule controller turns into the forward phase and moves the guide head right exactly when \(g = -R - 1\), and otherwise stays in the seek phase and moves the guide head left.

Suppose the base’s guide tape is the fixed guide of radius \(R\). From the forward phase with guide head at \(g\), one step of the schedule controller turns into the backward phase and moves the guide head left exactly when \(g = R + 1\), and otherwise stays in the forward phase and moves the guide head right.

Suppose the base’s guide tape is the fixed guide of radius \(R\). From the backward phase with guide head at \(g\), one step of the schedule controller turns into the return-to-center phase and moves the guide head right exactly when \(g = -R - 1\), and otherwise stays in the backward phase and moves the guide head left.

Suppose the base’s guide tape is the fixed guide of radius \(R\). From the return-to-center phase with guide head at \(g\), one step of the schedule controller commits exactly at the origin: when \(g = 0\) it enters the counter-test phase and advances the unary head by one, and otherwise it stays in the return phase and moves the guide head right.

Suppose the base’s guide tape is the fixed guide of radius \(R\) and let \(n \le R + 1\). Running the schedule controller for \(n\) steps from the leftward-seek phase with guide head at the origin stays in the seek phase and moves the guide head to \(-n\).

Suppose the base’s guide tape is the fixed guide of radius \(R\) and let \(n \le 2R + 1\). Running the schedule controller for \(n\) steps from the forward phase with guide head at \(-R\) stays in the forward phase and moves the guide head to \(-R + n\).

Suppose the base’s guide tape is the fixed guide of radius \(R\) and let \(n \le 2R + 1\). Running the schedule controller for \(n\) steps from the backward phase with guide head at \(R\) stays in the backward phase and moves the guide head to \(R - n\).

Suppose the base’s guide tape is the fixed guide of radius \(R\) and let \(n \le R\). Running the schedule controller for \(n\) steps from the return-to-center phase with guide head at \(-R\) stays in the return phase and moves the guide head to \(-R + n\).

Suppose the base’s guide tape is the fixed guide of radius \(R\) and its unary tape holds a unit marker at coordinate \(u\). Then running the schedule controller for exactly \(6R + 8\) steps from the counter-test phase with unary head at \(u\) and guide head at the origin executes the entire fixed path of one macrostep and returns to the counter-test phase with unary head at \(u + 1\) and guide head at the origin.

Suppose the base’s guide tape is the fixed guide of radius \(R\) and its unary tape holds unit markers at all coordinates \(1, 2, \dots , B\). Then for every \(j \le B\), running the schedule controller for \(j\, (6R + 8)\) steps from the counter-test phase with unary head at \(1\) and guide head at the origin reaches the counter-test phase with unary head at \(j + 1\) and guide head at the origin, regardless of all simulated data and of source halting behavior.

Suppose the base’s guide tape is the fixed guide of radius \(R\), its unary tape holds unit markers at all coordinates \(1, 2, \dots , B\), and the unary cell at coordinate \(B + 1\) is blank. Then running the schedule controller for \(B\, (6R + 8) + 1\) steps from the counter-test phase with unary head at \(1\) and guide head at the origin ends in the halted phase with unary head at \(B + 1\) and guide head at the origin: the schedule finishes after exactly the budgeted macrosteps plus one final counter test.