Dimension of the logical Pauli quotient

By [F1], phase classes of Paulis are the vectors of $V_n$. By [F2] the stabilizer labels form an $r$-dimensional subspace $W$. The commutator criterion [F3] identifies the normalizer labels exactly with $W^{\perp }$. The scalar phases label zero, so the subgroup $Z_{n}S$ has image $W$. Therefore $N(S)\mathrm{/}(Z_{n}S)$ is identified with $W^{\perp }\mathrm{/}W$.

The nondegenerate pairing [F6] gives an injective map $J:V_n\to V_n^{\ast }$, $J(v)=\omega (v,\cdot )$. Restricting functionals from $V_n$ to $W$ is onto: extend a basis of $W$ to one of $V_n$ by [F7], then extend each functional by assigning zero to the added basis vectors. Since $\dim V_n^{\ast }=\dim V_n=2n$ by [F9], injectivity and rank-nullity [F8] make $J$ onto. Thus the composite $V_n\to W^{\ast }$ is onto; its codomain has dimension $r$ by [F9], and its kernel is $W^{\perp }$. By [F8], $\dim W^{\perp }=2n-r$.

Since $W\subseteq W^{\perp }$, the quotient dimension is $\dim (W^{\perp }\mathrm{/}W)=(2n-r)-r=2(n-r)$. By [F5], $k=n-r$ is the number of encoded qubits; hence this dimension is $2k$, which is zero exactly when $k=0$.