The Exercise

The repetition code protects a message by copying it. Each of $k$ message symbols, taken from a field $K$, is written down $r$ times, turning a message of length $k$ into a word of length $rk$. The exercise asks for a parity check matrix for this code: a matrix $H$ with linearly independent rows whose kernel is exactly the code.

The Repetition Code

Over a field $K$, the generator matrix $G$ of the $[rk,k]$ repetition code, of length $rk$ and encoding $k$ symbols, is the $rk \times k$ matrix whose rows are labelled by pairs $(j,s)$ of a message position $j = 1, \dots, k$ and a copy number $s = 1, \dots, r$, whose columns are labelled by message positions $i$, and whose entries are $$G_{(j,s),\,i} = \delta_{ij}.$$(1)^✦

The $[rk,k]$ repetition code $C$ over $K$ is the linear code of length $rk$, a subspace of $K^{rk}$ with coordinates labelled by the same pairs $(j,s)$, whose codewords are the images of the messages under $G$: $$C = \{\, Gx : x \in K^k \,\}.$$(2)^✦

With $r \ge 1$ copies, the parity check matrix $H$ of the repetition code has $(r-1)k$ rows, labelled by pairs $(j,t)$ with $j = 1, \dots, k$ and $t = 1, \dots, r-1$, and $rk$ columns, labelled by the coordinates $(i,s)$ of the code; its entries are $$H_{(j,t),\,(i,s)} = \delta_{ij}\,\bigl(\delta_{st} - \delta_{s,t+1}\bigr).$$(3)^✦

The Claim

What Is Checked

The claim is stated over the repetition code (2), the image of the generator matrix (1), and over the matrix $H$ of (3).

What the library proves about these constructions is the theorem’s two statements, (4) and (5).