lemmaroutine

Clamping preserves final row functions

Clamping to a bounded range leaves final row functions unchanged
lets clamped values be treated as bounded in comparisons
Lemma·lem:buf-clamping·§8.5 Bounding numerical ranges

Statement (paper)

For fixed common increments satisfying Equation , these clamps do not change the final relevant row functions. Each clamp is sup-norm nonexpansive, so in comparisons of two calculations it preserves the uniform Lipschitz propagation bound. The analogous assertion holds for vector sums clipped beyond their final sensitivity range and all remaining additive variation.

In plain English

When the common increments satisfy the stated margin condition, clamping intermediate values to a bounded range leaves the final relevant row functions unchanged. Each clamp is nonexpansive in sup-norm, so the uniform Lipschitz propagation bound still holds when comparing two calculations. The same holds for vector sums clipped beyond their final sensitivity range and remaining additive variation.

Why it's here

This lets the paper bound the numerical range of intermediate quantities without changing the computed result or worsening error propagation. Later error-reserve and cost arguments, such as the error reserve with exact endpoint grouping, can therefore treat clamped values as bounded without a loss in the comparison estimates.
Classified routine:
Elementary bookkeeping: clamping to an interval is a 1-Lipschitz (sup-norm nonexpansive) map and is the identity on values already inside the margin, so the final row functions and the Lipschitz error propagation bounds are preserved.

Uses

Nothing else in the paper

Used by

propError reserve after compression and clampinglemDirect collision charge boundlemEstimator recipes have regenerable records and bounded controlclaimPropagated clean height has small row normclaimRanks, compression and list selection

Sources

PaperOpen
Section
§8.5 Bounding numerical ranges
Page
—
Label
lem:buf-clamping
Line
sections/compression.tex:581
Leannot aligned

Phase 2 aligns this node to a Lean declaration.