The Exercise

A stabilizer code on $n$ qubits whose stabilizer has $n-k$ independent commuting generators $g_1, \dots, g_{n-k}$ encodes $k$ logical qubits. A product $g$ of Pauli matrices on the $n$ qubits is recorded, up to phase, by its row $r(g) = (x \mid z)$ in $\mathbb{Z}_2^{2n}$, with $x_q = 1$ when $g$ acts on qubit $q$ with $X$ or $Y$, and $z_q = 1$ when it acts with $Z$ or $Y$. The rows of the generators make up the check matrix of the code.

The symplectic matrix $\Lambda$ is the $2n \times 2n$ matrix over $\mathbb{Z}_2$ made of $n \times n$ blocks, zero on the diagonal and the identity off it, $$\Lambda = \begin{bmatrix} 0 & I \\ I & 0 \end{bmatrix},$$(1)^✦ so that it exchanges the two halves of a row. The twisted inner product of rows $s = (x \mid z)$ and $t = (x' \mid z')$ is the element of $\mathbb{Z}_2$ $$s \Lambda t^T = s \cdot (\Lambda t^T) = x \cdot z' + z \cdot x'.$$(2)^✦ Two Pauli products $g$ and $g'$ commute when $r(g) \Lambda r(g')^T = 0$ and anticommute when it is $1$.

The exercise starts from a check matrix in standard form, made of blocks given below, and from encoded operators $\bar Z_1, \dots, \bar Z_k$ and $\bar X_1, \dots, \bar X_k$ for the logical qubits, read off those blocks. It asks for four properties of the $\bar X_a$: each commutes with every generator, so it maps the code space to itself^✦; they commute with one another^✦; $\bar X_a$ anticommutes with $\bar Z_a$ and commutes with $\bar Z_b$ for $b \neq a$^✦; and the generators together with $\bar X_1, \dots, \bar X_k$ are independent.^✦

The Check Matrix in Standard Form

The columns of each half of the check matrix are the qubits, which fall into three groups, the first $r$, the next $m$ and the last $k$: $$Q = \{1, \dots, r\} \sqcup \{1, \dots, m\} \sqcup \{1, \dots, k\}, \qquad n = r + m + k.$$(3)^✦ For blocks $u \in \mathbb{Z}_2^r$, $v \in \mathbb{Z}_2^m$ and $w \in \mathbb{Z}_2^k$, the vector $[\,u \;\; v \;\; w\,]$ on $Q$ assembled from them is $$[\,u \;\; v \;\; w\,]_q = \begin{cases} u_q, & q \text{ among the first } r,\\ v_q, & q \text{ among the next } m,\\ w_q, & q \text{ among the last } k. \end{cases}$$(4)^✦

Standard form data $S$ of sizes $r$, $m$, $k$ is a choice of six matrices over $\mathbb{Z}_2$, $$\begin{gathered} A_1 \in \mathbb{Z}_2^{r \times m}, \qquad A_2 \in \mathbb{Z}_2^{r \times k}, \qquad B \in \mathbb{Z}_2^{r \times r},\\ C \in \mathbb{Z}_2^{r \times k}, \qquad D \in \mathbb{Z}_2^{m \times r}, \qquad E \in \mathbb{Z}_2^{m \times k}. \end{gathered}$$(5)^✦

Write $e_i$ for the $i$th unit vector and $M_i$ for row $i$ of a matrix $M$; the bar in a row $[\,\cdot \mid \cdot\,]$ separates the $X$ half from the $Z$ half, each assembled from three blocks as in (4). The pivot generator $g_i$ of $S$, for $1 \le i \le r$, has the row $$r(g_i) = [\,e_i \;\; (A_1)_i \;\; (A_2)_i \mid B_i \;\; 0 \;\; C_i\,],$$(6)^✦ and the middle generator $g_{r+j}$, for $1 \le j \le m$, has the row $$r(g_{r+j}) = [\,0 \;\; 0 \;\; 0 \mid D_j \;\; e_j \;\; E_j\,].$$(7)^✦ The generators $g_1, \dots, g_{n-k}$ of $S$, with $n - k = r + m$, are the pivot generators followed by the middle ones; their rows form the check matrix in standard form, $$G = \left[\begin{array}{ccc|ccc} I & A_1 & A_2 & B & 0 & C\\ 0 & 0 & 0 & D & I & E \end{array}\right].$$(8)^✦

The Encoded Operators

The encoded operator $\bar Z_b$ of $S$, for $1 \le b \le k$, has the row $$r(\bar Z_b) = [\,0 \;\; 0 \;\; 0 \mid (A_2^T)_b \;\; 0 \;\; e_b\,],$$(9)^✦ where $(M^T)_b$, row $b$ of the transpose, is column $b$ of $M$. The encoded operator $\bar X_a$ of $S$, for $1 \le a \le k$, has the row $$r(\bar X_a) = [\,0 \;\; (E^T)_a \;\; e_a \mid (C^T)_a \;\; 0 \;\; 0\,].$$(10)^✦

The Claim

What Is Checked

The claim is stated over the rows that standard form data determine: the generator rows of the check matrix (8) and the rows (10) and (9) of the encoded operators, paired by the twisted inner product (2). The library proves (11), (12), (13) and (14) for every choice of the six blocks (5).