DefinitionDefinition: AI-adaptedProof: AI-generatedPipeline-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.

CSS code from nested binary codes

Definition

Let $n \geq 1$ and let $C_{2} \subseteq C_{1} \leq F_{2}^{n}$ be binary linear codes. Put $k = \dim C_{1} - \dim C_{2}$ . The CSS coset code associated with this nested pair is the subspace of the ordered $n$ -qubit register spanned by

$∣ x + C_{2} ⟩ : = ∣ C_{2} ∣^{- 1 / 2} \sum_{c \in C_{2}} ∣ x + c ⟩, x \in C_{1} .$

Here addition is coordinatewise in $F_{2}^{n}$ , and $∣ y ⟩$ is the computational-basis vector indexed by the bit string $y$ . The vector depends only on the coset $x + C_{2}$ . A basis of $C_{2}$ extended to a basis of $C_{1}$ chooses logical labels for the quotient $C_{1} / C_{2}$ ; the number of labels is $2^{k}$ . No additional inclusion $C_{2}^{⊥} \subseteq C_{1}$ is part of this nested-code convention.

For a binary code $C$ , $C^{⊥} = {y : x \cdot y = 0 for every x \in C}$ uses the standard bilinear dot product, as defined in Bilinear dual of a finite-field linear code.

Facts & Assumptions

Given: Binary linear codes $C_{2} \subseteq C_{1} \leq F_{2}^{n}$ with $n \geq 1$ .

[F1]

Classical linear code over a finite field: a classical binary linear code is a subspace of $F_{2}^{n}$ with its finite vector-space dimension.

[F2]

Finite registers and their ordered computational bases: the $n$ -qubit register has an ordered computational basis indexed by $F_{2}^{n}$ .

[F3]

The computational basis is orthonormal gives an orthonormal basis of each $Q_{2}$ factor. Equip their ordered tensor product with the inner product of Ordered tensor registers, their inner product, and wire permutations; then The product basis is orthonormal and tensor dimensions multiply makes the bit-string-indexed product basis orthonormal.

[F4]

If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ : in finite dimension every linearly independent subset of a subspace extends to a basis of that subspace, without a choice principle.

Verification

1.1givenF1construct

Since $C_{2} \subseteq C_{1}$ , every $x \in C_{1}$ has a coset in $C_{1} / C_{2}$ . If $x^{'} = x + c_{0}$ with $c_{0} \in C_{2}$ , then $c \mapsto c + c_{0}$ permutes $C_{2}$ ; reindexing the finite sum gives $∣ x^{'} + C_{2} ⟩ = ∣ x + C_{2} ⟩$ . Thus the displayed vector is independent of the representative.

2.1givenF1F4step 1.1construct

By [F4], $\dim C_{2} \leq \dim C_{1}$ , so $k \geq 0$ . Extend a basis of $C_{2}$ to a basis of $C_{1}$ . If the dimensions are $m$ and $m + k$ , respectively, the added $k$ basis vectors span a complement $D$ with $C_{1} = C_{2} \oplus D$ . Each coset has exactly one representative in $D$ , so $D \to C_{1} / C_{2}$ , $d \mapsto d + C_{2}$ , is a bijection. Coordinate expansion in the chosen basis identifies $D$ with $F_{2}^{k}$ . There are $2^{k}$ such coordinate lists, since each of the $k$ coordinates has two choices; for $k = 0$ there is one empty list. Hence $∣ C_{1} / C_{2} ∣ = 2^{k}$ .

3.1givenF2F3step 2.1algebra∎

For each coset, the basis vectors $∣ x + c ⟩$ in its sum are distinct, so [F3] gives squared norm $∣ C_{2} ∣^{- 1} ∣ C_{2} ∣ = 1$ . Different cosets have disjoint supports in that basis, so their inner product is zero. The code space therefore has the $2^{k}$ orthonormal coset vectors indexed by $C_{1} / C_{2}$ .

Remarks

Cleve’s §37.3 gives a special CSS construction with an additional dual containment hypothesis. That hypothesis is not used here: membership in $C_{2} \subseteq C_{1}$ alone makes the coset vectors well defined.

Depends on

Used by

Square planar surface code Definition
CSS encoding dimension and commutation Theorem

Dependency tree · two levels

44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Richard Cleve, Quantum Information Processing course notes, §§37.1–37.3 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 7: Quantum Error Correction (standard reference, not scraped)