Lemma: Stabilizer audit

The generators commute and are independent. The projector $P$ has rank two. Up to signs, the fifteen nonidentity elements of $G$ are the cyclic rotations of

In particular every nonidentity element has weight four. The vectors in (eq:encoder) are orthonormal.

Proof. Two Pauli strings commute when the number of positions at which their nonidentity factors anticommute is even. This verifies pairwise commutation. Multiplication of the four generators gives the fifteen strings listed by the three cyclic orbits; they are distinct and none is the identity. Thus the group has sixteen elements and the generators are independent. Since every nonidentity Pauli is traceless, $\mathrm{Tr}P=32/16=2$.

None of the fifteen strings contains only $I$ and $Z$. Hence $⟨00000|P|00000⟩=1/16$, proving the normalization of $|\overline{0}⟩$. Both $\overline{X}$ and $\overline{Z}$ commute with $G$, and they anticommute with each other. The vector $|\overline{0}⟩$ has $\overline{Z}$ eigenvalue $+1$; $|\overline{1}⟩$ has eigenvalue $-1$ and the same norm.