The Exercise

A circuit acts on two qubits, a control and a target. The gate $R_k$ is the phase gate with angle $2\pi/2^k$: it leaves $|0\rangle$ alone and multiplies $|1\rangle$ by $e^{2\pi i/2^k}$. The controlled $R_k$ gate applies $R_k$ to the target when the control is $|1\rangle$ and leaves the target alone when the control is $|0\rangle$. The exercise is to build this gate from controlled NOT (CNOT) gates, which flip the target when the control is $|1\rangle$, and gates on a single qubit.

The library states one such circuit for every $k$, with two CNOT gates, as an equality of unitaries of the two qubits.

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 vector of unit norm in the state space of $S$, $\lVert\psi\rVert = 1$, determined physically up to a global phase.^✦ 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 .$$(1)^✦ For two unitaries $U$ and $V$ of $S$, the product $UV$ is the unitary of $S$ that applies $V$ first and then $U$, so a circuit is the product of its gates with the last gate on the left.^✦

The Qubit

The qubit is the quantum system whose state space is $\mathbb{C}^2$, the two dimensional complex Euclidean space.^✦ The computational basis states $|0\rangle$ and $|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$.^✦ 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},$$(2) 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 a real vector $\vec n$ and a real angle $\theta$, the rotation operator $R_{\vec n}(\theta)$ about $\vec n$ is the matrix exponential $$R_{\vec n}(\theta) = \exp\left(-\frac{i\theta}{2}\, \vec n \cdot \vec\sigma\right),$$(3)^✦ written $R_{\hat n}(\theta)$ when the axis is a unit vector $\hat n$. About the axis $\hat z = (0, 0, 1)$ it is $R_z(\theta) = e^{-i\theta Z/2}$.^✦

A gate on the qubit is a unitary of the qubit, read off from its matrix in the computational basis: $X$ gives the Pauli $X$ gate, the quantum NOT, and $R_z(\theta)$ gives the rotation gate $R_z(\theta)$. For a real angle $\alpha$ the phase gate $P(\alpha)$ is diagonal in the computational basis, $$P(\alpha) = \begin{pmatrix} 1 & 0 \\ 0 & e^{i\alpha} \end{pmatrix} .$$(4)^✦ The gate $R_k$ of the exercise is $P(2\pi/2^k)$.

Two Qubits

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$.^✦ For unitaries $U$ of $S$ and $V$ of $T$, the product unitary $U \otimes V$ of $S \otimes T$ is the tensor product of the two operators.^✦ A gate on $S$ alone is $U \otimes 1$, with the identity evolution $1$ on $T$, and a gate on $T$ alone is $1 \otimes V$.

For a unitary $U$ of a system $S$, the controlled gate $C(U)$ is the unitary of $\mathrm{qubit} \otimes S$, a control qubit and a target $S$, with $$C(U) = |0\rangle\langle 0| \otimes 1 + |1\rangle\langle 1| \otimes U ,$$(5)^✦ where $|0\rangle\langle 0|$ and $|1\rangle\langle 1|$ project onto the basis states of the control. The CNOT gate is $C(X)$, the controlled NOT on two qubits, and for a real angle $\varphi$ the controlled phase gate is $C(P(\varphi))$.

The Claim

What Is Checked

The claim is stated over unitaries of the two qubits, the composite system $\mathrm{qubit} \otimes \mathrm{qubit}$.

About these constructions the library proves that each is a unitary. The controlled gate (5) satisfies (1) for every unitary $U$ of every system; $P(\alpha)$ is unitary because its diagonal entries have unit modulus, and $X$ and $R_z(\theta)$ because their matrices are.