theoremroutine

Controller interfaces have restoring O(B)-space implementations

Row, vector and prefix interfaces are implemented by restoring queries in O(B)O(B) space
space-bounded implementation of the estimators
Theorem·thm:ctrl-realization·§11.1 Parameters and interfaces

Statement (paper)

Fix the construction constants and an admissible top budget Mtop=O(B)M_{\mathrm{top}}=O(B). For every actual task tuple reachable from it, the row, vector and prefix interfaces defined in the preceding sections admit deterministic uniform implementations by restoring queries and cursor motions. The following assertions hold for every master environment, without an accuracy promise on its estimated values. \begin{enumerate} \item Every test or numerical digit query terminates, returns its defined value, and restores the cursor and catalyst. Its result is independent of incoming catalyst and scratch contents. Structural port and order choices are independent of a higher numerical request. \item Terminal motions give the specified endpoints. Their excursions restore the cursor. Capped correction motions are partial paired maps with bounded inverse ports and safe behavior on invalid ports. Incoming score ranks compute the stipulated zero-padded ranks. \item For a root numerical request at clock tt, all records retained by the call and its descendants have total length O(Mtop+t+1)O(M_{\mathrm{top}}+t+1), and every descendant clock is O(Mtop+t+1)O(M_{\mathrm{top}}+t+1); the shared facilities use O(B+Mtop+t+1)O(B+M_{\mathrm{top}}+t+1) space. In particular an actual top request with t=O(B)t=O(B) uses total deterministic O(B)O(B) space. \end{enumerate} These implementations use no estimator oracle and retain no second vertex address across recursive graph operations.

In plain English

For every reachable task tuple under an admissible top budget Mtop=O(B)M_{\mathrm{top}}=O(B), the row, vector and prefix interfaces have deterministic uniform implementations by restoring queries and cursor motions. Queries restore the cursor and catalyst and ignore scratch; terminal motions, capped paired maps and incoming ranks are as specified; and a root request at clock tt uses O(Mtop+t+1)O(M_{\mathrm{top}}+t+1) record length and O(B+Mtop+t+1)O(B+M_{\mathrm{top}}+t+1) shared space, hence O(B)O(B) for t=O(B)t=O(B).

Why it's here

This theorem combines the local graph, contour-tour, capped-port, score-rank, path and recipe lemmas into one statement that the interfaces are actually implementable with no estimator oracle and no second stored vertex address. Its inductive construction gives correctness and restoration, and the allowance and clock bookkeeping (telescoping live records, monotone clock potential) gives the total O(B)O(B) space. Later results use it as a black box that holds for every master environment, with no accuracy promise on its estimated values.
Classified routine:
This theorem assembles earlier lemmas (local graph, contour tours, capped ports, score ranks, paths, recipes) by induction and allowance/clock bookkeeping into one implementability statement. It is a direct consequence of those nodes, not a new idea in itself.

Uses

lemEstimator recipes have regenerable records and bounded controldefController allowance and clock certificatelemGuarded local graph for terminal recipesthmUniform numerical interface for arithmetic recipeslemUnbalanced estimator paths have ordered restoring formlemEndpoint comparisons are restoring with O(d) controllemControl records replay with later-salt independencelemContour tours of tree components without counterslemCapped incoming ports give restoring paired motionslemIncoming k-th largest score with short records

Used by

lemWalk variants avoid storing endpointsthmDeterministic logspace approximation of acceptance probabilityclaimOuter computation uses O(B) space total

Inside the proof

claimAllowance strictly drops at every boundaryclaimRaw certificates independent of physical constantsclaimInductive construction of total restoring proceduresclaimContours implement cap and rank wrappersclaimStack segments telescope to top potentialclaimClock invariant bounds shared facilities

Sources

PaperOpen
Section
§11.1 Parameters and interfaces
Page
—
Label
thm:ctrl-realization
Line
sections/implementation.tex:114
Leannot aligned

Phase 2 aligns this node to a Lean declaration.