Stabilizer labels form an isotropic space of the same rank

If $n=0$, then $S=\{I\}$: a subgroup contains $I$ and its only other possible Hermitian scalar Pauli is $-I$, which is excluded. Thus $\lambda {\mathrm{\mid }}_S$ is injective, its image is the zero subspace of dimension $0$, this dimension is independent of any generating list, and $\mathrm{\mid }S\mathrm{\mid }=1=2^0$.

Assume now $n\ge 1$. The identity of $S$ has zero label. If $P,Q\in S$, then $PQ\in S$ and $\lambda (PQ)=\lambda (P)+\lambda (Q)$ by [F3]. Thus $L=\lambda (S)$ contains zero and is closed under addition; over ${\mathbb{F}}_2$, closure under the only scalars $0,1$ follows, so $L$ is a subspace.

Suppose $P,Q\in S$ have the same label. By the homomorphism in [F3], $\lambda (P^{-1}Q)=0$, so $P^{-1}Q$ is a scalar Pauli. Since Hermitian Paulis square to $I$ by [F5], $P^{-1}=P$; as $P,Q$ commute and are Hermitian, $P^{-1}Q=PQ$ is Hermitian. The phase criterion [F5] then makes this scalar equal to $I$ or $-I$. The latter is excluded by [F1], hence $P=Q$ and $\lambda {\mathrm{\mid }}_S$ is injective.

For $n\ge 1$, any two labels in $L$ come from commuting elements of the abelian group $S$, so [F4] gives symplectic pairing zero. Bilinearity then makes every pair in their span pair to zero; hence $L$ is isotropic. The image $L$ is defined from $S$ alone, so its dimension is unchanged by replacing one generating list of $S$ by another.

For $n\ge 1$, the map $\lambda {\mathrm{\mid }}_S:S\to L$ is onto by the definition of $L$ and injective by step 1.3, so it is a bijection of finite sets by [F8]. If $r={\dim }_{{\mathbb{F}}_2}L$, [F6] and [F7] give $\mathrm{\mid }L\mathrm{\mid }=2^r$. Therefore $\mathrm{\mid }S\mathrm{\mid }=\mathrm{\mid }L\mathrm{\mid }=2^r$, as claimed.

Step 1.1 proves the claim for $n=0$, and step 1.2 and step 1.3 and step 2.1 and step 2.2 prove it for $n\ge 1$. These cases exhaust all $n\ge 0$.