lemmaroutine

Pre-overflow buffer loss and reference calculation

Before first overflow, loss is ≤ 6∑ρi6\sum\rho_i and a reference run matches roots
stationary reference for relative stability
Lemma·lem:buf-reference·§8.3 Deterministic comparison arguments

Statement (paper)

Let Lj−1=Tj−1−Sj−1L_{j-1}=T_{j-1}-S_{j-1} before the first overflow at jj. Then ∥Lj−1∥∞≤6∑i<jρi\|L_{j-1}\|_\infty\leq6\sum_{i<j}\rho_i, and at every endpoint with dy≥ηd_y\geq\eta, max⁡ν∣Lj−1ν(y)∣≤C∑i<jρiei(y). \max_\nu|L_{j-1}^\nu(y)| \leq C\sum_{i<j}\rho_i e_i(y). Start a reference calculation at the input of group jj with the true array (d,v)+Lj−1(d,v)+L_{j-1}, the same preceding default, and no further increments. Every subsequent compression preserves its relevant row outputs. Their root discrepancy from the true outputs is bounded by C∑i<jρieiC\sum_{i<j}\rho_i e_i.

In plain English

Before the first overflow at group jj, the loss Lj−1=Tj−1−Sj−1L_{j-1}=T_{j-1}-S_{j-1} has sup norm at most 6∑i<jρi6\sum_{i<j}\rho_i, and at endpoints with dy≥ηd_y\geq\eta each coordinate is at most C∑i<jρiei(y)C\sum_{i<j}\rho_i e_i(y). Starting a reference calculation at the input of group jj with the true array (d,v)+Lj−1(d,v)+L_{j-1}, the same preceding default, and no further increments, every later compression preserves its relevant row outputs, and the root outputs differ from the true ones by at most C∑i<jρieiC\sum_{i<j}\rho_i e_i.

Why it's here

This lemma turns the accumulated loss before the first overflow into a fixed, stationary reference computation whose root outputs are within C∑i<jρieiC\sum_{i<j}\rho_i e_i of the true ones. The later stability results at the first overflow and the preloss error bounds compare against this reference, since the loss is controlled in sup norm and endpoint-wise by the ρi\rho_i and eie_i weights.
Classified routine:
Bookkeeping estimate within the paper's own buffered compression scheme: it sums the per-group losses before the first overflow, bounded by the weights ρi\rho_i and eie_i, and sets up a stationary reference run for later comparison. It is a technical step supporting the main derandomization argument, not one of the paper's central new ideas.

Uses

Nothing else in the paper

Used by

lemRelative stability at first overflowclaimSentinel modification gives Lipschitz propagation boundclaimPreloss and no-overflow error bounds

Sources

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

Phase 2 aligns this node to a Lean declaration.