The Exercise

The three qubit bit flip code stores a state $a|0\rangle + b|1\rangle$ of one qubit, with $|a|^2 + |b|^2 = 1$, in three qubits. Two more qubits, each prepared in $|0\rangle$, are placed beside it, and the encoding circuit acts on all three. The exercise is to verify that the circuit returns $a|000\rangle + b|111\rangle$.

A Quantum System

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ A pure state $\psi$ of $S$ is a unit vector $\psi$ in the state space of $S$, $\lVert \psi \rVert = 1$, determined physically up to a global phase.^✦ The superposition $a\psi + b\varphi$ of two orthogonal pure states $\psi$ and $\varphi$ of $S$, with complex amplitudes $a$ and $b$ such that $|a|^2 + |b|^2 = 1$, is again a pure state of $S$.^✦

The composite system $S \otimes T$ of two systems $S$ and $T$ is the system whose state space is the tensor product of their state spaces.^✦ Given pure states $\psi$ of $S$ and $\varphi$ of $T$, the product $\psi \otimes \varphi$ is the pure state of $S \otimes T$ given by the tensor product of the two vectors.^✦

The Qubit

The qubit is the two level system whose state space is $\mathbb{C}^2$.^✦ The basis state $|i\rangle$ of the qubit, for a bit $i$, is the pure state given by the standard basis vector $e_i$ of $\mathbb{C}^2$; $|0\rangle$ and $|1\rangle$ are the computational basis states.^✦ With amplitudes $a$ and $b$ such that $|a|^2 + |b|^2 = 1$, the qubit state $$a|0\rangle + b|1\rangle$$(1)^✦ is the superposition of the two basis states.

The state space of three qubits is $\mathbb{C}^2 \otimes \mathbb{C}^2 \otimes \mathbb{C}^2$, and $|ijk\rangle$ stands for the product state $|i\rangle \otimes |j\rangle \otimes |k\rangle$. The bit flip codeword with the amplitudes $a$ and $b$ of (1) is the pure state of three qubits $$a|000\rangle + b|111\rangle.$$(2)^✦

Unitaries and Controlled Gates

A unitary $U$ of a quantum system $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = I$, where $I$ is the identity; it is a closed system evolution of $S$^✦, and it carries a pure state $\psi$ of $S$ to the pure state $U\psi$^✦. The identity $I$ is itself a unitary of $S$, the identity evolution.^✦ Two unitaries $U$ and $V$ of $S$ compose to the unitary $UV$, first $V$ then $U$.^✦ When $U$ is a unitary of $S$ and $V$ one of $T$, the product unitary $U \otimes V$ of $S \otimes T$ is the tensor product of the two operators.^✦

The Pauli $X$ of the qubit, the quantum NOT, is the unitary whose matrix in the computational basis is $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}.$$(3)^✦

Let $U$ be a unitary of a system $S$. The controlled gate $C(U)$ on the composite of a control qubit and the target $S$ is $$C(U) = |0\rangle\langle 0| \otimes I + |1\rangle\langle 1| \otimes U.$$(4)^✦

The Encoding Circuit

The encoding circuit $E$ is the unitary of three qubits $$E = C(X \otimes I)\, C(I \otimes X),$$(5)^✦ in which both controlled gates take the first qubit as control and the other two as target. The gate that acts first, $C(I \otimes X)$, is a controlled NOT on the third qubit, and $C(X \otimes I)$ is a controlled NOT on the second.

The Claim

What Is Checked

The claim is stated over the encoding circuit (5), built from the controlled gate (4), the Pauli $X$ and the identity evolution, over the product input state and the codeword (2), and over the action of a unitary on a pure state.

The library proves that the matrix (3) is unitary, and that $C(U)$ is unitary for every unitary $U$ of every system.