claimroutine

Existence of local code with large distance

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

Statement (paper)

With

c_G=\lceil d_G/(8B)\rceil

and

\delta=1/(100B\mu)

, there exists a binary matrix

A_{\mathrm{loc}}

with

c_G

rows and

d_G

columns such that every nonzero word in its kernel modulo

2

has weight at least

\delta d_G

. Such a matrix can be found by enumerating all

2^{c_Gd_G}

binary matrices and testing all words of weight less than

\delta d_G

, using

\exp(\poly(B,\log(m+2)))

bit operations.

In plain English

For

c_G=\lceil d_G/(8B)\rceil

and

\delta=1/(100B\mu)

, there is a binary

c_G\times d_G

matrix

A_{\mathrm{loc}}

whose nonzero kernel words mod 2 all have weight at least

\delta d_G

. It can be found by brute-force search over all such matrices within

\exp(\poly(B,\log(m+2)))

bit operations.

Why it's here

This supplies the small local code placed at every vertex of the Tanner-code construction, whose large minimum distance is what the next claim uses to show nonzero Tanner codewords are heavy. Since

d_G

is only polylogarithmic in size, exhaustive search over all

2^{c_Gd_G}

matrices keeps the construction deterministic within the stated time budget.

Classified routine:

Gilbert–Varshamov-type counting argument (random parity-check matrices give codes of linear distance) combined with brute-force search over small matrices, as in standard Tanner/expander code constructions (Sipser–Spielman 1996).

Uses

Nothing else in the paper

Used by

claimTanner code nonzero words have large weight

Sources

PaperOpen

Section: §6.1 Initial tests that exclude small violation sets
Page: —
Label: —
Line: main_full_version.tex:3363

Leannot aligned

Phase 2 aligns this node to a Lean declaration.