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.

Compute-copy-uncompute restores clean workspace

Statement

Let $C$ be a unitary circuit on input register $X$ and clean work register $W$ , with an available circuit for $C^{- 1}$ . Suppose that for every $x \in {0, 1}^{n}$ ,

C ∣ x, 0_{W} ⟩ = ∣ x, g (x), r (x) ⟩,

where $g (x)$ occupies a designated $m$ -bit subregister of $W$ and $r (x)$ is any remaining work string. Copying $g (x)$ into a distinct arbitrary target register $Y$ by bitwise CNOT and then applying $C^{- 1}$ to $X W$ maps

∣ x, y, 0_{W} ⟩ ⟼ ∣ x, y \oplus g (x), 0_{W} ⟩ .

The identity holds coherently on superpositions and with any reference register.

Facts & Assumptions

Given: The stated basis action of $C$ , disjoint target register $Y$ , and available inverse circuit. Prove that the work is restored.

[F1]

Clean and dirty ancillas: Clean workspace is initialized to the all-zero vector and must be returned exactly to that factor.

[F2]

Clean and dirty ancilla identities extend to references and mixed states: Clean identities extend to reference registers by tensoring with identity and to arbitrary matrices by linearity.

[F3]

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

[F4]

Tensor products of finitely many linear maps: The tensor map acts factorwise on elementary tensors and extends uniquely by linearity.

[F5]

Denotational semantics of a finite layered circuit: Chronological layers $L_{1}, \dots, L_{d}$ , with $L_{1}$ applied first, denote the ordered product $U_{L_{d}} \dots U_{L_{1}}$ .

[F6]

Reversing a circuit implements its inverse: If the inverses of all gates are explicitly available, reversing the chronological gate order and adjointing each gate implements $C^{†} = C^{- 1}$ .

[F7]

Finite registers and their ordered computational bases: An $n$ -qubit register is the ordered tensor product of $n$ copies of $Q_{2}$ , with the first wire most significant; the empty register is $C$ with basis ${1}$ .

[F8]

Big-endian encoding of ordered bit strings: A bit string occupies the computational-basis slot given by its big-endian index.

[F9]

Big-endian bit-string indices are bijective: Every length- $n$ bit string labels exactly one computational-basis vector.

[F10]

The computational basis is orthonormal: The computational basis of each nonempty qubit register is orthonormal.

[F11]

The product basis is orthonormal and tensor dimensions multiply: Ordered product bases of finite registers form a basis of their tensor product, including the empty-register case.

[F12]

X, CNOT, Toffoli, and Fredkin are involutions: CNOT is a unitary gate on its ordered register.

Proof

1.1givenF3F5F12algebra

On a basis input, the forward computation gives $∣ x, g (x), r (x) ⟩$ . Since $Y$ is disjoint, bitwise CNOT from the designated $g (x)$ subregister changes an arbitrary target $y$ to $y \oplus g (x)$ and leaves $X W$ unchanged. The intermediate state is therefore $∣ x, y \oplus g (x), g (x), r (x) ⟩$ , with $g (x), r (x)$ together occupying $W$ ; [F12] supplies the CNOT gate unitarity.

2.1givenF1F5F6step 1.1algebra

Applying $C^{- 1}$ to $X W$ returns $∣ x, g (x), r (x) ⟩$ to $∣ x, 0_{W} ⟩$ by the assumed forward basis action and [F6]. The inverse is supplied on $X W$ by the Given clause, so the disjoint target $Y$ is untouched and remains $y \oplus g (x)$ . This proves the displayed basis action and exact restoration of all work required by the clean-ancilla contract [F1].

3.1step 2.1F1F2F4F5F7F8F9F10F11algebra∎

By [F7]–[F11], the ordered basis vectors $∣ x, y, 0_{W} ⟩$ form a basis of the subspace with work fixed to zero. Step 2.1 therefore extends by linearity to every superposition in that subspace, with data action $V ∣ x, y ⟩ = ∣ x, y \oplus g (x) ⟩$ . This data map is an involutive permutation of its orthonormal computational basis, since applying it twice restores $y$ ; hence $V$ is unitary. The complete compute-copy-inverse operation thus satisfies the clean identity in [F1], and [F2] extends it to every finite reference register and matrix. The tensor-map and chronological-circuit conventions [F4]–[F5] preserve the ordered factors in these extensions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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)