claimroutineinferred_dep

Cursor-step predecessors via paired inverse

Cursor-step predecessors found via paired inverse with no saved cursor
predecessor case for cursor moves
Claim·§11.2 Program states and record bounds·inside lemGuarded local graph for terminal recipes

Statement (paper)

For a cursor-step edge, predecessor candidates can be tested using only the present cursor and output token. A candidate local record is built by a bounded inverse edit, its active records are replayed from the fixed root tuple, and all allocation and recipe checks are made before any motion without using the predecessor cursor. The partial inverse is then applied at the present cursor and output token, and a guessed preceding port is compared with the actual returned port. The probe is restored by the paired forward map with the same tuple and the actual returned token, with no saved cursor copy. Outgoing paired probes are likewise restored by the inverse with the actual output token. Both directions have the same lower-operation cost, and no second high-cost query or unrelated value query is used inside the step.

In plain English

For a cursor-step edge, predecessor candidates can be tested using only the present cursor and output token. The candidate is built by a bounded inverse edit and checked by replaying its records from the fixed root tuple. Probing then uses the partial inverse and the paired forward map, with no saved cursor copy and no second high-cost query.

Why it's here

This claim shows that predecessors along cursor-step edges can be found and verified locally on the guarded graph from the previous claim, with the probe restored exactly and at the same cost in both directions. It supplies the cursor-step case of the predecessor computation and the bounded-cost probe in the parent lemma, and the later canonical case-code claim builds on it for incidence order.
Classified routine:
A bookkeeping step inside the guarded local graph lemma. It checks predecessors via paired forward/inverse maps with no saved copy, the standard reversible-computation technique (Bennett-style uncomputation, as in Lange-McKenzie-Tapp reversible space simulation) applied to the graph from the preceding claim.

Uses

claimGuarded deterministic finite graph keeps designated paths

Used by

claimCanonical case codes give local incidence order

Sources

PaperOpen
Section
§11.2 Program states and record bounds
Page
—
Label
—
Line
sections/implementation.tex:371
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Cursor-step predecessors via paired inverse" rests on claim-lem-ctrl-local-graph-1