lemmaroutineinferred_dep

Control records replay with later-salt independence

Control records replay descendants, and procedures ignore later salt blocks
regenerability and later-salt independence for clean blocks
Lemma·lem:ctrl-replay·§11.4 Certificates for the estimator recipes

Statement (paper)

The records in Lemma  are regenerable in the sense of Definition . With respect to their own effective environments, actual procedures at a budget in block bb ignore all salt blocks later than bb, including in structural orders, graph universes, guards and predecessor probes. Re-querying a table entry or using a paired port in either direction uses the same effective table tuple.

In plain English

The control records of the estimator recipes are regenerable, so descendant tuples and clocks can be recomputed from the root data and the active records. Procedures at a budget in block bb ignore all later salt blocks, including in structural orders, graph universes, guards and predecessor probes, and re-querying a table entry or using a paired port in either direction uses the same effective table tuple.

Why it's here

This lemma checks that the recipe records meet the regenerability definition, using the walk-word, numerical-place and salt-permission claims in its proof. Regenerability keeps the stored control information small, and later-salt independence is what the clean-calculation lemma and the realization theorem need.
Classified routine:
A verification lemma: it checks that the estimator-recipe records satisfy the paper's own regenerability definition (def-ctrl-record). It does this by bookkeeping over the walk-word, numerical-interface and salt-independence results proved earlier (lem-est-paths, thm-arith-interface, lem-fp-clean), with no new idea.

Uses

lemAtom ports: bounded rows with smooth witnesseslemImmediate candidates are short and well-formedthmUniform numerical interface for arithmetic recipeslemClean calculation is independent of the saltdefRegenerable local records

Used by

lemClean calculation is independent of the saltthmController interfaces have restoring O(B)-space implementationsclaimInductive construction of total restoring procedures

Inside the proof

claimEstimator edges determine descendant tuplesclaimEnvironment regenerated from walk wordsclaimNumerical places recovered with one scratchclaimSalt permissions give later-salt independence

Sources

PaperOpen
Section
§11.4 Certificates for the estimator recipes
Page
—
Label
lem:ctrl-replay
Line
sections/implementation.tex:1086
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: lem:ctrl-replay states that the records "are regenerable in the sense of Definition " (implementation.tex 1087-1088). The definition is currently an orphan.