lemmaroutine

Incoming k-th largest score with short records

Incoming kkth-largest score has exact digits with records O(1+(t−j)+)O(1+(t-j)_+)
rank-selection wrapper for recipes
Lemma·lem:ctrl-score-rank·§11.3 Contours and incoming operations

Statement (paper)

Let a constant-size forward row class cover every positive entry of a bounded nonnegative score table, with distinct entries in each row. Suppose pre-incoming score digits are restoring queries, and the class has a terminal program with the preceding interfaces. A fixed incoming kkth-largest value, with zero padding, has exact redundant digits computed by a restoring procedure. Its local record above a place-jj score query at output approximation clock tt is O(1+(t−j)+)O(1+(t-j)_+), with a fixed overshoot j≤t+cj\le t+c, in addition to the structural allowance costs. A complete O(t+1)O(t+1)-bit score word is retained only over structural calls.

In plain English

If a constant-size forward row class covers all positive entries of a bounded nonnegative score table (distinct within each row) and has a terminal program, then the fixed incoming kkth-largest value, zero-padded, has exact redundant digits computed by a restoring procedure. Its local record above a place-jj score query at output clock tt is O(1+(t−j)+)O(1+(t-j)_+) with fixed overshoot j≤t+cj\le t+c, plus structural allowance costs, and a full O(t+1)O(t+1)-bit score word is kept only over structural calls.

Why it's here

This lemma packages the rank-selection step as a restoring procedure with tight memory. It combines quantized scores, a program that builds score digits from the least significant end, and decreasing-value contour tours that count initiations, then uses the guarded local graph lemma to bound inverse probes. The realization theorem and the recipe certificates rely on it for the inverse-rank wrapper and its record bounds.
Classified routine:
A technical bookkeeping lemma that packages rank selection (k-th largest via contour tours counting initiations) as a restoring procedure. Its record bounds come directly from the paper's earlier guarded local graph lemma and digit-by-digit score computation, so it is an adaptation rather than a headline new idea.

Uses

lemGuarded local graph for terminal recipes

Used by

thmController interfaces have restoring O(B)-space implementationslemEstimator recipes have regenerable records and bounded controlclaimContours implement cap and rank wrappersclaimFinal row classes and wrappers add fixed strataclaimUniform generation and arithmetic record bounds

Inside the proof

claimQuantized scores approximate and vanish at zeroclaimScoring program assembles short suffix onlyclaimDecreasing-value contour tours count rankclaimOrder statistic accuracy and inverse-probe bounds

Sources

PaperOpen
Section
§11.3 Contours and incoming operations
Page
—
Label
lem:ctrl-score-rank
Line
sections/implementation.tex:562
Leannot aligned

Phase 2 aligns this node to a Lean declaration.