lemmaroutine

Guarded local graph for terminal recipes

Terminal recipe gives outdegree-one local graph with local predecessors, bounded probes
graph traversed by tours, capped ports and rank wrappers
Lemma·lem:ctrl-local-graph·§11.2 Program states and record bounds

Statement (paper)

Suppose a fixed terminal recipe uses the preceding instruction types, has regenerable records, and obeys on its designated executions. Suppose all its opaque transition queries are already implemented, are total on admissible arguments, and have the stated safe invalid-port behavior. Their returned bits, success flags, cursor outputs and port tokens are independent of incoming scratch and catalytic contents, and they restore the catalyst. Then there is a finite graph with outdegree at most one, uniformly associated with its root tuple, with these properties. \begin{enumerate} \item Its designated executions are precisely the prescribed terminal executions. Success states have no successor, and initiation and success tags are distinct. \item Predecessor cases, ordered incidences, and paired edge movement are computable with a bounded number of case labels and one cursor. An opaque predecessor query is made only after its local bound has been checked. \item If a transition query at (w′,j)(w',j) is probed while the terminal root has parameters (w,t)(w,t), the complete live local portion of this probe, including a fixed number of edited or saved controller copies, has length A(w−w′)+D(t−j) A(w-w')+D(t-j) for fixed enlarged coefficients A,DA,D. Shared facilities and the outside stack are not copied. \end{enumerate} The graph and all its guards are independent of an originating row, an outer stack's data, and catalytic contents.

In plain English

For a fixed terminal recipe with regenerable records, local bounds on its designated executions, and total opaque queries that restore the catalyst and ignore scratch contents, there is a finite graph of outdegree at most one whose designated executions are exactly the prescribed terminal executions, with success states having no successor. Its predecessors, ordered incidences and paired edge movement are computable with boundedly many case labels and one cursor, and a probe at (w′,j)(w',j) from a root with parameters (w,t)(w,t) has live local length at most A(w−w′)+D(t−j)A(w-w')+D(t-j). The graph and its guards do not depend on an originating row, the outer stack, or catalytic contents.

Why it's here

This lemma turns a terminal recipe into a deterministic graph that can be traversed forward and backward locally, which the inverse contour, capped incoming port and score-rank lemmas and the realization theorem rely on. It combines the guarded graph claim (guards only add dead ends and never cut designated paths), the predecessor claims for local edits, branches and cursor steps, the canonical case codes that give an ordered duplicate-free incidence list, and the arithmetic showing that probe copies fit within the enlarged A,DA,D bound from the allowance certificate.
Classified routine:
Assembles earlier guarded-graph and predecessor claims with canonical case codes and allowance-certificate arithmetic into a reversible configuration graph, adapting standard reversible-computation techniques (Bennett-style / Lange–McKenzie–Tapp reversible space simulation) to the paper's controller setting.

Uses

defController allowance and clock certificate

Used by

thmController interfaces have restoring O(B)-space implementationslemContour tours of tree components without counterslemCapped incoming ports give restoring paired motionslemIncoming k-th largest score with short recordsclaimRaw certificates independent of physical constantsclaimInductive construction of total restoring proceduresclaimStack segments telescope to top potentialclaimOrder statistic accuracy and inverse-probe bounds

Inside the proof

claimGuarded deterministic finite graph keeps designated pathsclaimPredecessors of local edits and branchesclaimCursor-step predecessors via paired inverseclaimCanonical case codes give local incidence orderclaimProbe copies fit enlarged A,D bound

Sources

PaperOpen
Section
§11.2 Program states and record bounds
Page
—
Label
lem:ctrl-local-graph
Line
sections/implementation.tex:300
Leannot aligned

Phase 2 aligns this node to a Lean declaration.