FPRD LabShare an approach

← Claims

Mechanized scaffold-to-PEG theorem

FPRD-T110

Finite scaffolding automata transfer to ordinary PEGs

Exact statement

Every finite Loff–Moreira–Reis scaffolding automaton satisfying the published distance constraint has a finite total ordinary complete-match parsing expression grammar recognizing the reversal of its language, including automata whose transitions use SELF.

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

Context

A scaffold exposes only a bounded labelled neighbourhood around its newest node. The generated PEG reconstructs the unique compatible scaffold history while reading the input in reverse.

Hypotheses and scope

  • The input alphabet, control, scaffold-label carrier, and bounded-path data are finite.
  • The automaton satisfies the published distance constraint.
  • SELF targets are allowed; self-freedom is not assumed.

Proof or evidence

Lean proves the finite bounded-path grammar, totality, state, label, path, and neighbourhood invariants, nested SELF behavior, reversal, complete consumption, initial-state normalization, and transport to Fin n. Independent fixtures and six killing mutations exercise the construction.

Full sufficient direction →

Verification notes

The theorem signature, 23-file import manifest, 6,783-line proof inventory, proof-hole scan, logical axiom footprint, three fixtures, mutation results, and public-source parity record were checked against the pinned repository snapshot.

Limitations

  • Only the sufficient scaffold-to-PEG direction is formalized here; the converse direction of the published theorem is not.
  • The theorem recognizes the reverse language. Dropping reversal changes the statement.
  • The classical real-time palindrome recognizer and its ordinary-machine realization are separate source-verified premises, not part of this mechanization.

Open work

Obtain external formal-languages review of the LMR-model transcription, generated grammar, and SELF invariant.

Notes

Lean 4.30.0 checks the full sufficient direction of Loff--Moreira--Reis Theorem 16, not a SelfFree corollary. The finite bounded-path grammar, relational totality proof, I1--I4 including nested SELF, reversal, certified evaluator, three fixtures, six killing mutations, axiom audit, and 23-file public-source parity pass. The necessary direction and the classical palindrome recognizer are not formalized here.