claimroutine

Final row classes and wrappers add fixed strata

Final row classes and wrappers add a fixed number of strata at d=1d=1
handles the last layer of the estimator
Claim·§11.4 Certificates for the estimator recipes·inside lemEstimator recipes have regenerable records and bounded control

Statement (paper)

At the final slack d=1d=1, the list size, port alphabet and all threshold gaps are constants, and the row classes and witnesses of Lemma  are defined by canonical finite-margin entry and rank tests on the final raw arrays, which can be enumerated without testing positivity of a computed score. The incoming-gate and correction-precursor auxiliary classes, their initial restoring validity checks, and the capped-pair, inverse-score and vector wrappers (finitely many final wrapper types, with fixed-size counts and return ports) are separate terminal programs placed above their pre-incoming queries and call only the final buffer, fixed arithmetic recipes, or lower forward operations, so that they add a fixed number of strata at d=1d=1 obeying the recipe bounds.

In plain English

At final slack d=1d=1 the list size, port alphabet and threshold gaps are constants, so the row classes and witnesses of Lemma 5.6 come from finite-margin entry and rank tests on the final raw arrays, with no positivity test of a computed score. The incoming-gate and correction-precursor classes, their initial validity checks, and the capped-pair, inverse-score and vector wrappers are separate terminal programs above the pre-incoming queries, adding only a fixed number of strata at d=1d=1 that obey the recipe bounds.

Why it's here

This claim handles the last layer of the estimator in the proof of the recipes lemma. Because every size is constant at d=1d=1, the row classes are finitely enumerable, so the capped-port motions of Lemma 11.6 and the rank-selection records of Lemma 11.7 apply directly. The wrappers call only the final buffer, fixed arithmetic recipes or lower forward operations, so they add a fixed number of strata and meet the stated record bounds without disturbing the main recursion.
Classified routine:
Bookkeeping step inside the recipes lemma: at constant slack d=1 all sizes are constants, so the row classes are finitely enumerable and the earlier capped-port (lem-ctrl-cap) and rank-selection (lem-ctrl-score-rank) lemmas apply directly. The wrappers then add only a fixed number of strata.

Uses

lemAtom ports: bounded rows with smooth witnesseslemCapped incoming ports give restoring paired motionslemIncoming k-th largest score with short records

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.