claimroutine

Quantized scores approximate and vanish at zero

Quantized score qt(v)q_t(v) is within 2 of 2tv2^tv and qt(0)=0q_t(0)=0
lets rank be read from the forward class alone
Claim·§11.3 Contours and incoming operations·inside lemIncoming k-th largest score with short records

Statement (paper)

With qt(v)=clip⁡[0,2t](⌊2tv[t+c]⌋)q_t(v)=\operatorname{clip}_{[0,2^t]}\left(\left\lfloor 2^t v^{[t+c]}\right\rfloor\right) and a fixed extra margin cc chosen so that the digit tail, of absolute value at most a fixed constant times 2−t−c2^{-t-c}, is less than 2−t2^{-t}, we have ∣qt(v)−2tv∣<2|q_t(v)-2^t v|<2 for every normalized score v∈[0,1]v\in[0,1], and qt(0)=0q_t(0)=0. Consequently, since the forward class contains every positive score, enumerating its entries and padding by zero gives the rank of the whole quantized score column.

In plain English

The quantized score qt(v)q_t(v), built from the first t+ct+c digits of vv and clipped to [0,2t][0,2^t], is within 22 of 2tv2^t v for every v∈[0,1]v\in[0,1], and qt(0)=0q_t(0)=0. Hence listing the forward class's entries and padding with zeros yields the rank of the whole quantized score column.

Why it's here

The margin cc makes the digit truncation tail smaller than 2−t2^{-t}, so flooring and clipping cost less than 22 in total. Because qt(0)=0q_t(0)=0, zero scores do not matter, and the forward class, which covers every positive score, is enough to determine the rank. This lets the later claims treat the order statistic of the qtq_t values as an approximation of 2t2^t times the desired rank and use the program on the forward class alone.
Classified routine:
Elementary bookkeeping: the truncation-tail bound plus floor and clip errors give ∣qt(v)−2tv∣<2|q_t(v)-2^t v|<2, and qt(0)=0q_t(0)=0 is immediate. Padding by zeros to get the rank is direct order-statistic bookkeeping.

Uses

Nothing else in the paper

Used by

claimScoring program assembles short suffix onlyclaimOrder statistic accuracy and inverse-probe bounds

Sources

PaperOpen
Section
§11.3 Contours and incoming operations
Page
—
Label
—
Line
sections/implementation.tex:576
Leannot aligned

Phase 2 aligns this node to a Lean declaration.