Pipeline-generated

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.

✓ 1 result · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Reversible Computation, Ancillas, and Coherent Oracles — Examples

1 · Prerequisites

2 · Summary

The example checks the reversible AND computation on every classical input and both target values, then verifies that the clean work bit returns to zero. It distinguishes the explicit compiled gate sequence from an abstract oracle query.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passOpen item page →

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].