lemmaroutineinferred_dep

Capped incoming ports give restoring paired motions

Entries with ≤ KcK_c incoming have restoring paired motions with inverse ports
inverts row motions without storing endpoint addresses
Lemma·lem:ctrl-cap·§11.3 Contours and incoming operations

Statement (paper)

Let a fixed row class have a constant port alphabet, distinct entries within each row, and a deterministic terminal program which maps its valid row ports to their endpoints. Assume the program is of the form in Lemma . For every fixed KcK_c there are restoring tests and mutually inverse paired motions for precisely those class entries whose endpoint has at most KcK_c incoming class entries. The inverse ports belong to {1,…,Kc}\{1,\ldots,K_c\}. No additional endpoint address or unbalanced path is held across these operations.

In plain English

For a fixed row class with constant port alphabet, distinct entries per row, and a deterministic terminal program (of the form in Lemma 11.4) mapping valid row ports to endpoints, and for any fixed KcK_c, there are restoring tests and mutually inverse paired motions for exactly those entries whose endpoint has at most KcK_c incoming class entries. The inverse ports lie in {1,…,Kc}\{1,\ldots,K_c\}, and no extra endpoint address or unbalanced path is stored during these operations.

Why it's here

This turns the local graph of Lemma 11.4 and the counter-free contour tours of Lemma 11.5 into forward and backward moves over class entries, using only a bounded inverse-port label in place of a stored endpoint address. Restricting to endpoints with at most KcK_c incoming entries keeps the inverse ports in a constant alphabet, which the realization theorem and the recipe certificates rely on to invert row motions.
Classified routine:
Direct consequence of the guarded local graph (Lemma 11.4) and counter-free contour tours (Lemma 11.5), using the standard reversible/catalytic technique of indexing preimages by a bounded rank. This resembles inverting deterministic steps via Euler tours of the configuration tree (Sipser 1980; Lange–McKenzie–Tapp 2000).

Uses

lemGuarded local graph for terminal recipeslemContour tours of tree components without counters

Used by

thmController interfaces have restoring O(B)-space implementationslemEstimator recipes have regenerable records and bounded controlclaimContours implement cap and rank wrappersclaimFresh presence tests before value or motionclaimFinal row classes and wrappers add fixed strata

Sources

PaperOpen
Section
§11.3 Contours and incoming operations
Page
—
Label
lem:ctrl-cap
Line
sections/implementation.tex:493
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The proof of lem:ctrl-cap (implementation.tex 510-539) is built on contour marks: "go forward toward the sentinel, counting other initiation marks" and "inverse maps by the common contour order". These are the next-mark/previous-mark operations of lem:ctrl-tour, which has no incoming edge from cap.