The Exercise

On a single qubit, the rotations of the Bloch sphere by an angle $\theta$ about the $z$ and $y$ axes have, in the computational basis $|0\rangle, |1\rangle$, the matrices $$R_z(\theta) = \begin{pmatrix} e^{-i\theta/2} & 0 \\ 0 & e^{i\theta/2} \end{pmatrix}, \qquad R_y(\theta) = \begin{pmatrix} \cos\frac{\theta}{2} & -\sin\frac{\theta}{2} \\[4pt] \sin\frac{\theta}{2} & \cos\frac{\theta}{2} \end{pmatrix}.$$(1) The exercise is to show that every unitary operator $U$ on the state space of the qubit is, up to a global phase $e^{i\alpha}$, a product of three of these rotations, $U = e^{i\alpha} R_z(\beta) R_y(\gamma) R_z(\delta)$ for some real numbers $\alpha$, $\beta$, $\gamma$ and $\delta$.^✦

A Phase and Three Rotations

The library states the exercise for matrices in the computational basis. A unitary matrix $U$ is a $2\times 2$ complex matrix with $U^\dagger U = I$.

For real numbers $\alpha$, $\beta$, $\gamma$ and $\delta$, the matrix $M(\alpha,\beta,\gamma,\delta)$ is the $2\times 2$ complex matrix $$M(\alpha,\beta,\gamma,\delta) = \begin{pmatrix} e^{i(\alpha - \beta/2 - \delta/2)} \cos\frac{\gamma}{2} & -e^{i(\alpha - \beta/2 + \delta/2)} \sin\frac{\gamma}{2} \\[4pt] e^{i(\alpha + \beta/2 - \delta/2)} \sin\frac{\gamma}{2} & e^{i(\alpha + \beta/2 + \delta/2)} \cos\frac{\gamma}{2} \end{pmatrix}.$$(2)^✦

The Claim

What Is Checked

The claim is stated over the matrix $M(\alpha,\beta,\gamma,\delta)$ of (2) and over the unitary $2\times 2$ complex matrices. What the library proves about them is the claim (3).