lemmaroutine

Unbalanced estimator paths have ordered restoring form

Unbalanced estimator paths have fixed order with at most one terminal delegation
fixes path shape for recipe certificates
Lemma·lem:ctrl-paths·§11.4 Certificates for the estimator recipes

Statement (paper)

Every unbalanced path required by the estimator has the following ordered form: restoring selection and validity tests; local label maps and, if necessary, a paired left-factor motion; further restoring tests at that midpoint; at most one final terminal delegation; and then only local label completion. An excursion to its endpoint and back, for a pure local action, has regenerable records. It preserves the same allowance and clock bounds as this ordered path, up to fixed factors. No unbalanced spine is retained over a new high-cost query at its endpoint.

In plain English

Every unbalanced path the estimator needs has a fixed order: restoring selection and validity tests, local label maps (with a paired left-factor motion if needed), more restoring tests at the midpoint, at most one final terminal delegation, then only local label completion. Excursions to an endpoint and back for a pure local action have regenerable records and keep the same allowance and clock bounds up to fixed factors, and no unbalanced spine is held open over a new high-cost query at its endpoint.

Why it's here

This fixes the shape of the unbalanced control paths so the realization theorem and the recipe certificates can check allowance, clock and record bounds one stage at a time. It builds on the structural facts about immediate candidates and midpoint ordering in the earlier path lemma, and the 'at most one terminal delegation' and 'no spine over a new high-cost query' conditions prevent costs from compounding across nested calls.
Classified routine:
A structural bookkeeping lemma about the shape of control paths that follows from the earlier path lemma (lem-est-paths) on immediate candidates and midpoint ordering. It checks the order of stages and bounds allowance, clock and record costs stage by stage, rather than introducing a new idea.

Uses

lemImmediate candidates are short and well-formed

Used by

thmController interfaces have restoring O(B)-space implementationslemEndpoint comparisons are restoring with O(d) controllemEstimator recipes have regenerable records and bounded controlclaimInductive construction of total restoring proceduresclaimImmediate paths and factor values certifiedclaimFresh presence tests before value or motionclaimUniform generation and arithmetic record bounds

Sources

PaperOpen
Section
§11.4 Certificates for the estimator recipes
Page
—
Label
lem:ctrl-paths
Line
sections/implementation.tex:654
Leannot aligned

Phase 2 aligns this node to a Lean declaration.