The Exercise

The five qubit code encodes one qubit in five physical qubits and corrects an arbitrary error on any single one of them.

Take a code that encodes $k$ qubits in $n$ and corrects errors on up to $t$ qubits. The errors to consider are the Pauli errors, tensor products of $I$, $X$, $Y$ and $Z$ with at most $t$ factors other than $I$; there are $\binom{n}{j}3^j$ of them with exactly $j$ such factors, since each of the $j$ qubits carries $X$, $Y$ or $Z$. The quantum Hamming bound is $$\sum_{j=0}^{t} \binom{n}{j} 3^j \, 2^k \le 2^n .$$(1) A code saturates it when the two sides are equal.

Exercise 10.50 asks to show that the five qubit code saturates the bound.^✦

Pauli Strings

A Pauli string $g$ on $n$ qubits assigns to each qubit $i$ an index $g_i \in \{0,1,2,3\}$ and stands for the Pauli error $\sigma_{g_1} \otimes \cdots \otimes \sigma_{g_n}$, with $\sigma_0 = I$, $\sigma_1 = X$, $\sigma_2 = Y$ and $\sigma_3 = Z$.

The support of a Pauli string $g$ on $n$ qubits is the set of the qubits on which its factor is not the identity, $$\operatorname{supp} g = \{\, i : g_i \neq 0 \,\},$$(2)^✦ and the number of qubits in it, $|\operatorname{supp} g|$, is the weight of $g$.

The set $\mathcal{P}_{n,c}$ of $c$ local Pauli strings on $n$ qubits is the set of Pauli strings on $n$ qubits of weight at most $c$: $$\mathcal{P}_{n,c} = \{\, g : |\operatorname{supp} g| \le c \,\}.$$(3)^✦

The left side $H(n,k,t)$ of the quantum Hamming bound, for a code of $k$ qubits in $n$ that corrects errors on up to $t$ qubits, is the number of Pauli strings of weight at most $t$ on $n$ qubits times $2^k$: $$H(n,k,t) = |\mathcal{P}_{n,t}| \, 2^k .$$(4)^✦ It is the left side of (1), with the Pauli errors counted as strings rather than by weight.

The Claim

What Is Checked

The claim is stated over the left side $H$ of (4), the count of the Pauli strings of weight at most $t$, the weight of a string being the size of its support (2). What the library proves about these constructions is the equality (5) for the parameters of the five qubit code.