The Exercise

One qubit is in an unknown pure state $|\psi\rangle$ and a second is prepared in $|0\rangle$. Two controlled NOT gates swap them: one controlled by the first qubit flips the second, then one controlled by the second flips the first, and the pair ends in $|0\rangle \otimes |\psi\rangle$.^✦

The same transfer can be made in either of two circuits, each with a single controlled NOT, a Hadamard gate, a measurement of the first qubit in the computational basis and a Pauli gate on the second qubit applied when the outcome is $1$. In the first, the controlled NOT is followed by a Hadamard on the first qubit, and the correction is $Z$. In the second, a Hadamard on the second qubit precedes a NOT on the first controlled by it, and the correction is $X$. Whichever outcome $m$ is observed, the first qubit is left in $|m\rangle$ and the second carries $|\psi\rangle$.

Two Qubits

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $S \otimes T$ of two systems $S$ and $T$ is the system whose state space is the tensor product of their state spaces.^✦ The qubit $Q$ is the two level system whose state space is $\mathbb{C}^2$ itself, and a pair of qubits is the composite system $Q \otimes Q$.^✦

A pure state $|\psi\rangle$ of $S$ is a unit vector in the state space of $S$.^✦ A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$^✦; a pure state $|\psi\rangle$ determines the state $|\psi\rangle\langle\psi|$, the projector onto its vector.^✦ The computational basis states $|0\rangle$ and $|1\rangle$ of $Q$ are the pure states whose vectors are the standard basis vectors $e_0$ and $e_1$ of $\mathbb{C}^2$.^✦ For pure states $|\psi\rangle$ of $S$ and $|\varphi\rangle$ of $T$, the product $|\psi\rangle \otimes |\varphi\rangle$ is the pure state of $S \otimes T$ whose vector is the tensor product of the two vectors.^✦

Gates and Circuits

A unitary $U$ of $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$, where $1$ is the identity operator.^✦ It carries a pure state $|\psi\rangle$ of $S$ to $U|\psi\rangle$^✦, and a state $\rho$ of $S$ to $$U \rho\, U^\dagger .$$(1)^✦

For unitaries $U$ and $V$ of $S$, the unitary $U \circ V = UV$ applies $V$ first and then $U$.^✦ For a unitary $U$ of $S$ and a unitary $V$ of $T$, the product unitary $U \otimes V$ of $S \otimes T$ is the tensor product of the two operators^✦; with the identity unitary $1$, the gate $U \otimes 1$ acts with $U$ on the first factor alone^✦ and $1 \otimes V$ with $V$ on the second.^✦ The SWAP of $S \otimes S$ is the unitary of $S \otimes S$ that exchanges the two factors, $\mathrm{SWAP}(|a\rangle \otimes |b\rangle) = |b\rangle \otimes |a\rangle$.^✦

The Hadamard $H$, the NOT $X$ and the phase flip $Z$ are the unitaries of $Q$ whose matrices in the computational basis are $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}, \qquad X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.$$(2)

For a unitary $U$ of $S$, the controlled gate $C(U)$ is the unitary of $Q \otimes S$, with the qubit as control and $S$ as target, given by $$C(U) = |0\rangle\langle 0| \otimes 1 + |1\rangle\langle 1| \otimes U .$$(3)^✦ The controlled NOT on $Q \otimes Q$ is $\mathrm{CNOT}_{12} = C(X)$, with its control on the first qubit and its target on the second.^✦ The controlled NOT $\mathrm{CNOT}_{21}$ on $Q \otimes Q$, with its control on the second qubit and its target on the first, is the controlled NOT $\mathrm{CNOT}_{12}$ conjugated by the SWAP of the two qubits, $$\mathrm{CNOT}_{21} = \mathrm{SWAP} \circ \mathrm{CNOT}_{12} \circ \mathrm{SWAP} .$$(4)^✦

The swap circuit $W$ of two controlled NOTs and the circuits $W_1$ and $W_2$ with a single controlled NOT are the unitaries of $Q \otimes Q$ $$W = \mathrm{CNOT}_{21} \circ \mathrm{CNOT}_{12},$$(5)^✦ $$W_1 = (H \otimes 1) \circ \mathrm{CNOT}_{12},$$(6)^✦ $$W_2 = \mathrm{CNOT}_{21} \circ (1 \otimes H).$$(7)^✦

Measurement and Correction

A measurement $\{M_i\}$ on $S$ with a finite set of outcomes is a family of measurement operators $M_i$ on the state space of $S$, one for each outcome $i$, satisfying the completeness relation $\sum_i M_i^\dagger M_i = 1$.^✦ Its effects $E_i = M_i^\dagger M_i$ are positive and form the positive operator valued measure (POVM) of the measurement.^✦ On a state $\rho$ of $S$ the outcome $i$ occurs with probability $$p(i) = \mathrm{Tr}(E_i \rho) = \mathrm{Tr}(M_i \rho M_i^\dagger),$$(8)^✦ and when $p(i) \neq 0$ the state after the outcome $i$ is $$\rho_i = \frac{M_i \rho M_i^\dagger}{p(i)} .$$(9)^✦

The projective measurement of $S$ in an orthonormal basis $\{|b_i\rangle\}$ of its state space is the measurement whose operators are the projectors $|b_i\rangle\langle b_i|$.^✦ For a measurement $\{M_i\}$ on $S$ and a further system $T$, the measurement on the first factor of $S \otimes T$ is the measurement with the same outcomes and the operators $M_i \otimes 1$.^✦ The measurement of the control qubit on $Q \otimes S$ is the projective measurement of $Q$ in the computational basis, made on the first factor; its operators are $$P_m = |m\rangle\langle m| \otimes 1, \qquad m \in \{0, 1\}.$$(10)^✦ For a unitary $U$ of $S$, the classically controlled gate $1 \otimes U^m$ is the unitary of $Q \otimes S$ that is the identity when the measured bit $m$ is $0$ and $1 \otimes U$ when it is $1$.^✦

The Claim

What Is Checked

The claim is stated over the pair of qubits $Q \otimes Q$ and the product pure state $|\psi\rangle \otimes |0\rangle$; over the circuits (5), (6) and (7), built from the gates (2), the controlled NOTs and the SWAP; and over the measurement (10) of the control qubit, the state (9) after its outcome and the classically controlled corrections $1 \otimes Z^m$ and $1 \otimes X^m$.

The library proves that $C(U)$ in (3) is unitary for every unitary $U$ of every system, $C(U)^\dagger C(U) = C(U) C(U)^\dagger = 1$, so that $\mathrm{CNOT}_{12}$ and $\mathrm{CNOT}_{21}$ in (4) are unitaries of $Q \otimes Q$.^✦ It proves too that a state conjugated by a unitary as in (1) is again a state, and that the state (9) after an outcome of nonzero probability is a positive operator of unit trace.