Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Stabilizer and CSS Codes, Syndromes, and Procedures — Examples

1 · Prerequisites

2 · Summary

These worked binary examples check the nested-code CSS convention, coset normalization, stabilizer ranks, logical operators, and syndrome labels. The four-qubit example deliberately violates the extra dual-containment condition used in one special-source presentation while satisfying the general $C_{2} \subseteq C_{1}$ construction.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)Open item page →

CSS encoding from nested binary codes

Example

Let $n = 4$ , $C_{2} = {span}_{F_{2}} {1111}$ , and $C_{1} = {span}_{F_{2}} {1111, 1100}$ . A generator matrix for $C_{1}$ has columns $1111, 1100$ , and a parity-check matrix has rows $1100, 0011$ . The CSS code has $k = \dim C_{1} - \dim C_{2} = 1$ and encoded states

$∣ 0_{L} ⟩ = 2^{- 1 / 2} (∣ 0000 ⟩ + ∣ 1111 ⟩), ∣ 1_{L} ⟩ = 2^{- 1 / 2} (∣ 1100 ⟩ + ∣ 0011 ⟩) .$

The X checks are generated by $X^{1111}$ and the Z checks by $Z^{1100}, Z^{0011}$ . Logical operators can be chosen as $X_{L} = X^{1100}$ and $Z_{L} = Z^{1010}$ . This example has $C_{2}^{⊥} \subseteq̸ C_{1}$ .

Facts & Assumptions

Given: The binary dot product, the nested-code CSS convention, and the displayed generators and parity checks.

[F1]

CSS encoding dimension and commutation: $C_{2} \subseteq C_{1}$ encodes $\dim C_{1} - \dim C_{2}$ qubits, and $X$ checks from $C_{2}$ commute with $Z$ checks from $C_{1}^{⊥}$ .

[F2]

Bilinear dual of a finite-field linear code: $C^{⊥}$ consists of vectors having dot product zero with every vector of $C$ .

[F3]

Stabilizer syndromes and logical Pauli operators: normalizer classes outside scalar phases and stabilizers act as nontrivial logical Paulis.

Verification

1.1F1construct

The displayed generator rows of $C_{1}$ are independent, and the single generator of $C_{2}$ is nonzero and lies in $C_{1}$ . Thus $\dim C_{1} = 2$ , $\dim C_{2} = 1$ , $k = 1$ , and the two displayed cosets are $C_{2}$ and $1100 + C_{2}$ . Their supports are disjoint, so [F1] gives the orthonormal logical basis shown.

2.1F1F2step 1.1algebra

A vector $y = (y_{1}, y_{2}, y_{3}, y_{4})$ lies in $C_{1}^{⊥}$ exactly when $y_{1} + y_{2} + y_{3} + y_{4} = 0$ and $y_{1} + y_{2} = 0$ . These equations are equivalent to $y_{1} = y_{2}$ and $y_{3} = y_{4}$ , so $C_{1}^{⊥} = span {1100, 0011}$ . Both generators have even dot product with $1111$ , so the X and Z checks commute. The vector $1010$ has even weight and hence lies in $C_{2}^{⊥}$ , but it is not one of $0000, 1111, 1100, 0011$ , so it is not in $C_{1}$ . This verifies $C_{2}^{⊥} \subseteq̸ C_{1}$ .

3.1F1F3step 2.1algebra∎

Translation by $1100$ exchanges the two displayed logical coset states, so $X^{1100}$ acts as logical bit flip. The phase $(- 1)^{1010 \cdot y}$ is $+ 1$ for $y = 0000, 1111$ and $- 1$ for $y = 1100, 0011$ , so $Z^{1010}$ acts as logical phase flip. Their dot product is $1100 \cdot 1010 = 1$ in $F_{2}$ , hence the logical operators anticommute.