claimroutineinferred_dep

Scoring program assembles short suffix only

Score digits built least-significant first, so records are O(1+t+c−j)O(1+t+c-j)
gives the short-record bound for the scoring program
Claim·§11.3 Contours and incoming operations·inside lemIncoming k-th largest score with short records

Statement (paper)

The forward terminal program, which first tests the entire class and membership domain at its canonical initiation and sends invalid inputs to failure, has a success configuration with the endpoint in the cursor and qt(v)q_t(v) in its local state. It assembles the score digits from least to most significant before its final structural motion, so that before the place-jj digit is queried the accumulated suffix, its carry and a self-delimiting offset from t+ct+c occupy O(1+t+c−j)O(1+t+c-j) bits. The complete O(t+1)O(t+1)-bit word is then held only through structural motion and local clearing to success, so all its graph-query boundaries satisfy the claimed record bound.

In plain English

The forward terminal program first checks the class and membership domain and fails on invalid inputs; on success it holds the endpoint in the cursor and qt(v)q_t(v) in local state. It builds the score digits from least to most significant, so before querying the place-jj digit its stored suffix, carry and offset from t+ct+c take only O(1+t+c−j)O(1+t+c-j) bits, and the full O(t+1)O(t+1)-bit word is kept only during structural motion and clearing.

Why it's here

This claim establishes the local-record bound of the parent lemma: because digits are produced from the least significant end, the memory at each score-digit query depends on t+c−jt+c-j rather than on tt. The full score word, built from the quantized score of the previous claim, is held only over structural calls, which the lemma accounts for separately. The later contour-tour counting claim can then rely on a program that yields qt(v)q_t(v) with this bounded record.
Classified routine:
Bookkeeping within the parent lemma: least-significant-first digit assembly of the quantized score from the previous claim, with standard carry and self-delimiting offset encoding, gives the record bound by a direct space accounting.

Uses

claimQuantized scores approximate and vanish at zero

Used by

claimDecreasing-value contour tours count rank

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Scoring program assembles short suffix only" rests on claim-lem-ctrl-score-rank-1