CSS encoding dimension and commutation

There are $\mathrm{\mid }{C}_2\mathrm{\mid }$ distinct basis vectors in each coset sum. By [F4], its squared norm is $\mathrm{\mid }{C}_2{\mathrm{\mid }}^{-1}\mathrm{\mid }{C}_2\mathrm{\mid }=1$. Distinct cosets have disjoint supports, so their vectors are orthogonal. By [F1] there are $\mathrm{\mid }{C}_1\mathrm{/}{C}_2\mathrm{\mid }=2^{\dim C_1-\dim C_2}=2^k$ such vectors, giving an orthonormal basis indexed by a $k$-bit logical register.

By [F5], for $c\in C_2$, $X^c$ sends $\mathrm{\mid }x+u⟩$ to $\mathrm{\mid }x+u+c⟩$. Translation $u\mapsto u+c$ permutes $C_2$, so $X^c$ fixes the whole coset sum. For $h\in C_1^{\perp }$, each $x+u\in C_1$ and therefore $(-1{)}^{h\cdot (x+u)}=1$; the diagonal operator $Z^h$ fixes every term. Thus both check families fix every encoded basis state and hence their linear span.

The binary labels of $X^c$ and $Z^h$ are $(c,0)$ and $(0,h)$. Their symplectic pairing is $c\cdot h$. Since $c\in C_2\subseteq C_1$ and $h\in C_1^{\perp }$, this dot product is zero by [F2].

On a computational basis vector $\mathrm{\mid }w⟩$, multiplying the one-bit Hadamard formulas from [F7] gives $H^{\otimes n}\mathrm{\mid }w⟩=2^{-n\mathrm{/}2}{\sum }_{y\in {\mathbb{F}}_2^n}(-1{)}^{y\cdot w}\mathrm{\mid }y⟩$. Substituting the coset definition [F1] yields $H^{\otimes n}\mathrm{\mid }x+C_2⟩=2^{-n\mathrm{/}2}\mathrm{\mid }{C}_2{\mathrm{\mid }}^{-1\mathrm{/}2}{\sum }_{y\in {\mathbb{F}}_2^n}(-1{)}^{y\cdot x}({\sum }_{u\in C_2}(-1{)}^{y\cdot u})\mathrm{\mid }y⟩$. For $y\in C_2^{\perp }$, the inner sum is $\mathrm{\mid }{C}_2\mathrm{\mid }$. Otherwise choose $u_0\in C_2$ with $y\cdot u_0=1$; translation $u\mapsto u+u_0$ pairs terms with opposite signs, so the sum is zero.

Choose independent bases of $C_2$ and $C_1^{\perp }$. Their separate $X$- and $Z$-type labels are independent: a zero combined label has both binary halves zero. By [F3] the combined number is $\dim C_2+n-\dim C_1=n-k$. This includes $k=0$.

The checks are commuting Hermitian Paulis by steps 1.3 and [F5]. They fix the nonzero encoding from step 1.2, so their generated group cannot contain $-I$. Step 2.1 gives $n-k$ independent checks; [F9] therefore gives their common $+1$ eigenspace dimension $2^{n-(n-k)}=2^k$. By step 1.1 the encoding has dimension $2^k$, and step 1.2 says it lies in that eigenspace. Equal finite dimensions force equality: the CSS encoding is exactly the stabilizer code space [F8].

The transformed vector is supported exactly on $C_2^{\perp }$, with constant magnitude on that set. Since $x\in C_1$, the phase $(-1{)}^{x\cdot y}$ is constant on each coset of $C_1^{\perp }$ in $C_2^{\perp }$. Grouping terms by those cosets gives $H^{\otimes n}\mathrm{\mid }x+C_2⟩=2^{-k\mathrm{/}2}{\sum }_{y+C_1^{\perp }\in C_2^{\perp }\mathrm{/}{C}_1^{\perp }}(-1{)}^{x\cdot y}\mathrm{\mid }y+C_1^{\perp }⟩$. The coefficient is $2^{-k\mathrm{/}2}$ because $\mathrm{\mid }{C}_2\mathrm{\mid }\mathrm{\mid }{C}_1^{\perp }\mathrm{\mid }\mathrm{/}{2}^n=2^{-k}$ by [F3]. This is the dual coset basis Fourier transform; the pairing is independent of representatives since $C_2\subseteq C_1$ and $C_1^{\perp }\subseteq C_2^{\perp }$.