Stabilizer projector rank and code dimension

By [F1], [F2], and [F10], $0\le r\le n$ and $\mathrm{Tr}({\mathrm{\Pi }}_S)=\mathrm{\mid }S{\mathrm{\mid }}^{-1}{\sum }_{g\in S}\mathrm{Tr}(g)$. For $n>0$, the identity is $I^{\otimes n}$. In the ordered product basis [F5]–[F6], its trace is a sum over bit words; [F11] factors this finite sum into the product of its one-qubit diagonal sums, each equal to $2$. Thus its trace is $2^n$. When $n=0$, [F6]–[F8] give trace $1=2^0$. For $n>0$, every other $g\in S$ has nonzero binary label by [F2], hence at least one nonidentity tensor factor. By [F4] that factor is a scalar multiple of $X$, $Z$, or $XZ$. For any tensor Pauli, its trace is the sum over bit words of products of one-qubit diagonal coefficients; [F11] factors this finite sum into the product of the one-qubit traces. By [F3], $X$ and $XZ$ are off-diagonal, while $Z$ has diagonal entries $1,-1$, so the nonidentity factor has trace zero. Hence every such $g$ has trace zero. Therefore $\mathrm{Tr}({\mathrm{\Pi }}_S)=2^n\mathrm{/}\mathrm{\mid }S\mathrm{\mid }=2^{n-r}$.

As ${\mathrm{\Pi }}_S$ is idempotent, [F9] gives $\mathrm{Tr}({\mathrm{\Pi }}_S)={\dim }_{\mathbb{C}}\mathrm{im}{\mathrm{\Pi }}_S$. Combining with step 1.1 proves the dimension formula, including $r=0$ and $r=n$.

When $r=n$, step 2.1 gives a one-dimensional common fixed space, so the space is nonzero and all of its nonzero vectors determine the same ray. This is the existence and uniqueness assertion used in the definition of a pure stabilizer state.