claimroutineinferred_dep

Tanner code nonzero words have large weight

Claim·§6.1 Initial tests that exclude small violation sets·inside lemSparse parity checks force large supports

Statement (paper)

Every nonzero edge word accepted by all the vertex checks (the Tanner code with local code Cloc=ker⁡F2AlocC_{\mathrm{loc}}=\ker_{\mathbb F_2}A_{\mathrm{loc}} imposed at every vertex on both sides) has weight h′h' at least δ(δ−ε)qGdG=qGdG20000B2μ2⩾m/P\delta(\delta-\varepsilon)q_Gd_G=\frac{q_Gd_G}{20000B^2\mu^2}\ge m/P.

In plain English

Any nonzero edge word that satisfies every vertex check of the Tanner code, with local code ker⁡Aloc\ker A_{\mathrm{loc}} at each vertex on both sides, has weight h′h' at least δ(δ−ε)qGdG=qGdG20000B2μ2⩾m/P\delta(\delta-\varepsilon)q_Gd_G=\frac{q_Gd_G}{20000B^2\mu^2}\ge m/P.

Why it's here

This is the distance bound for the Tanner code, which the shortening step needs to get the m/Pm/P lower bound on the support. The idea is that, at each vertex touched by the word, the local code's minimum distance (from the local-code claim) forces at least δdG\delta d_G incident support edges. A small support would therefore span too many edges inside a small vertex neighbourhood, which the expander mixing bound forbids.
Classified routine:
This is the standard Sipser–Spielman / Zémor distance bound for Tanner codes on expanders, giving distance at least δ(δ−ε)\delta(\delta-\varepsilon) times the number of edges. It follows from the expander mixing bound and the local-code distance claims, with parameters plugged in.

Uses

claimExpander mixing bound from small biasclaimExistence of local code with large distance

Used by

claimShortened Tanner code has few sparse rows

Sources

PaperOpen
Section
§6.1 Initial tests that exclude small violation sets
Page
—
Label
—
Line
main_full_version.tex:3392
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Tanner code nonzero words have large weight" rests on claim-lem-sparse-checks-3
  • info
    inferred_dep
    outline: "Tanner code nonzero words have large weight" rests on claim-lem-sparse-checks-4