FPRD LabShare an approach

← Claims

Theorem with Lean verification

FPRD-T92

Exact derivative update for pushdown frontiers

Exact statement

For a forgotten-action frontier machine, (S_{ua}(q')) is the union of γ(X−1Su(q))\gamma(X^{-1}S_u(q)) over transitions (q,a,X,q′,γ)(q,a,X,q',\gamma). A word is accepted exactly when some final control state has a nonempty frontier component. Both identities hold from the initial frontier, including at the empty word.

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

Context

The recurrence separates the mathematical frontier from any particular data structure used to represent it.

Hypotheses and scope

  • The machine uses the finite real-time top-rewriting interface of FPRD-D33.
  • Stack tops are written on the left and acceptance is by final control state.

Proof or evidence

Splitting a run before its last transition gives one direction; appending the selected transition gives the converse. The Lean package checks the recurrence, readout, epsilon theorem, and push, pop, local, branch-union, mismatched-top, and initial-acceptance examples.

Frontier recurrence and readout →

Verification notes

The theorem names, executable verifier, examples, top-of-stack orientation, and exact-input readout were reconciled with the proof note. No epsilon or post-input transition is hidden in the statement.

Limitations

  • Lean does not verify the visibly pushdown projection theorem or the external PEG/scaffold correspondence.
  • Exact frontier evolution alone gives no bounded width, allocation, or access theorem.

Open work

Use the recurrence as the exact semantic target for proposed finite or persistent frontier representations.

Notes

Lean 4.30.0 checks the executor, recurrence frontier_append_singleton_iff, readout accepts_iff_final_frontier, epsilon theorem, and concrete push, pop, local, branch-union, mismatched-top, and initial-acceptance examples. Lean does not verify FPRD-T91, VPA determinization, regular-frontier normalization, LMR, or any CFL-to-PEL conclusion.