lemmaroutineinferred_dep

Column test separates heavy and light columns

Column test flags heavy columns and certifies light ones when multiplier is positive
keeps heavy columns out of the copy matrix
Lemma·lem:hier-column-test·§4.2 A finite pilot chooses the column multiplier

Statement (paper)

Let Drow=1+Cpairk∗/η−. D_{\rm row}=1+C_{\rm pair}k_*/\eta_-. Choose the integer K≥160DrowK\geq160D_{\rm row}, increasing it if necessary for the other finitely many row-gate estimates. For any fixed positive integer JJ, choose R∗≥cπ−1max⁡(4J,40Cvar). R_*\geq c_\pi^{-1}\max(4J,40C_{\rm var}). Then the pilot has the following properties. \begin{enumerate} \item If #{x:Gi(x,y)≥δ1f}>R∗/f\#\{x:G_i(x,y)\geq\delta_1f\}>R_*/f, then Ui(y)≥19/20>9/10U_i(y)\geq19/20>9/10. \item If Ui(y)>1/4U_i(y)>1/4, then #{x:Gi(x,y)>δ0f}>J4Cπf. \#\{x:G_i(x,y)>\delta_0f\} >\frac{J}{4C_\pi f}. \item For any pilot correction with multiplier g^i(y)>0\widehat g_i(y)>0, #{x:Gi(x,y)≥δ1f}≤R∗/f. \#\{x:G_i(x,y)\geq\delta_1f\}\leq R_*/f. For every actual correction, g(y)>0g(y)>0 implies #{x:Gi′(x,y)≥δ1f}≤R∗/f. \#\{x:G'_i(x,y)\geq\delta_1f\}\leq R_*/f. \end{enumerate}

In plain English

With K≥160DrowK\geq160D_{\rm row} and R∗≥cπ−1max⁡(4J,40Cvar)R_*\geq c_\pi^{-1}\max(4J,40C_{\rm var}), the column test Ui(y)U_i(y) behaves as a threshold detector. A column with more than R∗/fR_*/f entries Gi(x,y)≥δ1fG_i(x,y)\geq\delta_1f gives Ui(y)≥19/20U_i(y)\geq19/20, and Ui(y)>1/4U_i(y)>1/4 forces more than J/(4Cπf)J/(4C_\pi f) entries above δ0f\delta_0f. Whenever the correction multiplier is positive, the count of entries ≥δ1f\geq\delta_1f in that column is at most R∗/fR_*/f, for both pilot and actual matrices.

Why it's here

This turns the finite pilot's random test into a deterministic dichotomy: very heavy columns are flagged with high probability, flagged columns are genuinely heavy, and a positive multiplier certifies that the column is not too heavy. The proof uses the entry and row-sum bounds from the pilot-bounds lemma together with the retention estimates from the rank-channel lemma (pair inflation and variance bounds). The one-stage copy-step proposition then uses these properties to control the density and active counts.
Classified routine:
A threshold-detector estimate that follows from the pilot-bounds lemma and the rank-channel retention estimates (pair inflation, variance bounds) by a standard second-moment/Chebyshev-type calculation and choice of constants.

Uses

lemPilot and actual matrices are boundedlemRank channel retention estimates

Used by

propOne-stage copy step reduces density and active vertices

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The proof (hierarchy.tex 355, 375-376) applies Equations hier-sampling-pair and hier-sampling-tail. The text introduces these as "The consequences of Lemma  needed here" (lines 185-195).