The Exercise

A state of a single qubit is given by its Bloch vector $\vec r$, a real vector in three dimensions of length at most one. A rotation gate $R_{\hat n}(\theta)$ is fixed by a unit vector $\hat n$ and an angle $\theta$. The exercise asks to show that applying the gate to the qubit turns its Bloch vector through the angle $\theta$ about the axis $\hat n$ in ordinary space.

The library states this as an equality between two states of the qubit: the state after the gate, and the state whose Bloch vector is the rotated one.

The Qubit

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space, and any such space $H$ is the state space of a system. The qubit is the system whose state space is $\mathbb{C}^2$.^✦

A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$.^✦ A unitary $U$ of $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = I$.^✦ Under $U$ a state $\rho$ of $S$ evolves to the state $$\rho \mapsto U \rho U^\dagger .$$(1)^✦

Bloch States

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},$$(2) and 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$. The Bloch matrix of a real vector $\vec r$ in three dimensions is $$\tfrac12 \left( I + \vec r \cdot \vec\sigma \right).$$(3)^✦

The Bloch state $\rho_{\vec r}$ of a real vector $\vec r$ of length $|\vec r| \le 1$ is the state of the qubit whose matrix is the Bloch matrix (3).^✦

Rotations

For a real vector $\vec n$ in three dimensions and a real angle $\theta$, the rotation gate $R_{\vec n}(\theta)$ is the unitary of the qubit whose matrix is the rotation operator $$R_{\vec n}(\theta) = \exp\left( -\frac{i\theta}{2}\, \vec n \cdot \vec\sigma \right).$$(4)^✦ For a unit vector $\hat n$ the gate is written $R_{\hat n}(\theta)$.

In ordinary space, for real vectors $\vec n$ and $\vec v$ in three dimensions and an angle $\theta$, the vector $\mathcal{R}_{\vec n}(\theta)\, \vec v$ is $$\mathcal{R}_{\vec n}(\theta)\, \vec v = \cos\theta\, \vec v + \sin\theta\, \vec n \times \vec v + (1 - \cos\theta)(\vec n \cdot \vec v)\, \vec n .$$(5)^✦ When $\vec n$ is a unit vector $\hat n$, this is Rodrigues’ formula: $\mathcal{R}_{\hat n}(\theta)\, \vec v$ is $\vec v$ rotated through the angle $\theta$ about the axis $\hat n$.

The Claim

What Is Checked

The claim is stated over the qubit and its Bloch states, built from the Pauli matrices (2) through the Bloch matrix (3); over the rotation gate (4) as a unitary of the qubit and the evolution (1) it drives; and over the rotation of space (5).

The library proves what makes both sides of (6) states of the qubit. The Bloch matrix of $\vec r$ is positive exactly when $|\vec r| \le 1$, and its trace is one, so $\rho_{\vec r}$ is a state. The rotation operator (4) is a unitary matrix, so the gate is a unitary of the qubit, and conjugating a state by a unitary gives a state, so the evolved state (1) is again a state. For a unit axis the rotation (5) keeps lengths, $|\mathcal{R}_{\hat n}(\theta)\, \vec v| = |\vec v|$, so the rotated Bloch vector lies in the unit ball and the right side of (6) is a state.