The Exercise

A classical linear code on $n$ bits is described by a parity check matrix $H$, a $k \times n$ matrix of bits. The syndrome of a string $x = (x_1, \dots, x_n)$ of $n$ bits is the string $Hx$ of $k$ bits with entries $$(Hx)_i = \sum_{j=1}^{n} H_{ij}\, x_j \pmod{2}, \qquad i = 1, \dots, k .$$(1) The exercise asks for a quantum circuit made of controlled NOT (CNOT) gates alone that takes $n$ data qubits in the basis state $|x\rangle$ and $k$ ancilla qubits in $|0\rangle$ to $|x\rangle|Hx\rangle$.

A Register of Qubits

A quantum system $S$ is a physical system 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$.^✦ The closed evolutions of $S$ are its unitaries: a unitary $U$ of $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$^✦, and it acts on pure states by $|\psi\rangle \mapsto U|\psi\rangle$^✦.

The qubit $Q$ is the two level system whose state space is $\mathbb{C}^2$.^✦ The computational basis states $|0\rangle$ and $|1\rangle$ of the qubit $Q$ are the two standard basis vectors of $\mathbb{C}^2$.^✦

The composite system $\bigotimes_i S_i$ of systems $S_i$, one for each $i$ in a finite index set, is the system whose state space is the tensor product of the state spaces of the $S_i$.^✦ The product $\bigotimes_i |\psi_i\rangle$ of pure states $|\psi_i\rangle$ of the factors is the pure state of the composite whose vector is the tensor product of theirs.^✦ The register $Q^{\otimes m}$ of $m$ qubits is the tensor power of the qubit, the composite of $m$ copies of $Q$.^✦ The computational basis state $|c\rangle$ of $Q^{\otimes m}$ for a string $c = (c_1, \dots, c_m)$ of $m$ bits is the product $$|c\rangle = |c_1\rangle \otimes |c_2\rangle \otimes \cdots \otimes |c_m\rangle .$$(2)

Controlled NOT Gates

A multiply controlled NOT gate $g = (S, t)$ on $m$ wires, the $m$ positions of a string of $m$ bits, is a set $S$ of control wires together with a target wire $t$.^✦ The control bit of $g$ on a string $c$ of $m$ bits is $1$ when $c$ carries a $1$ on every wire of $S$ and $0$ otherwise, the product $\prod_{i \in S} c_i$.^✦ The gate takes $c$ to the string $g(c)$ in which the control bit has been added to the bit on the target wire modulo $2$: $$g(c)_t = c_t \oplus \prod_{i \in S} c_i , \qquad g(c)_w = c_w \quad (w \neq t) .$$(3)^✦ With one control it is the CNOT, and with two the Toffoli gate.

The classical action of a circuit $C = (g_1, \dots, g_L)$ of such gates on a string $c$ of $m$ bits applies the gates in turn, $g_L$ first: $$C(c) = g_1\bigl(g_2(\cdots g_L(c) \cdots)\bigr) .$$(4)^✦

The Claim

The wires of a circuit on $n + k$ wires are the qubits of the register $Q^{\otimes(n+k)}$, the first $n$ holding the data and the last $k$ the ancillas. For a string $x$ of $n$ bits, $|x\rangle|0\rangle$ is the basis state (2) of the string with $x$ on the data and zeros on the ancillas, and $|x\rangle|Hx\rangle$ the one with the syndrome (1) on the ancillas.

What Is Checked

The claim is stated over the register $Q^{\otimes(n+k)}$, the tensor power of the qubit, with its computational basis states (2) formed as products of the qubit states $|0\rangle$ and $|1\rangle$, and over a unitary of the register acting on them.

The library proves that the composite of finitely many systems has a finite dimensional state space, the products of basis vectors of the factors forming a basis of it, and that a product of pure states is a unit vector there, its squared norm being the product of the squared norms of the factors. It proves as well that $U|\psi\rangle$ is a unit vector whenever $|\psi\rangle$ is, since a unitary preserves norms.