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

X, CNOT, Toffoli, and Fredkin are involutions

Statement

On the ordered computational basis, $X$ , CNOT, Toffoli $T$ , and Fredkin $F$ are involutions. Their linear extensions are unitary. With chronological order meaning the gates are applied in the written order, Fredkin is implemented by CNOT $(a, b)$ , then $T (c, b, a)$ , then CNOT $(a, b)$ .

Facts & Assumptions

Given: The displayed gate actions and the ordered tensor-product computational basis. Prove involutivity, unitarity, and the stated Fredkin implementation.

[F5]

The Pauli matrices: In the ordered computational basis, $X = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ .

[F1]

CNOT and Control-Target Order: In the ordered two-qubit basis, ${CNOT}_{1 \to 2} ∣ a, t ⟩ = ∣ a, t \oplus a ⟩$ .

[F2]

Toffoli and Fredkin gates: $T ∣ a, b, t ⟩ = ∣ a, b, t \oplus a b ⟩$ ; $F ∣ 0, a, b ⟩ = ∣ 0, a, b ⟩$ and $F ∣ 1, a, b ⟩ = ∣ 1, b, a ⟩$ .

[F3]

The computational basis is orthonormal: For every $d \geq 1$ , the ordered computational basis of $Q_{d}$ is an orthonormal basis for its declared inner product.

[F4]

The product basis is orthonormal and tensor dimensions multiply: The elementary tensors of specified ordered orthonormal factor bases, in lexicographic order, form an orthonormal basis of the tensor register.

[F6]

Denotational semantics of a finite layered circuit: A chronological list of layers $L_{1}, \dots, L_{d}$ , with $L_{1}$ applied first, denotes $U_{L_{d}} \dots U_{L_{1}}$ .

Proof

1.1givenF5algebra

The matrix in [F5] sends $∣ t ⟩$ to $∣ t \oplus 1 ⟩$ . Applying it twice sends $t$ to $t \oplus 1 \oplus 1 = t$ , so $X^{2} = I$ .

1.2givenF1algebra

By [F1], applying CNOT twice sends $∣ a, t ⟩$ to $∣ a, t \oplus a \oplus a ⟩ = ∣ a, t ⟩$ , so ${CNOT}^{2} = I$ .

1.3givenF2algebra

Applying $T$ twice leaves $a, b$ unchanged and sends $t$ to $t \oplus a b \oplus a b = t$ . Thus $T^{2} = I$ .

1.4givenF2choose

When the Fredkin control is $0$ , each application fixes $(a, b)$ . When it is $1$ , each application swaps $a, b$ and leaves the control unchanged. In either case two applications restore all three bits, so $F^{2} = I$ .

2.1step 1.1step 1.2step 1.3step 1.4F1F2F3F4F5algebra

The four maps permute the ordered orthonormal computational basis by [F1]–[F5]. A permutation of an orthonormal basis preserves inner products, so each linear extension is unitary; by Steps 1.1–1.4 each is its own inverse.

3.1givenF1F2F6choosealgebra∎

Apply the gates chronologically as prescribed by [F6] to $∣ c, a, b ⟩$ . After CNOT $(a, b)$ the last two bits are $(a, b \oplus a)$ . If $c = 0$ , Toffoli does nothing and the last CNOT restores $(a, b)$ . If $c = 1$ , Toffoli changes its target to $a \oplus (b \oplus a) = b$ , and the last CNOT changes the other bit to $(b \oplus a) \oplus b = a$ . Thus the output is $∣ c, a, b ⟩$ for $c = 0$ and $∣ c, b, a ⟩$ for $c = 1$ , exactly the Fredkin action.

Depends on

Used by

Reversible embedding of a Boolean circuit Algorithm
Fresh-target NOT and OR gadgets Lemma
Toffoli computes into a clean target and uncomputes it Lemma
Compute-copy-uncompute restores clean workspace Theorem
Gate, workspace, and serial-depth costs of reversible embedding Theorem
Parallel depth of reversible Boolean embedding Theorem

Cited to discharge well-definedness by Toffoli and Fredkin gates.

Dependency tree · two levels

23 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 5: Classical and Quantum Circuits (updated July 2015) (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)