claimroutineinferred_dep

Uniform generation and arithmetic record bounds

Indices and coefficients generated uniformly; record certificate holds regardless of guards
closes the recipe lemma's record bound
Claim·§11.4 Certificates for the estimator recipes·inside lemEstimator recipes have regenerable records and bounded control

Statement (paper)

Each enumerated object in the estimator recipes has a literal O(d)O(d)-bit index or is a Boolean path in one of the stated arithmetic recipes, and index generation, constants, field/rate coefficients and walk probabilities (with O(B)O(B)-bit rational descriptions) are produced without recursive graph calls, so the uniformity and public-coefficient hypotheses of the arithmetic theorem hold. Structural selection words and loop counters have O(d)O(d) bits, the only longer local numerical words obey their explicit clock-decrement bounds, and a fixed number of arithmetic and structural layers, together with ordered terminal delegations including on rollback, only enlarges the constants in ; hence the record certificate holds on the designated executions independently of any graph guards.

In plain English

Every enumerated object in the estimator recipes is either indexed by a literal O(d)O(d)-bit index or is a Boolean path in a stated arithmetic recipe. Indices, constants, coefficients and walk probabilities are produced without recursive graph calls, so the arithmetic theorem's hypotheses hold. Selection words and loop counters stay at O(d)O(d) bits, longer numerical words obey their clock-decrement bounds, and fixed numbers of layers and ordered terminal delegations (including on rollback) only enlarge the constants in the record bound, so the record certificate holds on designated executions regardless of graph guards.

Why it's here

This claim closes the proof of the parent lemma. It checks the uniformity and public-coefficient hypotheses of the arithmetic interface for every recipe, so the numerical record bound applies. Combined with the ordered path form, the rank wrapper's record bound and the stratum ordering, it shows the structural and numerical pieces add up to the stated bound with only constant-factor losses, independent of guards.
Classified routine:
Bookkeeping check that the recipes satisfy the uniformity and public-coefficient hypotheses of the paper's arithmetic interface theorem (thm-arith-interface). It combines this with the earlier ordered-path, rank-wrapper and stratum-ordering results, which only enlarge constants in the record bound.

Uses

lemIncoming k-th largest score with short recordsthmUniform numerical interface for arithmetic recipeslemUnbalanced estimator paths have ordered restoring formclaimFinite acyclic stratum ordering within group

Used by

Nothing in the paper

Sources

PaperOpen
Section
§11.4 Certificates for the estimator recipes
Page
—
Label
—
Line
sections/implementation.tex:1047
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Uniform generation and arithmetic record bounds" rests on claim-lem-ctrl-recipes-5