FPRD LabShare an approach

← Claims

Mechanized composition theorem

FPRD-T111

The scaffold theorem composes with both FPRD compilers

Exact statement

The full scaffold-to-PEG theorem composes unchanged with the strict real-time multitape compiler and the source-selecting root-sharing compiler. Each finite source machine therefore receives an ordinary PEG for its reverse language; the even-palindrome implications remain explicitly conditional on an exact source recognizer.

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

Context

The useful value of the generic theorem is compositional: an existing exact compiler may be passed to it without altering the source-machine model.

Hypotheses and scope

  • The strict real-time source satisfies the exact FPRD-T89 interface and finite-carrier boundary.
  • The source-selecting stack machine satisfies the exact FPRD-T101 fixed-slot interface and finite-carrier boundary.

Proof or evidence

Lean checks both reverse-language PEG corollaries, their finite carrier instances, and conditional even-palindrome wrappers. The compositions consume the original compiler theorems rather than stronger replacements.

Compiler corollaries →

Verification notes

The two composition endpoints, dependency chain, reversal orientation, empty-word behavior, finite enumeration transport, exported formal sources, and conditional premise boundaries were rechecked. No classical recognizer theorem was smuggled in as an axiom.

Limitations

  • The result does not strengthen strict real-time machines or source-selecting stack machines.
  • It does not machine-check the classical Slisenko or Leong–Seiferas results used by the full even-palindrome argument.
  • The mixed-assurance proper-containment claim FPRD-T90 remains distinct from these wholly mechanized compositions.

Open work

Seek external review of both interface compositions while keeping the classical palindrome premise separately sourced.

Notes

Lean 4.30.0 checks both compositions, their exact finite carriers, and the explicitly conditional EPAL wrappers without changing either source compiler. Executable fixtures, mutations, axiom audits, and public export gates pass. FPRD-T89, FPRD-T100, and FPRD-T101 retain their statuses; FPRD-T90 remains informal-proof while gaining this discharged Theorem 16 dependency. This result does not machine-check Slisenko or Leong--Seiferas.