Termination and gate count of symplectic stabilizer elimination

After $j$ pivots, the first $j$ rows are $+Z_0,\dots ,+Z_{j-1}$, and every remaining row has zero $X$ and $Z$ coordinates on those $j$ wires. This holds before the first pivot. At pivot $j$, the selected row is interchanged into row $j$ when necessary; the interchange also updates the signed row-operation data and is not a circuit gate. All circuit gates act only on unused wires. For any zero-based circuit wire $q$, the one-based factor index in [F2]–[F4] is $q+1$; a CNOT with circuit control $q$ and target $s$ therefore uses supplier indices $q+1,s+1$. The local Clifford gates turn each nonidentity pivot factor into $Z$, and [F4] clears every other pivot-row $Z$ using a control on that wire and target $j$. Commutation is preserved by conjugation, so remaining rows have no $X_j$ factor. Row multiplication by the pivot then clears $Z_j$ without changing earlier wires.

The remaining $r-j$ binary row labels are independent on the unused $n-j$ wires: a dependence there would be a dependence among the original labels because all earlier coordinates are already zero. Since $r-j>0$ when $j<r$, at least one remaining row is nonidentity on an unused wire. Thus every valid pivot finds a row and a wire, and the loop executes exactly $r$ iterations. This proves termination, including $r=0$.

During one pivot, at most one SWAP is used. On each of at most $n$ unused wires, normalization uses at most two one-qubit gates. Clearing the pivot's other $Z$ factors uses at most $n-1$ CNOTs, and correcting its sign uses at most one $X$. The total is at most $1+2n+(n-1)+1=3n+1$ gates per pivot, hence at most $r(3n+1)$ overall.

The current phase-aware tableau and the phase-aware input-combination rows together store $4rn$ label bits and $O(r)$ phase bits. The signed row-operation output stores $r^2$ bits for $M$ and $O(r)$ bits for $\kappa$. The output has at most $r(3n+1)$ gates; each gate type takes constant space and each wire index takes at most $\lceil {\log }_2(n+1)\rceil$ bits. Their total is $O(rn+r^2+rn\log (n+1))$. For $r=0$, the output and signed row-operation data are empty, as specified.