The Exercise

A single spin in a static field along the $\hat z$ axis precesses freely about that axis. In nuclear magnetic resonance this precession is undone with pulses that turn the spin by $180^\circ$ about the $\hat x$ axis. The exercise asks what the free evolution becomes when it is sandwiched between two applications of the Pauli matrix $X$, the spin flip about the $\hat x$ axis, and between two such pulses. The library answers with two identities between $2 \times 2$ complex matrices, one for each sandwich.

Precession and Pulses

The Pauli matrices are the $2 \times 2$ complex 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)

For real numbers $a$ and $t$, the free precession $e^{-iaZt}$ is the $2 \times 2$ complex matrix obtained as the matrix exponential of $-iat$ times $Z$, $$e^{-iaZt} = \exp\bigl(-i\,at\,Z\bigr),$$(2)^✦ the evolution over the time $t$ under the Hamiltonian $aZ$.

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 of the Pauli matrices with the components of $\vec n$ as coefficients, $$\vec n \cdot \vec\sigma = n_x X + n_y Y + n_z Z.$$(3)^✦ The rotation operator $R_{\vec n}(\theta)$ about the axis $\vec n$ by a real angle $\theta$ is the $2 \times 2$ complex matrix $$R_{\vec n}(\theta) = \exp\Bigl(-\frac{i\theta}{2}\,\vec n \cdot \vec\sigma\Bigr),$$(4)^✦ written $R_{\hat n}(\theta)$ when the axis is a unit vector $\hat n$.

The rotation $R_x(\theta)$ about the $\hat x$ axis is the rotation (4) with axis $\hat n = (1, 0, 0)$, the matrix $\exp(-i\theta X/2)$.^✦ The refocusing pulse $R_x^2$ is the rotation by $180^\circ$ about the $\hat x$ axis, $$R_x^2 = R_x(\pi) = \exp\Bigl(-\frac{i\pi}{2}\,X\Bigr).$$(5)^✦

The Claim

The free precession for the time $-t$ is $e^{iaZt}$.

What Is Checked

The claim is stated over two matrix exponentials of $2 \times 2$ complex matrices: the free precession (2), built on the Pauli matrix $Z$ of (1), and the refocusing pulse (5), which is the general rotation (4) at the axis $\hat x$ and the angle $\pi$, built on $X$ through the matrix $\vec n \cdot \vec\sigma$ of (3).

About these constructions the library proves the identities (6) and (7) for every real $a$ and $t$, as exact equalities of matrices, the global sign of the second included.