The Exercise

A word of seven bits is a vector $y = (y_1, \dots, y_7)$ in $\mathbb{Z}_2^7$, where $\mathbb{Z}_2 = \{0, 1\}$ and all arithmetic is modulo $2$. A generator matrix $G$ of a code $C$ of such words is a $7 \times k$ matrix over $\mathbb{Z}_2$ whose images $Gx$, as the message $x$ runs over $\mathbb{Z}_2^k$, are exactly the words of $C$. The Hamming code $C_1$ is given instead by three parity checks on the seven bits, the rows of a $3 \times 7$ parity check matrix $H$ over $\mathbb{Z}_2$: the words of $C_1$ are the $y$ with $Hy = 0$.

The exercise gives a $4 \times 7$ matrix $H[C_2]$, the parity check matrix of a second code $C_2$, and asks to verify that its transpose is a generator matrix of $C_1$, so that $H[C_2] = G[C_1]^T$.

Three Matrices

The parity check matrix $H$ of the Hamming code is the $3 \times 7$ matrix over $\mathbb{Z}_2$ $$H = \begin{pmatrix} 0 & 0 & 0 & 1 & 1 & 1 & 1 \\ 0 & 1 & 1 & 0 & 0 & 1 & 1 \\ 1 & 0 & 1 & 0 & 1 & 0 & 1 \end{pmatrix},$$(1)^✦ whose $j$th column is $j$ written in binary, most significant bit on top.

The matrix $H[C_2]$ of the exercise is the $4 \times 7$ matrix over $\mathbb{Z}_2$ $$H[C_2] = \begin{pmatrix} 1 & 0 & 0 & 0 & 0 & 1 & 1 \\ 0 & 1 & 0 & 0 & 1 & 0 & 1 \\ 0 & 0 & 1 & 0 & 1 & 1 & 0 \\ 0 & 0 & 0 & 1 & 1 & 1 & 1 \end{pmatrix}.$$(2)^✦ The matrix $G = H[C_2]^T$ is the $7 \times 4$ matrix over $\mathbb{Z}_2$ obtained by transposing $H[C_2]$, $$G = H[C_2]^T = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 1 & 1 & 1 \\ 1 & 0 & 1 & 1 \\ 1 & 1 & 0 & 1 \end{pmatrix}.$$(3)^✦ Applied to a message $x \in \mathbb{Z}_2^4$, it gives the word $Gx$, whose first four bits are those of $x$ and whose last three are the parities $x_2 + x_3 + x_4$, $x_1 + x_3 + x_4$ and $x_1 + x_2 + x_4$.

The Claim

What Is Checked

The claim is stated over the matrices (1), (2) and (3).

What the library shows about them is the equality (4).