The Exercise

The Steane code stores one qubit in seven. Its logical operators $\bar X$ and $\bar Z$ act on the encoded qubit as $X$ and $Z$ act on a bare one, with the logical states $|0_L\rangle$ and $|1_L\rangle$ in place of $|0\rangle$ and $|1\rangle$. On a bare qubit the Hadamard gate exchanges $X$ and $Z$ by conjugation, and the exercise is the converse on the code. Let $U$ be a unitary on the seven qubits that keeps $U|0_L\rangle$ and $U|1_L\rangle$ in the code, with $U\bar Z U^\dagger = \bar X$ and $U\bar X U^\dagger = \bar Z$. Up to a global phase, $U$ then does to $|0_L\rangle$ and $|1_L\rangle$ what the Hadamard gate does to $|0\rangle$ and $|1\rangle$, which it sends to $(|0\rangle + |1\rangle)/\sqrt 2$ and $(|0\rangle - |1\rangle)/\sqrt 2$.

A Register of Qubits

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ For a finite group $G$, the group system $\mathbb{C}[G]$ is the quantum system whose state space is the space of complex functions on $G$, with one basis vector $|g\rangle$ for each element $g$ of $G$.^✦ The register of $n$ qubits is the group system of the group $\mathbb{Z}_2^n$ of bit vectors of length $n$.^✦ Its computational basis is the orthonormal basis $\{|w\rangle\}$ indexed by the bit vectors $w$, in which $|w\rangle$ is the function equal to $1$ at $w$ and $0$ elsewhere.^✦

A pure state $|\psi\rangle$ of a system $S$ is a unit vector in the state space of $S$, fixed physically up to a global phase.^✦ A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$^✦, and a pure state $|\psi\rangle$ gives the state $|\psi\rangle\langle\psi|$, the projector onto its vector.^✦ The overlap $\langle\psi|\varphi\rangle$ of two pure states of $S$ is the inner product of their vectors, conjugate linear in the first.^✦

A unitary $U$ of $S$ is an operator on the state space of $S$ with $U^\dagger U = UU^\dagger = 1$.^✦ The adjoint $U^\dagger$ of a unitary $U$ of $S$ is the Hilbert space adjoint of $U$, and the product $UV$ of two unitaries $U$ and $V$ of $S$ applies $V$ first and then $U$. A unitary $U$ carries a pure state $|\psi\rangle$ to the pure state $U|\psi\rangle$.^✦

On the register, a bit vector $v$ gives the bit flip string $X^v = X^{v_1}\otimes\cdots\otimes X^{v_n}$, the unitary that applies the Pauli operator $X$ to exactly the qubits where $v$ has a $1$, and a bit vector $u$ gives the phase flip string $Z^u = Z^{u_1}\otimes\cdots\otimes Z^{u_n}$, built from the Pauli operator $Z$ and diagonal in the computational basis: $$X^v|w\rangle = |w + v\rangle, \qquad Z^u|w\rangle = (-1)^{u\cdot w}\,|w\rangle,$$(1) with the sum and the dot product $u\cdot w$ taken modulo $2$.

The Steane Code

For a binary linear code $C_2$ of length $n$ and a bit vector $x$ of length $n$, the coset state $|x + C_2\rangle$ is the pure state of the register of $n$ qubits 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.$$(2)^✦

The Steane code takes for $C_2$ the dual of a Hamming code $C$ of length $7$, given by its parity check matrix.^✦ The parity check matrix of the Hamming code is the $3 \times 7$ matrix over $\mathbb{Z}_2$ 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}.$$(3)^✦ 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 = C^\perp$ is the linear code of length $7$ over $\mathbb{Z}_2$ whose codewords are the words orthogonal to every codeword of $C$; it has dimension $3$ and eight codewords.

The logical zero $|0_L\rangle$ and the logical one $|1_L\rangle$ of the Steane code are the coset states of $C_2$ at $0000000$ and $1111111$, each a sum of eight basis states of the register of seven qubits with amplitude $1/\sqrt 8$: $$|0_L\rangle = |0000000 + C_2\rangle = \frac{1}{\sqrt 8}\sum_{y\in C_2}|y\rangle, \qquad |1_L\rangle = |1111111 + C_2\rangle = \frac{1}{\sqrt 8}\sum_{y\in C_2}|1111111 + y\rangle.$$(4) A pure state $|\psi\rangle$ of the register of seven qubits lies in the Steane code when it is a combination of the two logical states: $$|\psi\rangle = a|0_L\rangle + b|1_L\rangle \quad \text{for some } a, b \in \mathbb{C}.$$(5)^✦

The logical operators $\bar X$ and $\bar Z$ of the Steane code are the flip strings (1) of the all ones word $\mathbf{1} = 1111111$, with $X_i$ and $Z_i$ the Pauli operators on the $i$th qubit: $$\bar X = X^{\mathbf 1} = X_1X_2X_3X_4X_5X_6X_7, \qquad \bar Z = Z^{\mathbf 1} = Z_1Z_2Z_3Z_4Z_5Z_6Z_7.$$(6)

For orthogonal pure states $|\psi\rangle$ and $|\varphi\rangle$ of a system and complex amplitudes $a$ and $b$ with $|a|^2 + |b|^2 = 1$, the superposition $a|\psi\rangle + b|\varphi\rangle$ is the pure state of the same system with that vector.^✦ The encoded plus state $|+_L\rangle$ and minus state $|-_L\rangle$ of the Steane code are the superpositions of its logical states $|0_L\rangle$ and $|1_L\rangle$ with amplitudes $1/\sqrt 2$ and $1/\sqrt 2$, respectively $1/\sqrt 2$ and $-1/\sqrt 2$: $$|+_L\rangle = \frac{1}{\sqrt 2}\bigl(|0_L\rangle + |1_L\rangle\bigr),$$(7)^✦ $$|-_L\rangle = \frac{1}{\sqrt 2}\bigl(|0_L\rangle - |1_L\rangle\bigr).$$(8)^✦

The Claim

What Is Checked

The claim is stated over a unitary $U$ of the register of seven qubits and the constructions of the Steane code: the logical operators (6), the logical states (4) built on the dual Hamming code, the membership (5), and the encoded states (7) and (8), compared through their projectors and their overlaps.

The library proves that the two logical states are orthogonal, $\langle 0_L|1_L\rangle = 0$^✦, which makes $|+_L\rangle$ and $|-_L\rangle$ unit vectors, and that every coset state (2) has unit norm. It proves that the bit flip string, the isometry $|w\rangle \mapsto |w + v\rangle$ of the state space onto itself, is unitary, and so are the phase flip string, the adjoint $U^\dagger$ and the product $UV$.