claimroutineinferred_dep

Order statistic accuracy and inverse-probe bounds

Order statistic

N_t

is within 2 of

2^t

times the rank, with short probes

finishes accuracy and memory of the rank lemma

Claim·§11.3 Contours and incoming operations·inside lemIncoming k-th largest score with short records

Statement (paper)

The procedure computes the integer order statistic

N_t

of the values

q_t(v)

, and

N_t

has error less than

2

as an approximation to

2^t

times the desired rank. Moreover, during a tour the live program state may be a partial suffix state preceding a high-place query, containing only that short suffix rather than a saved copy of the final score, so Lemma also gives the required bound for inverse neighbor queries.

In plain English

The procedure outputs the integer order statistic

N_t

of the quantized values

q_t(v)

, and

N_t

approximates

2^t

times the desired rank with error less than

2

. The live state during a tour may be a partial suffix state before a high-place query, not a saved final score, so the local-graph lemma also gives the needed bound for inverse neighbor queries.

Why it's here

The accuracy follows because the tour finds the exact rank-th largest of the

q_t

values, and the quantization claim says each

q_t(v)

is within

2

2^t v

(zeros contribute nothing). The memory part applies the guarded local graph lemma: live state holds only a short suffix, so inverse probes stay within the local-record bound and no full score copy is retained.

Classified routine:

Direct consequence of the earlier claims: the contour tour computes the exact order statistic (claim-3), and the quantization claim bounds each

q_t(v)

within 2 of

2^t v

. The memory part is a straightforward application of the paper's guarded local graph lemma (lem-ctrl-local-graph).

Uses

lemGuarded local graph for terminal recipesclaimQuantized scores approximate and vanish at zeroclaimDecreasing-value contour tours count rank

Used by

Nothing in the paper

Sources

PaperOpen

Section: §11.3 Contours and incoming operations
Page: —
Label: —
Line: sections/implementation.tex:627

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Order statistic accuracy and inverse-probe bounds" rests on claim-lem-ctrl-score-rank-1
info
inferred_dep
outline: "Order statistic accuracy and inverse-probe bounds" rests on claim-lem-ctrl-score-rank-3