claimroutineinferred_dep

Sentinel modification gives Lipschitz propagation bound

With few heavy entries, sentinels give discrepancies at most CECE by Lipschitz
light-entry case giving the CECE bound
Claim·§8.3 Deterministic comparison arguments·inside lemRelative stability at first overflow

Statement (paper)

Suppose fewer than KK true first entries exceed L0L_0, and in both calculations replace, at the at most K−1K-1 positions with dy>L1d_y>L_1, the first input at group jj by a common positive sentinel larger than L1L_1, with zero later first-channel increments there. Then every array and threshold discrepancy is at most CECE, where E=∑i≥jC1m∗−i+1eiE=\sum_{i\geq j}C_1^{m_*-i+1}e_i and C1C_1 exceeds the fixed update constant. If EE is sufficiently small, all these thresholds remain below 2L0+12L_0+1, and the final root-output discrepancy is at most CECE.

In plain English

If fewer than KK true first entries exceed L0L_0, and in both calculations the at most K−1K-1 positions with dy>L1d_y>L_1 get a common sentinel first input larger than L1L_1 (with zero later first-channel increments), then all array and threshold discrepancies are at most CECE, where E=∑i≥jC1m∗−i+1eiE=\sum_{i\geq j}C_1^{m_*-i+1}e_i. For sufficiently small EE, the thresholds stay below 2L0+12L_0+1 and the final root-output discrepancy is at most CECE.

Why it's here

Replacing the heavy entries by a shared sentinel removes the large first-channel values that would otherwise break the relative error bounds, so the uniform Lipschitz property of the update map (lem-buf-update) applies to the remaining entries with the increment bounds from the reduction claim. Iterating this through the groups gives the geometric factors C1m∗−i+1eiC_1^{m_*-i+1}e_i, and keeping thresholds below 2L0+12L_0+1 lets the final root outputs be compared with the same CECE bound, which the next claim uses to show the sentinels do not alter the perturbed calculation.
Classified routine:
Follows by iterating the uniform Lipschitz property of the buffer update map (lem-buf-update) group by group, using the small relative prefix errors from the reduction claim. The geometric factors C_1^{m_*-i+1} come from standard error-propagation bookkeeping, once the heavy entries are replaced by a common sentinel.

Uses

lemPre-overflow buffer loss and reference calculationlemBuffer update map: replacement, monotonicity, LipschitzclaimReduction to small relative prefix errors

Used by

claimSentinels leave perturbed calculation unchanged

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Sentinel modification gives Lipschitz propagation bound" rests on claim-lem-buf-relative-stability-1