claimroutineinferred_dep

Matrix chart lift has Grassmann retention

Graph-subspace lift has Grassmann retention at least η/4\eta/4
moves the fiber into the Grassmann setting
Claim·§5.1 The inverse shortcode theorem·inside thmInverse shortcode theorem

Statement (paper)

Let S⊆Mat⁡ℓ,mS\subseteq \operatorname{Mat}_{\ell,m} be a set whose retention under the matrix step is at least η/2\eta/2 conditional on both perturbation factors being nonzero, and let S~={LM:M∈S}⊆C\widetilde S=\{L_M:M\in S\}\subseteq\mathcal C, where LM={(x,M⊤x):x∈F2ℓ}⊆E=F2ℓ⊕F2mL_M=\{(x,M^\top x):x\in\F_2^\ell\}\subseteq E=\F_2^\ell\oplus\F_2^m. Then S~\widetilde S has Grassmann retention at least η/4\eta/4.

In plain English

If a set SS of matrices has retention at least η/2\eta/2 under the step M↦M+al⊤M\mapsto M+al^\top (conditioned on a,la,l both nonzero), then the set S~={LM:M∈S}\widetilde S=\{L_M:M\in S\} of graph subspaces LM={(x,M⊤x)}L_M=\{(x,M^\top x)\} has Grassmann retention at least η/4\eta/4.

Why it's here

This transfers the fiber's retention from the matrix setting, obtained in the previous claim, to the Grassmann setting of subspaces in E=F2ℓ⊕F2mE=\F_2^\ell\oplus\F_2^m where the expansion theorem applies. The loss from η/2\eta/2 to η/4\eta/4 is the price of this translation, and it sets the parameter ζ=η/4\zeta=\eta/4 used in the next claim to get a row-column slice.
Classified routine:
This is a direct translation step inside the inverse shortcode theorem. It identifies matrices with graph subspaces LML_M in the Grassmannian, so the matrix step M↦M+al⊤M\mapsto M+al^\top corresponds to the Grassmann random walk. It is a standard chart computation, as in the Khot–Minzer–Safra Grassmann expansion work, with a constant-factor loss.

Uses

claimSome fiber has retention at least eta/2

Used by

claimExpansion interval yields row-column slice

Sources

PaperOpen
Section
§5.1 The inverse shortcode theorem
Page
—
Label
—
Line
sections/04-matrix.tex:88
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Matrix chart lift has Grassmann retention eta/4" rests on claim-thm-shortcode-1