claimroutineinferred_dep

Finite acyclic stratum ordering within group

Estimator operations form a finite acyclic order of strata within a group
rules out circular dependence among operations
Claim·§11.4 Certificates for the estimator recipes·inside lemEstimator recipes have regenerable records and bounded control

Statement (paper)

The operations within a group admit a fixed finite acyclic ordering of strata, from an exported operation down to its dependencies: compressed entries, baseline and list-port operations; ordinal remapping, compression and exception selection; size and first-signal ranks of intermediate entries; intermediate domain flags and entry or bucket-sum values; first-representative and key-match predicates; endpoint comparisons of outer-valid paths; outer-valid visits and then outer path validity; and intrinsic visits, constituent tests, factor digits and ordered motions. Within this ordering, outer-valid visits use outer validity, outer validity uses intrinsic visits, key comparisons use outer-valid visits, and bucket predicates use those comparisons. Between these layers Theorem  gives , structural loops add O(d)O(d) bits, and all remaining path calls go to the preceding prefix or to the lower-budget factors already described.

In plain English

Within a group, the estimator operations can be arranged in a fixed finite acyclic order of strata, running from exported operations down to ordered motions and digits. Between strata, the arithmetic interface gives the numerical record bound, structural loops add O(d)O(d) bits, and other path calls go to the preceding prefix or to lower-budget factors.

Why it's here

This orders the operations handled in the earlier claims (candidate domain and bucket sums, ranks and compression, list selection) so that each stratum calls only lower ones, which rules out circular dependence. The fixed finite order together with Theorem thm:arith-interface for numerical steps gives the regenerable records and control bounds that the parent lemma asserts, and the later record-bound claim builds on it.
Classified routine:
Bookkeeping step that organizes the operations from the earlier claims (candidate domains, bucket sums, ranks, compression) into a finite acyclic call order. Combined with the paper's arithmetic interface theorem, this gives the control bound, in the style of standard composition-of-space-bounded-subroutines arguments.

Uses

thmUniform numerical interface for arithmetic recipesclaimCandidate domain and bucket sumsclaimRanks, compression and list selection

Used by

claimUniform generation and arithmetic record bounds

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Finite acyclic stratum ordering within group" rests on claim-lem-ctrl-recipes-2
  • info
    inferred_dep
    outline: "Finite acyclic stratum ordering within group" rests on claim-lem-ctrl-recipes-3