Run 09: timing, reversal, and the empty word

Date: 23 September 2026

Result

The transfer route is an exact composition of two different statements:

$$M \xrightarrow[\text{same word}]{\text{one source step = one scaffold append}} A_M \xrightarrow[\text{one reversal}]{\text{LMR sufficient direction}} G_M.$$

For every word $w$, the machine and compiled scaffold agree after every prefix, including their control state and every work-tape cell. Hence

$$A_M(w)=M(w).$$

The PEG produced by the formalized sufficient direction satisfies

$$G_M(x)=A_M(x^R)=M(x^R).$$

Therefore $L(G_M)=L(M)^R$. The reversal is introduced exactly once, by the scaffold-to-PEG construction. It is not part of the tape zipper or the machine-to-scaffold compiler.

Strict timing

The source machine is defined by one transition

$$\delta(q,a,t_1,\ldots,t_m)$$

for each arriving input symbol. A transition writes and moves every fixed work-tape head simultaneously. The zipper performs at most one operation on each of the $2m$ stacks, and the parallel-stack compiler realizes all of those operations in one newly appended scaffold node. Thus an input of length $n$ produces exactly $n$ source transitions and $n$ scaffold appends. There is no cleanup phase.

This compiler preserves strict real time; it does not manufacture it. If a candidate source recognizer uses several microsteps per input letter, or a number of microsteps growing with the prefix, this theorem does not compress that work into one scaffold transition. The source recognizer must already satisfy the strict interface.

The Lean endpoints realtime_transfer_decides, realtime_transfer_tape, and realtime_transfer_tape_contents establish the exact operational equality. The machine run itself is a fold with one stepConfig call per input letter.

Reversal

The sufficient direction of Loff, Moreira, and Reis’s characterization turns a scaffolding automaton for $K^R$ into a PEG for $K$. In the formalized orientation, a scaffold $A$ gives a PEG for

$$\{x:A(x^R)=1\}.$$

Substituting $A=A_M$ yields exactly the reverse of the machine language. The formal corollary revRT_multitape_subset_PEG contains this single word.reverse. No second reversal is hidden in the compiler.

For even palindromes, reversal invariance removes the visible orientation:

$$\mathsf{EPAL}_2^R=\mathsf{EPAL}_2.$$

This is why the generic transfer theorem produces a PEG for the same named palindrome language.

Empty input

All layers use their initial acceptance value on the empty word:

• the source machine performs zero transitions and tests its initial control;
• the compiled scaffold performs zero appends and has the same acceptance bit;
• fresh-initial-state normalization copies the old initial acceptance bit;
• reversal fixes $\varepsilon$; and
• the PEG theorem is stated for all words, including $\varepsilon$.

No artificial input step or endmarker is inserted. The Lean theorem normalize_decides proves preservation for both the empty and nonempty cases.

Assurance boundary

The composition from an arbitrary finite strict real-time ordinary multitape machine to a PEG for its reversed language is machine-checked. The Lean EPAL endpoint is deliberately conditional: epal₂_inPEG_of_multitape_recognizer takes an exact strict recognizer and its correctness theorem as arguments and introduces no recognizer axiom.

The unconditional EPAL application in the paper additionally imports the classical Slisenko and Leong-Seiferas recognizer route, including its fixed-rate strictification. That premise is source-audited in the paper but is not mechanized in this repository. Run 09 found no timing, reversal, or empty-word mismatch inside the checked compiler chain. It also does not upgrade the classical recognizer premise to machine-checked status.

The separate reconstructed palindrome controller that takes growing microtime per input round cannot instantiate this interface. That limitation belongs to that reconstruction, not to the classical theorem or to the conditional transfer compiler.

Cross-paper disposition

This route does not use the direct receipt recurrence, the causal batch compiler, or the unary coherence theorem. The earlier receipt, sequence, initialization, and native-observation findings therefore do not alter the transfer composition. Conversely, this timing audit supplies no new assurance for those three papers.

Executable evidence

check_transfer_composition.py exhaustively checks two small machine families:

• 326,592 control-and-orientation executions, including 5,184 empty-word cases, 1,337,472 letter steps, and the fresh-initial normalization; and
• 81,648 two-symbol tape executions, with 334,368 source/zipper steps and 5,015,520 tape-offset comparisons.

It also checks exact source markers for the Lean endpoints and the paper’s stated assurance boundary. These finite checks exercise the interfaces. The universal conclusion comes from the Lean theorems and the composition above.

Disposition

The transfer half of R05 is complete. No circulated paper body or PDF changed. The remaining R05 task is the unary paper’s guard and base-termination audit.

Primary references:

• Loff, Moreira, and Reis, The Computational Power of Parsing Expression Grammars: https://arxiv.org/abs/1902.08272
• Slisenko, Recognition of palindromes by multihead Turing machines in real time: https://link.springer.com/article/10.1007/BF01404109
• Leong and Seiferas, New real-time simulations of multihead tape units: https://dl.acm.org/doi/10.1145/322234.322246