TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

Pauli commutator is symplectic pairing

Statement

For $a = (x, z)$ and $b = (x^{'}, z^{'})$ in $V_{n}$ and any phases $k, k^{'}$ ,

$P (k, x, z) P (k^{'}, x^{'}, z^{'}) = (- 1)^{ω (a, b)} P (k^{'}, x^{'}, z^{'}) P (k, x, z) .$

Thus the Pauli operators commute exactly when their labels are symplectically orthogonal.

Facts & Assumptions

Given: the exact phase-aware product formula and the form $ω ((x, z), (x^{'}, z^{'})) = x \cdot z^{'} + z \cdot x^{'}$ .

[F1]

Pauli product and adjoint: the ordered product phase is $k + k^{'} + 2 (z \cdot x^{'})$ modulo $4$ .

[F2]

Binary symplectic form: $ω (a, b) = x \cdot z^{'} + z \cdot x^{'}$ over $F_{2}$ .

Proof

1.1givenF1F2algebra

The forward product has phase $k + k^{'} + 2 (z \cdot x^{'})$ by [F1]; the reversed product has phase $k + k^{'} + 2 (z^{'} \cdot x)$ . Their binary labels agree. The difference of the exponents modulo $4$ is $2 ((z \cdot x^{'}) - (z^{'} \cdot x))$ , and subtraction equals addition in $F_{2}$ , so this difference is $2 ω (a, b)$ modulo $4$ .

2.1givenstep 1.1algebra∎

Multiplication by the phase ratio $i^{2 ω (a, b)} = (- 1)^{ω (a, b)}$ gives the displayed identity. If $ω = 0$ it is commutation; if $ω = 1$ , equality with the negative is impossible because a Pauli is a nonzero invertible matrix over $C$ .

Depends on

Used by

Stabilizer encoder by symplectic elimination Algorithm
Noncontractible toric logical loops Definition
Pauli-path energy barrier Definition
Phase-aware stabilizer tableau Definition
Stabilizer code space Definition
Stabilizer subgroup Definition
Stabilizer syndromes and logical Pauli operators Definition
Pauli commutator and binary symplectic sign Example
Computational basis states have an extended stabilizer tableau Lemma
Deterministic Pauli measurement on a pure stabilizer state Lemma
Graph-state stabilizer generators Lemma
Random Pauli measurement updates stabilizer generators Lemma
Stabilizer labels form an isotropic space of the same rank Lemma
Tableau row reduction returns the deterministic Pauli sign Lemma
Toric checks commute and have two global relations Lemma
A single primal-dual crossing anticommutes Theorem
Clifford induces symplectic map Theorem
CSS encoding dimension and commutation Theorem
CSS syndrome correction Theorem
Dimension of the logical Pauli quotient Theorem
Exact indistinguishability in a contractible disk Theorem
Square planar surface-code distance and path count Theorem
Toric code distance is L Theorem
Two anticommuting toric logical Pauli pairs Theorem

Dependency tree · two levels

14 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 Error Correction, Physics 229 Lecture Notes, Chapter 7 (standard reference, not scraped)
M. Hein et al., Entanglement in Graph States and Its Applications (standard reference, not scraped)
Scott Aaronson and Daniel Gottesman, Improved Simulation of Stabilizer Circuits (standard reference, not scraped)