claimroutineinferred_dep

Salt permissions give later-salt independence

Syntactic salt permissions make lower-block structure independent of later salts
supplies later-salt independence for the clean calculation
Claim·§11.4 Certificates for the estimator recipes·inside lemControl records replay with later-salt independence

Statement (paper)

Each recipe is given the syntactic permission to address only salt blocks at most its budget block in its effective environment, checked directly on the requested salt index and not on the salt's value. A synthetic record cannot change this permission, choose a higher-budget recipe, or bypass the fixed parent-to-child rules. Consequently the entire lower-block structure, including the replay and checks used before predecessor queries, is independent of later salts.

In plain English

Each recipe may only address salt blocks up to its own budget block in its effective environment, and this is checked on the salt index requested, not its value. Synthetic records cannot alter this permission, pick a higher-budget recipe, or skip the fixed parent-to-child rules, so all lower-block structure, including replay and checks before predecessor queries, is independent of later salts.

Why it's here

This is the step of the parent lemma that gives the later-salt independence part: because the restriction is syntactic, no value of a later salt can affect any lower-block structure. It builds on the regeneration of environments from walk words (claim-lem-ctrl-replay-2), which fixes what each recipe's environment is, and it is the salt-visibility fact that the clean-calculation lemma (lem-fp-clean) relies on.
Classified routine:
This step is bookkeeping inside the paper's own construction. Later-salt independence follows directly from the syntactic budget restriction on salt indices, combined with the environment regeneration in claim-lem-ctrl-replay-2. That is a standard information-flow or locality argument, not a new idea.

Uses

lemClean calculation is independent of the saltclaimEnvironment regenerated from walk words

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Salt permissions make lower structure later-salt independent" rests on claim-lem-ctrl-replay-2