claimroutineinferred_dep

Shortened Tanner code has few sparse rows

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

Statement (paper)

The matrix A(0)A^{(0)} obtained by shortening the Tanner code to mm retained edge coordinates and restricting all vertex checks to them has every row with at most dG⩽D0d_G\le D_0 nonzero entries and at most 2qGcG⩽3n2q_Gc_G\le 3n rows. If qG=1q_G=1 then dG=md_G=m and 2cG⩽m/(4B)+2⩽n/4+2⩽3n2c_G\le m/(4B)+2\le n/4+2\le 3n, and if qG>1q_G>1 then dG=D0⩾8Bd_G=D_0\ge 8B and 2qGcG⩽qGdG/(2B)<m/B⩽n2q_Gc_G\le q_Gd_G/(2B)<m/B\le n.

In plain English

The shortened matrix A(0)A^{(0)}, with mm columns and all vertex checks restricted to the retained edge coordinates, has every row with at most dG⩽D0d_G\le D_0 nonzero entries and at most 2qGcG⩽3n2q_Gc_G\le 3n rows.

Why it's here

This is the size and sparsity half of the lemma, complementing the distance bound from the previous claim. It is proved by splitting into cases: if qG=1q_G=1 the graph is trivial and the row count is small directly, and if qG>1q_G>1 then dG=D0d_G=D_0 and the count 2qGcG⩽qGdG/(2B)<m/B⩽n2q_Gc_G\le q_Gd_G/(2B)<m/B\le n gives the bound.
Classified routine:
This is direct parameter bookkeeping: a case split on qGq_G that counts rows and row weights of the shortened Tanner code from the chosen graph and local-code parameters. No new idea is involved.

Uses

claimTanner code nonzero words have large weight

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Shortened code: row count and sparsity" rests on claim-lem-sparse-checks-5