The Exercise

Two qubits are in a state $\rho_1$ that is diagonal in the computational basis $|00\rangle$, $|01\rangle$, $|10\rangle$, $|11\rangle$, with populations $a$, $b$, $c$, $d$.^✦ A circuit $P$ of two controlled NOT (CNOT) gates acts on them: first a CNOT with the first qubit as control, then a CNOT with the second qubit as control.^✦ The exercise is to show that the state $P\rho_1P^\dagger$ after the circuit, and the state $P^\dagger\rho_1P$ after its adjoint $P^\dagger$, are again diagonal: the population of $|00\rangle$ stays in place, and those of the other three basis states are permuted cyclically, in one sense under $P$ and in the other under $P^\dagger$.

Two Qubits and Two Gates

All matrices below are written in the computational basis, in the order above. The CNOT gate $C_{12}$, with control on the first qubit and target on the second, is the $4\times4$ matrix that exchanges $|10\rangle$ and $|11\rangle$ and leaves $|00\rangle$ and $|01\rangle$ in place: $$C_{12} = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix}.$$(1)^✦ The CNOT gate $C_{21}$, with control on the second qubit and target on the first, is the $4\times4$ matrix that exchanges $|01\rangle$ and $|11\rangle$ and leaves $|00\rangle$ and $|10\rangle$ in place: $$C_{21} = \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 0 \end{pmatrix}.$$(2)^✦

The circuit $P$ on the two qubits is the product of the two gates: $$P = C_{21}\, C_{12}.$$(3)^✦

For any four complex numbers $a$, $b$, $c$, $d$, not only the populations of a state, the diagonal matrix $\rho_1$ is the $4\times4$ matrix with $a$, $b$, $c$, $d$ on its diagonal, in the order of the basis, and zeros elsewhere: $$\rho_1 = \operatorname{diag}(a, b, c, d).$$(4)^✦ The permuted matrices $\rho_2$ and $\rho_3$ are the diagonal matrices with the same four numbers in two other orders: $$\rho_2 = \operatorname{diag}(a, c, d, b),$$(5) $$\rho_3 = \operatorname{diag}(a, d, b, c).$$(6)

The Claim

What Is Checked

The claim is stated over the circuit $P$ of (3), built from the two CNOT matrices (1) and (2), and over the diagonal matrices $\rho_1$, $\rho_2$, $\rho_3$. What the library proves about these constructions is the pair of identities (7) and (8), as equalities of $4\times4$ complex matrices.