lemmaroutine

Relative stability at first overflow

At first overflow, root outputs differ from reference by C∑C1m∗−i+1eiC\sum C_1^{m_*-i+1}e_i
propagates per-group errors in the compression bound
Lemma·lem:buf-relative-stability·§8.3 Deterministic comparison arguments

Statement (paper)

At a first overflow in group jj, the discrepancy of final row-root outputs from the stationary reference of Lemma  is at most C∑i≥jC1m∗−i+1ei. C\sum_{i\geq j} C_1^{m_*-i+1}e_i. The constant does not depend on the largest true first entry.

In plain English

At a first overflow in group jj, the final row-root outputs differ from the stationary reference calculation by at most C∑i≥jC1m∗−i+1eiC\sum_{i\geq j} C_1^{m_*-i+1}e_i. The constant CC does not depend on the largest true first entry.

Why it's here

This lemma converts the per-group errors eie_i into a bound on the final row-root discrepancy, with geometric weights C1m∗−i+1C_1^{m_*-i+1}, by comparing against the reference from lem-buf-reference. The proof reduces to small relative errors, then either closes all gates when many entries are heavy or replaces the few heavy entries by sentinels so that the Lipschitz property of lem-buf-update applies. The error propagation bound is used in the integrated compression bound, where the errors are split into mean and noise parts.
Classified routine:
Error-propagation bookkeeping that follows from the Lipschitz and monotonicity properties of the buffer update (lem-buf-update) and the pre-overflow reference bound (lem-buf-reference). It uses a standard geometric accumulation of per-group errors together with a case split on how many entries are heavy.

Uses

lemPre-overflow buffer loss and reference calculationlemBuffer update map: replacement, monotonicity, Lipschitz

Used by

propCompression preserves row error budgetclaimTrue-type overflow mean part via rarityclaimNoise part needs no sum over overflow groups

Inside the proof

claimReduction to small relative prefix errorsclaimMany heavy entries close all gatesclaimSentinel modification gives Lipschitz propagation boundclaimSentinels leave perturbed calculation unchanged

Sources

PaperOpen
Section
§8.3 Deterministic comparison arguments
Page
—
Label
lem:buf-relative-stability
Line
sections/compression.tex:301
Leannot aligned

Phase 2 aligns this node to a Lean declaration.