claimroutineinferred_dep

High-rank families detect with probability 3/16

Families of rank ≥ b+2b+2 detect the noise with probability ≥ 3/16
gives the detection property of the lemma
Claim·§3.5 Quotients and enlargement·inside lemLatent alphabet gadget with detecting noise

Statement (paper)

Let G≤V∗G\le\mathcal V^* be any linear subspace with r=dim⁡(G∣K)≥r∗=b+2r=\dim(G|_K)\ge r_*=b+2. Then Pr⁡L[L∗S≠B∗]≤2b−r≤14\Pr_L[L^*S\ne B^*]\le 2^{b-r}\le\frac14, where S=G∣KS=G|_K, and for each remaining copy LL the subspace GLG_L detects with probability at least 1/41/4. Hence Pr⁡a∼μ[there exists g∈G with g(a)≠0]≥34⋅14=316≥18\Pr_{a\sim\mu}[\text{there exists }g\in G\text{ with }g(a)\ne0]\ge\frac34\cdot\frac14=\frac3{16}\ge\frac18, which is Equation , for every ℓ≥b+2\ell\ge b+2.

In plain English

If G≤V∗G\le\mathcal V^* has dim⁡(G∣K)=r≥b+2\dim(G|_K)=r\ge b+2, then for a random injection LL the pullback L∗(G∣K)L^*(G|_K) equals B∗B^* except with probability at most 2b−r≤1/42^{b-r}\le 1/4. For every other copy, GLG_L detects with probability at least 1/41/4, so GG detects under μ\mu with probability at least 3/16≥1/83/16\ge 1/8 (for ℓ≥b+2\ell\ge b+2).

Why it's here

This closes the proof of the parent lemma by verifying the detection property in Equation (latent-detection). A high-rank S=G∣KS=G|_K restricts onto all of B∗B^* for most injections LL, and for those copies the full-lift detection proposition gives probability at least 1/41/4. Combining the 3/43/4 fraction of good copies with this 1/41/4 gives 3/16≥1/83/16\ge 1/8, with the threshold r∗=b+2r_*=b+2 fixed independently of ℓ\ell.
Classified routine:
A direct combination of the full-lift detection proposition with a standard random-injection rank bound: a random linear map pulls back an r-dimensional subspace of K^* onto all of B^* except with probability at most 2^{b-r}, giving 3/4 · 1/4 = 3/16.

Uses

propFull lifts detect the leaf symbolclaimEnlargement by injections gives equivariant map

Used by

Nothing in the paper

Sources

PaperOpen
Section
§3.5 Quotients and enlargement
Page
—
Label
—
Line
sections/02-latent.tex:711
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "High-rank families restrict onto B and detect" rests on prop:latent-full-lift-detection
  • info
    inferred_dep
    outline: "High-rank families restrict onto B and detect" rests on claim-lem-latent-2