The Exercise

A string of bits sent through a noisy channel may arrive with some of its bits flipped. A binary linear code guards against this by admitting only the strings that pass a fixed set of parity checks, each check a sum of chosen bits modulo $2$ that must vanish. The Hamming code with $r$ checks labels each bit position by a nonzero string of $r$ bits, using every such string once, and its $i$th check adds the bits whose label has a $1$ in place $i$. The exercise asks for the length $n$ of this code, the number of bits in a codeword, for its dimension $k$ over $\mathbb{Z}_2$ and its minimum distance, and whether it corrects a flip of any single bit.

Linear Codes

A linear code $C$ over a field $K$ is a subspace of the strings with one entry from $K$ at each of its positions. The Hamming weight $\mathrm{wt}(c)$ of a string $c$ 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 \{\, \mathrm{wt}(c) : c \in C,\ c \neq 0 \,\},$$(1)^✦ and is infinite for the zero code, which has no nonzero codeword. A linear code $C$ corrects $t$ errors when $d(C) \ge 2t + 1$.^✦

The Hamming Code

Fix a natural number $r$ and let $P_r$ be the set of nonzero strings $s = (s_1, \dots, s_r)$ in $\mathbb{Z}_2^r$; these label the positions of the code. The Hamming parity check matrix $H_r$ is the $r \times |P_r|$ matrix over $\mathbb{Z}_2$ whose column at position $s$ is the string $s$ itself: $$(H_r)_{i s} = s_i, \qquad i = 1, \dots, r, \quad s \in P_r.$$(2)^✦ The Hamming code $C_r$ is the binary linear code with parity check matrix $H_r$.^✦ Its codewords are the strings $x$ with one bit $x_s$ at each position $s \in P_r$ that pass all $r$ checks: $$C_r = \{\, x \in \mathbb{Z}_2^{P_r} : H_r x = 0 \,\}.$$(3)^✦

The Claim

What Is Checked

The claim is stated over the Hamming code $C_r$ of (3), built on the parity check matrix $H_r$ of (2), and over the minimum distance (1) of a linear code with the correction of $t$ errors defined from it. What the library proves about these constructions is the theorem above, all four of its parts.