lemmaroutine

Order statistics have linear-space residue procedures

Order statistics of 2κd2^{\kappa d} values have residue procedures with linear records
rank primitive covered by the common clock coefficient
Lemma·lem:arith-rank·§10.5 Indexed ranks, sums, scales, and structural leaves

Statement (paper)

Fix κ>0\kappa>0 and d≥1d\geq1. Consider at most 2κd2^{\kappa d} normalized values, indexed by descriptors of length at most κd\kappa d, and an order statistic specified by an O(d)O(d)-bit index. The semantic list length nn is public; the requested index is in {1,…,n}\{1,\ldots,n\}, or an out-of-range request returns a prescribed normalized constant. Absent descriptors may be assigned prescribed constant dummy values by structural validity predicates. This order statistic has deterministic integer approximations NtN_t satisfying Equation . Their residue procedures have constants a,b,ca,b,c, depending only on the descriptor bounds, such that an operand digit query at jj obeys j≤t+cd,L≤ad+b(t−j), j\leq t+cd,\qquad L\leq ad+b(t-j), where LL is the total suspended local record length. A structural validity query is assigned clock zero and has suspended length O(d+t)O(d+t). The intrinsic local length is O(d+t)O(d+t).

In plain English

For at most 2κd2^{\kappa d} normalized values indexed by descriptors of length at most κd\kappa d, and an O(d)O(d)-bit rank index (out-of-range returning a fixed constant), the order statistic has deterministic integer approximations NtN_t whose residue procedures have constants a,b,ca,b,c such that every operand digit query at jj satisfies j≤t+cdj\leq t+cd and L≤ad+b(t−j)L\leq ad+b(t-j), where LL is the suspended local record length. Structural validity queries have clock zero and suspended length O(d+t)O(d+t), and the intrinsic local length is O(d+t)O(d+t).

Why it's here

This extends the elementary-gate bounds to rank selection, which is built from compositions of min, max and comparisons evaluated depth-first with path-only storage. It gives rank operations the same clock and suspended-record bounds as elementary gates, so the uniform arithmetic interface can use one common clock coefficient across all primitive types.
Classified routine:
Follows by expressing rank selection as a composition of min/max/comparison gates and applying the paper's elementary-gate residue bounds (lem-arith-elementary) together with depth-first path-only circuit evaluation (lem-arith-gate-evaluation). This is bookkeeping that extends the earlier lemmas to one more primitive type.

Uses

lemElementary arithmetic operations have linear-space residue procedureslemDepth-first circuit evaluation uses path-only storage

Used by

claimOne clock coefficient works throughout

Sources

PaperOpen
Section
§10.5 Indexed ranks, sums, scales, and structural leaves
Page
—
Label
lem:arith-rank
Line
sections/arithmetic.tex:543
Leannot aligned

Phase 2 aligns this node to a Lean declaration.