The Exercise

In a spin flip, a qubit in the state $\rho$ interacts with an environment, a second qubit prepared in the state $|0\rangle$. The interaction either applies the Pauli matrix $X$ to the qubit and leaves the environment alone, or applies the Pauli matrix $Y$ to the qubit and $X$ to the environment, the two alternatives superposed with equal amplitudes. The environment is then discarded, and what remains is an operation $\mathcal{E}$ on the qubit alone. The exercise asks for its operator sum representation: operators $E_k$ on the qubit with $\mathcal{E}(\rho) = \sum_k E_k \rho E_k^\dagger$.

A Qubit and Its Environment

The library defines the operation in the computational basis, where an operator on a qubit is a complex $2 \times 2$ matrix. For $i \in \{0, 1\}$, the computational basis ket $|i\rangle$ is the vector of $\mathbb{C}^2$ with entry $1$ in position $i$ and $0$ in the other.^✦ For $i, j \in \{0, 1\}$, the outer product $|i\rangle\langle j|$ is the complex $2 \times 2$ matrix obtained by multiplying the column $|i\rangle$ by the row $\langle j|$, whose entries are the complex conjugates of those of $|j\rangle$.^✦ The environment starts in the state $|0\rangle\langle 0|$.

The Pauli matrices in the interaction are the identity $I$ and the matrices $X$ and $Y$: $$I = \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix}, \qquad X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}.$$(1) Both terms of the interaction carry the amplitude $$c = \frac{1}{\sqrt{2}}.$$(2)^✦ The spin flip interaction $U$ is the operator on the joint space $\mathbb{C}^2 \otimes \mathbb{C}^2$ of the qubit and the environment, with the qubit’s factor first, given by $$U = c\, X \otimes I + c\, Y \otimes X.$$(3)^✦

The partial trace over the environment, $\operatorname{tr}_E$, is the linear map that takes a matrix $M$ on the joint space of a system and a finite dimensional environment, with rows and columns labelled by pairs $(i, e)$ of a system label $i$ and an environment label $e$, to the matrix on the system with entries $$(\operatorname{tr}_E M)_{ij} = \sum_{e} M_{(i,e),(j,e)}.$$(4)^✦

The spin flip operation $\mathcal{E}$ is the map on complex $2 \times 2$ matrices that sends $\rho$ to $$\mathcal{E}(\rho) = \operatorname{tr}_E\bigl( U (\rho \otimes |0\rangle\langle 0|) U^\dagger \bigr).$$(5)^✦

The Claim

The spin flip elements $E_0$ and $E_1$ are the complex $2 \times 2$ matrices $X$ and $Y$, each scaled by the amplitude $c$: $$E_0 = c\, X, \qquad E_1 = c\, Y.$$(6)^✦

What Is Checked

The claim is stated over the spin flip operation (5), which is built from the interaction (3), the environment’s state $|0\rangle\langle 0|$ and the partial trace (4), and over the elements (6); the Pauli matrices (1) and the amplitude (2) enter both sides. What the library proves about these constructions is the equality (7), as an identity of complex $2 \times 2$ matrices that holds for every $\rho$.