The Exercise

A controlled NOT (CNOT) gate acts on two qubits: it flips the second, the target, exactly when the first, the control, is $|1\rangle$ .^✦ That description is made in the computational basis $|0\rangle, |1\rangle$ . The exercise asks how the same gate looks in the basis of the eigenstates $|+\rangle$ and $|-\rangle$ of the Pauli operator $X$ : what it does to the four products of these states, and what it does to the computational basis once a Hadamard gate is applied to each qubit before and after it. The library answers with five equalities between pure states of two qubits.

Two Qubits

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

A pure state $|\psi\rangle$ of a quantum system $S$ is a unit vector in the state space of $S$ .^✦ For pure states $|\psi\rangle$ of $S$ and $|\varphi\rangle$ of $T$ , the product state $|\psi\rangle \otimes |\varphi\rangle$ is the pure state of $S \otimes T$ whose vector is the tensor product of the two vectors.^✦ For two qubits we write $|a, b\rangle$ for $|a\rangle \otimes |b\rangle$ .

The basis state $|i\rangle$ of the qubit, for a bit $i \in \{0, 1\}$ , is the pure state whose vector is the $i$ th standard basis vector of $\mathbb{C}^2$ .^✦ The states $|+\rangle$ and $|-\rangle$ of the qubit are the pure states whose vectors are $|\pm\rangle = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 \\ \pm 1 \end{pmatrix} = \frac{|0\rangle \pm |1\rangle}{\sqrt{2}}.$ (1)

Gates

A unitary $U$ of a quantum system $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$ ; it carries a pure state $|\psi\rangle$ of $S$ to the pure state $U|\psi\rangle$ . For unitaries $U$ and $V$ of $S$ , the composite $UV$ is the unitary of $S$ that applies $V$ first and then $U$ .^✦ The product unitary $U \otimes V$ of a unitary $U$ of $S$ and a unitary $V$ of $T$ is the unitary of $S \otimes T$ whose operator is the tensor product of the two operators.^✦

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

For a unitary $U$ of a system $S$ , the controlled gate $C(U)$ is the unitary of the composite of a control qubit with the target $S$ given by $C(U) = |0\rangle\langle 0| \otimes 1 + |1\rangle\langle 1| \otimes U.$ (3)^✦ The CNOT gate is the controlled gate $C(X)$ of two qubits.^✦

The Claim

Theorem 1. On products of the states $|+\rangle$ and $|-\rangle$ the CNOT gate acts with control and target exchanged: $\mathrm{CNOT}\,|-,-\rangle = |+,-\rangle,$ (4)^✦ $\mathrm{CNOT}\,|-,+\rangle = |-,+\rangle,$ (5)^✦ $\mathrm{CNOT}\,|+,-\rangle = |-,-\rangle,$ (6)^✦ $\mathrm{CNOT}\,|+,+\rangle = |+,+\rangle.$ (7)^✦ For bits $c$ and $t$ , with $c \oplus t$ their sum modulo $2$ , the product unitary $H \otimes H$ applied before and after the CNOT gate gives a controlled NOT with the second qubit as control and the first as target: $(H \otimes H)\, \mathrm{CNOT}\, (H \otimes H)\, |c, t\rangle = |c \oplus t, t\rangle.$ (8)^✦

What Is Checked

The claim is stated over the CNOT gate, which is the controlled gate (3) with the Pauli $X$ gate as $U$ , and over the composite of that gate with the product unitary $H \otimes H$ . The states it is stated over are the product states of two qubits built from the basis states $|0\rangle, |1\rangle$ and from the states (1).

The library proves that $C(U)$ is unitary for every unitary $U$ of a system $S$ .^✦ It proves the same of the matrices (2), of product unitaries and of composites, and it proves that the vectors (1) have unit norm, as do the tensor product of two unit vectors and the image of a unit vector under a unitary.