claimroutine

Contours implement cap and rank wrappers

Contour tours implement capped-port and incoming-rank wrappers exactly
realizes the cap and rank wrappers
Claim·§11.5 The uniform space theorem·inside thmController interfaces have restoring O(B)-space implementations

Statement (paper)

The finite graph contours of Lemma  implement the higher cap and inverse-rank wrappers of Lemmas  and . They terminate on success-root components even if other graph components contain cycles or guard-created dead ends, and they count only the canonical initial executions of these programs, so their paired maps and ranks are the mathematical ones specified by the tables; by the common root tuple and salt convention the same maps are obtained in either direction and on every re-query.

In plain English

The finite contour tours of the tree-component lemma realize the capped inverse-port wrappers and the incoming-rank wrappers. They terminate on success-root components even if other components have cycles or dead ends, and they count only canonical initial executions, so the resulting paired maps and ranks are exactly the specified ones, the same in either direction and on every re-query.

Why it's here

This step of the realization theorem's proof shows that the wrappers of the capped-port and score-rank lemmas are actually implemented by the counter-free contour walks. Because the walk stays inside the tree component of the success root, stray cycles or guard-created dead ends elsewhere cannot affect termination, and counting only canonical initiations makes the maps and ranks match the tables. The common root tuple and salt convention makes the results consistent in both directions and across repeated queries.
Classified routine:
Direct consequence of the contour-tour lemma (lem-ctrl-tour) applied to the wrappers of lem-ctrl-cap and lem-ctrl-score-rank. This is implementation bookkeeping in the style of Cook–McKenzie/Reingold-type tree-walk arguments, with termination following from the tree structure of the success-root component.

Uses

lemContour tours of tree components without counterslemCapped incoming ports give restoring paired motionslemIncoming k-th largest score with short records

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.5 The uniform space theorem
Page
—
Label
—
Line
sections/implementation.tex:1271
Leannot aligned

Phase 2 aligns this node to a Lean declaration.