claimroutineinferred_dep

Good advice mass lower bound

Good advice has probability ≥ 10η22−ℓrs=g010\eta^2 2^{-\ell r_{\rm s}}=g_0
gives the lemma's probability bound
Claim·§5.4 Obtaining many useful row fibers·inside lemGood row advice is common and gives short answer sets

Statement (paper)

The set BB of matrices satisfies Pr⁡[B]≥η\Pr[B]\ge\eta at each such fixed (U,T)(U,T). Hence, for each of the at least 10η10\eta pairs (U,T)(U,T) supplied by Lemma , the probability over A,MA,M that (U,T,A,AM)(U,T,A,AM) is good is at least η2−ℓrs\eta2^{-\ell r_{\rm s}}, and therefore Pr⁡U,T,A,M[(U,T,A,AM) is good]≥10η2 2−ℓrs=g0\Pr_{U,T,A,M}[(U,T,A,AM)\text{ is good}]\ge 10\eta^2\,2^{-\ell r_{\rm s}}=g_0.

In plain English

For each of the at least 10η10\eta fraction of pairs (U,T)(U,T) from the spectral lemma, the set BB of matrices has probability at least η\eta, so (U,T,A,AM)(U,T,A,AM) is good with probability at least η2−ℓrs\eta 2^{-\ell r_{\rm s}}. Averaging over (U,T)(U,T) gives Pr⁡[(U,T,A,AM) is good]≥10η22−ℓrs=g0\Pr[(U,T,A,AM)\text{ is good}]\ge 10\eta^2 2^{-\ell r_{\rm s}}=g_0.

Why it's here

This closes the lemma's probability bound. The previous claim gives Pr⁡[B]≥η\Pr[B]\ge\eta at each fixed good pair (U,T)(U,T) by the shortcode contradiction. Choosing AA costs a factor 2−ℓrs2^{-\ell r_{\rm s}}, and the 10η10\eta fraction of pairs from the matrix-spectral lemma supplies the remaining factor 10η10\eta.
Classified routine:
A direct averaging calculation that multiplies the per-pair bound Pr⁡[B]≥η\Pr[B]\ge\eta from the previous claim by the 2−ℓrs2^{-\ell r_{\rm s}} cost of choosing AA. It then averages over the 10η10\eta fraction of pairs (U,T)(U,T) supplied by lem-matrix-spectral.

Uses

lemMatrix test implies surrogate acceptance boundclaimShortcode contradiction forces large good set

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.4 Obtaining many useful row fibers
Page
—
Label
—
Line
sections/04-matrix.tex:407
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Lower bound g_0 on good advice mass" rests on claim-lem-good-row-advice-3