claimroutineinferred_dep

Ranks, compression and list selection

Ranks, compression and list selection run in

2^{O(d)}

indices with

O(d)

control

controls compression and list-selection stage

Claim·§11.4 Certificates for the estimator recipes·inside lemEstimator recipes have regenerable records and bounded control

Statement (paper)

At a prefix of slack

d

, the rank, compression and list-selection operations (ranks, max, min, absolute value, clipping, the threshold test strictly between

u_0

and

2u_0

, and the remapping of a list ordinal to its selected intermediate descriptor) are evaluated over a finite domain of

2^{O(d)}

indices with ranges

2^{O(d)}

, normalizing shifts of magnitude

O(d)

and a numerical clock

O(d)

. Every nondefault compressed position is included and fewer than

n_d

positions are selected, as in Lemma , and a terminal list motion selects its descriptor before delegating to an old prefix path or a new valid path.

In plain English

At slack

d

, the rank, max/min, absolute value, clipping, threshold test strictly between

u_0

and

2u_0

, and list-ordinal remapping operations run over

2^{O(d)}

indices with ranges

2^{O(d)}

, normalizing shifts

O(d)

and numerical clock

O(d)

. Every nondefault compressed position is kept and fewer than

n_d

positions are selected, as in the buffer update lemma, and a terminal list motion selects its descriptor before delegating to an old prefix path or a new valid path.

Why it's here

This supplies the control bounds for the compression and list-selection stage that follows the candidate domain and bucket sums, so these operations fit the same

O(d)

structural control as the other strata. Compression keeps all exceptions with fewer than

n_d

positions by the buffer update lemma, and the clamping and atom-margin facts bound the ranges. The ordering of descriptor selection before delegation is what lets the later claim arrange these operations into a finite acyclic stratum order.

Classified routine:

Bookkeeping step inside the estimator-recipe control lemma: the domain and range bounds follow directly from the paper's buffer update, clamping and atom-margin lemmas and the preceding candidate-domain claim, with no new idea of its own.

Uses

lemBuffer update map: replacement, monotonicity, LipschitzlemClamping preserves final row functionslemAtom margins: sparse rows with exposed classesclaimCandidate domain and bucket sums

Used by

claimFinite acyclic stratum ordering within group

Sources

PaperOpen

Section: §11.4 Certificates for the estimator recipes
Page: —
Label: —
Line: sections/implementation.tex:867

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Ranks, compression and list selection" rests on claim-lem-ctrl-recipes-2