The Theorem

Theorem 10.6 of Nielsen and Chuang concerns the unitaries on $n$ qubits that map the Pauli group $G_n$, the group generated by tensor products of Pauli matrices and phases, to itself under conjugation; these unitaries form the normalizer $N(G_n)$. The theorem is about how many elementary gates such a unitary needs.

The Pauli Group

The Pauli matrices are the four complex $2 \times 2$ matrices $\sigma_0, \dots, \sigma_3$: the identity and the matrices $X$, $Y$ and $Z$, $$\sigma_0 = I, \qquad \sigma_1 = X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad \sigma_2 = Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \qquad \sigma_3 = Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.$$(1)^✦

For a choice $a = (a_1, \dots, a_n)$ of one Pauli matrix for each of $n$ qubits, the Pauli string $\sigma_a$ is the operator on the $n$ qubits whose matrix element between computational basis states $|x\rangle$ and $|y\rangle$, with $x, y \in \{0,1\}^n$, is the product of the single qubit entries: $$\sigma_a = \sigma_{a_1} \otimes \cdots \otimes \sigma_{a_n}, \qquad \langle x | \sigma_a | y \rangle = \prod_{k=1}^{n} (\sigma_{a_k})_{x_k y_k}.$$(2)^✦

The Pauli group $G_n$ on $n$ qubits consists of the operators, with $s$ an integer modulo 4 and $a$ a choice of one Pauli matrix for each qubit, $$g = i^s \sigma_a .$$(3)^✦

The Normalizer

An operator $U$ on $n$ qubits lies in the normalizer $N(G_n)$ of the Pauli group if it is unitary and, for every $g \in G_n$, there is a $g' \in G_n$ with $$U g U^\dagger = g' .$$(4)^✦

Clifford Circuits

An elementary Clifford gate on $n$ qubits is a Hadamard gate $H$ on a qubit $j$, a phase gate $S$ on a qubit $j$, or a controlled NOT gate with control qubit $j$ and target qubit $k$ distinct from $j$.^✦ Its operator acts as $H$, as $S$ or as the controlled NOT on the qubits the gate names, and as the identity on the others.^✦

A Clifford circuit $C$ on $n$ qubits is a finite sequence of elementary Clifford gates.^✦ If its gates have the operators $V_1, \dots, V_m$ in the order of the sequence, the operator of $C$ is their product and its length $|C|$ is its number of gates, $$U_C = V_1 V_2 \cdots V_m , \qquad |C| = m ,$$(5) so that the last gate of the sequence acts first.

The Claim

What Is Checked

The claim is stated over the normalizer $N(G_n)$, whose condition (4) runs over the Pauli group operators (3) built from the matrices (1), and over the operator $U_C$ of a Clifford circuit, the product (5) of its Hadamard, phase and controlled NOT gates.

What the library proves about these constructions is the decomposition (6) itself.