lemmaroutine

Swap matrix with few rows fixes M_0

Lemma·lem:swaps-matrix·§4.2 The matrices M_0 and C^B

Statement (paper)

For

\mathcal B

\mathcal I

and

M_0

as above, there is a matrix

C^{\mathcal B}\in\{0,1,-1\}^{[c_{\mathcal B}]\times\mathcal B}

such that

c_{\mathcal B}\le D\Pr[W\notin\mathcal I],\qquad W\sim\operatorname{Bin}\!\left(Q,\frac{r-1}{2r}\right),

and

M_0\xi=\xi

for every

\xi\in\ker C^{\mathcal B}

In plain English

There is a matrix

C^{\mathcal B}

with entries in

\{0,1,-1\}

, indexed by

[c_{\mathcal B}]\times\mathcal B

, whose number of rows satisfies

c_{\mathcal B}\le D\Pr[W\notin\mathcal I]

for

W\sim\operatorname{Bin}(Q,\frac{r-1}{2r})

. Every vector

\xi

in the kernel of

C^{\mathcal B}

satisfies

M_0\xi=\xi

Why it's here

This lemma turns the condition that

M_0

fixes a vector into a small set of linear constraints with

0,\pm1

coefficients. The row count is bounded by a binomial tail probability, so the constraints stay few. The later lemmas on the row forms (Lemma 4.3) and row coefficients (Lemma 4.6) work with these rows.

Classified routine:

This appears to be a direct linear-algebra construction. If

M_0

acts by swapping coordinates, its fixed vectors are cut out by

\pm1

difference constraints

\xi_b-\xi_{\sigma(b)}=0

, one per moved coordinate. Counting the coordinates outside

\mathcal I

then gives the binomial-tail row bound. That is bookkeeping specific to the paper's setup rather than a new idea, though the reading of

M_0

as a swap matrix is inferred from the node's name, not shown.

Uses

Nothing else in the paper

Used by

lemPolynomial rows vanish on off-block vectorslemRow coefficients are bounded and constructiblelemLayout data is efficiently constructible

Sources

PaperOpen

Section: §4.2 The matrices M_0 and C^B
Page: —
Label: lem:swaps-matrix
Line: main_full_version.tex:2232

Leannot aligned

Phase 2 aligns this node to a Lean declaration.