The Exercise

A classical linear code sends a message of $k$ symbols from a field $K$ as a word of $n$ symbols, so that $n - k$ of them are redundant and protect the message against errors. How many errors the code can catch is measured by its minimum distance $d$. The exercise asks how large $d$ can be once $n$ and $k$ are fixed; its answer, the Singleton bound, limits $d$ by the redundancy alone.

Linear Codes

A linear code $C$ of length $n$ over a field $K$ is a subspace of $K^n$, the space of words $c = (c_1, \dots, c_n)$ with entries in $K$. A codeword of $C$ is an element $c \in C$. The dimension $k = \dim_K C$ of the code is the number of message symbols it carries. The zero code is the subspace $\{0\}$.

The Hamming weight $\operatorname{wt}(c)$ of a word $c$ in $K^n$ is the number of its nonzero entries. The minimum distance $d(C)$ of a linear code $C$ is the least Hamming weight of a nonzero codeword, $$d(C) = \min \{\, \operatorname{wt}(c) : c \in C,\ c \neq 0 \,\},$$(1)^✦ and the zero code, having no nonzero codeword, has $d(C) = \infty$.

The Claim

What Is Checked

The claim is stated over the minimum distance $d(C)$ of (1), the length $n$ of the code and its dimension $k$ over $K$. What the library proves about them is the inequality (2) between the three numbers.