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

Controlled-Z matching action on a Pauli frame

Statement

Let $n \geq 0$ and let $M$ be a matching, meaning a set of pairwise disjoint two-element subsets of the ordered wire set ${1, \dots, n}$ . Give the graph $G_{M} = ({1, \dots, n}, M)$ the vertex order $1, \dots, n$ , so vertex $j$ is coordinate $j$ (position $j - 1$ in the zero-based vertex list) of its binary adjacency matrix. Let $A_{M} : = A_{2} (G_{M}) \in M_{n} (F_{2})$ from Binary adjacency matrix of an ordered finite simple graph, so $(A_{M})_{j k} = 1$ exactly when ${j, k} \in M$ . For $x, z \in F_{2}^{n}$ , all coordinates use this wire order, and binary dot products mean $a \cdot b : = \sum_{j = 1}^{n} a_{j} b_{j}$ in $F_{2}$ . Define $q_{M} (x) : = \sum_{{j, k} \in M} x_{j} x_{k} \in F_{2}$ . For $n \geq 1$ , put $P (x, z) : = X^{x} Z^{z} = P (0, x, z)$ as in Phase aware n qubit pauli group. For $n = 0$ , the unique empty vectors satisfy $X^{x} = Z^{z} = I_{C}$ and we define $P (x, z) = I_{C}$ ; the register is the empty tensor product from Ordered tensor registers, their inner product, and wire permutations. With $C Z_{M} : = \prod_{{j, k} \in M} C Z_{j k}$ ,

$C Z_{M} P (x, z) = (- 1)^{q_{M} (x)} P (x, z \oplus A_{M} x) C Z_{M} .$

For the empty wire set or empty matching the sum is zero and the formula is the identity.

Facts & Assumptions

Given: A finite ordered set of $n$ qubits, a matching $M$ , and binary vectors $x, z \in F_{2}^{n}$ .

[F1]

The angle- $π$ controlled phase acts on $∣ y_{j} y_{k} ⟩$ by $(- 1)^{y_{j} y_{k}}$ (Controlled Phase Rotation).

[F2]

$A_{M}$ is symmetric with zero diagonal and records precisely the matching edges (Binary adjacency matrix of an ordered finite simple graph).

[F3]

For $n \geq 1$ , the Pauli frame convention is $P (x, z) = P (0, x, z) = X^{x} Z^{z}$ on the ordered register (Phase aware n qubit pauli group). The $n = 0$ identity convention is specified in the Statement.

[F4]

The zero-wire tensor register is $C$ with basis ${1}$ , and the product basis spans each finite ordered register (Ordered tensor registers, their inner product, and wire permutations).

Proof

1.1F1F2algebra

For $y \in F_{2}^{n}$ , write $q_{M} (y) = \sum_{{j, k} \in M} y_{j} y_{k}$ . By [F1], $C Z_{M} ∣ y ⟩ = (- 1)^{q_{M} (y)} ∣ y ⟩$ . Expanding each edge term over $F_{2}$ gives the cross term $\sum_{{j, k} \in M} (y_{j} x_{k} + x_{j} y_{k})$ . By the stated coordinate order and dot-product convention, $(A_{M} x)_{j} = \sum_{k : {j, k} \in M} x_{k}$ , so this cross term is exactly $(A_{M} x) \cdot y$ . Hence $q_{M} (y \oplus x) = q_{M} (y) + q_{M} (x) + (A_{M} x) \cdot y$ .

2.1step 1.1F3F4algebracases∎

Applying the left side of the claimed identity to $∣ y ⟩$ gives $(- 1)^{z \cdot y + q_{M} (y \oplus x)} ∣ y \oplus x ⟩$ . Applying the right side gives $(- 1)^{q_{M} (x) + q_{M} (y) + (z \oplus A_{M} x) \cdot y} ∣ y \oplus x ⟩$ ; step 1.1 makes these signs equal. The ordered computational basis spans the register, so the operators agree. When $n = 0$ or $M = \emptyset$ , every sum is empty and both sides are the identity frame relation by [F3]--[F4].

Depends on

Used by

Dependency tree · two levels

31 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

Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415, §20.6 (standard reference, not scraped)
Robert Raussendorf, Daniel E. Browne, and Hans J. Briegel, Measurement-based quantum computation on cluster states, §II B (standard reference, not scraped)