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.

Fresh-target NOT and OR gadgets

Statement

Let $a, b$ be distinct source wires and let $t$ be a distinct target wire initialized to $0$ . The chronological sequence $X (t)$ followed by ${CNOT}_{a \to t}$ writes $1 \oplus a$ into $t$ . The sequence ${CNOT}_{a \to t}$ , ${CNOT}_{b \to t}$ , $T (a, b, t)$ writes $a \lor b$ into $t$ , since $a \lor b = a \oplus b \oplus a b$ . Every source wire is unchanged.

Facts & Assumptions

Given: Distinct source and target wires and the stated Pauli- $X$ , CNOT, and Toffoli actions on the ordered computational basis. Verify the target values and preservation of controls.

[F1]

The Pauli matrices: In the ordered computational basis, $X = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ , which sends $∣ t ⟩$ to $∣ t \oplus 1 ⟩$ by matrix multiplication.

[F2]

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

[F3]

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

[F4]

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

[F5]

X, CNOT, Toffoli, and Fredkin are involutions: $X$ , CNOT, and Toffoli are unitary gates on their ordered registers.

Proof

1.1givenF1F2F4F5algebra

Starting with $t = 0$ , $X (t)$ sets it to $1$ and the following CNOT changes it to $1 \oplus a$ . Both gates target only $t$ , so $a$ is unchanged; [F5] supplies their gate unitarity.

2.1givenF2F3F4F5choosealgebra∎

For the second sequence, the final target is $0 \oplus a \oplus b \oplus a b$ . For $(a, b) = (0, 0), (0, 1), (1, 0), (1, 1)$ these values are $0, 1, 1, 1$ , respectively, which are exactly $a \lor b$ . The two CNOTs and Toffoli have controls only on $a, b$ , so neither source changes; [F5] supplies their gate unitarity.

Depends on

Used by

Dependency tree · two levels

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