The Exercise

A qubit evolves under a term $\vec{c} \cdot \vec{\sigma}$ of its Hamiltonian, where $\vec{c}$ is a real vector in three dimensions and $\vec{\sigma}$ is the Pauli vector. Between two pulses of a Pauli operator $P$, the term acts as its conjugate $P(\vec{c} \cdot \vec{\sigma})P$, since $P$ is unitary and squares to the identity. Divide a stretch of free evolution into four equal pieces, leave the first alone, and bracket the other three with pulses of the Pauli operators $X$, $Y$ and $Z$ in turn. To first order in the length of the stretch, the term then acts through the mean of itself and its three conjugates. The exercise is to show that this mean vanishes for every $\vec{c}$, so that the term is refocused.^✦

In a second form of the exercise, the fourth piece is bracketed by $Y$ pulses and these in turn by $X$ pulses, so that pulses about two axes suffice. The mean must vanish in this sequence as well.^✦

The Pauli Matrices

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)

For a real vector $\vec{c} = (c_x, c_y, c_z)$ in three dimensions, the matrix $\vec{c} \cdot \vec{\sigma}$ is the complex $2 \times 2$ matrix $$\vec{c} \cdot \vec{\sigma} = c_x X + c_y Y + c_z Z,$$(2)^✦ with $\vec{\sigma} = (X, Y, Z)$ the Pauli vector.

The Claim

What Is Checked

The claim is stated over the Pauli matrices $X$, $Y$ and $Z$, given by their entries in (1), and over the matrix $\vec{c} \cdot \vec{\sigma}$ of (2). The library proves the identities (3) and (4) for these matrices and for every real vector $\vec{c}$.