Let \(M\) be a multi-tape Turing machine over the Boolean alphabet and \(c\) a configuration of \(M\). If after \(t\) steps from \(c\) the machine has not halted, then for every \(u \le t\) the machine has not halted after \(u\) steps either.

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet and \(c\) a configuration of \(M\). If the output after \(t\) steps from \(c\) is empty, then the output after \(u\) steps is empty for every \(u \le t\), since output is append-only.

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet and \(c\) a configuration whose control state is live. If \(M\) has halted \(t\) steps after \(c\), then there is a time \(u\) with \(0 \lt u \le t\) such that \(M\) is not halted at any time strictly before \(u\), is halted at time \(u\), and the configuration at time \(u\) equals the configuration at time \(t\).

Let \(I\) be a binary predicate on Boolean words, let \(F\) be a step function on Boolean words indexed by an input word, and let \(s_0\) assign an initial word to each input. If \(I(x, s_0(x))\) holds for every input \(x\) and \(I(x, s)\) implies \(I(x, F(x, s))\), then \(I(x, F(x, \cdot )^{i}(s_0(x)))\) holds for every input \(x\) and every iteration count \(i\).

Let \(F\) be a bundled finite machine over the Boolean alphabet that computes, in time \(T\), the function sending each input \(x\) to the binary digit word of \(R(|x|)\). Then for every input \(x\), the length of that digit word is at most \(T(|x|)\), since a run can append at most one output symbol per step.

For every clamped input-head position \(p\) among the \(n+2\) positions of an input of length \(n\) and every direction \(m\) (left, stay, or right), the position reached by one native input-head move in direction \(m\) has value at most the value of \(p\) plus one.

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet and \(c\) a configuration of \(M\). After running \(t\) steps from \(c\), the input-head position is at most the input- head position of \(c\) plus \(t\).

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet and \(c\) a configuration of \(M\). After running \(t\) steps from \(c\), the output length is at most the output length of \(c\) plus \(t\).

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet with two distinguished control states: a start state whose every transition moves the input head left and enters a scan state, and a scan state that keeps moving left while it reads an input symbol and, on reading the left boundary blank, moves right and enters a given destination state. Then from any configuration \(c\) in the start state there is a time \(t\) at most the input-head position of \(c\) plus two after which the machine sits in the destination state with input head at position one and every other component of \(c\) unchanged.

For every Boolean word \(u\), the length of the maximal \(\mathrm{false}\) prefix of \(u\) is at most the length of \(u\).

For every Boolean word \(u\), the word produced by the fixed-width little-endian decrement of \(u\) has exactly the length of \(u\), both on success and on underflow.

For every natural number \(n\), the little-endian counter value of the standard binary digit word of \(n\) equals \(n\).

For every Boolean word \(u\) read as a little-endian counter: if the fixed-width decrement of \(u\) reports success then the value of the decremented word plus one equals the value of \(u\), and if it reports underflow then the value of \(u\) is zero.

For every Boolean word \(u\) read as a little-endian counter, the fixed-width decrement of \(u\) reports success if and only if the value of \(u\) is positive.

For every Boolean word \(u\) and every iteration count \(i\), applying the fixed-width little-endian decrement \(i\) times to \(u\) yields a word of exactly the length of \(u\).

For all natural numbers \(R\) and \(i\) with \(i \le R\), applying the fixed-width little- endian decrement \(i\) times to the binary digit word of \(R\) yields a word of counter value exactly \(R - i\).

For all Boolean words \(p\) and \(b\), the buffer tape holding the concatenation of \(p\) and \(b\) (cells \(0, \dots \) hold the word, every other cell is blank) reads, at cell \(|p|\), the first bit of \(b\), or blank when \(b\) is empty.

For all Boolean words \(p\) and \(b\) and bits \(u\) and \(v\): updating cell \(|p|\) of the buffer tape that holds \(p\) followed by \(u\) followed by \(b\), writing the bit \(v\) there, produces exactly the buffer tape that holds \(p\) followed by \(v\) followed by \(b\).

Let \(p\) and \(b\) be Boolean words. One step of the one-tape counter decrement machine from its borrow state, at cell \(|p|\) of the buffer tape holding \(p\) followed by \(b\), behaves as follows: on an empty \(b\) it enters the rewind state with failure flag one cell to the left without writing; on a leading \(\mathrm{true}\) bit it writes \(\mathrm{false}\), moves left, and enters the rewind state with success flag; on a leading \(\mathrm{false}\) bit it writes \(\mathrm{true}\), moves right, and stays in the borrow state.

Let \(p\) and \(u\) be Boolean words and let \(j\) be the length of the maximal \(\mathrm{false}\) prefix of \(u\). Starting the one-tape counter decrement machine in its borrow state at cell \(|p|\) of the buffer tape holding \(p\) followed by \(u\), after exactly \(j + 1\) steps it is in the rewind state carrying the decrement’s success flag, at cell \(|p| + j - 1\), with tape contents \(p\) followed by the decremented word.

Let \(u\) be a Boolean word, \(b\) a flag bit, and \(j \le |u|\). Starting the one-tape counter decrement machine in its rewind state with flag \(b\) at cell \(j - 1\) over the buffer tape of \(u\), after exactly \(j + 1\) steps it is in the return state indexed by \(b\), at cell zero, with the word \(u\) unchanged.

Let \(u\) be a Boolean word and \(j\) the length of its maximal \(\mathrm{false}\) prefix. Then \(2j + 2 \le 2|u| + 2\), and running the one-tape counter decrement machine for exactly \(2j + 2\) steps from its borrow state at cell zero over the buffer tape of \(u\) ends in the return state indexed by the decrement’s success flag, at cell zero, holding the decremented word, with nothing emitted.

Let \(c\) be a configuration of the loop body whose control state is the anchor and whose release bit is clear. One step of the stop wrapper from the embedding of \(c\) halts the wrapper, writes \(\mathrm{false}\) on the flag cell, and changes no other component of the embedded configuration.

Let \(c\) be a configuration of the loop body in a live control state \(q\), and suppose it is not the case that \(q\) is the anchor with the release bit clear. Then one step of the stop wrapper from the embedding of \(c\) equals the embedding of the body’s one-step successor of \(c\), with the release bit cleared and the flag set to \(\mathrm{true}\) exactly when that body step is a halting transition.

Let \(c\) be a live configuration of the loop body, let \(r\) be a release bit, and let \(t\) be a time such that the body stays live before \(t\) and, except possibly for a released step at time zero, does not visit the anchor before \(t\). Then the stop wrapper run for \(t\) steps from the embedding of \(c\) with release bit \(r\) equals the embedding of the body run at time \(t\), with the release bit consumed after the first action and the flag set to \(\mathrm{true}\) exactly when the body has halted at time \(t\).

Let a host machine agree, on a family of embedded control states, with the capture transformation of the stop wrapper of a loop body, and let \(c\) be a live body configuration together with a release bit and a time \(t\) satisfying the liveness and no- early-anchor guards. Then the host run for \(t\) steps from the capture embedding of \(c\) equals the capture embedding of the simulated stop-wrapper endpoint at time \(t\), including any output bit emitted by a halting transition.

Let \(c\) be a configuration of the extended stopped-body source on the loop host’s tape layout and \(t\) a time before which that source does not halt. Then the loop host run for \(t\) steps from the capture embedding of \(c\) (with the return phase determined by whether the call is a startup call) equals the capture embedding of the source run at time \(t\).

Let \(c\) be a configuration of the relocated fuel source on the loop host’s tape layout and \(t\) a time before which that source does not halt. Then the loop host run for \(t\) steps from the capture embedding of \(c\) equals the capture embedding of the fuel source run at time \(t\).

For every input word \(x\), the initial configuration of the loop host on \(x\) equals the capture embedding (with empty capture buffers and return phase zero) of the initial configuration of the relocated fuel source on \(x\).

For every input direction and successor state, the loop-controller action that performs no flag, counter, or payload operation and emits nothing equals the standard input-only control action with that direction and successor.

Let \(c\) be a configuration of the loop host in controller phase four. Then there is a time \(t\) at most the input-head position of \(c\) plus two after which the host sits in the startup body-call state with input head at position one and every other component of \(c\) unchanged.

Let a controller frame of the loop host be given, together with a controller action specified by an input direction, an optional flag write, counter and payload write-and- move pairs, an optional emitted bit, and a successor state. Applying the action to the frame yields the frame with the successor state, the moved input head, the three tracks updated by their optional writes at their current heads, the counter and payload heads moved as instructed, and the emitted bit appended to the output.

Let \(p\) and \(r\) be Boolean words. One step of the one-tape replay machine from its live state at cell \(|p|\) of the buffer tape holding \(p\) followed by \(r\) either halts without writing when \(r\) is empty, or, when \(r\) starts with a bit \(b\), appends \(b\) to the output and advances the head by one, leaving the stored word unchanged.

Let \(p\) and \(r\) be Boolean words and let an output prefix be given. After running the one-tape replay machine for exactly \(|r| + 1\) steps from its live state at cell \(|p|\) of the buffer tape holding \(p\) followed by \(r\), the machine is halted with the head at cell \(|p| + |r|\), the stored word is unchanged, and the output is extended by exactly \(r\) in order.

For every head direction \(d\), optional emitted bit, and successor state, the loop- controller action that only moves the payload head by \(d\) and emits that bit equals the right-block extension (leaving all earlier tapes stationary) of the corresponding one- tape action.

Let \(w\) be a captured word, let an output prefix and arbitrary completed body and fuel tapes with their head positions be given, and consider the loop host in its replay phase with the payload head at cell zero of the buffer tape of \(w\). After running the host for exactly \(|w| + 1\) steps, the host is halted, its output is extended by exactly \(w\), and the stored word, all inactive tapes, and all inactive heads are unchanged.

Let \(c\) be a configuration of the fuel machine and \(t\) a time. Running the relocated fuel source for \(t\) steps from the relocated embedding of \(c\) equals the relocated embedding of the fuel machine’s run from \(c\) at time \(t\).

For every input word \(x\), the initial configuration of the relocated fuel source on \(x\) equals the relocated embedding of the fuel machine’s initial configuration on \(x\).

For every controller frame of the loop host with payload tape \(f\) and payload head \(h\), the symbol scanned on the capture (payload) track of the frame is exactly \(f(h)\).

For every controller frame of the loop host with counter tape \(f\) and counter head \(h\), the symbol scanned on the counter track of the frame is exactly \(f(h)\).

Let \(w\) be a stored word and \(j \le |w|\). Starting the loop host in its fuel-rewind phase on a controller frame whose payload track is the buffer tape of \(w\) with payload head at cell \(j - 1\), after exactly \(j + 1\) steps the host is in the counter-copy phase with the payload head at cell zero and every other frame component unchanged.

For all Boolean words \(p\) and \(r\), the partially cleared copying tape with processed prefix \(p\) and suffix \(r\) reads, at cell \(|p|\), the first bit of \(r\), or blank when \(r\) is empty.

For all Boolean words \(p\) and \(r\) and every bit \(b\), blanking cell \(|p|\) of the partially cleared copying tape with processed prefix \(p\) and suffix \(b\) followed by \(r\) yields the partially cleared copying tape with processed prefix \(p\) extended by \(b\) and suffix \(r\).

For every Boolean word \(w\), the partially cleared copying tape with empty processed prefix and suffix \(w\) equals the buffer tape of \(w\).

For every Boolean word \(w\), the partially cleared copying tape with processed prefix \(w\) and empty suffix equals the blank buffer tape.

Let \(p\) be the already-copied prefix and \(r\) the remaining fuel suffix. Starting the loop host in its counter-copy phase on a controller frame whose counter track is the buffer tape of \(p\) and whose payload track is the partially cleared copying tape, with both heads at cell \(|p|\), after exactly \(|r| + 1\) steps the host is in the synchronized- rewind phase with the counter track holding the full fuel word, the payload track blank, and both heads one cell left of the word’s right end.

Let \(w\) be the copied counter word and \(j \le |w|\). Starting the loop host in its synchronized-rewind phase on a controller frame whose counter track is the buffer tape of \(w\) and whose payload track is blank, with both heads at cell \(j - 1\), after exactly \(j + 1\) steps the host is in the input-rewind phase with both heads at cell zero and every other frame component unchanged.

Let \(w\) be the captured fuel word. Starting the loop host in controller phase zero on a frame whose counter track is blank and whose payload track is the buffer tape of \(w\) with payload head at cell \(|w|\), after exactly \(3|w| + 4\) steps the host is in the input-rewind phase with the counter track holding \(w\), the payload track blank, both heads at cell zero, and all inactive data unchanged. The empty word is included.

Let \(c\) be a halted configuration of the fuel machine. The captured fuel endpoint of the loop host equals the controller frame over itself in phase zero whose flag and counter tracks are blank, whose payload track is the buffer tape of the output of \(c\) with payload head at its length, with the input head of \(c\) and empty output.

Let the fuel machine compute, in time \(T\), the function sending each input \(x\) to the binary digit word of \(R(|x|)\). Then for every input \(x\) there are a halted fuel configuration \(c\) with output exactly that digit word and a time \(t \le 5\, T(|x|) + 7\) such that the loop host, run for \(t\) steps from its initial configuration on \(x\), reaches the prepared startup configuration built from \(c\).

Let \(c\) be a configuration of the body’s stop wrapper, and let arbitrary counter and fuel tapes and heads be given. Running the extended stopped-body source for \(t\) steps from the left-block embedding of \(c\) over those inactive tapes equals the left-block embedding of the stop wrapper’s run at time \(t\) over the same inactive tapes.

Let \(c\) be a body configuration, \(t\) a time at which the body run from \(c\) sits in the anchor state, with no earlier anchor visit except possibly a released step at time zero, and with the release bit clear whenever \(t = 0\). Then the loop host, run for \(t + 1\) steps from the body call built on \(c\), reaches the stopped call whose body data is the body run at time \(t\) with control removed, release clear, and stop flag \(\mathrm{false}\), with the counter word and fuel residue unchanged.

For every halted fuel configuration \(f\), the prepared startup configuration of the loop host equals the startup body call built on the body’s initial configuration with release clear, no flag, counter word the output of \(f\), and fuel residue \(f\).

Let \(c\) be a body configuration, \(w\) a counter word, and \(f\) a fuel configuration. One step of the loop host from the startup call on \(c\) with control removed, release clear, and flag \(\mathrm{false}\) yields the active (non-startup) call on \(c\) with control the anchor, release set, and no flag, changing no body, counter, or fuel data.

Let \(s\) be a word, \(f\) a fuel configuration, and \(t\) a time such that the body, run from its initial configuration, first visits the anchor at time \(t\), arriving at the clean seam that carries \(s\) on work tape zero with all other work tapes blank. Then the loop host, run for \(t + 2\) steps from the prepared startup configuration, reaches the active released call on that seam with counter word the output of \(f\) and fuel residue \(f\).

Let \(c\) be a body configuration and \(t \gt 0\) a time such that the body stays live before \(t\), does not visit the anchor strictly between times zero and \(t\), and is halted at time \(t\). Then the loop host, run for \(t\) steps from the active released call on \(c\), reaches the stopped call on the body run at time \(t\) with release clear and stop flag \(\mathrm{true}\), the complete body output captured, including any bit emitted by the halting transition.

For every body call of the loop host, built on a body configuration \(c\) with flag bit, counter word \(w\), and fuel residue, the call equals the controller frame over itself whose flag track stores the flag bit at the origin, whose counter track is the buffer tape of \(w\) with head at zero, and whose payload track is the buffer tape of the output of \(c\) with head at that output’s length, with empty physical output.

Let \(c\) be a body configuration with counter word \(w\) and fuel residue, and let new startup, release, flag, counter-word, and control-state parameters be given. The controller frame built over the original call with the new call’s control state, the new flag at the origin, and the buffer tape of the new counter word equals the call built on \(c\) with the replaced control state and the new parameters.

Let \(p\) and \(r\) be Boolean words. One step of the loop host from its borrow phase on a frame whose counter track is the buffer tape of \(p\) followed by \(r\) with counter head at \(|p|\) behaves as the standalone decrement machine: an empty \(r\) enters the underflow- rewind phase moving left; a leading \(\mathrm{true}\) writes \(\mathrm{false}\) and enters the success-rewind phase moving left; a leading \(\mathrm{false}\) writes \(\mathrm{true}\) and continues the borrow moving right. Only the counter track changes.

Let \(p\) and \(w\) be Boolean words and \(j\) the length of the maximal \(\mathrm{false}\) prefix of \(w\). Running the loop host for exactly \(j + 1\) steps from its borrow phase on a frame whose counter track holds \(p\) followed by \(w\) with head at \(|p|\) reaches the success- or underflow-rewind phase according to the decrement’s flag, with the counter track holding \(p\) followed by the decremented word and head at \(|p| + j - 1\); all non- counter tracks are preserved.

Let \(w\) be a counter word, \(b\) a success bit, and \(j \le |w|\). Running the loop host for exactly \(j + 1\) steps from the rewind phase selected by \(b\) on a frame whose counter track is the buffer tape of \(w\) with head at cell \(j - 1\) returns the counter head to zero and dispatches: success releases the next anchor call, underflow enters the exhaustion phase without yet emitting. All inactive residue is retained.

Let \(w\) be a counter word and \(j\) the length of its maximal \(\mathrm{false}\) prefix. Then \(2j + 2 \le 2|w| + 2\), and running the loop host for exactly \(2j + 2\) steps from its borrow phase on a frame whose counter track is the buffer tape of \(w\) with head at zero ends with the counter track holding the decremented word, head at zero, in the released next-anchor call state on success and in the exhaustion phase on underflow.

For every controller frame of the loop host with flag tape \(f\), the symbol scanned on the flag track of the frame is exactly \(f(0)\), independently of all inactive residue.

For every optional flag bit, blanking the origin cell of the tape that stores that bit at the origin and is blank elsewhere yields the completely blank buffer tape.

Let \(c\) be a halted body configuration with empty output, \(w\) a counter word, and \(f\) a fuel configuration. Then there is a time \(t \le 2|w| + 4\) such that, from the stopped call on \(c\) with stop flag \(\mathrm{false}\): if the fixed-width decrement of \(w\) succeeds, the loop host at time \(t\) is at the released next-anchor call with the decremented counter word; otherwise the host at time \(t\) has halted with output empty in find mode and the single bit \(\mathrm{false}\) in decision mode.

Let \(w\) be a captured payload word and \(j \le |w|\). Running the loop host for exactly \(j + 1\) steps from its payload-rewind phase on a frame whose payload track is the buffer tape of \(w\) with payload head at cell \(j - 1\) reaches the replay phase with the payload head at cell zero and every other frame component unchanged.

Let \(w\) be a captured payload word and consider the loop host in its replay phase on a frame with empty output whose payload track is the buffer tape of \(w\) with head at zero. After exactly \(|w| + 1\) steps the host has halted and its output is exactly \(w\).

Let \(c\) be a halted body configuration, \(w\) a counter word, and \(f\) a fuel configuration. Then there is a time \(t \le 2\, |o| + 3\), where \(o\) is the output of \(c\), such that from the stopped call on \(c\) with stop flag \(\mathrm{true}\) the loop host at time \(t\) has halted with output \(o\) in find mode and output the single bit \(\mathrm{true}\) in decision mode.

Let \(s\) be a round word, \(w\) a counter word, \(f\) a fuel configuration, and \(t \gt 0\) a time such that the body, started at the clean anchor seam carrying \(s\), does not revisit the anchor strictly between times zero and \(t\) and at time \(t\) either halts with a declared payload (acceptance) or sits at the clean seam carrying the stepped word. Then there is a time \(v \le 3t + 2|w| + 5\) such that from the released call on the seam of \(s\): acceptance halts the host with the payload (find mode) or the bit \(\mathrm{true}\) (decision mode); a rejection with successful decrement reaches the released call on the next seam with the decremented counter; and a rejection with underflow halts with empty output (find mode) or the bit \(\mathrm{false}\) (decision mode).

Let a loop body with anchor, a fuel machine computing the binary digits of \(R(|x|)\) in time \(T\), an invariant preserved from the initial word by the step function, a bounded anchor-free startup, and a per-round contract (positive duration at most \(T(|x|)\), no early anchor revisit, and accept-with-output or advance-to-stepped-seam) be given, together with an output mode. Then there is a constant \(c\) such that for every input \(x\) the loop host has a round-configuration family: a startup segment of at most \(c (T(|x|) + 1)\) steps reaching round zero, empty output at every round configuration up to \(R(|x|)\), a halted terminal at index \(R(|x|) + 1\) with output empty in find mode and the bit \(\mathrm{false}\) in decision mode, and for each round \(i \le R(|x|)\) a segment of at most \(c (T(|x|) + 1)\) steps that halts with the declared output when round \(i\) accepts and reaches round \(i + 1\) otherwise.

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet, let \(c_0, \dots , c_N\) be configurations of \(M\) on a common input with \(c_N\) halted with output the single bit \(\mathrm{false}\), and let \(a\) be a Boolean predicate on round indices. Assume for each \(j \lt N\) that within \(B\) steps the machine either halts from \(c_j\) with output the single bit \(\mathrm{true}\) (when \(a(j)\) holds) or reaches \(c_{j+1}\) (when \(a(j)\) fails). Then from \(c_0\) the machine halts within \(N \cdot B\) steps with output the single bit recording whether \(a(j)\) holds for some \(j \lt N\).

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet, let \(c_0, \dots , c_N\) be configurations of \(M\) on a common input with \(c_N\) halted with empty output, let \(a\) be a Boolean predicate on round indices, and let \(w\) assign a payload word to each index. Assume for each \(j \lt N\) that within \(B\) steps the machine either halts from \(c_j\) with output \(w(j)\) (when \(a(j)\) holds) or reaches \(c_{j+1}\) (when \(a(j)\) fails). Then from \(c_0\) the machine halts within \(N \cdot B\) steps, with output \(w(i)\) for the least accepting index \(i \lt N\) when one exists and empty output otherwise.

Let \(M\) be a bundled finite machine, \(c\) a configuration of \(M\) on a simulated argument carrying a valid virtual boundary tag, and \(t\) a time before which the run of \(M\) from \(c\) stays live. Then there is a valid tag for the endpoint such that running the capture-wrapped evaluator for \(t\) steps from the evaluator configuration of \(c\) equals the evaluator configuration of the run of \(M\) from \(c\) at time \(t\).

For every physical input \(w\) and argument word \(s\), the evaluator configuration built from the initial configuration of \(M\) on \(s\), with initial tag and physical input head at one, equals the canonical seam configuration of the capture-wrapped evaluator whose first work tape holds \(s\), all other work tapes blank, all heads at their origins, and output empty.

Let \(M\) compute output \(o\) on argument \(s\) within time \(T\). Then there is a time \(t \le T\) and a boundary tag such that the run of \(M\) from its initial configuration on \(s\) is halted at \(t\) with output \(o\), the capture-wrapped evaluator started on the prepared candidate does not visit its return state before \(t\), and at time \(t\) it is exactly the evaluator configuration of that halted run.

For every data tape \(d\), integer \(\ell \), and count \(j\), blanking the cell \(\ell + j\) of the tape obtained from \(d\) by erasing the first \(j\) interval cells yields the tape obtained from \(d\) by erasing the first \(j + 1\) interval cells.

Let \(d\) be a data tape and let an interval of width \(m\) start at \(\ell \). For every \(j \lt m\), running the interval cleaner for exactly \(j + 2\) steps from its initial state with all heads at \(\ell + j\) reaches its rightward-erasure state with all heads at \(\ell \), independently of blank holes in \(d\).

For every data tape \(d\) and integer \(\ell \), erasing the first zero cells of the interval starting at \(\ell \) yields \(d\) unchanged.

Let \(d\) be a data tape that is blank outside the interval of width \(m\) starting at \(\ell \). Then erasing all \(m\) interval cells of \(d\) yields the completely blank tape, with no assumption on the values inside the interval.

Let \(d\) be a data tape and let an interval of width \(m\) start at \(\ell \). For every \(j \le m\), running the interval cleaner for exactly \(j\) steps from its rightward-erasure state with all heads at \(\ell \) erases the first \(j\) cells of both the data and the marker, moves all heads to \(\ell + j\), and leaves the origin marker intact.

Blanking the origin cell of the tape that holds \(\mathrm{true}\) exactly at the origin yields the completely blank tape.

For every natural number \(n\), running the interval cleaner for exactly \(n + 1\) steps from its rewind state with blank data and marker tapes and all heads at \(n\) reaches the silent return state with all three tapes blank and all heads at the origin, the origin marker being erased by the final transition.

Let \(d\) be a data tape blank outside an interval of width \(m\) starting at \(\ell \), with \(\ell \le 0 \lt \ell + m\), and let the heads start at \(\ell + j\) for some \(j \lt m\). Then there is a positive time \(t \le 3m + 4\) after which the interval cleaner, started in its initial state on \(d\), the interval marker, and the origin marker, is in its silent return state with all three tapes blank and all heads at the origin.

Let \(\ell \le h\) be integers and let \(p\) be a cell with \(\ell - 1 \le p \le h + 1\). Writing the mark at \(p\) on the closed-span marker for \([\ell , h]\) yields the closed-span marker for \([\min (\ell ,p), \max (h,p)]\).

Let \(c\) be a live configuration of the source machine with visited bounds \(\ell \) and \(h\). One step of the tracked evaluator from the completed tracked configuration of \(c\) equals the intermediate stamp configuration of the one-step successor of \(c\) with the same bounds: the data bank performs the source write and emission, and all three per- tape heads move by the same source action.

Let \(c\) be a source configuration with visited bounds \(\ell _i \le h_i\) such that each head of \(c\) lies within one cell of its span. One step of the tracked evaluator from the intermediate stamp configuration of \(c\) equals the completed tracked configuration of \(c\) with each span extended to include the current head, after which the stored successor control (possibly a halt) is dispatched.

For every machine \(M\), input \(x\), time \(t\), and work tape \(i\): the leftmost visited position is at most zero, the rightmost is at least zero, the current head at time \(t\) lies between them, and they lie within \([-t, t]\), so the visited interval has width at most \(2t + 1\).

For every machine \(M\), input \(x\), time \(t\), work tape \(i\), and cell \(z\) outside the visited interval of tape \(i\) at time \(t\), the cell \(z\) of tape \(i\) after running \(M\) for \(t\) steps from its initial configuration on \(x\) is blank.

The closed-span marker of the one-point interval \([0,0]\) equals the buffer tape holding the single bit \(\mathrm{true}\).

For every machine \(M\) and input \(x\), one step of the tracked evaluator from its initial configuration on \(x\) equals the completed tracked configuration of the initial configuration of \(M\) on \(x\) with all visited bounds zero: both marker banks hold origin marks, the data bank is blank, and the output is empty.

For every machine \(M\), input \(x\), and time \(t\), running the tracked evaluator for \(1 + 2t\) steps from its initial configuration on \(x\) equals the completed tracked configuration of the run of \(M\) at time \(t\) with the true leftmost and rightmost visited bounds, including after the source has halted.

Let \(M\) compute output \(o\) on input \(x\) within time \(T\). Then the tracked evaluator of \(M\) computes the same output \(o\) on \(x\) within time \(1 + 2T\).

For all integers \(\ell \le h\), the closed-span marker of \([\ell , h]\) equals the half- open interval marker starting at \(\ell \) of width \(h - \ell + 1\).

Let \(M\) be a machine, \(x\) an input, \(T\) a time, and \(i\) a work tape. Then there is a positive time \(t \le 6T + 7\) after which the interval cleaner, started on the actual tape \(i\) of the run of \(M\) at time \(T\), the closed-span marker of the visited interval, and the origin marker, with heads at the actual head position, reaches its return state with all three tapes blank and all heads at the origin.

Let \(M\) be a multi-tape Turing machine over the Boolean alphabet, let a set of stop control states be absorbing (a step from any configuration in a stop state changes nothing), and suppose the run from a configuration \(c\) reaches a configuration \(d\) in a stop state at time \(T\). Then there is a time \(t \le T\) such that no stop state is visited strictly before \(t\) and the run from \(c\) at time \(t\) equals \(d\).

Let \(M\) be a machine, \(x\) an input, \(T\) a time, and \(i\) a work tape. Then there is a positive time \(t \le 6T + 7\) such that the interval cleaner, started on the actual tape \(i\) of the run of \(M\) at time \(T\) with its visited-span and origin markers, does not visit its return state before \(t\) and at time \(t\) is exactly the blank-endpoint return configuration with all heads at the origin.

Let \(c\) be a live configuration of the source machine. One step of the right-boundary wrapper from the embedding of \(c\) equals the embedding of the one-step successor of \(c\), including any halting emission; only the successor control encoding differs.

Let \(c\) be a configuration of the source machine and \(t\) a time before which the source run from \(c\) stays live. Then the right-boundary wrapper run for \(t\) steps from the embedding of \(c\) equals the embedding of the source run at time \(t\).

Let \(c\) be a completed source configuration on an input \(x\) and let \(j\) and \(r\) satisfy \(j + r = |x|\). Running the right-boundary wrapper for exactly \(r + 1\) steps from the live scan configuration at position \(j\) halts it silently at the right-boundary scan configuration at position \(|x|\), never confusing a blank work cell with the input end.

Let \(c\) be a halted configuration of the source machine on an input \(x\). Then there is a time \(t \le |x| + 2\) such that the right-boundary wrapper, run for \(t\) steps from the embedding of \(c\), is the halted scan configuration at position \(|x|\), with the work tapes and output of \(c\) unchanged.

Let \(M\) be a machine and \(x\) an input such that the run of \(M\) from its initial configuration is halted at time \(T\). Then the right-boundary wrapper of \(M\), run for \(T + |x| + 2\) steps from its initial configuration on \(x\), equals the halted scan configuration built on the run of \(M\) at time \(T\), with input head at position \(|x| + 1\).

Let \(M\) compute output \(o\) on input \(x\) within time \(T\). Then the right-boundary wrapper of \(M\) computes \(o\) on \(x\) within time \(T + |x| + 2\), and after exactly that many steps its input head is at position \(|x| + 1\).

Let \(M\) compute output \(o\) on argument \(s\) within time \(T\), and consider the capture- wrapped evaluator of the right-boundary wrapper of the tracked evaluator of \(M\), started on the prepared candidate seam for \(s\). Then there is a positive time \(t \le 1 + 2T + |s| + 2\) such that the evaluator does not visit its return state before \(t\) and at time \(t\) is exactly the evaluator configuration of the halted, right-normalized tracked endpoint: full trace banks, complete capture buffer, and candidate head at the right boundary.

For every partial tape selection, control embedding, default tapes and heads, source action \(a\), and source configuration \(c\): applying the relocated action to the relocated configuration of \(c\) equals the relocated configuration of \(a\) applied to \(c\), including the write, head motion, and emission; unselected tapes and heads are fixed.

Let a source machine, a host machine, a tape index map with a partial inverse selection, and a control embedding be given such that on all good source states the host transition equals the relocated source transition. If every live state visited by the source run from a configuration \(c\) before time \(t\) is good, then the host run for \(t\) steps from the relocated configuration of \(c\) equals the relocated configuration of the source run at time \(t\).

For every Boolean word \(w\) and bit \(b\), blanking cell \(|w|\) of the buffer tape holding \(w\) followed by \(b\) yields the buffer tape of \(w\).

Let the finalizer run in a fixed mode on an argument word \(a\) and a capture word \(c\), and let \(p\) be a prefix of \(a\). Starting from its argument-scan state with the argument head at cell \(|p| - 1\) – the argument tape holding \(a\) in emit mode and only \(p\) in install mode – after exactly \(|p| + 1\) steps it is in the capture-rewind state with the argument tape holding \(a\) in emit mode and empty in install mode, the argument head at the origin, and the capture head one cell left of \(|c|\).

Let the finalizer run in a fixed mode with capture word \(c\), and let \(p\) be a prefix of \(c\). Starting from its capture-rewind state with the capture head at cell \(|p| - 1\), after exactly \(|p| + 1\) steps it is in the transfer state with the capture head at the origin, the capture word intact, and the argument head still at the origin.

Let the finalizer run on an argument word \(a\) and capture word \(c\), and write \(c\) as a processed prefix \(p\) followed by a remainder \(r\). Starting from its transfer state with the capture head at \(|p|\) – having already transferred \(p\) to the argument tape (install mode) or the output (emit mode) – after exactly \(|r| + 1\) steps it is in the erasure state with the full capture transferred: the argument tape holds \(c\) in install mode and \(a\) in emit mode, the output holds \(c\) exactly in emit mode, and the capture word itself is still intact.

Let the finalizer run in a fixed mode with a remaining captured word \(p\). Starting from its erasure state with the capture head at cell \(|p| - 1\) (and, in install mode, the argument head moving along with it), after exactly \(|p| + 1\) steps it is in its final silent state with the capture tape completely blank and both heads at the origin, the output untouched.

Let the finalizer run in a fixed mode on an argument word \(a\) and a capture word \(c\), entering at its start state with the argument head at \(|a|\) and the capture head at \(|c|\) and empty output. After exactly \(|a| + 3|c| + 5\) steps it is in its final silent state with both heads at the origin and the capture tape blank; the argument tape holds \(c\) in install mode and \(a\) in emit mode, and the output is \(c\) in emit mode and empty in install mode. Empty words are included.

For every source tape \(i\) and component \(r\) among data, visited marks, and origin marks, selecting at the physical index of component \(r\) of bank \(i\) returns exactly \(r\).

For each of the finalizer’s two tape roles, selecting at its physical call-layout index returns exactly that role.

Every physical tape index of the clean-call layout is the argument slot, the capture slot, or the slot of one component (data, visited, or origin) of one source bank.

For every assignment of per-slot values and every source tape \(i\), the clean-call layout evaluated at the physical index of component \(r\) of bank \(i\) gives the data value, the visited value, or the origin value of tape \(i\) according to \(r\).

For every assignment of per-slot values, the clean-call layout evaluated at the argument slot gives the argument value and evaluated at the capture slot gives the capture value.

For every source tape \(i\), the triple selection of bank \(i\) is undefined at the argument slot and at the capture slot.

For all source tapes \(i\) and \(j\) and every component \(r\), the triple selection of bank \(i\) evaluated at the physical index of component \(r\) of bank \(j\) returns \(r\) when \(j = i\) and selects nothing otherwise.

For every source tape \(i\) and component \(r\), the pair selection of the finalizer is undefined at the physical index of component \(r\) of bank \(i\).