claimroutineinferred_dep

Expansion interval yields row-column slice

Expansion gives a row-column slice where ff is constant on an α\alpha fraction
finishes the shortcode theorem
Claim·§5.1 The inverse shortcode theorem·inside thmInverse shortcode theorem

Statement (paper)

Applying the expansion theorem with ζ=η/4\zeta=\eta/4 to S~\widetilde S yields an interval whose intersection with C\mathcal C is a slice S\mathcal S of the required form, defined by the equations di⊤M=si⊤d_i^\top M=s_i^\top and Mqj=tjMq_j=t_j with nr,nc≤rsn_r,n_c\le r_{\rm s} equations in total, such that ff equals the value uu defining SS on at least an α\alpha fraction of S\mathcal S. Hence Pr⁡M∣S[f(M)=Mz+u]≥α\Pr_{M\mid\mathcal S}[f(M)=Mz+u]\ge\alpha with z=0z=0.

In plain English

Applying the expansion theorem with ζ=η/4\zeta=\eta/4 to the lifted set S~\widetilde S gives an interval whose intersection with the chart C\mathcal C is a slice S\mathcal S cut out by at most rsr_{\rm s} row and column equations di⊤M=si⊤d_i^\top M=s_i^\top and Mqj=tjMq_j=t_j. On this slice ff equals its value uu on at least an α\alpha fraction, so Pr⁡M∣S[f(M)=Mz+u]≥α\Pr_{M\mid\mathcal S}[f(M)=Mz+u]\ge\alpha with z=0z=0.

Why it's here

This finishes the proof of the shortcode theorem. The previous claim shows S~\widetilde S has Grassmann retention at least η/4\eta/4, which is the hypothesis the expansion theorem needs. Its dense interval, restricted to the matrix chart, becomes a row-column slice on which ff is constant on an α\alpha fraction. Taking z=0z=0 gives the affine form Mz+uMz+u with uu constant, which is the conclusion of the theorem.}
Classified routine:
A direct application of the Grassmann expansion theorem (Khot–Minzer–Safra) to the lifted set from the previous claim. It translates the dense interval back to the matrix chart as a row-column slice, and choosing z=0 is bookkeeping.

Uses

claimMatrix chart lift has Grassmann retention

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Expansion interval yields row-column slice" rests on claim-thm-shortcode-2