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.

Concatenation multiplies rate and relative distance

Statement

Let $m \geq 1$ , $q = 2^{m}$ , $K = q / 2$ , let ${R S}_{q, K} \subseteq F_{q}^{q}$ be the Reed-Solomon outer code with rate $R_{o} = K / q$ and relative distance at least $δ_{o}$ , and let $E_{i n} = M (\cdot) : F_{2}^{m} \to F_{2}^{16 m}$ be the inner encoding of Conditional expectation constructs the inner code deterministically, injective and linear of rate $R_{i} = 1 / 16$ and relative distance at least $δ_{i}$ , so that $wt (E_{i n} (w)) \geq δ_{i} \cdot 16 m$ for every nonzero $w \in F_{2}^{m}$ . Then the concatenated code of Reed-Solomon outer code and binary linear inner code, which encodes $K m$ bits into $16 q m$ bits, is injective with $rate = R_{o} R_{i} = \frac{K}{16 q}, relative distance \geq δ_{o} δ_{i} .$ For the outer parameters of Reed-Solomon outer code has constant rate and distance and the inner parameters of Conditional expectation constructs the inner code deterministically these are rate at least $\frac{1}{2} \cdot \frac{1}{16} = \frac{1}{32}$ and relative distance at least $\frac{1}{2} \cdot \frac{1}{4} = \frac{1}{8}$ .

Facts & Assumptions

Given: integers $m \geq 1$ , $q = 2^{m}$ , $K = q / 2$ ; the bit encoding $e n c : F_{q} \to F_{2}^{m}$ of the field, which is $F_{2}$ -linear by the power basis; the outer code ${R S}_{q, K}$ with rate $R_{o} = K / q$ and relative distance at least $δ_{o}$ ; an injective $F_{2}$ -linear $E_{i n} : F_{2}^{m} \to F_{2}^{16 m}$ with $wt (E_{i n} (w)) \geq δ_{i} 16 m$ for $w \neq 0$ .

[F1]

The concatenated encoding sends a message $u = (u_{1}, \dots, u_{K}) \in (F_{2}^{m})^{K}$ to the word obtained by applying $E_{i n} \circ e n c$ to each of the $q$ coordinates of the outer word ${R S}_{q, K} ({e n c}^{- 1} (u_{1}), \dots, {e n c}^{- 1} (u_{K}))$ ; it has $K m$ input bits and $16 q m$ output bits, and the field element $0$ has bit encoding the zero vector (Reed-Solomon outer code and binary linear inner code).

[F2]

Relative distance of a code of length $n$ over an alphabet is the minimum, over distinct codewords, of the fraction of differing coordinates; over a binary alphabet the coordinates are bits. Rate is the input length in bits divided by the output length in bits (Explicit binary codes of constant rate and distance).

[L1]

Distinct messages of ${R S}_{q, K}$ have outer words differing in at least $δ_{o} q$ coordinates, and distinct messages have distinct outer words (Reed-Solomon outer code has constant rate and distance).

[L2]

The map $E_{i n}$ is linear and injective with $wt (E_{i n} (w)) \geq δ_{i} 16 m$ for every nonzero $w$ ; in particular $u \mapsto M u$ has rate $R_{i} = 1 / 16$ and relative distance at least $δ_{i}$ (Conditional expectation constructs the inner code deterministically).

Proof

technique · direct

1.1

The concatenated encoding is injective: if two messages $u \neq u^{'}$ had the same concatenated word, then their outer words would agree in every coordinate, since $E_{i n} \circ e n c$ is injective and the blocks of the concatenation are read off coordinatewise; but distinct messages have distinct outer words by [L1, F1]. Moreover the rate is $K m / (16 q m) = K / (16 q) = R_{o} R_{i}$ , because the outer code has $K$ $F_{q}$ -symbols ( $K m$ bits) and the concatenated word has $q$ blocks of $16 m$ bits.

F1F2L1algebra

2.1

Let $u \neq u^{'}$ be distinct messages with outer words $c \neq c^{'}$ , and let $S = {j : c_{j} \neq c_{j}^{'}}$ be the set of differing coordinates, of size at least $δ_{o} q$ by [L1]. For $j \in S$ the field element $c_{j} - c_{j}^{'} \neq 0$ has nonzero bit encoding $e n c (c_{j} - c_{j}^{'}) = e n c (c_{j}) - e n c (c_{j}^{'})$ by linearity of $e n c$ , so the block difference $E_{i n} (e n c (c_{j})) - E_{i n} (e n c (c_{j}^{'})) = E_{i n} (e n c (c_{j} - c_{j}^{'}))$ is a nonzero word of weight at least $δ_{i} 16 m$ by [L2].

F1L2step 1.1algebra

3.1

The blocks indexed by $S$ occupy disjoint sets of coordinates of the concatenated word, so the total Hamming distance between the two concatenated words is the sum over $j \in S$ of the block weights, at least $∣ S ∣ δ_{i} 16 m \geq δ_{o} q δ_{i} 16 m$ ; dividing by the word length $16 q m$ gives relative distance at least $δ_{o} δ_{i}$ , and with the outer and inner parameters this is at least $\frac{1}{2} \cdot \frac{1}{4} = \frac{1}{8}$ while the rate is $\frac{1}{2} \cdot \frac{1}{16} = \frac{1}{32}$ .

F2step 2.1L1L2algebra∎

Remarks

Both factors are honest minima. The outer distance loses a factor $q$ in the number of surviving coordinates and the inner distance loses a factor $16 m$ in the surviving bits per coordinate, and the product is exactly the product of the relative distances; nothing is lost to the intermediate field or to the choice of inner matrix, because the inner map is linear and injective and its blocks are disjoint.
The lemma is stated for the concrete outer and inner codes of this page, but the proof uses only [F1], [F2], [L1] and [L2], so the same computation applies to any outer code with rate $R_{o}$ and relative distance $δ_{o}$ whose alphabet is identified with $F_{2}^{m}$ and any injective linear inner code with parameters $R_{i}, δ_{i}$ .

Depends on

Used by

A polynomial-time explicit constant-rate constant-distance code Theorem

Dependency tree · two levels

12 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

Arora and Barak, Computational Complexity: A Modern Approach, §17.5.3 Definition 17.19 and Claim 17.20 (concatenation multiplies distance), printed p. 348. (standard reference, not scraped)
Irit Dinur, The PCP theorem by gap amplification, §9 (Reed-Solomon outer code concatenated with a binary inner code), printed pp. 29-30. (standard reference, not scraped)