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.

Toffoli computes into a clean target and uncomputes it

Statement

Let $a, b$ be the values on two distinct control wires, let $t$ be a distinct clean target wire with value $0$ , and let $y$ be another distinct target wire with arbitrary value. Toffoli changes $t$ to $a b$ while preserving the controls. Copying that value into $y$ by CNOT and applying Toffoli again, in the written chronological order, sends

∣ a, b, y, 0 ⟩ ⟼ ∣ a, b, y \oplus a b, 0 ⟩ .

The same operator identity holds on superpositions.

Facts & Assumptions

Given: The Toffoli action, a zero-initialized workspace bit, and a distinct arbitrary target bit. Prove the stated compute-copy-uncompute identity.

[F1]

Toffoli and Fredkin gates: Toffoli maps $∣ a, b, t ⟩$ to $∣ a, b, t \oplus a b ⟩$ .

[F2]

X, CNOT, Toffoli, and Fredkin are involutions: Toffoli is its own inverse.

[F3]

Clean and dirty ancillas: A clean ancilla is initialized in $∣ 0 ⟩$ and the complete subroutine must return it exactly to $∣ 0 ⟩$ .

[F4]

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

[F5]

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}}$ .

[F6]

Tensor products of finitely many linear maps: A tensor map extends its factor maps linearly and acts factorwise on each elementary tensor.

[F7]

The computational basis is orthonormal: The one-qubit computational basis is an orthonormal basis for its declared inner product.

[F8]

The product basis is orthonormal and tensor dimensions multiply: The ordered tensor product of finite orthonormal factor bases is an orthonormal basis of the register.

Proof

1.1givenF1F3algebra

Since $t = 0$ , Toffoli sets $t$ to $0 \oplus a b = a b$ . The four control cases $00, 01, 10, 11$ give target values $0, 0, 0, 1$ , respectively, and the controls are unchanged.

2.1givenF1F2F4F5step 1.1algebra

CNOT from this work bit to the disjoint target changes $y$ to $y \oplus a b$ and leaves $a, b, t$ otherwise unchanged. The final Toffoli toggles $t$ by the same $a b$ , returning it to $a b \oplus a b = 0$ ; by [F2] it is the inverse compute gate. Thus each basis input has the stated output and clean work.

3.1step 2.1F5F6F7F8algebra∎

The vectors $∣ a, b, y, 0 ⟩$ , as $(a, b, y)$ ranges over its eight values, form a basis of the input subspace with the work factor fixed to $∣ 0 ⟩$ , by [F7]–[F8]. Every gate is linear, so the basis-vector identity in Step 2.1 extends to every superposition in that subspace. The tensor-map rule [F6] makes each gate act factorwise on the ordered wires, preserving the displayed register order.

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

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)