The Exercise

A classical message of $k$ symbols is protected against noise by sending every symbol $r$ times, so that it goes out as a word of length $rk$ ; with $k = 2$ and $r = 3$ the message $x_1 x_2$ is sent as $x_1 x_1 x_1 x_2 x_2 x_2$ . The encoding is linear: a generator matrix $G$ with $rk$ rows and $k$ columns takes a message $x$ to its codeword $Gx$ . The exercise asks for $G$ , and for the code it generates to be an $[rk,k]$ code, a subspace of dimension $k$ in the words of length $rk$ .

The Repetition Code

The symbols are elements of a field $K$ , bits when $K = \mathbb{Z}_2$ , and a message is a vector $x = (x_1, \dots, x_k)$ in $K^k$ . The positions of a word of length $rk$ are labelled by pairs $(i,j)$ , with $i$ running from $1$ to $k$ and $j$ from $1$ to $r$ , so that a word is a vector of $K^{rk}$ with one entry for each pair.

The generator matrix $G$ of the repetition code is the $rk \times k$ matrix over $K$ with rows labelled by the positions $(i,j)$ , columns labelled by the symbols $l$ , and entries $G_{(i,j),\,l} = \begin{cases} 1, & l = i,\\ 0, & l \neq i. \end{cases}$ (1)^✦

The repetition code $C$ over $K$ is the linear code of length $rk$ , a subspace of $K^{rk}$ , whose codewords are the images of all messages under $G$ : $C = \{\, Gx : x \in K^k \,\} \subseteq K^{rk}.$ (2)^✦

The Claim

Theorem 1. Let $K$ be a field and $k$ and $r$ natural numbers. For every message $x \in K^k$ , the codeword $Gx$ carries $x_i$ at each of the $r$ positions $(i,j)$ of the $i$ th symbol: $(Gx)_{(i,j)} = x_i .$ (3)^✦ If $r \ge 1$ , the repetition code has dimension $k$ : $\dim_K C = k .$ (4)^✦

For $r \ge 1$ this is the exercise: $C$ is an $[rk,k]$ code with generator matrix $G$ .

What Is Checked

The claim is stated over the generator matrix $G$ of (1) and the repetition code $C$ of (2) that it generates. About these two constructions the library proves the encoding rule (3), for every $r$ , and the dimension (4), for $r \ge 1$ .