Stabilizer encoder correctness

The procedure terminates after $r$ pivots on every valid input by [F2]. By [F7]–[F8], each appended local gate acts on its ordered wires and the chronological list denotes its composed unitary. Each tableau coordinate and circuit wire $q$ corresponds to supplier factor $q+1$, as fixed in [F1]; in particular, one-wire updates use factor $q+1$ and a CNOT on circuit wires $q,s$ uses supplier control and target indices $q+1,s+1$. At each pivot, the local $H$, $S^{†}$, and $H$ transformations send the pivot row's nonidentity one-wire Pauli factors to signed $Z$ factors. The $S^{†}$ step sends $Y$ to $X$ by the inverse phase-gate action [F4], and then [F3] sends $X$ to $Z$. For each remaining pivot-row $Z_q$, the control-$q$, target-$j$ CNOT changes the pivot label $Z_q{Z}_j$ to $Z_j$ by [F5]. If the resulting row is negative, $X_j$ changes $-Z_j$ to $+Z_j$. Conjugation preserves commutation, while the exact phase-aware gate actions track every resulting sign.

Interchanging the selected pivot row into position $j$ and each subsequent row multiplication are invertible elementary operations on the generator list; the former swaps rows of $M$ and $G$, and the latter updates them by the same binary row addition and exact Pauli product. Thus $M$ remains invertible and $G_i={\prod }_a{g}_a^{M_{ia}}$ retains its recorded phase ${\kappa }_i$. Row multiplication by the pivot clears the remaining row's $Z_j$ coordinate because that row has no $X_j$ coordinate: it commutes with the now-$Z_j$ pivot. Consequently the transformed input-product rows are exactly $+Z_0,\dots ,+Z_{r-1}$, as asserted by [F1].

A vector is fixed by every $Z_j$ for $j<r$ exactly when all its computational-basis coordinates with a $1$ among the first $r$ bits vanish. Thus the common $+1$ eigenspace of the canonical checks is $\mathrm{\mid }{0}^r⟩\otimes ({\mathbb{C}}^2{)}^{\otimes (n-r)}$. By the row-basis equivalence in step 2.1 and the denotation [F8], this is exactly $D\mathcal{C}(S)$.

The ordered computational basis is orthonormal by [F9], and $x\mapsto \mathrm{\mid }{0}^r⟩\otimes \mathrm{\mid }x⟩$ embeds the logical computational basis as an orthonormal family. The finite product unitary $D^{†}$ from [F8] therefore defines the isometry $V$ in the Statement and sends these $2^{n-r}$ vectors to orthonormal vectors in $\mathcal{C}(S)$. Step 3.1 shows they span that space, and [F6] confirms its dimension is $2^{n-r}$. Hence they form the stated stabilizer code basis.