LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A random inner linear code has fewer than one bad word in expectation

Statement

Let $m \geq 1$ , let $M$ be a uniformly random binary $16 m \times m$ matrix whose $16 m^{2}$ entries are independent fair bits, and let $wt$ denote Hamming weight in $F_{2}^{16 m}$ . Then the expected number of nonzero $u \in F_{2}^{m}$ with $wt (M u) < 4 m$ satisfies $E [# {u \in F_{2}^{m} ∖ {0} : wt (M u) < 4 m}] \leq (2^{m} - 1) e^{- m} < (\frac{2}{e})^{m} < 1.$ Consequently, with positive probability a random matrix has no such $u$ , and the map $u \mapsto M u$ of every such matrix is injective with relative distance at least $1 / 4$ and rate $1 / 16$ , in the conventions of Explicit binary codes of constant rate and distance. The deterministic construction of such a matrix is the content of Conditional expectation constructs the inner code deterministically.

Facts & Assumptions

Given: an integer $m \geq 1$ , the uniform random matrix $M$ with independent fair entry bits, and the set of nonzero $u \in F_{2}^{m}$ .

[F1]

For $N \geq 1$ the Hamming weight of $x \in {0, 1}^{N}$ is the number of nonzero coordinates, and the relative distance of two binary words of length $N$ is their Hamming distance divided by $N$ (Explicit binary codes of constant rate and distance).

[L1]

If $X_{1}, \dots, X_{k}$ are independent Bernoulli $(p)$ variables with sum $S$ and mean $μ = p k$ , then for $0 < α < 1$ , $\Pr [S \leq (1 - α) μ] \leq \exp (- α^{2} μ / 2)$ (A Chernoff bound for sums of independent Bernoulli trials).

[L2]

On a finite probability space the expectation of a sum of random variables is the sum of the expectations, and the expectation of an indicator is the probability of its event (Expectation of a real random variable on a finite probability space, The expectation of an indicator is the probability of the event).

[L3]

A finite family of classes of events is independent when the probability of every finite intersection of chosen events factors as the product of their probabilities; events determined by disjoint blocks of independent coordinates therefore factorize (Independent families of event classes).

Proof

technique · direct

1.1

Fix $u \neq 0$ and let $Y_{i}$ be the $i$ -th coordinate of $M u$ , so $Y_{i} = \sum_{j \leq m} M_{i j} u_{j}$ in $F_{2}$ and $wt (M u) = \sum_{i \leq 16 m} Y_{i}$ . For fixed $u \neq 0$ the row $i$ of $M$ has at least one free coordinate in the support of $u$ , and the entries of the row are independent fair bits, so $Y_{i}$ is a fair bit; distinct rows involve disjoint blocks of entries and are independent, so $Y_{1}, \dots, Y_{16 m}$ is an independent family of Bernoulli $(1 / 2)$ variables by [L3].

F1L3algebra

2.1

Applying [L1] to this family with $k = 16 m$ , $p = 1 / 2$ , $μ = 8 m$ and $α = 1 / 2$ gives $\Pr [wt (M u) \leq 4 m] \leq e^{- m}$ , and since weights are integers, $\Pr [wt (M u) < 4 m] \leq \Pr [wt (M u) \leq 4 m] \leq e^{- m}$ .

L1step 1.1algebra

3.1

By [L2] the expectation of the number of bad $u$ is the sum of the probabilities $\Pr [wt (M u) < 4 m]$ over the $2^{m} - 1$ nonzero $u$ , hence at most $(2^{m} - 1) e^{- m} < 2^{m} e^{- m} = (2 / e)^{m}$ ; since $2 < e$ , this is strictly less than $1$ .

L2step 2.1algebra

4.1

A random variable with expectation $< 1$ takes a value $< 1$ , so some matrix $M$ has no $u \neq 0$ with $wt (M u) < 4 m$ ; for such $M$ the weight of $M u$ is at least $4 m$ for every nonzero $u$ , whence $M u \neq 0$ and $u \mapsto M u$ is injective, with relative distance at least $4 m / (16 m) = 1 / 4$ and rate $m / (16 m) = 1 / 16$ in the conventions of [F1].

F1step 3.1algebra∎

Remarks

The strict inequality $wt (M u) < 4 m$ is what produces relative distance $1 / 4$ rather than the weaker $1 / 4 - ε$ ; it is also what makes the counting bound $< 1$ rather than $\leq 1$ , which is needed in step 4.1 to conclude existence without any tie.
The argument uses only the $2^{m} - 1$ nonzero messages and the fairness of the row functionals; the value $16$ is chosen so that the mean $8 m$ of the weight is twice the threshold $4 m$ , giving the Chernoff exponent $m$ and the base $2 / e < 1$ . With $16 m$ rows replaced by $c m$ rows for a constant $c > 8$ , the same computation gives the base $2 \exp (- c (1 - 8 / c)^{2} / 4)$ , which is less than $1$ exactly when $c^{2} - (16 + 4 \ln 2) c + 64 > 0$ ; the positive root of that quadratic is about $14.3$ , so the same estimate tolerates any number of rows $c m$ with $c$ above that root, and $c = 16$ is the convenient integer choice.
The positive-probability statement is already enough for a non-uniform existence claim; the point of Conditional expectation constructs the inner code deterministically is to make the matrix computable rather than merely existent.

Depends on

Used by

Conditional expectation constructs the inner code deterministically Lemma

Dependency tree · two levels

17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Irit Dinur, The PCP theorem by gap amplification, §9 (binary inner code with a probabilistic existence argument), printed pp. 29-30. (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §17.5.2 (distance of a code, counting bound), printed pp. 346-347. (standard reference, not scraped)