TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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 projector and code dimension

Statement

Let $n \geq 1$ and let $S$ be an abelian group of Hermitian $n$ -qubit Pauli operators with $- I \notin S$ , generated by $r$ independent checks. Then

$P_{S} : = ∣ S ∣^{- 1} \sum_{g \in S} g$

is the orthogonal projector onto the stabilizer code space and has rank $2^{n - r}$ . In particular, the code space is nonzero, including when $r = n$ .

Facts & Assumptions

Given: $n \geq 1$ and a stabilizer code space $C (S)$ with $r$ independent generators on the ordered $n$ -qubit register.

[F1]

Stabilizer code space: $C (S)$ is the common $+ 1$ eigenspace of every element of $S$ .

[F2]

Stabilizer average is the fixed-space projector: the finite average $∣ S ∣^{- 1} \sum_{g \in S} g$ is self-adjoint and idempotent with image $C (S)$ .

[F3]

Stabilizer projector rank and code dimension: for the same stabilizer subgroup of rank $r$ , its fixed-space projector has trace and image dimension $2^{n - r}$ .

[F4]

An endomorphism is an orthogonal projection exactly when it is idempotent and self-adjoint: a self-adjoint idempotent on a finite-dimensional inner-product space is the orthogonal projection onto its image.

[F5]

Stabilizer labels form an isotropic space of the same rank: the span of the binary labels of $r$ independent stabilizer checks has dimension $r$ , so the rank convention agrees with the generator count.

Proof

1.1F1F2given

The subgroup in the Statement meets the definition in [F1]. By [F2], $P_{S}$ is self-adjoint and idempotent with image equal to the common $+ 1$ eigenspace.

2.1F3F5step 1.1

The rank- $r$ hypothesis is the same rank convention used in [F3]: independent Hermitian generators give a binary label space of dimension $r$ by [F5]. Therefore [F3] gives $\dim C (S) = Tr (P_{S}) = 2^{n - r}$ .

3.1F4step 2.1algebra∎

By [F4] and step 1.1, $P_{S}$ is the orthogonal projector onto $C (S)$ . Since $2^{n - r} \geq 1$ , this space is nonzero; the endpoint $r = n$ has rank one and $r = 0$ gives the full $2^{n}$ -dimensional register.

Depends on

Used by

Steane seven-qubit CSS code Example
Twice-Concatenated Steane Code and Its Transversal Clifford Gates Lemma
CSS encoding dimension and commutation Theorem
Dimension of the logical Pauli quotient Theorem
Exact indistinguishability in a contractible disk Theorem
Stabilizer distance detection and correction Theorem
Stabilizer encoder correctness Theorem
The periodic toric code encodes two qubits Theorem

Cited to discharge well-definedness by Stabilizer code space.

Dependency tree · two levels

34 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

John Preskill, Quantum Computation, Chapter 7: Quantum Error Correction (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, §20.3 (standard reference, not scraped)