claimroutine

Reduction to small relative prefix errors

Reduces to small EE, giving relative prefix error and increment bounds
normalization used by both heavy-entry cases
Claim·§8.3 Deterministic comparison arguments·inside lemRelative stability at first overflow

Statement (paper)

Let E=∑i≥jC1m∗−i+1eiE=\sum_{i\geq j}C_1^{m_*-i+1}e_i. It suffices to treat the case where EE is at most a sufficiently small fixed constant, since otherwise bounded output ranges give the bound. In that case all clipped errors involved are strictly below 11, so ∣Si1(y)−dy∣≤(1+dy)ei|S_i^1(y)-d_y|\leq(1+d_y)e_i and ∣Si2(y)−vy∣≤ei|S_i^2(y)-v_y|\leq e_i, and later increments have first magnitude at most (1+dy)(ei+ei−1)(1+d_y)(e_i+e_{i-1}) and second magnitude at most ei+ei−1e_i+e_{i-1}; moreover the input difference at group jj is exactly Sj−(d,v)S_j-(d,v), with both calculations including the same previous preloss.

In plain English

With E=∑i≥jC1m∗−i+1eiE=\sum_{i\geq j}C_1^{m_*-i+1}e_i, it suffices to prove the bound when EE is below a small fixed constant. In that regime the clipped prefix errors are below 11, so ∣Si1(y)−dy∣≤(1+dy)ei|S_i^1(y)-d_y|\leq(1+d_y)e_i and ∣Si2(y)−vy∣≤ei|S_i^2(y)-v_y|\leq e_i, later increments are bounded by (1+dy)(ei+ei−1)(1+d_y)(e_i+e_{i-1}) in the first coordinate and ei+ei−1e_i+e_{i-1} in the second, and the input difference at group jj is exactly Sj−(d,v)S_j-(d,v).

Why it's here

If EE is not small, the bounded range of the final row-root outputs already gives the claimed discrepancy bound, so only the small-error case needs real work. This normalization supplies the entrywise error and increment bounds, with the same previous preloss in both calculations, that the later claims use to compare the two computations, including the heavy-entry gate argument and the sentinel Lipschitz bound.
Classified routine:
A standard normalization step: the large-error case follows trivially from bounded output ranges, and in the small-error case the entrywise bounds come directly from unpacking the definitions of the clipped relative errors.

Uses

Nothing else in the paper

Used by

claimMany heavy entries close all gatesclaimSentinel modification gives Lipschitz propagation bound

Sources

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

Phase 2 aligns this node to a Lean declaration.