propositionroutine

Error reserve after compression and clamping

Compression, clamping and assembly use only half the error budget

C_b2^{-p}

clean-block error reserve for the coupling induction

Proposition·prop:est-clean·§8.6 The error reserve with exact endpoint grouping

Statement (paper)

Suppose the earlier row and vector tasks have error bound

C_b2^{-p'}

and the support and common-parameter properties of the atom section. Use exact comparisons locally, and vary every variable on which the sample terms depend. After compression and the range clamps above, all active row outputs, pre-incoming scores, and witnesses have error at most

(C_b/2)2^{-p}

. The same holds for the final clipped vectors and the assembled correction outputs, after choosing the fixed constants in the order specified below.

In plain English

Assuming earlier row and vector tasks have error at most

C_b2^{-p'}

and the atom-section support and common-parameter properties hold, then after compression and range clamps, all active row outputs, pre-incoming scores and witnesses have error at most

(C_b/2)2^{-p}

. The same bound holds for the final clipped vectors and assembled correction outputs, once the fixed constants are chosen in the specified order.

Why it's here

This is where the error budget is closed: it shows that compression, clamping and assembly together use only half of the allowed error

C_b2^{-p}

, leaving a reserve. It combines the compression error bound (prop-buf-error), the mean/noise prefix estimates (lem-est-prefix), the fact that clamps do not worsen comparisons (lem-buf-clamping), and the assembly of row and cutoff discrepancies (lem-atom-assembly). The block-coupling and estimator error bounds in Section 9 then rely on it for the clean-block estimates.

Classified routine:

This step closes the error budget by combining the paper's earlier compression bound (prop-buf-error), the prefix estimates (lem-est-prefix), the clamping lemma (lem-buf-clamping) and the assembly lemma (lem-atom-assembly). The work is bookkeeping over the order in which the constants are chosen, so no new idea is introduced here.

Uses

propCompression preserves row error budgetlemMean prefixes small, noise prefixes tinylemClamping preserves final row functionslemAssembly of row and cutoff discrepancies

Used by

lemClean calculation is independent of the saltpropActual runs stay close to clean runsthmFixed-precision estimators meet error boundclaimClean active tasks meet target bounds

Sources

PaperOpen

Section: §8.6 The error reserve with exact endpoint grouping
Page: —
Label: prop:est-clean
Line: sections/compression.tex:652

Leannot aligned

Phase 2 aligns this node to a Lean declaration.