lemmaroutineinferred_dep

Residual matrix D is bounded and dominating

Residual DD is substochastic, small on good columns, and dominates C+E+ECC+E+EC
single matrix bounding all terms in the copy step
Lemma·lem:hier-residual·§4.3 The finite residual

Statement (paper)

For the k∗k_* chosen in Lemma , put K∗=k∗+1,εgood=θ2+q−1/32<q−1/16,cdom=θ1/(2k∗). K_*=k_*+1,\qquad \varepsilon_{\rm good}=\theta_2+q^{-1}/32<q^{-1}/16, \qquad c_{\rm dom}=\theta_1/(2k_*). The matrix DD in Equation  is nonnegative, strictly forward, and substochastic. Its entries satisfy D(x,y)≤K∗f,g(y)=1 ⟹ D(x,y)≤εgoodf. D(x,y)\leq K_*f, \qquad g(y)=1\ \Longrightarrow\ D(x,y)\leq\varepsilon_{\rm good}f. Furthermore, D≥cdom(C+E+EC). D\geq c_{\rm dom}(C+E+EC). Thus every unsigned term in C−E+ECC-E+EC is bounded by a fixed multiple of DD. In the formulas Gi=C+E^i−1CG_i=C+\widehat E_{i-1}C and Gi′=C+Ei−1CG'_i=C+E_{i-1}C, each unsigned term is bounded by the corresponding input itself. Moreover, R(D)⊆R(C)\mathcal R(D)\subseteq\mathcal R(C) and T(D)⊆T(C)\mathcal T(D)\subseteq\mathcal T(C).

In plain English

The residual matrix DD is nonnegative, strictly forward and substochastic, with entries at most K∗fK_*f (where K∗=k∗+1K_*=k_*+1) and at most εgoodf\varepsilon_{\rm good}f on columns yy with g(y)=1g(y)=1, where εgood<q−1/16\varepsilon_{\rm good}<q^{-1}/16. It also dominates cdom(C+E+EC)c_{\rm dom}(C+E+EC) with cdom=θ1/(2k∗)c_{\rm dom}=\theta_1/(2k_*), and its row and column supports lie inside R(C)\mathcal R(C) and T(C)\mathcal T(C).

Why it's here

This lemma packages the finite residual into a single matrix DD with uniform size, good-column and domination bounds. Later steps such as the copy-step proposition can then control every unsigned term of C−E+ECC-E+EC, and the inputs GiG_i, Gi′G'_i, by a fixed multiple of DD. The entry bounds come from the pilot bounds on Gi,Gi′,E^i,EiG_i,G'_i,\widehat E_i,E_i, and the smallness εgood\varepsilon_{\rm good} comes from the factorial convergence of the fixed-point iteration at the chosen k∗k_*.
Classified routine:
Direct bookkeeping consequence of the pilot bounds (lem-hier-pilot-bounds) and the factorial convergence at the chosen k_* (lem-hier-fixed-point): D is defined as a sum of those bounded nonnegative forward matrices, so the entry, good-column and domination bounds follow by summing termwise.

Uses

lemPilot and actual matrices are boundedlemFixed point with factorial convergence

Used by

propOne-stage copy step reduces density and active vertices

Sources

PaperOpen
Section
§4.3 The finite residual
Page
—
Label
lem:hier-residual
Line
sections/hierarchy.tex:411
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The proof of lem:hier-residual (hierarchy.tex 471-479) uses "the fixed point with this same multiplier g" and "Equation  gives Δ(x,y)≤q^{-1}f/32". Both come from Lemma 4.1, and the statement also cites the k_* chosen there, but no edge exists.