lemmaroutine

Estimator recipes have regenerable records and bounded control

Estimator operations have regenerable records and control cstrd+cnum(t−j)c_{\rm str}d+c_{\rm num}(t-j)
record and control bounds for building restoring procedures
Lemma·lem:ctrl-recipes·§11.4 Certificates for the estimator recipes

Statement (paper)

All actual estimator operations admit regenerable records and a fixed finite ordering of operation strata. At a prefix of slack dd, each ordinary layer has O(d)O(d) structural control, and a numerical path to an operand at clock jj has suspended record cstrd+cnum(t−j),j−t≤cdigd, c_{\mathrm{str}}d+c_{\mathrm{num}}(t-j),\qquad j-t\le c_{\mathrm{dig}}d, with fixed coefficients. Beyond the fixed strata of this prefix, a call is to the preceding prefix of slack 2d2d, or to an estimator of budget at most M−dM-d. The final row and incoming wrappers add a fixed number of strata at d=1d=1. Every designated terminal execution obeys the corresponding boundary bounds before guards are imposed.

In plain English

Every actual estimator operation has regenerable records and sits in a fixed finite ordering of strata. At prefix slack dd, ordinary layers have O(d)O(d) structural control, and a numerical path to an operand at clock jj has suspended record cstrd+cnum(t−j)c_{\mathrm{str}}d+c_{\mathrm{num}}(t-j) with j−t≤cdigdj-t\le c_{\mathrm{dig}}d. Beyond the fixed strata, calls go to the prefix of slack 2d2d or to an estimator of budget at most M−dM-d, the final row and incoming wrappers add a fixed number of strata at d=1d=1, and terminal executions obey the boundary bounds.

Why it's here

This lemma certifies that every operation in the estimator construction fits the restoring-procedure framework with uniform constants. Its proof combines the structural facts about immediate candidates, the arithmetic interface for numerical steps, and the buffer, clamping, port and rank lemmas into an acyclic stratum ordering, with the final-row wrappers handled at constant size. The realization theorem uses these record and control bounds to build total restoring procedures by induction on allowance.
Classified routine:
This is bookkeeping that assembles earlier nodes into an acyclic stratum ordering with uniform constants. It draws on the immediate-candidate bounds, the ordered restoring paths, the arithmetic interface, and the buffer, clamping, port and rank lemmas, verifying that each estimator operation fits the restoring-procedure framework.

Uses

lemImmediate candidates are short and well-formedlemUnbalanced estimator paths have ordered restoring formthmUniform numerical interface for arithmetic recipeslemBucket discrepancy bound with collision chargelemBuffer update map: replacement, monotonicity, LipschitzlemClamping preserves final row functionslemAtom margins: sparse rows with exposed classeslemCapped incoming ports give restoring paired motionslemAtom ports: bounded rows with smooth witnesseslemIncoming k-th largest score with short records

Used by

thmController interfaces have restoring O(B)-space implementationsclaimAllowance strictly drops at every boundaryclaimRaw certificates independent of physical constantsclaimInductive construction of total restoring procedures

Inside the proof

claimImmediate paths and factor values certifiedclaimCandidate domain and bucket sumsclaimRanks, compression and list selectionclaimFresh presence tests before value or motionclaimFinite acyclic stratum ordering within groupclaimFinal row classes and wrappers add fixed strataclaimUniform generation and arithmetic record bounds

Sources

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

Phase 2 aligns this node to a Lean declaration.