lemmaroutine

Escape contribution charged to child discrepancies

Escape contribution is at most 2−p∑2Cdλm2^{-p}\sum 2^{Cd}\lambda_m in child discrepancies
escape charge in the coupling recurrence
Lemma·lem:fp-escape·§9.3 Witness envelopes and escaped paths

Statement (paper)

Suppose actual--clean child discrepancies at budget mm have their prescribed metric bounds 2−pmλm2^{-p_m}\lambda_m. The contribution of Fx\mathcal F_x to any bounded final pre-incoming row output has norm at most 2−p∑d≤2h∗m∈Ib, m≤M−d2Cdλm, 2^{-p}\sum_{\substack{d\le2h_*\\m\in\mathcal I_b,\ m\le M-d}} 2^{C d}\lambda_m, where the sum includes the finitely many dependency types and their descriptor multiplicities in its constant CC. Equivalently, one may use the maximum of λm\lambda_m over the children of each slack group and increase CC.

In plain English

If actual–clean child discrepancies at each budget mm obey their prescribed bounds 2−pmλm2^{-p_m}\lambda_m, then the contribution of the escape event Fx\mathcal F_x to any bounded final pre-incoming row output has norm at most 2−p∑2Cdλm2^{-p}\sum 2^{Cd}\lambda_m. The sum runs over slack d≤2h∗d\le 2h_* and budgets m∈Ibm\in\mathcal I_b with m≤M−dm\le M-d, and CC absorbs the finitely many dependency types and descriptor multiplicities.

Why it's here

The lemma turns the combinatorial event that an actual endpoint leaves the witness envelope into a weighted sum of child discrepancies. It does so by bounding the output error by the escape indicator, bounding that indicator by witness discrepancies at offending ports, and charging each port to its child's metric bound, with the scale and reset costs absorbed by the precision gain. The resulting escape charge is one of the terms used in the block coupling recurrence of the later proposition.
Classified routine:
This is a bookkeeping step inside the paper's own coupling recurrence. It bounds the escape indicator by witness discrepancies at offending ports and charges each port to its child's metric bound, using the earlier variant expansion (lem-env-variants) and the raw difference bounds (lem-est-raw-difference).

Uses

lemWalk variants avoid storing endpointslemRaw difference bounds at slack-d groups

Used by

propActual runs stay close to clean runsclaimCoupling recurrence from child charges

Inside the proof

claimEscape indicator bounded by witness discrepancyclaimOutput error dominated by row-failure indicatorclaimRight-factor charge via actual incoming capclaimDirect and left offending ports chargedclaimPrecision gain absorbs scale and reset costs

Sources

PaperOpen
Section
§9.3 Witness envelopes and escaped paths
Page
—
Label
lem:fp-escape
Line
sections/fingerprints.tex:351
Leannot aligned

Phase 2 aligns this node to a Lean declaration.