ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck pass

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.

A reversible AND oracle with clean work

Facts & Assumptions

[F1]

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

[F4]

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

[F2]

Clean and dirty ancillas: A clean work bit starts in $∣ 0 ⟩$ and must return exactly to $∣ 0 ⟩$ .

[F3]

Gate, workspace, and serial-depth costs of reversible embedding: A bounded-fan-in Boolean circuit can be compiled with explicit gate and clean-work costs.

[F5]

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

[F6]

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

[F7]

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

Example

This circuit implements

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

For each fixed $(a, b)$ , it is a one-gate reversible computation of $a b$ into clean work, one target copy, and the inverse compute. It uses three elementary gate occurrences and one clean work bit; for the one-AND Boolean DAG, this is within the bound of Gate, workspace, and serial-depth costs of reversible embedding. This is a compiled circuit, not a black-box query unless separately provided as an oracle.

The complete basis check is

$(a, b, y)$	after first Toffoli $(a, b, y, w)$	after CNOT $(a, b, y, w)$	final $(a, b, y, w)$
$(0, 0, 0)$	$(0, 0, 0, 0)$	$(0, 0, 0, 0)$	$(0, 0, 0, 0)$
$(0, 0, 1)$	$(0, 0, 1, 0)$	$(0, 0, 1, 0)$	$(0, 0, 1, 0)$
$(0, 1, 0)$	$(0, 1, 0, 0)$	$(0, 1, 0, 0)$	$(0, 1, 0, 0)$
$(0, 1, 1)$	$(0, 1, 1, 0)$	$(0, 1, 1, 0)$	$(0, 1, 1, 0)$
$(1, 0, 0)$	$(1, 0, 0, 0)$	$(1, 0, 0, 0)$	$(1, 0, 0, 0)$
$(1, 0, 1)$	$(1, 0, 1, 0)$	$(1, 0, 1, 0)$	$(1, 0, 1, 0)$
$(1, 1, 0)$	$(1, 1, 0, 1)$	$(1, 1, 1, 1)$	$(1, 1, 1, 0)$
$(1, 1, 1)$	$(1, 1, 1, 1)$	$(1, 1, 0, 1)$	$(1, 1, 0, 0)$

Verification

Given: Input bits $a, b$ , arbitrary target bit $y$ , and clean work bit $w = 0$ . Verify the chronological circuit Toffoli $(a, b, w)$ , CNOT $(w, y)$ , Toffoli $(a, b, w)$ .

1.1givenF1F2F5choose

The first Toffoli changes $w = 0$ to $a b$ and preserves $a, b$ . For $(a, b) = (0, 0), (0, 1), (1, 0), (1, 1)$ , this gives $w = 0, 0, 0, 1$ , respectively, as the eight-row table records for both values of $y$ .

2.1givenF1F4F5step 1.1algebra

The CNOT changes $y$ to $y \oplus a b$ and does not change $a, b, w$ ; the final Toffoli again toggles $w$ by $a b$ , so $w = a b \oplus a b = 0$ . The chronological product in [F5] is therefore exactly the tabled action on all eight basis inputs and clean-work outputs.

3.1step 2.1F2F3F5F6F7algebra∎

The vectors $∣ a, b, y, 0 ⟩$ in the eight table rows form a basis of the subspace with clean work fixed to zero, by [F6]–[F7]. Each gate is linear, so the verified basis action in Step 2.1 extends to every superposition in that subspace. For $S = 1$ , $E = 2$ , and $m = 1$ , the circuit uses three gate occurrences and one clean work bit, within the stated bounds $6 S + 4 E + m = 15$ and $S + E = 3$ from [F3].

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)