The Exercise

The Steane code stores one qubit in seven. Its logical basis states $|0_L\rangle$ and $|1_L\rangle$ are equal superpositions of computational basis states of seven qubits, built from the Hamming code. The exercise is to show that flipping every one of the seven qubits acts on the code as the logical $X$: it takes $|0_L\rangle$ to $|1_L\rangle$ and $|1_L\rangle$ back to $|0_L\rangle$.

A Quantum System

A quantum system $S$ is a physical object whose state space is a finite dimensional complex Hilbert space.^✦ A pure state $|\psi\rangle$ of $S$ is a unit vector in the state space of $S$, $\langle \psi | \psi \rangle = 1$, determined physically up to a global phase.^✦ A unitary $U$ of $S$, a closed system evolution of $S$, is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$.^✦ It carries a pure state $|\psi\rangle$ of $S$ to the pure state $U|\psi\rangle$.^✦

Each finite dimensional complex Hilbert space $H$ defines a quantum system, the one whose state space is $H$.^✦ For a finite set $G$, taking for $H$ the space of complex functions on $G$ gives the system $\mathbb{C}[G]$, with one computational basis vector $|g\rangle$ for each element $g$ of $G$.^✦

Seven Qubits

For a finite set $\iota$ of $n$ elements, the register of qubits indexed by $\iota$ is the system $\mathbb{C}[\mathbb{Z}_2^\iota]$ of the group of bit vectors $w$ indexed by $\iota$ with entries in $\mathbb{Z}_2$: $n$ qubits, one for each element of $\iota$.^✦ The computational basis $\{|w\rangle\}$ of the register indexed by $\iota$ is the orthonormal basis of the state space of the register indexed by the bit vectors $w$, where $|w\rangle$ is the vector with a single entry $1$ at position $w$.^✦ The Steane code lives on the register indexed by $\{1, \ldots, 7\}$, with basis states $|w\rangle$ for $w \in \mathbb{Z}_2^7$.

For a bit vector $v$ indexed by $\iota$, the bit flip string $X^v$ is the unitary on the register that applies the bit flip $X$, which exchanges $|0\rangle$ and $|1\rangle$, to exactly the qubits where $v$ has a $1$: $$X^v = X^{v_1} \otimes \cdots \otimes X^{v_n}, \qquad X^v |w\rangle = |w + v\rangle ,$$(1)^✦ the sum of bit vectors taken bitwise modulo $2$.

The Steane Code

The parity check matrix $H$ of the Hamming code is the matrix over $\mathbb{Z}_2$ with three rows and seven columns whose $j$th column is the binary numeral of $j$, most significant bit on top: $$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}.$$(2)^✦ The Hamming code $C$ is the linear code of length $7$ over $\mathbb{Z}_2$ whose codewords are the words $x$ with $Hx = 0$. The dual Hamming code $C_2$ of the Hamming code $C$ is the linear code of length $7$ over $\mathbb{Z}_2$ consisting of the words whose inner product modulo $2$ with every codeword of $C$ vanishes; it has dimension $3$ and eight codewords.^✦

For a binary linear code $C_2$ and a bit vector $x$, the coset state $|x + C_2\rangle$ is the pure state of the register that superposes with equal amplitudes the basis states $|x + y\rangle$, one for each codeword $y$ of $C_2$: $$|x + C_2\rangle = \frac{1}{\sqrt{|C_2|}} \sum_{y \in C_2} |x + y\rangle .$$(3)^✦

The Steane logical states $|0_L\rangle$ and $|1_L\rangle$ of the register of seven qubits are the coset states of the dual Hamming code $C_2$ at the zero word and at the word of all ones: $$|0_L\rangle = |0000000 + C_2\rangle = \frac{1}{\sqrt 8} \sum_{y \in C_2} |y\rangle ,$$(4)^✦ $$|1_L\rangle = |1111111 + C_2\rangle = \frac{1}{\sqrt 8} \sum_{y \in C_2} |1111111 + y\rangle .$$(5)^✦

The logical $\bar X$ of the Steane code is the bit flip string of the word of all ones, a bit flip on each of the seven qubits: $$\bar X = X^{1111111} = X^{\otimes 7} .$$(6)^✦

The Claim

What Is Checked

The claim is stated over the Steane logical states (4) and (5), coset states of the dual Hamming code built from the parity check matrix (2), and over the logical $\bar X$, a unitary of the register of seven qubits applied to them as pure states.

The library proves that the coset state $|x + C_2\rangle$ has unit norm for every binary linear code $C_2$ and every bit vector $x$. The map $|w\rangle \mapsto |w + v\rangle$ is a linear isometry of the state space of the register onto itself, and a linear isometry of a state space onto itself is a unitary^✦; $X^v$ is the unitary so obtained.