claimroutineinferred_dep
Decreasing-value contour tours count rank
Decreasing-value contour tours find the rank-th largest quantized value
turns contour tours into rank selection
Claim·§11.3 Contours and incoming operations·inside lemIncoming k-th largest score with short records
Statement (paper)
Starting at the requested endpoint with the success state initialized at , touring the root component for each value , counting canonical initiations (saturating at the desired fixed rank), continuing to the sentinel, and decrementing the value field by pure local steps between components, with the zero padding applied at value zero, determines the desired rank-th largest quantized value. The only data retained across a tour are the root parameter , the value field itself (the loop variable, with no separate copy), and a saturated count with control bits of constant size. At the sentinel the same endpoint and quantized value are recovered by unique-sink recovery, and no other success halt occurs in that component.
In plain English
Starting at the requested endpoint with value field , touring the root component for each value , counting canonical initiations (saturating at the desired rank), and then decrementing locally between components, finds the rank-th largest quantized value, with zero padding at value zero. Across a tour only , the value field , and a saturated count with constant-size control bits are retained, and at the sentinel the same endpoint and value are recovered by unique-sink recovery, with no other success halt in that component.
Why it's here
This claim turns the counter-free contour tours of the tree components into a rank-selection procedure. It scans values downward and counts initiations until the fixed rank is reached, so the memory stays at , and a constant-size saturated count. The next claim uses this to bound the accuracy of the order statistic and the live memory during a tour.
Classified routine:
This step applies the paper's counter-free contour-tour lemma (lem-ctrl-tour) and the scoring-program claim. It uses a standard downward scan over thresholds with a saturating counter to select the k-th largest value, which is bookkeeping rather than a new idea.
Uses
Used by
Sources
PaperOpen
- Section
- §11.3 Contours and incoming operations
- Page
- —
- Label
—- Line
sections/implementation.tex:607
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depoutline: "Decreasing-value contour tours count rank" rests on lem:ctrl-tour
- infoinferred_depoutline: "Decreasing-value contour tours count rank" rests on claim-lem-ctrl-score-rank-2