The Exercise

Two qubits enter a circuit, the first as control and the second as target. The target is rotated by $\pi/2$ about the $y$ axis, a controlled $Z$ gate acts on the pair, and the target is rotated by $-\pi/2$ about the same axis. This is the ion trap construction of the controlled NOT (CNOT) gate. The exercise is to show that the three steps give a CNOT up to a relative phase on the control: the circuit is the CNOT followed by the phase flip $Z$, the Pauli matrix $\operatorname{diag}(1, -1)$, on the control qubit.

Qubits and Their Gates

A quantum system $S$ is given by its state space, 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 $Q$ is the quantum system whose state space is $\mathbb{C}^2$, and a pair of qubits is the composite system $Q \otimes Q$.

A pure state $\lvert\psi\rangle$ of $S$ is a unit vector of the state space of $S$, $\lVert\psi\rVert = 1$.^✦ The computational basis states $\lvert 0\rangle$ and $\lvert 1\rangle$ of the qubit are the pure states whose vectors are the standard basis vectors $e_0$ and $e_1$ of $\mathbb{C}^2$.^✦

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$.^✦ The identity evolution of $S$ is the unitary whose operator is $1$.^✦ Two unitaries $U$ and $V$ of $S$ compose to the unitary $U$ after $V$, with operator $UV$: first $V$, then $U$.^✦ 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 two operators.^✦ A gate on one factor alone is its product with the identity evolution of the other: $U$ on the first factor of $S \otimes T$, the first wires, is $U \otimes 1$, and $V$ on the last factor, the last wires, is $1 \otimes V$.

Pauli Matrices and Rotations

The Pauli matrices are the complex $2 \times 2$ matrices $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.$$(1) The Pauli vector is $\vec{\sigma} = (X, Y, Z)$; for a real vector $\vec{n} = (n_x, n_y, n_z)$ in three dimensions, the matrix $\vec{n} \cdot \vec{\sigma}$ is the combination $n_x X + n_y Y + n_z Z$ of the Pauli matrices.^✦ The rotation about the axis $\vec{n}$ by a real angle $\theta$ is the matrix $$R_{\vec{n}}(\theta) = \exp\Bigl(-\frac{i\theta}{2}\, \vec{n} \cdot \vec{\sigma}\Bigr),$$(2)^✦ written $R_{\hat{n}}(\theta)$ when the axis is a unit vector $\hat{n}$. The rotation about the $y$ axis is $R_y(\theta) = R_{\hat{y}}(\theta) = e^{-i\theta Y/2}$, with $\hat{y} = (0, 1, 0)$.^✦

The $y$ rotation gate is the unitary of the qubit whose operator is the matrix $R_y(\theta)$ acting on $\mathbb{C}^2$.^✦ The Pauli $X$ gate of the qubit, the quantum NOT, is the unitary of the qubit whose operator is the matrix $X$, and the Pauli $Z$ gate of the qubit, the phase flip, is the unitary of the qubit whose operator is the matrix $Z$.

Controlled Gates

For a unitary $U$ of a system $S$, the controlled gate $C(U)$ is the unitary of $Q \otimes S$, a control qubit and a target $S$, with operator $$C(U) = \lvert 0\rangle\langle 0\rvert \otimes 1 + \lvert 1\rangle\langle 1\rvert \otimes U.$$(3)^✦ The CNOT gate is $C(X)$ on a pair of qubits; it flips the target exactly when the control is $\lvert 1\rangle$.^✦ The controlled $Z$ gate is $CZ = C(Z)$, whose matrix in the computational basis is $\operatorname{diag}(1, 1, 1, -1)$.^✦

The Claim

The ion trap circuit $U_{\mathrm{ion}}$ of the exercise is the unitary of $Q \otimes Q$ $$U_{\mathrm{ion}} = \bigl(1 \otimes R_y(-\tfrac{\pi}{2})\bigr)\, CZ\, \bigl(1 \otimes R_y(\tfrac{\pi}{2})\bigr),$$(4)^✦

What Is Checked

The library proves that every controlled gate is unitary: for each unitary $U$ of a system $S$, the operator (3) satisfies $C(U)^\dagger C(U) = C(U)\, C(U)^\dagger = 1$.^✦ It proves the same for the tensor product of two unitaries, for the composite $UV$ of two unitaries, and for the operators that the matrices $X$, $Z$ and $R_y(\theta)$ define on $\mathbb{C}^2$.