For every input length \(n\), tape count \(k\), horizon \(T\), and any choice of the six clause-family generators, the ordered list of clause groups has length exactly \(n + (k+3)T + k + 2\), one more than the last round index; groups are counted, not individual clauses.

For CNF formulas \(\varphi \) and \(\psi \), the serialized fragment of \(\varphi \) followed by \(\psi \) equals the fragment of \(\varphi \) concatenated with the fragment of \(\psi \), with all clauses kept in their original order.

Let \(R\) be the last round index and let a family assign a clause group to each round. For every \(j \le R\), the concatenation of the chunks of rounds \(0,\dots ,j-1\) equals the serialized fragment of the concatenation of the first \(j\) groups, so no formula terminator appears in a proper prefix of the rounds.

Let \(R\) be the last round index and let a family assign a clause group to each round. The concatenation of the chunks of rounds \(0,\dots ,R\) equals the full serialization of the concatenation of all \(R+1\) groups, formula terminator included. The identity concerns output words only and makes no satisfiability claim.

For every list \(L\) of CNF formulas, the list obtained by looking up the entries of \(L\) at indices \(0,\dots ,|L|-1\), with the empty formula as default for out-of-range lookups, is \(L\) itself; the default is never used at a legal index.

For all parameters \(n\), \(k\), \(T\) and all six clause-family generators, concatenating the round chunks of the six-family group list over rounds \(0,\dots ,R\), where \(R = n+(k+3)T+k+1\) is its computed last round, equals the serialization of the flattened six-family formula, without rearranging any clause.

Let \(V\) be a language in \(\mathrm{P}\). Then there exist a finite machine \(M\) and constants \(c, A, d \gt 0\) such that \(M\) is oblivious, meaning its head positions depend only on the input length and the time, and \(M\) decides \(V\) within time \(c\, (A(n+1)^d + 1)^2\) on inputs of length \(n\). Only the time bound is enlarged; the language, and hence the certificate relation, is unchanged.

Let \(P\) and \(R\) be polynomially bounded functions on the naturals and let \(c\) be a constant. Then the function \(n \mapsto c\, (P(n)+1)(R(n)+2)\) is polynomially bounded.

For every arity \(\ell \) and predicate \(p\) on \(\ell \)-bit vectors, the chosen CNF table uses at most \(\ell \) variables, has at most \(2^\ell \) clauses, has width at most \(\ell \), and evaluates under any assignment \(a\) to exactly \(p\) applied to the first \(\ell \) bits of \(a\).

For every arity \(\ell \), predicate \(p\) on \(\ell \)-bit vectors, wiring map \(w\) on variable indices, and assignment \(a\), the relabeling of the chosen CNF table along \(w\) evaluates to \(p\) applied to the bits \(a(w(0)),\dots ,a(w(\ell -1))\); repeated wire indices are permitted and no injectivity is assumed.

For every optional Boolean symbol \(s\), decoding the two-bit encoding of \(s\) returns \(s\), including the blank case and the false-valued case.

For every snapshot \(s\) of a machine with a fixed optional-state binary code, the state slice of the encoded block of \(s\) equals the code’s encoding of the state of \(s\).

For every snapshot \(s\) of a machine with a fixed optional-state binary code, the input slice of the encoded block of \(s\) equals the two-bit encoding of the input symbol of \(s\).

For every snapshot \(s\) and every work tape \(\tau \) of a machine with a fixed optional-state binary code, the work slice at \(\tau \) of the encoded block of \(s\) equals the two-bit encoding of the symbol of \(s\) on tape \(\tau \).

If two snapshot blocks of \(B + 2 + 2k\) bits have equal state slices, equal input slices, and equal work slices on every tape, then the blocks are equal bit for bit. Equality of the decoded fields alone would not suffice; the claim pins every individual bit.

For a fixed machine and a fixed binary code of its optional states, the snapshot block encoding is injective: distinct snapshots produce distinct bit blocks, because each individual field code is injective.

For every snapshot \(s\) of a machine with a fixed optional-state binary code, decoding the encoded block of \(s\) returns \(s\); the junk fallback is never reached on genuine encodings.

For every verifier machine with a state code, certificate parameters, instance, and horizon, concatenating the round chunks of the tableau’s ordered group list over all rounds yields exactly the serialization of the tableau formula, including the empty-template and final-terminator cases.

Suppose the last-visit function for input count \(m\), time \(t\), and tape \(\tau \) returns a time \(s\). Then \(s \lt t\), the work-head position on \(\tau \) at time \(s\) equals the position at time \(t\), and every time \(r \lt t\) scanning the same position satisfies \(r \le s\).

Let \(R\) be a bound, let a packing map assign a word to each cursor value, and suppose a step function sends the packed word of \(i\) to the packed word of \(\min (i+1, R+1)\) for every \(i \le R+1\). Then for all \(i\), iterating the step function \(i\) times from the packed word of \(0\) yields the packed word of \(\min (i, R+1)\): the cursor reaches each legal round and then stalls at the one-past-last value.

Suppose a native machine with a distinguished anchor state, a packing of cursor values into words, abstract step and emission functions, a round bound \(R\), and a budget \(P\) are given, where \(R\) and \(P\) are polynomially bounded and some helper machine computes the binary representation of \(R\) within time \(P\). Assume: stepping a packed cursor advances it saturatingly up to one past the last round; emission at cursor \(i \le R\) produces exactly the chunk of round \(i\), and nothing beyond the last round; from any input the machine reaches the packed start word, first returning to the anchor, within time \(P\); and from each packed cursor the machine returns to the anchor in positive time at most \(P\), having appended exactly the prescribed chunk to its output. Then the function sending an input to the serialization of the concatenation of all clause groups over all rounds is computable in polynomial time. No preparation producer or native body is constructed here.

Let \(L\) be a language in \(\mathrm{NP}\). Then there exist certificate parameters \(C\) and \(e\), a verifier language \(V\), a finite oblivious machine \(M\), and constants \(c, A, d \gt 0\) such that a string \(x\) belongs to \(L\) exactly when some certificate \(u\) of length \(C(|x|+1)^e\) makes the concatenation of \(x\) and \(u\) belong to \(V\), and \(M\) decides \(V\) within time \(c\, (A(n+1)^d+1)^2\) on inputs of length \(n\). Neither certificate parameter is enlarged by the normalization.

If some finite machine computes a string function \(f\) within time \(a(n+1)\) on inputs of length \(n\), for a constant \(a\), then \(f\) is polynomial-time computable.

If \(g\) is a polynomial-time computable string function, then so is the function that decodes its input as an encoded pair \((a,b)\) and returns the encoded pair \((a, g(b))\), returning the empty string when the input is not an encoded pair. The first field is retained with its exact bytes.

If \(f\) and \(g\) are polynomial-time computable string functions, then so is the function sending a string \(x\) to the encoded pair of \(f(x)\) and \(g(x)\), where both component computations may consult the original input.

If \(f\) and \(g\) are polynomial-time computable string functions, then so is the function sending a string \(x\) to the concatenation of \(f(x)\) and \(g(x)\).

For all constants \(C\) and \(e\), the function sending a string \(x\) to the word of exactly \(C(|x|+1)^e\) true bits is polynomial-time computable, including the zero-coefficient and zero-degree cases; the exact value is never replaced by a majorant.

For a fixed bit \(b\), an input \(x\), a position \(i \le |x|\), and a current output word \(w\), running the constant-fill machine for \(|x| - i + 1\) steps from the configuration scanning position \(i\) with output \(w\) halts at the right boundary with output \(w\) extended by \(|x| - i\) copies of \(b\).

For every fixed bit \(b\), the function sending an input \(x\) to the word of \(|x|\) copies of \(b\) is polynomial-time computable, witnessed by an actual native scan of the input rather than by substituting the instance for the simulator’s physical input.

For all parameters \(C, e, c, A, d\), the arithmetic preparation header, comprising the retained instance, the exact binary certificate length, reference length, and horizon, the all-false reference input, and the unary horizon clock, is computable in polynomial time by native machines with sequential access; no positivity assumption is placed on any parameter.

Let \(c\) be a source configuration over a virtual input, with a valid position tag bit \(b\). Applying the embedded reference action to the embedded host configuration of \(c\) yields exactly the embedded configuration of the stepped source configuration, for some valid new tag bit: each administrative tape is updated by its requested write and head move, while the host input position and the physical output are unchanged.

For every natural number \(n\), applying the list increment to the little-endian binary representation of \(n\) yields the binary representation of \(n+1\), including the overflow case.

For every bit list \(w\), the incremented list has length at most \(|w| + 1\), and the carry count of \(w\) is at most the length of the incremented list, so all cleared cells lie within the incremented word.

For bit lists \(u\) and \(v\), the tape holding \(u\) followed by \(v\) reads, at cell \(|u|\), the first bit of \(v\), or a blank when \(v\) is empty.

For bit lists \(u\) and \(v\) and a bit \(b\), updating the tape that holds \(u\) followed by \(v\) at cell \(|u|\) with the symbol \(b\) yields the tape holding \(u\) followed by \(b\) and then the tail of \(v\): the write either replaces the first suffix bit or extends the word, all other cells are unchanged, and negative cells stay blank.

For an input word, an input position, and a stored word split as a prefix \(u\) followed by a suffix \(v\), one step of the increment machine in carry control at cell \(|u|\) yields: when \(v\) starts with a true bit, the cell rewritten to false with the head moved right, still in carry control; and otherwise the cell rewritten to true with the head moved left, in rewind control. Only the scanned cell changes.

For every input word, input position, prefix \(u\), and suffix \(v\), running the increment machine in carry control at cell \(|u|\) for one more step than the carry count of \(v\) replaces \(v\) by its increment and leaves the machine in rewind control one cell left of the last written position. Exactly the initial true bits of \(v\) are cleared before the final true bit is written.

For every input word, input position, stored word \(w\), and count \(j \le |w|\), running the increment machine in rewind control at cell \(j - 1\) for \(j + 1\) steps crosses the written cells, detects the untouched blank at cell \(-1\), and ends at cell \(0\) in the absorbing return control, with the stored word unchanged.

For every bit list \(w\), the carry count of \(w\), the number of initial true bits, is at most the length of \(w\).

For every input word, input position, and stored word \(w\), running the increment machine from carry control at cell \(0\) for exactly twice the carry count of \(w\) plus two steps ends in the return control at cell \(0\) with the stored word replaced by its increment; the native input head never moves from its supplied position.

For every configuration of the increment machine whose control is the return state, one step leaves the entire configuration unchanged, so any upper bound on the running time can be cut to the actual first return.

For every configuration of the increment machine in the return control and every duration \(t\), running for \(t\) steps leaves the whole configuration, not merely its control, unchanged.

For every input word, input position, and stored word \(w\), there is a time \(t\) with \(0 \lt t \le 2|w| + 2\) such that the increment machine, started in carry control at cell \(0\), is never in the return control before \(t\) and at time \(t\) sits in the return control at cell \(0\) with the stored word replaced by its increment.

For every bit list \(w\), the tape holding \(w\) on the nonnegative cells with blanks elsewhere coincides with the library’s canonical buffer tape for \(w\), including every negative cell and both empty-word boundaries.

For every source configuration, tag bit, and counter value \(n\), there is a strictly positive time \(t\), at most twice the binary length of \(n\) plus two, such that the counter-beside-reference host first reaches its return control exactly at \(t\), at which point the counter tape holds the binary representation of \(n+1\) with its head restored to zero, while the source configuration, tag, and every bank tape and head are untouched, and the represented source clock has not advanced.

For all naturals \(n\) and \(w\) with \(n \lt 2^w\), the binary representation of \(n\) has at most \(w\) bits, so one administrative increment is charged by two \(w\)-bit scans plus two transitions, with no unary representation of positions.

For every input position, every family of component configurations, and every coordinate \(i\), the bank’s component action at \(i\) computed from the product configuration equals the one-tape counter transition of component \(i\) on its own scanned symbol, or the stationary action when component \(i\) has stopped.

For every input position and family of component configurations, one step of the counter bank equals the product of one single-tape counter step per component: tape contents and independently positioned heads are each updated by their own component, the physical input stays fixed, and all component outputs are suppressed.

For every input position, family of component configurations, and duration \(t\), running the counter bank for \(t\) steps yields the product of the \(t\)-step runs of all components, so every counter trajectory is an exact projection of the one native bank run.

For every input word, input position, selection flag, counter value \(n\), and width bound \(W\) with the binary representation of \(n\) at most \(W\) bits long, running one counter component for \(2W + 2\) steps from its selection-dependent start control ends in the return control at head zero, holding the binary representation of \(n+1\) if the component was selected and of \(n\) otherwise.

For every input word, input position, selection vector, counter values, and common width bound \(W\) covering all the values’ binary representations, running the counter bank for \(2W + 2\) steps increments exactly the selected coordinates, leaves the unselected ones unchanged, and restores every head to zero; the cost is independent of the number of counters.

Every configuration of the counter bank whose control has all components in the return state is left entirely unchanged by one step of the bank.

For every input word, input position, selection vector, counter values, and common width bound \(W\), there is a time \(t \le 2W + 2\) such that the bank control is not all-returned at any earlier time, and at \(t\) the bank holds exactly the requested incremented values with every head restored to zero. The duration may be zero when nothing is selected; positivity is supplied by the surrounding dispatch controller.

Let \(c\) be a source configuration with a valid position tag bit. For every coordinate, the reference position of the stepped configuration equals the reference position of \(c\) plus the recorded displacement, including blocked input moves and the halting transition.

For every displacement vector, movement counts, and coordinate \(i\), the signed value of the advanced counts at \(i\) equals the signed value of the original counts plus the displacement at \(i\).

If every movement count is at most \(t\), then after advancing along any displacement vector every count is at most \(t + 1\).

For movement-count vectors \(n\) and \(m\) and a coordinate \(i\), the signed positions at \(i\) agree exactly when the two cross-sums of first-bank and second-bank counts are equal; the criterion compares values rather than the non-unique two-counter codes.

Let \(c\) be a source configuration with a valid position tag bit and let movement counts be given in canonical form. One step of the tracking host from the canonical seam applies the full source action, produces a valid tag for the stepped configuration, and enters the bank phase with exactly the counters of the actual displacements selected; no counter has yet changed, and the physical output is still empty.

Suppose a host machine agrees, on every embedded non-exit control, with the disjoint-bank lift of a smaller machine acting on the left tapes. Then for every start configuration of the smaller machine, every retained right-bank contents and heads, and every horizon \(t\) such that the smaller machine does not reach the exit control before \(t\), the host run agrees with the lifted run of the smaller machine at every time up to \(t\). No agreement is required after the first exit.

For every source configuration, tag bit, component controls, and counter values, the left-bank lift of the counter-bank product configuration over the retained source tapes coincides literally with the embedded reference configuration whose administrative tapes hold the counters in binary, including the virtual input buffer, every source tape, and all heads.

For every source configuration, tag bit, and counter values, one step of the tracking host from the all-returned bank phase yields the anchor control, with no change to the source time, any tape, any head, or the output.

Let \(c\) be a source configuration with a valid position tag bit, and let movement counts be given whose binary representations fit a common width \(W\). Then there is a strictly positive time \(\tau \le 2W + 4\) such that: every intermediate time strictly between \(0\) and \(\tau \) is in the bank phase, not at the anchor; and at \(\tau \) the tracking host is back at the canonical seam for the stepped source configuration, with a valid new tag and with exactly the clamped displacement counts advanced. Source output is suppressed and every counter head is restored.

For every word \(w\) and bit \(b\), updating the canonical buffer tape of \(w\) at cell \(|w|\), its right blank, with \(b\) yields the canonical buffer tape of \(w\) extended by \(b\); no other cell changes, including negative cells and the empty-buffer boundary.

For every copier configuration and every action that writes a bit \(b\) at the record head while moving the source head by \(d\), applying the action yields the configuration with exactly \(b\) appended to the record and the source head moved by \(d\); nothing else changes.

For every input word, input position, source prefix \(u\), remaining source bits starting with \(b\), and record, two steps of the copier from its reading control at cell \(|u|\) append the two bits \(b, b\) to the record and advance the source head to cell \(|u| + 1\); the source tape is unchanged.

For every input word, input position, source word split into a prefix \(u\) and suffix \(w\), and record, running the copier for \(2|w|\) steps from the reading control at cell \(|u|\) appends the doubling of every bit of \(w\) to the record and leaves the source head at the right end; the field separator has not yet been written.

For every input word, input position, source word \(w\), and record, two steps of the copier from the reading control at the source’s right blank yield the rewinding control, with the aligned separator bits false, true appended to the record and the source head moved one cell left.

For every input word, input position, source word \(w\), record, and count \(j \le |w|\), running the copier in rewinding control at source cell \(j - 1\) for \(j + 1\) steps returns the source head to cell zero and enters the completed control, preserving the entire accumulated record; each crossed bit costs one transition and leaving the left blank costs one more.

For every input word, input position, source word \(w\), and record, running the copier for \(3|w| + 3\) steps from the start yields the completed control, in which the record is extended by exactly the self-delimiting pair encoding of \(w\) with empty payload and the source head is restored to zero; the empty field still takes three positive transitions.

Every copier configuration in the completed control is left entirely unchanged by one step of the copier.

For every input word, input position, source word \(w\), and record, there is a time \(t\) with \(0 \lt t \le 3|w| + 3\) such that the copier is never in the completed control before \(t\), and at \(t\) it holds the record extended by the self-delimiting encoding of \(w\), with the source untouched and both heads as specified; a host can therefore dispatch on completion without knowing the field length.

For every partial selection, state embedding, retained tapes and heads, action, and local configuration, applying the relocated action to the relocated configuration equals relocating the result of applying the action locally; writes, head motion, and final emission are preserved, and inactive host tapes and heads are fixed.

Let a host machine agree, on every embedded control satisfying a guard, with the relocation of a smaller machine’s transition through a tape injection whose selection is a left inverse. Then for every retained host contents and heads, every local start configuration, and every horizon \(t\) such that all local controls strictly before \(t\) satisfy the guard, the host run up to time \(t\) equals the relocation of the local run; the guard is not needed at the endpoint itself.

For every selected counter coordinate \(i\) and each of the two local copy tapes, the row-copy selection applied to the embedded slot returns that local tape, so both actual copy tapes are selected back to their local indices.

For every input word, input position, selected counter \(i\), copier control, counter words, and record, relocating the two-tape copier configuration for counter \(i\) into the row controller’s slots, with all other counters retained, yields exactly the row seam at field \(i\); every unselected counter retains its whole word, not just its current cell.

For every input word, input position, selected counter \(i\), counter words \(w\), and record, there is a strictly positive time \(t \le 3|w(i)| + 4\) after which the row controller has appended the self-delimiting encoding of \(w(i)\) to the record and advanced its field index from \(i\) to \(i+1\), with the entire counter bank, the input head, and the empty physical output restored.

For every input word, input position, counter words all of length at most \(W\), record, and count \(j \le l\), there is a time \(t \le j(3W + 4)\) after which the row controller, started at field zero, has appended exactly the stored prefix of the first \(j\) fields to the record and sits at field index \(j\) with every counter and head restored.

For every input word, input position, counter words of length at most \(W\), and record, there is a time \(t \le l(3W+4)\) after which the row controller has appended the complete stored row, all \(l\) self-delimiting fields in tape order, to the record, with every source counter unchanged and its head at zero.

Every configuration of the row controller whose control is the end-of-row state with copier control zero is left entirely unchanged by one step.

For a positive number \(l\) of counters, every input word, input position, counter words of length at most \(W\), and record, there is a time \(t\) with \(0 \lt t \le l(3W+4)\) such that the row controller never shows the end-of-row control before \(t\), and at \(t\) the record has been extended by the complete stored row with all counter heads restored; positivity comes from the fixed positive field count.

For counter words of length at most \(W\) and every count \(j\), the stored row prefix of the first \(j\) fields has length at most \(j(2W + 2)\): each field costs its doubled bits plus the two separator bits, independently of the native copying runtime.

For all naturals \(n \le t\), the binary representation of \(n\) has at most \(t\) bits. The bound coarsely charges native scans; all stored movement counts remain in canonical binary form.

For every input position, the deterministic nonzero-position tag correctly identifies both boundary blanks and is a valid virtual-input tag for that position.

For any two of the three native move symbols, if their integer displacements are equal then the symbols themselves are equal.

Let \(c\) be a source configuration and let \(b\) be any valid position tag for its input position. The displacement vector computed from \(b\) equals the displacement vector computed from the deterministic nonzero-position tag; at an interior cell either tag yields the same clamped movement.

For every source machine, virtual input \(y\), time \(t\), and valid tag \(b\) for the position reached at time \(t\), advancing the counts at time \(t\) by the displacements computed from \(b\) yields exactly the counts at time \(t+1\).

For every source machine, virtual input \(y\), time \(t\), and coordinate, the stored movement count at time \(t\) is at most \(t\).

For every source machine, virtual input \(y\), time \(t\), and coordinate, the signed value of the stored count pair equals the reference position of the configuration reached at time \(t\): the shifted clamped input position on the first coordinate and the signed work-head positions on the rest.

For every tracking-machine tape coordinate, the recorder’s tracking selection applied to the embedded coordinate returns that coordinate.

For every row-controller tape coordinate, the recorder’s row selection applied to the embedded coordinate returns that coordinate.

For every source configuration, tag, movement counts, record, clock budget, logical time, field index, and copier control, relocating the row-copy seam into the recorder’s tapes, retaining every inactive slot from the recorder configuration itself, yields exactly the recorder configuration in the row-copying phase; the inactive bank includes every source cell and head and the unchanged clock.

For every source configuration, tag, movement counts, clock budget, and logical time, the retained inactive tapes and heads used when relocating a row-copy configuration into the recorder are the same for any two record contents and row controls, so consecutive fields and rows can append to the record without changing source time.

For every source configuration, tag, movement counts with binary representations of width at most \(W\), record, clock budget, and logical time, there is a time \(s \le F(3W+4) + 1\), where \(F\) is the field count, after which the recorder has appended the complete stored row of the counters to the record and dispatched into its clock-test phase; all source storage and the logical clock are unchanged throughout.

For every left coordinate among the first \(a\) tapes and every right coordinate among the following \(b\) tapes of a disjoint bank, the two embedded tape indices are distinct.

For every right coordinate and left coordinate of a disjoint tape bank, the embedded right index is distinct from the embedded left index.

For every source configuration, tag, movement counts, record, clock budget \(T\), and logical time \(t \lt T\), one recorder step from the clock-test phase reads the live unary clock cell, advances only the clock head from \(t\) to \(t+1\), and enters the source-release phase; no source head moves and no record bit is appended.

For every source configuration, tag, movement counts, record, and clock budget \(T\), one recorder step from the clock-test phase at logical time \(T\) reads the exhausted clock blank and yields the completed live control, silently; no further source transition can occur.

For every source configuration, tag, movement counts, record, clock budget, and logical time, relocating the canonical tracking seam into the recorder’s tapes, retaining the record and clock slots from the recorder configuration itself, yields exactly the recorder configuration in the counter-update phase.

The retained inactive tapes and heads used when relocating a tracking configuration into the recorder depend only on the stored record and clock, so they agree for any two source configurations, tags, and movement counts; source writes and counter updates therefore do not disturb the frame.

Suppose a host control acts, on all reads, as the relocation of a smaller machine’s transition at a fixed local state \(q\), through a tape injection whose selection is a left inverse. Then one host step from the relocated configuration of any local configuration in state \(q\), with its control replaced by that release control, equals the relocation of one local step. Executing the first action before observing any return guard handles equal entry and exit controls.

Let \(c\) be a source configuration with a valid position tag, and let the movement counts have binary representations of width at most \(W\). From the source-release phase, there is a time \(s \le 2W + 5\) after which the recorder has executed exactly one source transition together with its full signed counter update and dispatched to the next row-copy phase, with a valid tag for the stepped configuration; the record and clock contents and heads are framed throughout.

For every source machine, physical input, virtual input \(y\), horizon \(T\), and logical time \(j \le T\), there is a time \(s \le j\, (F(3T+4) + 2T + 7)\), where \(F\) is the field count, after which the recorder, started from the prepared blank seam, holds on its record tape exactly the stored rows of times \(0,\dots ,j-1\), carries the movement counts and source configuration of time \(j\) with a valid tag, and is ready to store the current row. The invariant concerns actual tape contents, not merely a running schedule.

For every source machine, physical input, virtual input \(y\), and horizon \(T\), there is a time \(s \le (T+1)(F(3T+4) + 2T + 7)\), where \(F\) is the field count, after which the recorder, started from the prepared blank seam, is in its completed live control with the stored rows of all times \(0,\dots ,T\) on the record tape, the movement counts and the exact horizon configuration of the source, and an empty physical output.

For every source machine, physical input, virtual input \(y\), and horizon \(T\), the configuration assembled from words, blank movement counters, empty record, a unary clock of \(T\) true cells, the virtual input, and blank source work tapes, equals the recorder’s prepared seam at logical time zero over the initial source configuration. No claim is made about native initialization from raw input.

For every source machine and horizon \(T\), the complete stored-row ledger \((T+1)(F(3T+4) + 2T + 7)\), where \(F\) is the field count, is at most \((4F + 7)(T+1)^2\), so native recording work is polynomial in the source horizon, separately from the formula output size.

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

For every bit list \(w\), the value of \(w\) equals twice the value of its tail plus the numeric value of its first digit, where an empty word contributes a zero digit.

For every carry bit \(c\) and addend bits \(u\) and \(v\), the sum of the three digit values equals twice the outgoing carry’s value plus the low result bit’s value.

For every comparator registers \(q\) and four words, the comparator invariant on the full words holds exactly when it holds for the updated registers on the four tails: equal sums are equivalent to equal low bits together with equal remaining high sums, and unequal low bits have opposite parity, which no later column can repair.

For every four words and every column count \(j\), the comparator invariant at the control after \(j\) columns, applied to the words with their first \(j\) bits dropped, holds exactly when the value of the first word plus the second equals the value of the third plus the fourth; columns beyond a short word read zeros, never uncharged random access.

For every four comparator words and every index, the length of the chosen word is at most the maximum of the four lengths.

For every four comparator words and every position \(j\), all four aligned reads at \(j\) are blank exactly when the common maximum width is at most \(j\), so a word attaining the maximum prevents an early return.

For all Boolean digits \(a\) and \(b\), their numeric values are equal exactly when the digits themselves are equal.

For every four words, the verdict computed from the comparator control after scanning the common maximum width is true exactly when the value of the first word plus the second equals the value of the third plus the fourth.