FPRD LabShare an approach

← Claims

Compiler theorem

FPRD-T89

Strict real-time multitape machines compile to distance-two scaffolds

Exact statement

Every finite deterministic strict real-time (m)-tape Turing machine with ordinary single-head work tapes, no input-length advice, one global transition per arriving input symbol, and no post-input computation has an equivalent Loff--Moreira--Reis scaffolding automaton of degree (2m) and distance two. Each tape is represented by a two-stack zipper, and one appended scaffold node updates every persistent stack root after each input letter.

StatusMechanically checked and internally audited
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

Cutting each mutable work tape at its head turns it into two persistent stacks plus one scanned symbol in finite control.

Hypotheses and scope

  • The source machine is deterministic, finite, and strict real time: exactly one global transition consumes each input symbol.
  • There is no input-length advice, endmarker transition, epsilon step, or post-input computation.
  • For the published LMR application, the number of tapes is positive and all alphabets and control carriers are finite.

Proof or evidence

Lean proves the stack compiler, clean-empty invariant, tape zipper, all-prefix simulation, full tape reconstruction at every integer offset, structural distance and SELF constraints, and language equality. Independent mutation tests exercise the published scaffold interface on a four-stack machine.

Strict real-time transfer →

Verification notes

The theorem inventory checks 23 Lean files with no proof holes, identifies the empty-pop invariant omitted by the early informal argument, and records exhaustive and mutation-based corroboration.

Limitations

  • The result covers the stated strict model, not arbitrary online or multitape machines with delayed work.
  • Finiteness is an external specialization at the LMR boundary rather than a premise carried by the polymorphic Lean structures.
  • The theorem transfers languages through a specific zipper representation; it is not a lower bound or a model equivalence in the reverse direction.

Open work

Seek specialist review of the machine-interface correspondence and the finite-carrier boundary used in the PEG composition.

Notes

The machine-to-scaffold compiler, CleanEmpty invariant, stack simulation, tape zipper, run correspondence, and language equality are formalized in Lean 4.30.0 without Mathlib or admitted proofs. The formal endpoint reconstructs each source tape from the scaffold and proves equality through Tape.get at every integer offset. The separate Python harness instantiates the published scaffold interface on a four-stack middle-bit machine and catches eight deliberate mutations. The separate FPRD-T110 development now formalizes the published scaffold-to-PEG sufficient direction; the historical palindrome machines remain outside Lean.