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.

Conditional expectation constructs the inner code deterministically

Statement

For every integer $m \geq 1$ there is a deterministic algorithm which, given $m$ , runs in time polynomial in $2^{m} m$ and outputs a binary $16 m \times m$ matrix $M$ such that $wt (M u) \geq 4 m$ for every nonzero $u \in F_{2}^{m}$ . Hence $u \mapsto M u$ is an injective $F_{2}$ -linear map $F_{2}^{m} \to F_{2}^{16 m}$ of rate $1 / 16$ and relative distance at least $1 / 4$ , in the conventions of Explicit binary codes of constant rate and distance, the same algorithm serves every $m$ , and the output matrix is a function of $m$ alone, with no random choices.

Facts & Assumptions

Given: an integer $m \geq 1$ , the number $N : = 16 m^{2}$ of entries, and the identification of binary $16 m \times m$ matrices with the points of $Ω : = {0, 1}^{N}$ by listing the entries in a fixed order.

[F1]

For the uniform random matrix $M$ on $Ω$ and $X (M) : = # {u \in F_{2}^{m} ∖ {0} : wt (M u) < 4 m}$ one has $E X < 1$ ; indeed $E X \leq (2^{m} - 1) e^{- m} < (2 / e)^{m} < 1$ (A random inner linear code has fewer than one bad word in expectation).

[F2]

On a finite probability space with weights, the expectation of a real random variable is the weighted sum $\sum_{ω} X (ω) w (ω)$ ; on $Ω$ the uniform weights are $2^{- N}$ (Expectation of a real random variable on a finite probability space).

[F3]

For binary words, Hamming weight and relative distance are as in the code conventions; an injective linear map with minimum nonzero weight at least $4 m$ has relative distance at least $4 m / (16 m) = 1 / 4$ and rate $m / (16 m) = 1 / 16$ (Explicit binary codes of constant rate and distance).

Proof

technique · constructive

1.1

For a partial assignment $a \in {0, 1}^{s}$ of the first $s$ entries let $F (a) : = {M \in Ω : M_{j} = a_{j} for j \leq s}$ be its fiber and define $\overset{ˉ}{X} (a) : = \frac{1}{∣ F (a) ∣} \sum_{M \in F (a)} X (M) = 2^{- (N - s)} \sum_{M \in F (a)} X (M),$ the average of $X$ over the fiber. Then $\overset{ˉ}{X} (\emptyset) = E X$ by [F2], and for every $s < N$ $\overset{ˉ}{X} (a) = \frac{1}{2} (\overset{ˉ}{X} (a 0) + \overset{ˉ}{X} (a 1)),$ because $F (a)$ is the disjoint union of the two fibers $F (a 0)$ and $F (a 1)$ , which have equal size $2^{N - s - 1}$ ; this is the elementary averaging identity for finite sums.

F2algebra

1.2

Fix $a \in {0, 1}^{s}$ and $u \neq 0$ . A row $i$ is determined for $(a, u)$ when all coordinates $j$ in the support of $u$ have $a_{j}$ already fixed, in which case the $i$ -th bit of $M u$ equals the known value $\sum_{j \in supp u} M_{i j} u_{j}$ ; otherwise that bit is a fair coin, because at least one of its summands is an undecided uniform bit and the bits of distinct rows are independent. Writing $D_{u}$ for the number of determined rows whose determined bit is $1$ and $R_{u}$ for the number of undetermined rows, the conditional law of $wt (M u)$ over the uniform fiber $F (a)$ is $D_{u} + Bin (R_{u}, \frac{1}{2})$ ; hence $\Pr [wt (M u) < 4 m ∣ F (a)] = \Pr [Bin (R_{u}, \frac{1}{2}) < 4 m - D_{u}]$ , a number of the form $2^{- R_{u}} c$ with $c$ a nonnegative integer.

algebragiven

2.1

Define a path of partial assignments by $a_{0} : = \emptyset$ and, for $s < N$ , $a_{s + 1} : = a_{s} 0$ if $\overset{ˉ}{X} (a_{s} 0) \leq \overset{ˉ}{X} (a_{s} 1)$ and $a_{s + 1} : = a_{s} 1$ otherwise, so ties go to the $0$ branch; this is a deterministic choice. The averaging identity of step 1.1 gives $\overset{ˉ}{X} (a_{s + 1}) \leq \overset{ˉ}{X} (a_{s})$ at every step, hence $\overset{ˉ}{X} (a_{N}) \leq \overset{ˉ}{X} (\emptyset) = E X < 1$ by [F1].

F1step 1.1construct

3.1

The terminal fiber is a single matrix $M^{*}$ , so $\overset{ˉ}{X} (a_{N}) = X (M^{*})$ is a nonnegative integer strictly below $1$ , hence equal to $0$ : the produced matrix satisfies $wt (M^{*} u) \geq 4 m$ for every nonzero $u$ .

step 2.1algebradischarge-construct

4.1

For the running time, evaluating $\overset{ˉ}{X} (a)$ for one partial assignment means summing the $2^{m} - 1$ conditional probabilities of step 1.2; for each $u$ , the support, the numbers $D_{u}$ and $R_{u}$ and the binomial tail are computed in $O (m)$ operations using a precomputed table of the binomial coefficients $(\binom{R}{t})$ for $R \leq 16 m$ , and all arithmetic is exact on integers of $O (m)$ bits, so one evaluation costs $O (2^{m} m^{2})$ and the whole path costs $O (2^{m} m^{4})$ operations, which is polynomial in $2^{m} m$ . By step 3.1 the output has $wt (M^{*} u) \geq 4 m$ for all $u \neq 0$ , so it is injective and has rate $1 / 16$ and relative distance at least $1 / 4$ by [F3].

F3step 1.2step 3.1discharge-constructalgebra∎

Remarks

The argument is the method of conditional expectations in its finite form: no conditional expectation as an abstract object is needed, only the identity that the average over a fiber is the average of the averages over the two half-fibers. That is also why the procedure is deterministic: the two candidate values are computed exactly, not estimated.
The inner code is produced in time polynomial in $2^{m} m$ , which is polynomial in the message length of the concatenated code of Reed-Solomon outer code and binary linear inner code because that message length is $2^{m - 1} m$ . The procedure is uniform in $m$ , so no choice of a matrix is made anywhere on the page: every consumer uses the matrix $M^{*}$ output for its own $m$ .

Depends on

Used by

Dependency tree · two levels

9 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 (explicit binary inner code obtained by derandomizing the counting argument), printed pp. 29-30. (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §7.4 and §17.5.2 (method of conditional expectations; code distance), printed pp. 123-125 and 346-347. (standard reference, not scraped)