LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Graph-state stabilizer generators

Statement

Let $G = (V, E)$ be an ordered finite simple graph and let $∣ G ⟩$ be its graph state. Write $X_{v}, Z_{v}$ for the one-qubit Pauli matrices embedded on the tensor factor indexed by $v$ ; in the phase-aware Pauli convention, vertex at zero-based position $r$ is wire $r + 1$ . For $v \in V$ , put $K_{v} : = X_{v} \prod_{u \in N (v)} Z_{u}$ . Each $K_{v}$ is a Hermitian involution, $K_{v} ∣ G ⟩ = ∣ G ⟩$ , the generators commute pairwise, and their binary Pauli labels are independent. This includes $V = \emptyset$ , where the generating family is empty.

Facts & Assumptions

Given: A finite simple graph $G = (V, E)$ , its ordered graph state, and the one-qubit Pauli matrices.

[F1]

The graph state is $U_{G} ∣ + ⟩^{\otimes V}$ with one $C Z_{u v}$ per edge, and the embedded edge gates commute (Graph state of an ordered finite simple graph, Controlled-Z edge gates commute).

[F2]

The angle- $π$ controlled phase is the diagonal Hermitian involution $diag (1, 1, 1, - 1)$ (Controlled Phase Rotation).

[F3]

Number coordinates by the vertices in their fixed order; $e_{v}$ is the coordinate unit vector at vertex $v$ , and $(A_{2} (G))_{u v} = 1$ exactly when ${u, v} \in E$ . The binary dot product is the coordinate sum $\sum_{w \in V} a_{w} b_{w}$ in $F_{2}$ . Thus $A_{2} (G)$ is symmetric with zero diagonal (Binary adjacency matrix of an ordered finite simple graph).

[F4]

The one-qubit $X, Y, Z$ matrices are Hermitian involutions, and the phase-aware tensor Pauli frame has binary $X$ - and $Z$ -support with zero-scalar convention $X^{x} Z^{z}$ (The Pauli matrices, Phase aware n qubit pauli group).

[F5]

Pauli operators commute exactly when their binary labels have zero symplectic pairing (Pauli commutator is symplectic pairing).

Proof

1.1F1F2F3algebra

Every $C Z_{u v}$ is a diagonal Hermitian involution by [F2]. Conjugating $X_{v}$ by an incident gate gives $C Z_{u v} X_{v} C Z_{u v} = Z_{u} X_{v}$ by checking the four computational-basis pairs; a nonincident edge gate commutes with $X_{v}$ . Since the edge gates commute by [F1], $U_{G} X_{v} U_{G}^{†} = X_{v} \prod_{u \in N (v)} Z_{u} = K_{v}$ . The tensor factors are Hermitian involutions, so $K_{v}$ is also a Hermitian involution.

1.2F3F4F5algebra

The binary label of $K_{v}$ is $(e_{v}, A_{2} (G) e_{v})$ because the $Z$ coordinate at $u$ is $(A_{2} (G) e_{v})_{u} = (A_{2} (G))_{u v}$ . For distinct $v, w$ , the binary symplectic pairing of these labels is $e_{v} \cdot A_{2} (G) e_{w} + A_{2} (G) e_{v} \cdot e_{w} = (A_{2} (G))_{v w} + (A_{2} (G))_{w v} = 0$ in $F_{2}$ by [F3]. Thus [F5] gives pairwise commutation. Equivalently, when ${v, w} \in E$ the two local $X / Z$ anticommutations cancel, and when it is not an edge all overlapping factors are both $Z$ or act on different sites.

2.1step 1.1F1algebra

Using $X_{v} ∣ + ⟩^{\otimes V} = ∣ + ⟩^{\otimes V}$ and $U_{G}^{†} = U_{G}$ , we obtain $K_{v} ∣ G ⟩ = U_{G} X_{v} U_{G}^{†} U_{G} ∣ + ⟩^{\otimes V} = U_{G} ∣ + ⟩^{\otimes V} = ∣ G ⟩$ .

3.1F4algebra∎

In a product of generators indexed by $S \subseteq V$ , the binary $X$ -support is $\sum_{v \in S} e_{v} = 1_{S}$ by [F4]. It vanishes only for $S = \emptyset$ , so no nonempty product has identity binary label; the generators are independent. For empty $V$ this assertion is vacuous.

Depends on

Used by

One-edge graph state and two-wire CZ pattern Example
Graph state is the unique joint stabilizer ray Theorem

Dependency tree · two levels

27 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

M. Hein et al., Entanglement in graph states and its applications, Proposition 2, p. 15 (standard reference, not scraped)
Robert Raussendorf, Daniel E. Browne, and Hans J. Briegel, Measurement-based quantum computation on cluster states, pp. 3–5 (standard reference, not scraped)