claimroutine

Estimator edges determine descendant tuples

Active records of an estimator edge determine the descendant tuple
recomputes descendant parameters without hidden state
Claim·§11.4 Certificates for the estimator recipes·inside lemControl records replay with later-salt independence

Statement (paper)

Starting from the fixed top parameters, the active records of an estimator edge (its task type, prescribed stage change, budget offset, bin-scale offset if present, bounded copy choice and channel-role recipe) determine the next absolute stage, rates and suffixes, and hence the descendant effective tuple. A projection appends the stored symbol before the inherited suffix, and a fresh midpoint or vector role uses the specified public stage rate and its prescribed suffix without carrying the old source; these are the common-tuple recipes of Lemma  and Lemma .

In plain English

From the fixed top parameters, the active records of an estimator edge (task type, stage change, budget offset, optional bin-scale offset, bounded copy choice, channel-role recipe) determine the next absolute stage, rates, suffixes and hence the descendant effective tuple. A projection prepends the stored symbol to the inherited suffix, while a fresh midpoint or vector role uses the public stage rate and its prescribed suffix without the old source.

Why it's here

This is the step of the replay lemma showing that descendant tuples can be recomputed from the root data and active records alone, so no hidden state is needed. It rests on the common-tuple recipes of the atom-port and estimator-path lemmas, in particular that a product's right-hand task tuple does not depend on the discarded old source.
Classified routine:
Direct bookkeeping consequence of the common-tuple recipes already established in Lemma lem:atom-ports and Lemma lem:est-paths: the active records deterministically specify stage, rates and suffixes, so the descendant tuple is recomputed from them.

Uses

lemAtom ports: bounded rows with smooth witnesseslemImmediate candidates are short and well-formed

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.