The Exercise

Two qubits are given, a control and a target. The controlled NOT (CNOT) gate flips the target exactly when the control is $\lvert 1 \rangle$; the controlled $Z$ gate applies the phase flip $Z$ to the target exactly when the control is $\lvert 1 \rangle$. The exercise asks for a CNOT gate made of one controlled $Z$ gate and two Hadamard gates, with the control and the target qubits specified. The library’s answer is an equality of two unitaries of a pair of qubits.

Two Qubits

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$, fixed physically up to a global phase.^✦ 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 whose state space is $\mathbb{C}^2$.^✦ The 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$.^✦ The exercise takes place on the composite system of two qubits, the first factor the control and the second the target.

Unitaries and 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$.^✦ 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$, whose operator is $UV$: first $V$ acts, then $U$.^✦ When $U$ is a unitary of $S$ and $V$ one of a second system $T$, the product unitary $U \otimes V$ is the unitary of $S \otimes T$ whose operator is the tensor product of the two operators.^✦ Taking the identity evolution for the first factor gives the gate $1 \otimes V$ on the last factor, which applies $V$ to $T$ and leaves $S$ alone.^✦

The Hadamard gate $H$, the Pauli $X$ or quantum NOT, and the Pauli $Z$ or phase flip are the unitaries of the qubit whose operators, in the basis $\lvert 0 \rangle, \lvert 1 \rangle$, are the matrices $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}, \qquad X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.$$(1)

For a unitary $U$ of a system $S$, the controlled gate $C(U)$ is the unitary of the composite system of a control qubit and the target $S$ with operator $$C(U) = \lvert 0 \rangle\langle 0 \rvert \otimes 1 + \lvert 1 \rangle\langle 1 \rvert \otimes U .$$(2)^✦ The CNOT gate is $C(X)$, and the controlled $Z$ gate, written $\mathrm{CZ}$, is $C(Z)$; both are unitaries of two qubits.

The Claim

What Is Checked

The claim is stated over the controlled gate (2) with target $X$ on the left and target $Z$ on the right, and over the gate $1 \otimes H$ on the target, composed one after another.

The library proves that the operator (2) is unitary for every unitary $U$ of every system, $C(U)^\dagger C(U) = C(U) C(U)^\dagger = 1$.^✦ It proves as well that a unitary after a unitary is unitary, that the tensor product of two unitaries is unitary, and that the three matrices of (1) are unitary.