claimroutine

Inductive construction of total restoring procedures

Builds total restoring procedures by induction on allowance
induction step giving the implementations
Claim·§11.5 The uniform space theorem·inside thmController interfaces have restoring O(B)-space implementations

Statement (paper)

Construct the procedures in increasing allowance. Assume that the lower operations are total, have their claimed cursor and catalyst behavior, and obey the local bounds. Then the finite restoring and numerical recipes compute exactly their specified bit or digit and terminate, and the canonical terminal programs terminate with all designated boundaries within the local bounds. Their parameters and static guards are uniform and independent of a discarded cursor, and invalid canonical initiations are sent to failure. Guards remove no designated execution and ensure that every probed query at synthetic states has an admissible lower tuple and available space, so the induction hypothesis is preserved.

In plain English

Building the procedures in increasing allowance, if the lower operations are total, restore cursor and catalyst, and meet the local bounds, then the recipes compute exactly their specified bits or digits and the canonical terminal programs halt within the bounds. Parameters and guards are uniform and independent of a discarded cursor, invalid initiations fail, and guards remove no designated execution while keeping every probed lower tuple admissible with space available.

Why it's here

This is the induction step of the realization theorem: it turns the recipe, path, equality, replay, arithmetic and local-graph results into actual total restoring implementations at each allowance. Because guards only cut dead ends and never designated executions, the hypotheses needed for the next allowance are preserved, so the induction closes.
Classified routine:
This is the induction step of the realization theorem. It assembles the earlier recipe, path, equality, replay, arithmetic and local-graph lemmas into total restoring procedures by bookkeeping over increasing allowance; no new idea is introduced beyond those lemmas.

Uses

lemEstimator recipes have regenerable records and bounded controlthmUniform numerical interface for arithmetic recipeslemUnbalanced estimator paths have ordered restoring formlemEndpoint comparisons are restoring with O(d) controllemControl records replay with later-salt independencelemGuarded local graph for terminal recipes

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.