The Exercise

Two numbers $x$ and $y$ from $\{0, 1, 2, 3\}$ are each held in two qubits, one qubit for each of their two binary digits. The exercise asks for a quantum circuit that adds $x$ to $y$ modulo $4$ and keeps $x$, taking the basis state $|x, y\rangle$ to $|x, x + y \bmod 4\rangle$.

The library builds such a circuit on four qubits from one Toffoli gate and two controlled NOT (CNOT) gates.

Four Qubits

A quantum system $S$ is a physical object whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $S \otimes T$ of two quantum systems $S$ and $T$ is the quantum system whose state space is the tensor product of their state spaces.^✦ The qubit is the two level quantum system with state space $\mathbb{C}^2$.^✦

A pure state $|\psi\rangle$ of a quantum system $S$ is a unit vector in the state space of $S$, determined physically up to a global phase.^✦ For a bit $i \in \{0, 1\}$, the basis state $|i\rangle$ of the qubit is the pure state whose vector is the standard basis vector $e_i$ of $\mathbb{C}^2$.^✦ Given pure states $|\psi\rangle$ of $S$ and $|\varphi\rangle$ of $T$, their product $|\psi\rangle \otimes |\varphi\rangle$ is the pure state of $S \otimes T$ whose vector is the tensor product of the two vectors.^✦

The low binary digit of a number $x \in \{0, 1, 2, 3\}$ is $x_0 = x \bmod 2$ and its high binary digit is $x_1 = \lfloor x/2 \rfloor$, so that $x = 2x_1 + x_0$. The adder acts on four qubits, with state space $\mathbb{C}^2 \otimes \mathbb{C}^2 \otimes \mathbb{C}^2 \otimes \mathbb{C}^2$, which hold in turn the low digits of $x$ and $y$ and then their high digits. The input of the adder for numbers $x$ and $y$ is the product of basis states $$|x, y\rangle = |x_0\rangle \otimes |y_0\rangle \otimes |x_1\rangle \otimes |y_1\rangle .$$(1)^✦

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 = 1$, a closed system evolution of $S$.^✦ A unitary $U$ of $S$ applied to a pure state $|\psi\rangle$ of $S$ gives the pure state $U|\psi\rangle$, whose vector is that of $|\psi\rangle$ acted on by $U$.^✦ For unitaries $U$ and $V$ of the same system, $U$ after $V$ is the unitary $UV$: first $V$, then $U$.^✦ The identity evolution of $S$ is the unitary $1$ of $S$.^✦

For unitaries $U$ of $S$ and $V$ of $T$, the product unitary $U \otimes V$ is the unitary of $S \otimes T$ whose operator is the tensor product of the operators of $U$ and $V$.^✦ With the identity evolution as one factor it places a gate on part of the qubits, each qubit being a wire of the circuit: the gate $U$ on the first qubits is $U \otimes 1$, and the gate $V$ on the last qubits is $1 \otimes V$.

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

For a unitary $U$ of a system $S$, the controlled gate $C(U)$ is the unitary of the composite of a control qubit and the target $S$ given by $$C(U) = |0\rangle\langle 0| \otimes 1 + |1\rangle\langle 1| \otimes U .$$(3)^✦ The CNOT gate is $C(X)$, a unitary of two qubits that flips the second qubit exactly when the first, the control, is $|1\rangle$.^✦

The Adder Circuit

The four qubits are named by the digits they hold, $x_0, y_0, x_1, y_1$. The carry Toffoli is $$U_{\mathrm{carry}} = C\bigl(C(1 \otimes X)\bigr),$$(4)^✦ a Toffoli gate controlled by $x_0$ and $y_0$, with $X$ on $y_1$ and the identity on $x_1$. The high CNOT is the CNOT gate on the last two wires, with control $x_1$ and target $y_1$, $$U_{\mathrm{high}} = 1 \otimes 1 \otimes \mathrm{CNOT},$$(5) and the low CNOT is controlled by $x_0$, with $X$ on $y_0$: $$U_{\mathrm{low}} = C(X \otimes 1 \otimes 1).$$(6) The mod $4$ adder applies the three in this order: $$U_{+} = U_{\mathrm{low}}\, U_{\mathrm{high}}\, U_{\mathrm{carry}} .$$(7)^✦

The Claim

What Is Checked

The claim is stated over the four qubits and the products (1) of their basis states, and over the circuit (7), built from the Pauli $X$ by controlled gates, gates on part of the wires and composition. The two sides of (8) are equal as unit vectors, with no global phase between them.

The library proves that the controlled gate of a unitary $U$ is unitary, $C(U)^\dagger C(U) = C(U) C(U)^\dagger = 1$; with the unitarity of the Pauli $X$ and of the products $UV$ and $U \otimes V$ of unitaries, this makes each of the three gates and $U_{+}$ a unitary of the four qubits. A unitary preserves norms, and the norm of a product vector is the product of the norms, so $U|\psi\rangle$ and $|\psi\rangle \otimes |\varphi\rangle$ are again pure states.