The Exercise

Take $l$ Pauli operators $g_1, \dots, g_l$ on $n$ qubits, each a tensor product of single qubit Paulis $I$, $X$, $Y$ and $Z$, one on each qubit, and suppose that the rows of their check matrix, the binary matrix with one row for each $g_j$, are linearly independent over $\mathbb{Z}_2$. Fix one of them, $g_i$. Then there is a Pauli operator $p$ on the same qubits whose conjugation turns $g_i$ into $-g_i$ and leaves every other $g_j$ as it is.^✦

On three qubits, take $g_1 = Z \otimes Z \otimes I$ and $g_2 = I \otimes Z \otimes Z$.

Pauli Strings

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

A Pauli string on $n$ qubits is an operator $\sigma_{a_1} \otimes \cdots \otimes \sigma_{a_n}$ on the $n$ qubits, the tensor product of one Pauli matrix $\sigma_{a_k}$ for each qubit $k$, with $a_k \in \{0, 1, 2, 3\}$.^✦ With rows and columns labelled by strings of bits, its matrix has the entries $$\langle b_1 \cdots b_n |\, \sigma_{a_1} \otimes \cdots \otimes \sigma_{a_n} \,| b_1' \cdots b_n' \rangle = \prod_{k=1}^{n} (\sigma_{a_k})_{b_k b_k'} .$$(2)^✦

Check Rows

The $X$ bit $x_a$ of a Pauli matrix $\sigma_a$ is $1$ for $X$ and $Y$ and $0$ for $I$ and $Z$^✦; its $Z$ bit $z_a$ is $1$ for $Y$ and $Z$ and $0$ for $I$ and $X$.^✦ The check bits of a Pauli matrix $\sigma_a$ are the pair $(x_a, z_a)$ of its $X$ bit and its $Z$ bit, read in $\mathbb{Z}_2$.^✦

The check row $r(g)$ of a Pauli string $g = \sigma_{a_1} \otimes \cdots \otimes \sigma_{a_n}$ is the row of $2n$ bits in $\mathbb{Z}_2$ that lists the $X$ bits of its factors, qubit by qubit, and then their $Z$ bits: $$r(g) = \left( x_{a_1}, \dots, x_{a_n} \,\middle|\, z_{a_1}, \dots, z_{a_n} \right).$$(3) The check matrix of $g_1, \dots, g_l$ has the rows $r(g_1), \dots, r(g_l)$.

The Claim

What Is Checked

The claim is stated over Pauli strings on $n$ qubits, the tensor products (2) of the Pauli matrices (1), and over the check rows (3) of those strings, built from the check bits of their factors. What the library proves about these constructions is the existence of the Pauli string $p$ in (4).