Stabilizer, logical basis, and exact distance

One theorem

The common +1 eigenspace of XXXX and ZZZZ is a binary CSS [[4,2,2]] stabilizer code. The following representatives form a symplectic logical basis:

This choice is optimized for the square incidence drawing: the four supports are its four edges. It is symplectically equivalent to the representatives used by Meier, Eastin, and Knill (primary source).

CSS rank calculation

In binary CSS form,

H_X = [1 1 1 1], and H_Z = [1 1 1 1].

Their product is H_X H_Z^T = 4 mod 2 = 0, so the checks commute. Each matrix has rank one and the X and Z symplectic rows are independent. Hence

k = n - rank(S) = 4 - 2 = 2.

The constructor creates exactly these rows from the Pauli strings and the verifier recomputes the rank.

Logical commutation

For CSS Pauli operators, an X-type support and a Z-type support anticommute exactly when their intersection has odd size. The chosen supports obey

Thus each numbered pair anticommutes and the cross-pairs commute. Every row has even intersection with the opposite-type global stabilizer, so it lies in the normalizer. No row is in the two-dimensional stabilizer row space.

Codewords

Choose simultaneous Zbar_1,Zbar_2 eigenstates:

|00bar>=(|0000>+|1111>)/sqrt(2),

|01bar>=(|1010>+|0101>)/sqrt(2),

|10bar>=(|1100>+|0011>)/sqrt(2),

|11bar>=(|0110>+|1001>)/sqrt(2).

Every computational string has even Hamming weight, hence eigenvalue +1 under ZZZZ. XXXX complements all four bits and exchanges the two terms inside each superposition, hence also has eigenvalue +1. The two Z logicals give the signs encoded in the labels, while the two X logicals permute the four states in the expected bit directions. reproduce.py checks these statements as matrices, so normalization and phase conventions are not left to inspection.

Exact distance

Every weight-one Pauli anticommutes with at least one stabilizer:

• X_i anticommutes with ZZZZ;
• Z_i anticommutes with XXXX;
• Y_i anticommutes with both.

Therefore no weight-one Pauli is a nontrivial normalizer element and d>=2. But XX__=Xbar_1 is a weight-two normalizer element outside the stabilizer, so d<=2. These two constructive bounds give d=2. The generic exact CSS enumerator independently returns the same value.

Rains proves the stronger classification statement: the optimal distance-two code of length four is unique up to local equivalence (primary source). That theorem supports the identity history; the Atlas constructor still fixes one exact binary CSS representative so downstream computation is unambiguous.