The Exercise

On a qubit, the rotation by an angle $\theta$ about the $x$ axis is the operator $R_x(\theta) = \exp(-i\theta X/2)$, the exponential of a multiple of the Pauli matrix $X$.^✦ The exercise asks for this exponential written out as a $2 \times 2$ matrix, with entries given by the cosine and the sine of half the angle.

Rotations About an Axis

The Pauli matrices $X$, $Y$ and $Z$ 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},$$(1) with $i$ the imaginary unit, and $\vec{\sigma} = (X, Y, Z)$ is the Pauli vector.

The matrix $\vec{n} \cdot \vec{\sigma}$ of a real vector $\vec{n} = (n_x, n_y, n_z)$ in three dimensions is the complex $2 \times 2$ matrix $$\vec{n} \cdot \vec{\sigma} = n_x X + n_y Y + n_z Z .$$(2)^✦

The rotation $R_{\vec{n}}(\theta)$ about an axis $\vec{n}$, any real vector in three dimensions, by a real angle $\theta$ is the complex $2 \times 2$ matrix $$R_{\vec{n}}(\theta) = \exp\!\left(-\frac{i\theta}{2}\, \vec{n} \cdot \vec{\sigma}\right),$$(3)^✦ where $\exp$ is the matrix exponential. For a unit vector $\hat{n}$ it is written $R_{\hat{n}}(\theta)$.

The rotation $R_x(\theta)$ about the $x$ axis by a real angle $\theta$ is the rotation about the unit vector $\hat{x} = (1, 0, 0)$: $$R_x(\theta) = R_{\hat{x}}(\theta) .$$(4)^✦ Since $\hat{x} \cdot \vec{\sigma} = X$, this is the operator $\exp(-i\theta X/2)$ of the exercise.

The Claim

What Is Checked

The claim is stated over the rotation $R_x(\theta)$ of (4), hence over the general rotation (3), whose exponent is built from the Pauli matrices (1) through the matrix (2) of the axis.

What the library proves about these constructions is the identity (5), which evaluates the matrix exponential (3) at the axis $\hat{x}$ in closed form for every real angle.