claimroutine

Candidate domain and bucket sums

Candidate domain and bucket sums reproduce the bucket array with

O(d)

control

first stratum of the recipe ordering

Claim·§11.4 Certificates for the estimator recipes·inside lemEstimator recipes have regenerable records and bounded control

Statement (paper)

The candidate domain and bucket sums are realized by operations of the fixed strata at prefix slack

d

with

O(d)

structural control: the representative flags are decided by enumerating the

2^{O(d)}

descriptors using only lower validity and endpoint comparison operations on the unmerged paths and the preceding prefix's already-defined positions (never the new value of the bucket being defined), and each intermediate entry, equal to the old entry at an old representative or the previous baseline at a new representative plus the sum of all valid matching increments in each channel, is evaluated by the balanced sum construction of Theorem . The resulting rule preserves distinct actual representatives, including two old representatives with the same key, and gives exactly the intermediate array used in Lemma .

In plain English

At prefix slack

d

, the candidate domain (which descriptors are representatives) and the intermediate bucket sums are computed by operations in the fixed strata with

O(d)

structural control. They reproduce exactly the intermediate array of Lemma lem:fp-buckets, distinguishing all actual representatives, including two old ones with the same key.

Why it's here

Representative flags are decided by looping over the

2^{O(d)}

descriptors using only lower-stratum validity and endpoint comparisons, and never the bucket being defined, so there is no circularity. Each entry is a sum of valid matching increments, evaluated by the balanced sum construction of the arithmetic interface. This ties the actual operations to the array that the bucket discrepancy bound analyzes, and supplies the first stratum for the rank, compression and ordering claims that follow.

Classified routine:

A bookkeeping step inside lem-ctrl-recipes: it realizes the intermediate array of Lemma lem:fp-buckets by enumerating 2^{O(d)} descriptors with lower-stratum comparisons and evaluating the sums with the balanced sum construction of Theorem thm:arith-interface, a direct consequence of those earlier nodes.

Uses

thmUniform numerical interface for arithmetic recipeslemBucket discrepancy bound with collision charge

Used by

claimRanks, compression and list selectionclaimFinite acyclic stratum ordering within group

Sources

PaperOpen

Section: §11.4 Certificates for the estimator recipes
Page: —
Label: —
Line: sections/implementation.tex:843

Leannot aligned

Phase 2 aligns this node to a Lean declaration.