TheoremStatement: Literature-sourcedProof: 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.

Reversible binary dot product: correctness and exact cost

Statement

For every $n \geq 0$ , the algorithm Reversible binary dot-product query maps every computational-basis input to

∣ a ⟩ ∣ x ⟩ ∣ z ⟩ ∣ 0 ⟩_{r} ⟼ ∣ a ⟩ ∣ x ⟩ ∣ z \oplus (a \cdot x) ⟩ ∣ 0 ⟩_{r} .

It therefore implements the same linear map on superpositions. Its exact cost is $2 n$ Toffoli gates, one CNOT, and one clean work bit; it has no failure branch.

Facts & Assumptions

Given: $n \geq 0$ , binary strings $a, x$ , an arbitrary target bit $z$ , a clean work bit $r = 0$ , and the stated gate sequence. The operation model's declared finite nonoracle gate alphabet contains and permits Toffoli and CNOT as callable gates, each occurrence is counted once under [F7], and this circuit makes no black-box oracle calls.

[F1]

Reversible binary dot-product query: the sequence accumulates coordinate products into $r$ , copies $r$ to $z$ , and reverses the Toffoli sequence.

[F2]

Binary dot product as parity: $a \cdot x$ is the left-to-right XOR fold of the bits $a_{i} \land x_{i}$ , with empty fold $0$ .

[F3]

Toffoli and Fredkin gates: Toffoli preserves its two controls and toggles its target by their product.

[F4]

CNOT and Control-Target Order: CNOT preserves its control and toggles its target by the control value.

[F5]

Clean and dirty ancillas: a clean ancilla starts and ends exactly at zero.

[F6]

The computational basis is orthonormal and The product basis is orthonormal and tensor dimensions multiply: the ordered computational-basis product vectors of the data, target and work registers form a basis of their joint register.

[F8]

Dirac Notation Conversion: ket notation denotes the corresponding vectors, with the repository's stated inner-product convention.

[F7]

Finite circuit resource accounting: each occurrence of a declared gate contributes one occurrence to the gate count.

Proof technique: induction on the forward and reverse loop indices.

Proof

1.1givenF1F2base

Before any Toffoli gate, $r = 0$ , which is the empty parity $p_{0}$ .

1.2givenF1F2F3ihalgebra

If after processing coordinates $0, \dots, i - 1$ the work bit is $p_{i} = ⨁_{j < i} (a_{j} \land x_{j})$ , the next Toffoli leaves the controls unchanged and changes $r$ to $p_{i} \oplus (a_{i} \land x_{i}) = p_{i + 1}$ by [F3]. Thus the forward invariant holds for every $i \leq n$ .

2.1step 1.1step 1.2F2discharge-induction

At the end of the forward loop, $r = p_{n} = a \cdot x$ by [F2]. This includes $n = 0$ , for which step 1.1 is already the final state.

3.1step 2.1F4algebra

The CNOT now changes $z$ to $z \oplus r = z \oplus (a \cdot x)$ and leaves $a, x, r$ unchanged by [F4].

4.1step 2.1step 3.1F1F2F3F5inductionalgebra

In the reverse loop, define $q_{i}$ to be the accumulator after the gates for coordinates $n - 1, n - 2, \dots, i$ have been applied. Before any reverse gate, $q_{n} = p_{n}$ . If $q_{i + 1} = p_{i + 1}$ , the next Toffoli toggles $q_{i + 1}$ by $a_{i} \land x_{i}$ , so $q_{i} = p_{i + 1} \oplus (a_{i} \land x_{i}) = p_{i}$ . Descending through $i = n - 1, \dots, 0$ therefore ends at $q_{0} = p_{0} = 0$ . The reverse gates do not change $a, x, z$ , so the work bit is clean.

5.1step 3.1step 4.1F1F6F7F8algebradischarge-induction∎

The input basis map is the claimed map by steps 3.1 and 4.1. Every gate is linear, and the computational basis spans the finite joint register by [F6], so the same identity holds on every superposition. The forward and reverse loops each have $n$ Toffoli occurrences and there is one CNOT, giving the exact stated nonoracle gate-occurrence count; the algorithm has no branch and makes no oracle call.

Depends on

Used by

Oracle conversion and uncomputation examples Example

Dependency tree · two levels

37 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

Ronald de Wolf, Quantum Computing: Lecture Notes (arXiv:1907.09415v6) (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (17 April 2025) (standard reference, not scraped)