lemmaroutineinferred_dep

Matrix test implies surrogate acceptance bound

Passing the test gives rank-one invariance probability ≥ 0.9⋅2−r∗0.9\cdot 2^{-r_*}
supplies good (U,T)(U,T) pairs to the good-advice lemma
Lemma·lem:matrix-spectral·§5.3 Comparing the two matrix perturbations

Statement (paper)

If the table family passes Equation  with probability at least 0.990.99, then EU,TPr⁡M,a,l[FU(M,T)=FU(M+al⊤,T)]≥0.9 2−r∗, \E_{U,T}\Pr_{M,a,l} [F_U(M,T)=F_U(M+a l^\top,T)] \ge 0.9\,2^{-r_*}, where aa is uniform in KK and the other matrix and vector samples are uniform in their respective spaces. Consequently at least 10η10\eta of the pairs (U,T)(U,T) have the inner probability at least 4η4\eta.

In plain English

If the table family passes the matrix test with probability at least 0.990.99, then averaging over U,TU,T, the probability over M,a,lM,a,l that FU(M,T)=FU(M+al⊤,T)F_U(M,T)=F_U(M+al^\top,T) is at least 0.9⋅2−r∗0.9\cdot 2^{-r_*}, where aa is uniform in KK. Consequently, at least a 10η10\eta fraction of pairs (U,T)(U,T) have this inner probability at least 4η4\eta.

Why it's here

This turns passing the matrix test into a quantitative statement that a rank-one perturbation al⊤al^\top of the matrix rarely changes the table's output. The bound 2−r∗2^{-r_*} uses the threshold r∗r_* from the latent gadget lemma, which is independent of ℓ\ell. The final averaging step gives a large set of good pairs (U,T)(U,T), which the good-row-advice lemma and its lower bound on good advice mass then use.
Classified routine:
The bound is a direct consequence of the matrix-test acceptance probability combined with the detecting-noise property from the latent gadget lemma (threshold r∗r_*). The final step is a standard Markov-type averaging argument over pairs (U,T)(U,T).

Uses

lemLatent alphabet gadget with detecting noise

Used by

lemGood row advice is common and gives short answer setsclaimGood advice mass lower bound

Sources

PaperOpen
Section
§5.3 Comparing the two matrix perturbations
Page
—
Label
lem:matrix-spectral
Line
sections/04-matrix.tex:244
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    the proof refers to "the ordinary shortcode equality tests" at fixed (U,T), which are the tests of the inverse shortcode theorem