lemmaroutine

Pilot and actual matrices are bounded

Pilot and actual matrices have row sums ≤ ii, entries ≤ ifif, monotone
shared size and support bounds for the hierarchy lemmas
Lemma·lem:hier-pilot-bounds·§4.2 A finite pilot chooses the column multiplier

Statement (paper)

All pilot and actual inputs and corrections are nonnegative and strictly forward. For 1≤i≤k∗1\leq i\leq k_*, Gi1, E^i1, Gi′1, Ei1≤i1,Gi(x,y), E^i(x,y), Gi′(x,y), Ei(x,y)≤if.\begin{aligned} G_i\mathbf 1,\ \widehat E_i\mathbf 1, \ G'_i\mathbf 1,\ E_i\mathbf 1&\leq i\mathbf 1,\\ G_i(x,y),\ \widehat E_i(x,y), \ G'_i(x,y),\ E_i(x,y)&\leq if. \end{aligned} Moreover, Ei−1≤Ei≤E^i,Gi′≤Gi. E_{i-1}\leq E_i\leq\widehat E_i, \qquad G'_i\leq G_i. The row and column supports of every matrix in this statement are contained in R(C)\mathcal R(C) and T(C)\mathcal T(C), respectively.

In plain English

For 1≤i≤k∗1\leq i\leq k_*, the pilot and actual inputs Gi,Gi′G_i,G'_i and corrections E^i,Ei\widehat E_i,E_i are nonnegative and strictly forward, with row sums at most ii and every entry at most ifif. The corrections are monotone, Ei−1≤Ei≤E^iE_{i-1}\leq E_i\leq\widehat E_i, and Gi′≤GiG'_i\leq G_i. All row and column supports lie in R(C)\mathcal R(C) and T(C)\mathcal T(C).

Why it's here

This lemma collects the uniform size, monotonicity and support bounds on the pilot and actual matrices at every level i≤k∗i\leq k_*. The later column-test, residual, copy-step and fine-product estimates cite these bounds instead of re-deriving them, so the row-sum and entry caps (ii and ifif) and the ordering of corrections are available throughout.
Classified routine:
Bookkeeping lemma: nonnegativity, row-sum and entry caps, monotonicity and support bounds follow by induction on the level ii from the definitions of the pilot and actual matrices. It collects these bounds for later estimates rather than introducing a new idea.

Uses

Nothing else in the paper

Used by

lemColumn test separates heavy and light columnslemResidual matrix D is bounded and dominatingpropOne-stage copy step reduces density and active verticeslemCorrection-bin products have bounded size

Sources

PaperOpen
Section
§4.2 A finite pilot chooses the column multiplier
Page
—
Label
lem:hier-pilot-bounds
Line
sections/hierarchy.tex:263
Leannot aligned

Phase 2 aligns this node to a Lean declaration.