FPRD LabShare an approach

← Claims

Written-proof claim

FPRD-T22

Claim FPRD-T22

Exact statement

A language is regular exactly when its residual recognition dynamic is finite; in that case residual actions and empty-word output recognize it exactly, every reachable deterministic recognizer maps uniquely and surjectively onto the residual dynamic by accepted-future language, and the residual dynamic is the unique minimal exact recognizer up to labeled isomorphism, recovered after finite bounded observational refinement.

Statusinformal proof
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

This row is imported exactly from the governed FPRD claims ledger. The matrix assignment records normalized inventory coverage; it is not a new proof or a promotion of the ledger status.

Proof or evidence

The ledger points to OPEN_PROBLEMS.md. The matrix has not yet rewritten that source into a self-contained public proof summary.

OPEN_PROBLEMS.md →

Verification notes

Reviewed on 2026-08-25 for identifier, status, provenance, evidence-link presence, and dependency import only. Mathematical proof audit remains the next action unless separately documented.

Limitations

  • This is a reconstruction of the classical Myhill-Nerode/Brzozowski result inside the FPRD object interface, not a novelty claim for the classical theorem.

Open work

Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity.

Notes

This is a reconstruction of the classical Myhill-Nerode/Brzozowski result inside the FPRD object interface, not a novelty claim for the classical theorem.