propositionnovel

Compression preserves row error budget

Compressed rows are within Cbufc∗2−pC_{\rm buf}c_*2^{-p} of the true outputs in ss-norm
compression error term in the error reserve
Proposition·prop:buf-error·§8.4 Charging overflow events

Statement (paper)

For fixed sufficiently large c1c_1, then c2c_2, and sufficiently rapid prefix-noise decay KnK_n, compression preserves the prescribed row error budget, with an arbitrarily small fixed coefficient when c∗c_* is chosen small. More precisely, (∫∑H∈H∑y∣H(Tm∗;y)1/s−H(d,v;y)1/s∣s dμ)1/s≤Cbufc∗2−p, \left(\int\sum_{H\in\mathcal H}\sum_y |H(T_{m_*};y)^{1/s}-H(d,v;y)^{1/s}|^s\,d\mu\right)^{1/s} \leq C_{\mathrm{buf}}c_*2^{-p}, where CbufC_{\mathrm{buf}} is fixed, independent of the number of groups, row width, and requested precision.

In plain English

With c1c_1 fixed large, then c2c_2, then fast enough prefix-noise decay KnK_n, the ss-norm of the total discrepancy between the true row outputs H(Tm∗;y)1/sH(T_{m_*};y)^{1/s} and the compressed outputs H(d,v;y)1/sH(d,v;y)^{1/s} is at most Cbufc∗2−pC_{\mathrm{buf}}c_*2^{-p}. The constant CbufC_{\mathrm{buf}} is independent of the number of groups, row width and precision, so the coefficient can be made arbitrarily small by choosing c∗c_* small.

Why it's here

This is the error-accounting result for buffer compression: it shows that overflow events, however they arise, cost only a small multiple of the target error 2−p2^{-p}. The proof splits the error into preloss, no-overflow, false-type overflow and true-type overflow (mean and noise) parts, bounds each using relative stability and rarity, and then fixes c1c_1, c2c_2, KnK_n so all the series converge before c∗c_* is chosen.
Classified novel:
This is the paper's central error-accounting step for its new buffer-compression derandomization scheme. It charges overflow events via relative stability and rarity, and no prior derandomization (Nisan, Saks–Zhou) gives a precision-independent budget of this form.

Uses

lemRelative stability at first overflow

Used by

propError reserve after compression and clamping

Inside the proof

claimRow sup bounds convert to summed powersclaimPreloss and no-overflow error boundsclaimFalse-type first overflow charge boundclaimTrue-type overflow mean part via rarityclaimNoise part needs no sum over overflow groupsclaimFloor and capacity exponents make sums converge

Sources

PaperOpen
Section
§8.4 Charging overflow events
Page
—
Label
prop:buf-error
Line
sections/compression.tex:469
Leannot aligned

Phase 2 aligns this node to a Lean declaration.