The Exercise

In nuclear magnetic resonance (NMR) the qubits are nuclear spins, and two of them are coupled by the Hamiltonian $H = J Z_1 Z_2$, with $J$ a real coupling constant and $Z_1$, $Z_2$ the Pauli $Z$ of the first and of the second spin. Rotate each spin by $R_z(-\pi/2)$ about the $\hat z$ axis, then let the pair evolve under $H$ for a time $t$, in units with $\hbar = 1$. When $Jt = \pi/4$ the result is the controlled $Z$ gate up to the global phase $e^{i\pi/4}$, and so it acts on every state of the two spins as the controlled $Z$ gate does.

The library states both conclusions as theorems, for all real $J$ and $t$ with $Jt = \pi/4$, over the definitions that follow.

Two Qubits

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ A pure state $|\psi\rangle$ of $S$ is a unit vector in the state space of $S$.^✦ A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$.^✦

The qubit is the two level system whose state space is $\mathbb{C}^2$.^✦ The basis states $|0\rangle$ and $|1\rangle$ of the qubit, its computational basis, are the pure states whose vectors are the standard basis vectors $(1,0)$ and $(0,1)$ of $\mathbb{C}^2$.^✦ The composite system $S \otimes T$ of two systems $S$ and $T$ is the system whose state space is the tensor product of their state spaces.^✦ The two spins form the composite system $\mathrm{qubit} \otimes \mathrm{qubit}$.

Gates

A unitary $U$ of $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$, and the identity evolution is the unitary $1$. Under $U$ a state $\rho$ evolves to the state $U \rho U^\dagger$.^✦ For two unitaries $U$ and $V$ of $S$, $U$ after $V$ is the unitary $UV$: first $V$, then $U$.^✦ For a unitary $U$ of $S$ and a unitary $V$ of $T$, the product unitary $U \otimes V$ of $S \otimes T$ is the unitary whose operator is the tensor product of those of $U$ and $V$.^✦ A gate $U$ on the first factor is $U \otimes 1$, with the identity evolution on $T$, and a gate $V$ on the last factor is $1 \otimes V$. For a real angle $\alpha$, the global phase gate $e^{i\alpha}$ of $S$ is the unitary $e^{i\alpha}\, 1$.^✦

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 with the Pauli vector $\vec\sigma = (X, Y, Z)$, for a real vector $\vec n$ in three dimensions $\vec n \cdot \vec \sigma = n_x X + n_y Y + n_z Z$. The rotation $R_{\vec n}(\theta)$ 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)$ for a unit vector $\hat n$, the rotation about $\hat n$. About $\hat z = (0,0,1)$ it is $R_z(\theta) = e^{-i\theta Z/2}$.^✦ The rotation gate $R_z(\theta)$ is the unitary of the qubit with this matrix in the computational basis, and the Pauli $Z$ gate, the phase flip, is the unitary of the qubit with matrix $Z$.

For a unitary $U$ of $S$, the controlled gate $C(U)$ is the unitary of $\mathrm{qubit} \otimes S$, a control qubit and the target $S$, with operator $$C(U) = |0\rangle\langle 0| \otimes 1 + |1\rangle\langle 1| \otimes U .$$(3)^✦ The controlled $Z$ gate is $CZ = C(Z)$ on two qubits, the first one the control; its matrix in the computational basis is $\mathrm{diag}(1, 1, 1, -1)$.^✦

The Coupling

An observable $A$ of $S$ is a self adjoint operator on the state space of $S$, $A^\dagger = A$.^✦ For observables $A$ of $S$ and $B$ of $T$, the observable $A \otimes B$ of $S \otimes T$ has as operator the tensor product of theirs.^✦ For a real vector $\vec n$, the Pauli observable $\vec n \cdot \vec \sigma$ is the observable of the qubit with that matrix, and for $\hat n = \hat z$ it is the observable $Z$. The coupling Hamiltonian of the two spins with a real coupling constant $J$ is the observable $$H = J\, Z_1 Z_2 = J\, Z \otimes Z .$$(4)^✦

The Hamiltonian propagator of an observable $H$ of $S$, with Planck’s constant $\hbar$, from time $t_1$ to time $t_2$ is the unitary $$U(t_1, t_2) = \exp\bigl[-iH(t_2 - t_1)/\hbar\bigr].$$(5)^✦

For a real coupling constant $J$ and a time $t$, the NMR controlled $Z$ sequence is the unitary of the two spins $$U_{\mathrm{NMR}}(J, t) = U(0, t)\, \bigl(R_z(-\pi/2) \otimes 1\bigr) \bigl(1 \otimes R_z(-\pi/2)\bigr),$$(6)^✦ with $U(0, t) = e^{-iJt\, Z \otimes Z}$ the propagator of (4) from time $0$ to time $t$ at $\hbar = 1$.

The Claim

The phase $e^{i\pi/4}$ cancels between $U_{\mathrm{NMR}}(J,t)$ and $U_{\mathrm{NMR}}(J,t)^\dagger$ in the evolution of a state.

What Is Checked

About these constructions the library proves that every gate in them is unitary: $C(U)$ for every unitary $U$, the propagator (5) of every observable, the rotation gate $R_z(\theta)$, the Pauli $Z$ gate and the global phase gate, and with $U$ and $V$ also $UV$ and $U \otimes V$. It proves that $U \rho U^\dagger$ is again a state, and that $\vec n \cdot \vec \sigma$ and $A \otimes B$ are self adjoint, which makes $J\, Z \otimes Z$ an observable.