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.

Reed-Solomon outer code has constant rate and distance

Statement

Let $m \geq 1$ , $q = 2^{m}$ and $K = q / 2$ , and let ${R S}_{q, K} : F_{q}^{K} \to F_{q}^{q}$ be the Reed-Solomon evaluation code of Reed-Solomon outer code and binary linear inner code. Then ${R S}_{q, K}$ is injective, its rate over the alphabet $F_{q}$ is $K / q = 1 / 2$ , and its relative Hamming distance over $F_{q}$ is at least $\frac{q - K + 1}{q} \geq \frac{1}{2},$ that is, distinct codewords differ in at least $q - K + 1 = q / 2 + 1$ coordinates. In the bit metric of Explicit binary codes of constant rate and distance applied to the words encoded by the power-basis map this is a statement about $F_{q}$ -symbols; the binary distance of the concatenated code is computed separately in Concatenation multiplies rate and relative distance.

Facts & Assumptions

Given: integers $m \geq 1$ , $q = 2^{m}$ , $K = q / 2$ , the field $F_{q}$ with its fixed listing of the $q$ elements, and the evaluation code ${R S}_{q, K}$ .

[F1]

$F_{q} = F_{2} [z] / (f)$ is a field with exactly $q$ elements; the code ${R S}_{q, K}$ sends a message $(c_{0}, \dots, c_{K - 1})$ to the word $(P (α))_{α \in F_{q}}$ where $P = \sum_{i < K} c_{i} X^{i}$ has degree less than $K$ , evaluated at all $q$ elements of the field in the fixed listing; the map is $F_{q}$ -linear (Reed-Solomon outer code and binary linear inner code).

[L1]

A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots in that domain (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

[L2]

Every field has no zero divisors, so a field with its ring structure is an integral domain (A field has no zero divisors: $a b = 0 \Rightarrow a = 0$ or $b = 0$ ).

Proof

technique · direct

1.1

Let $c \neq c^{'}$ be two distinct messages and let $P, P^{'}$ be the associated polynomials. Then $P - P^{'} \neq 0$ because the coefficient vectors differ, and it is a polynomial of degree at most $K - 1$ , so by [L1] applied over the field $F_{q}$ , which is an integral domain by [L2], it has at most $K - 1$ roots; equivalently $P (α) = P^{'} (α)$ for at most $K - 1$ of the $q$ evaluation points $α$ .

F1L1L2

2.1

Among the $q$ coordinates of the two words, therefore, at least $q - (K - 1) = q - K + 1$ differ; the code is injective because $q - K + 1 \geq 1$ , and its relative distance is at least $(q - K + 1) / q$ . With $K = q / 2$ this is $(q / 2 + 1) / q = 1 / 2 + 1 / q \geq 1 / 2$ .

step 1.1F1algebra

3.1

The message space $F_{q}^{K}$ has $q^{K}$ elements and the rate over $F_{q}$ is the dimension divided by the length, $K / q = 1 / 2$ ; the input and output sizes in bits are $K m = q m / 2$ and $q m$ respectively.

F1algebra∎

Remarks

The count is exact for the evaluation code: the bound $q - K + 1$ is attained by polynomials vanishing on $K - 1$ evaluation points, so the distance cannot be improved by this method, but only the lower bound $1 / 2$ is used on this page.
The alphabet here is $F_{q}$ , not the binary alphabet: the lemma is a statement about the outer code alone, and the passage to binary distance is the content of Concatenation multiplies rate and relative distance, which uses the injectivity and distance of the inner code. The case $m = 1$ is included: then $q = 2$ , $K = 1$ , and the code is the length-two repetition code over $F_{2}$ , with rate $1 / 2$ and relative distance $1 \geq 1 / 2$ .

Depends on

Used by

Dependency tree · two levels

14 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.2 Lemma 17.18 (Reed-Solomon distance), printed p. 347. (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §17.5.2 Definition 17.17, printed p. 347. (standard reference, not scraped)