The Exercise

Take two qubits, a control and a target, and a real angle $\theta$. The exercise asks for a circuit that applies the rotation $R_x(\theta)$ about the $\hat x$ axis to the target when the control is $\lvert 1\rangle$ and leaves the target alone when the control is $\lvert 0\rangle$, and for the same circuit with the rotation $R_y(\theta)$ about the $\hat y$ axis. The circuits are built from controlled NOT (CNOT) gates and single qubit gates.

The library states the answer for every real angle $\theta$ as two equalities between unitaries of the two qubits.

Qubits and Unitaries

A quantum system 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 the state spaces of $S$ and $T$.^✦ The qubit is the two level quantum system whose state space is $\mathbb{C}^2$.^✦

A pure state $\psi$ of a quantum system $S$ is a vector of unit norm in the state space of $S$.^✦ 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 a quantum system $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$, an evolution of $S$ as a closed system.^✦ The identity evolution of $S$ is the unitary $1$.^✦ For unitaries $U$ and $V$ of $S$, the unitary $U$ after $V$ is their composite $UV$: first $V$ acts, then $U$.^✦

For a unitary $U$ of $S$ and a unitary $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$.^✦ The gate $V$ on the second factor of $S \otimes T$ is the product unitary $1 \otimes V$, with the identity evolution on $S$ and $V$ on $T$.^✦

Single Qubit Gates

The Pauli matrices are $$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) and for a real vector $\vec n = (n_x, n_y, n_z)$ in three dimensions the matrix $\vec n \cdot \vec\sigma$ is $n_x X + n_y Y + n_z Z$. For such a vector and a real angle $\theta$, the rotation matrix $R_{\vec n}(\theta)$ is the complex $2 \times 2$ matrix $$R_{\vec n}(\theta) = \exp\left(-\frac{i\theta}{2}\, \vec n \cdot \vec\sigma\right),$$(2)^✦ and for a unit vector $\hat n$ it is the rotation $R_{\hat n}(\theta)$ by $\theta$ about the axis $\hat n$. The rotations about the coordinate axes are the cases $\hat n = (1, 0, 0)$, $(0, 1, 0)$ and $(0, 0, 1)$ of (2): $$R_x(\theta) = e^{-i\theta X/2}, \qquad R_y(\theta) = e^{-i\theta Y/2}, \qquad R_z(\theta) = e^{-i\theta Z/2}.$$(3) The Hadamard matrix is $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}.$$(4)^✦

The Pauli $X$ gate, the quantum NOT, is the unitary of the qubit whose matrix in the computational basis is $X$ of (1), and the Hadamard gate $H$ is the unitary of the qubit whose matrix is (4). For a real angle $\theta$, the rotation gates $R_x(\theta)$, $R_y(\theta)$ and $R_z(\theta)$ are the unitaries of the qubit whose matrices in the computational basis are those of (3).

Controlled Gates

For a unitary $U$ of a quantum system $S$, the controlled gate $C(U)$ is the unitary of the composite of a control qubit with the target $S$ given by $$C(U) = \lvert 0\rangle\langle 0\rvert \otimes 1 + \lvert 1\rangle\langle 1\rvert \otimes U,$$(5)^✦ with $\lvert 0\rangle\langle 0\rvert$ and $\lvert 1\rangle\langle 1\rvert$ the projectors onto the computational basis states of the control. The CNOT gate is the controlled gate $C(X)$ of two qubits, with the Pauli $X$ gate acting on the target.^✦

The Claim

What Is Checked

The two equalities are stated over the controlled gate $C(U)$ of (5), with the rotation gates $R_x(\theta)$ and $R_y(\theta)$ as $U$ and with the Pauli $X$ gate as $U$ in the CNOT, and over the gates $1 \otimes H$, $1 \otimes R_y$ and $1 \otimes R_z$ on the target, composed one after another as unitaries of two qubits.

The library proves that the controlled gate $C(U)$ is unitary for every unitary $U$ of every quantum system, $C(U)^\dagger C(U) = C(U) C(U)^\dagger = 1$.^✦ The product $U \otimes V$ and the composite $UV$ of two unitaries are again unitary, and so is each single qubit gate, since its matrix is.