lemmaroutinestructure_uncertain

Clean calculation is independent of the salt

Clean calculation is independent of the block's salt and matches actual before small groups
salt-free model the coupling compares against
Lemma·lem:fp-clean·§9.2 The update rule and the clean calculation

Statement (paper)

Every clean value and structural choice for block bb is independent of that block's effective salt and of later effective salts. In a task of budget M∈IbM\in\mathcal I_b, the actual and clean row states immediately before the first group with d≤2h∗d\le2h_* are identical and independent of that salt. Their stored lists at this boundary have size 2O(h∗)2^{O(h_*)}. The deterministic slice-mean assertion required by Lemma  holds for the clean calculation.

In plain English

For block bb, all clean values and structural choices do not depend on that block's effective salt or on later effective salts. In a task of budget M∈IbM\in\mathcal I_b, the actual and clean row states just before the first group with d≤2h∗d\le2h_* coincide, are independent of that salt, and have stored lists of size 2O(h∗)2^{O(h_*)}; the deterministic slice-mean assertion needed by Lemma lem:est-prefix holds for the clean calculation.

Why it's here

This lemma sets up the clean model that the block coupling compares against: the clean calculation is salt-free, and the actual run agrees with it up to the boundary where the small groups begin. The envelope-size and coupling arguments (lem-fp-envelope, prop-fp-coupling) rely on it, and the slice-mean assertion allows the prefix estimates behind the error-reserve bound to be applied to the clean calculation. It relies on the parameter replay and salt-visibility facts (lem-ctrl-replay) and the mixing walk operator and its variants (lem-env-gap, lem-env-variants).
Classified routine:
This is bookkeeping internal to the paper's construction. Salt-independence of the clean calculation follows directly from the replay and later-salt-independence properties (lem-ctrl-replay). The list-size bound and the slice-mean assertion follow from the walk-operator facts (lem-env-gap, lem-env-variants).

Uses

lemControl records replay with later-salt independencelemExponentially mixing averaging operator on conditional spacelemWalk variants avoid storing endpointspropError reserve after compression and clamping

Used by

lemWitness envelope is small and collision-controlledpropActual runs stay close to clean runslemControl records replay with later-salt independenceclaimClean active tasks meet target boundsclaimSalt permissions give later-salt independence

Sources

PaperOpen
Section
§9.2 The update rule and the clean calculation
Page
—
Label
lem:fp-clean
Line
sections/fingerprints.tex:202
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    structure_uncertain
    lem:fp-clean cites lem:ctrl-replay for the salt-access implementation, while lem:ctrl-replay's proof cites lem:fp-clean; the reference is mutual rather than a strict dependency order.