claimroutineinferred_dep

Sentinels leave perturbed calculation unchanged

Replacing heavy coordinates by sentinels leaves the perturbed run unchanged
transfers the sentinel bound to the actual run
Claim·§8.3 Deterministic comparison arguments·inside lemRelative stability at first overflow

Statement (paper)

Replacing the fewer than KK coordinates with dy>L1d_y>L_1 by sentinels does not change the perturbed calculation: the defaults and thresholds agree with those of the unmodified calculation, the compression is the identity in both channels at these positions, all other coordinates agree, and the relevant output behavior is the same.

In plain English

Replacing the fewer than KK coordinates with dy>L1d_y>L_1 by sentinels does not alter the perturbed calculation. Defaults and thresholds match the unmodified calculation, compression is the identity in both channels at those positions, all other coordinates agree, and the relevant output behavior is the same.

Why it's here

This lets the Lipschitz bound of the previous claim, proved for the sentinel-modified calculation, be applied to the actual perturbed calculation. That transfers the CECE discrepancy bound on final row-root outputs to the original calculation and finishes the parent lemma's relative-stability estimate.
Classified routine:
A direct bookkeeping check, following from the definitions of the defaults, thresholds and compression map, that the sentinel modification from the previous claim (claim-lem-buf-relative-stability-3) agrees with the actual perturbed calculation. It needs no new idea.

Uses

claimSentinel modification gives Lipschitz propagation bound

Used by

Nothing in the paper

Sources

PaperOpen
Section
§8.3 Deterministic comparison arguments
Page
—
Label
—
Line
sections/compression.tex:365
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Sentinels do not change perturbed calculation" rests on claim-lem-buf-relative-stability-3