lemmaroutine

Sparse parity checks force large supports

Lemma·lem:sparse-checks·§6.1 Initial tests that exclude small violation sets

Statement (paper)

Let n,m,Bn,m,B be positive integers with m⩽Bnm\le Bn, and put μ=⌊log⁡2m⌋+1,P=20000B2μ2,D0=320000B2μ3. \mu=\lfloor\log_2 m\rfloor+1,\qquad P=20000B^2\mu^2,\qquad D_0=320000B^2\mu^3. There is a deterministic construction of a binary matrix A(0)A^{(0)} with mm columns and at most 3n3n rows such that every row has at most D0D_0 nonzero entries and z∈{0,1}m∖{0⃗},A(0)z=0⃗(mod2)⟹∣supp⁡z∣⩾m/P. z\in\{0,1\}^m\setminus\{\vec{0}\},\quad A^{(0)}z=\vec{0}\pmod2 \quad\Longrightarrow\quad |\operatorname{supp}z|\ge m/P. The construction uses exp⁡(poly⁡(B,log⁡(m+2)))\exp(\poly(B,\log(m+2))) bit operations and poly⁡(n,m,B)\poly(n,m,B) bits of working space.

In plain English

For m⩽Bnm\le Bn, one can deterministically build a binary matrix A(0)A^{(0)} with mm columns, at most 3n3n rows, and at most D0=320000B2μ3D_0=320000B^2\mu^3 ones per row, such that every nonzero zz with A(0)z=0(mod2)A^{(0)}z=0 \pmod 2 has support size at least m/Pm/P, where P=20000B2μ2P=20000B^2\mu^2 and μ=⌊log⁡2m⌋+1\mu=\lfloor\log_2 m\rfloor+1. The construction costs exp⁡(poly⁡(B,log⁡(m+2)))\exp(\poly(B,\log(m+2))) bit operations and poly⁡(n,m,B)\poly(n,m,B) space.

Why it's here

This supplies the initial sparse parity checks that exclude every small violation set, since all nonzero kernel vectors are heavy. It is built as a shortened Tanner code on a small-bias Cayley expander with a brute-force local code at each vertex, and later lemmas (the greedy hashes and the leaf counts in the main theorem) start from it.
Classified routine:
A standard Tanner-code / LDPC construction with linear minimum distance, in the style of Sipser–Spielman expander codes. It uses an explicit small-bias Cayley-graph expander and brute-forced local codes, shortened to the given parameters, so it is a parameter-tracking adaptation of known expander-code distance bounds.

Uses

Nothing else in the paper

Used by

thmSubexponential deterministic k-CNF model countinglemGreedy appended rows give exact countclaimLeaf counts via parity rows and queries

Inside the proof

claimBipartite Cayley graph on shiftsclaimSmall-bias shifts exist and can be foundclaimExpander mixing bound from small biasclaimExistence of local code with large distanceclaimTanner code nonzero words have large weightclaimShortened Tanner code has few sparse rows

Sources

PaperOpen
Section
§6.1 Initial tests that exclude small violation sets
Page
—
Label
lem:sparse-checks
Line
main_full_version.tex:3261
Leannot aligned

Phase 2 aligns this node to a Lean declaration.