The Exercise

On a single qubit, take the $\pi/8$ gate $T$ and apply a Hadamard gate $H$ before and after it. The exercise is to show that the result, $HTH$, is the rotation $R_x(\pi/4)$ by $\pi/4$ about the $x$ axis, up to a global phase.

The Gates

The Hadamard gate $H$ and the $\pi/8$ gate $T$ are the complex $2 \times 2$ matrices, in the computational basis $\{|0\rangle, |1\rangle\}$, $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}, \qquad T = \begin{pmatrix} 1 & 0 \\ 0 & e^{i\pi/4} \end{pmatrix}.$$(1)

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}.$$(2) For a real vector $\vec{n} = (n_x, n_y, n_z)$ in three dimensions, $\vec{n} \cdot \vec{\sigma}$ is the complex $2 \times 2$ matrix $n_x X + n_y Y + n_z Z$.^✦

For a real vector $\vec{n}$ in three dimensions and a real angle $\theta$, the rotation operator $R_{\vec{n}}(\theta)$ about $\vec{n}$ by $\theta$ is the complex $2 \times 2$ matrix $$R_{\vec{n}}(\theta) = \exp\Bigl(-\frac{i\theta}{2}\, \vec{n} \cdot \vec{\sigma}\Bigr),$$(3)^✦ written $R_{\hat{n}}(\theta)$ when the axis is a unit vector $\hat{n}$. The rotation $R_x(\theta)$ about the $x$ axis by $\theta$ is the one with axis $\hat{n} = (1, 0, 0)$, for which $\hat{n} \cdot \vec{\sigma} = X$: $$R_x(\theta) = \exp\bigl(-i\theta X/2\bigr).$$(4)^✦

The Claim

The library states the exercise with the global phase fixed.

What Is Checked

The claim is stated over the gates $H$ and $T$ of (1) and the rotation $R_x(\pi/4) = \exp(-i\pi X/8)$, the case $\theta = \pi/4$ of (4). What the library proves about them is the identity (5).