DefinitionDefinition: AI-adaptedProof: AI-generatedPipeline-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.

CNOT and Control-Target Order

Definition

In the ordered two-qubit basis $∣ 00 ⟩, ∣ 01 ⟩, ∣ 10 ⟩, ∣ 11 ⟩$ , the controlled-NOT with first wire control and second wire target is

${CNOT}_{1 \to 2} ∣ a, t ⟩ = ∣ a, t \oplus a ⟩, a, t \in {0, 1} .$

Equivalently, it is the control block $C (X) = diag (I, X)$ of Controlled Unitary Access, where $X$ is the Pauli bit-flip matrix. The wire order is part of the definition.

Facts & Assumptions

Given: The two ordered qubit factors, their computational basis, and $a, t \in {0, 1}$ .

[L1]

Controlled Unitary Access defines $C (X)$ to fix the control-zero block and apply $X$ in the control-one block. Its carrier is present in this batch.

[L2]

The Pauli matrices defines the exact Pauli- $X$ matrix in the ordered computational basis. Its current draft definition body was read; its item is now present in the QC07 manifest and page; the page remains draft.

[L3]

The computational basis is orthonormal: each qubit computational basis is orthonormal.

[L4]

The product basis is orthonormal and tensor dimensions multiply: elementary tensors of ordered orthonormal factor bases form an orthonormal basis of the ordered tensor register.

[L5]

Exact one-qubit gates and rotations verifies that the Pauli- $X$ matrix is unitary; this result is in the dependency closure of [L1].

Verification

1.1givenL1L2L5

By [L5], $X$ is unitary, so [L1] defines its controlled block. For control bit $a = 0$ , the first block of $C (X)$ is the identity, so $∣ 0, 0 ⟩ \mapsto ∣ 0, 0 ⟩$ and $∣ 0, 1 ⟩ \mapsto ∣ 0, 1 ⟩$ .

1.2givenL1L2algebra

For control bit $a = 1$ , [L2] flips the target, so $∣ 1, 0 ⟩ \mapsto ∣ 1, 1 ⟩$ and $∣ 1, 1 ⟩ \mapsto ∣ 1, 0 ⟩$ . These are exactly $∣ a, t \oplus a ⟩$ for the two remaining basis inputs.

2.1step 1.1step 1.2L3L4algebra∎

The columns in the stated ordered basis are therefore $e_{00}, e_{01}, e_{11}, e_{10}$ , giving $CNOT = (\begin{array}{cccc} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{array})$ . By [L3] and [L4], this is a permutation of an orthonormal basis, so it preserves the sum of squared coordinate moduli and thus every vector norm. The permutation is its own inverse, so the operator is invertible and hence unitary. The displayed action fixes the stated control-target order.

Depends on

Used by

Costed coherent evaluation of cyclic group powers Algorithm
Dense-coding procedure Algorithm
Gray-Path Synthesis of a Two-Level Gate Algorithm
Power-of-two dihedral hidden-subgroup sieve Algorithm
Qubit teleportation procedure Algorithm
Reversible binary dot-product query Algorithm
Reversible embedding of a Boolean circuit Algorithm
Stabilizer encoder by symplectic elimination Algorithm
QFT ideal and finite-set gate-cost models Definition
Toffoli and Fredkin gates Definition
A reversible AND oracle with clean work Example
Oracle conversion and uncomputation examples Example
A SWAP Is Three CNOTs Lemma
Clean reversible controlled multiplication by a cyclic constant Lemma
CNOT Pauli action Lemma
Effective synthesis of fixed-dimensional unitaries Lemma
Exact Central Controlled-Z Absorption at a QSD Node Lemma
Exact Gray-code synthesis of multiplexed y- and z-axis rotations Lemma
Fresh-target NOT and OR gadgets Lemma
Gray-Code Synthesis of a Multiplexed Axis Rotation Lemma
Gray-code synthesis of a multiplexed Z rotation Lemma
Linear Multicontrolled X with One Borrowed Wire Lemma
Ninefold nearest-neighbor multiplexor routing Lemma
Parameter Count for a Fixed CNOT Skeleton Lemma
Toffoli computes into a clean target and uncomputes it Lemma
Twice-Concatenated Steane Code and Its Transversal Clifford Gates Lemma
Two-CNOT Synthesis up to a Migrating Terminal Diagonal Lemma
Uniform interpretation of an input-generated quantum circuit Lemma
X, CNOT, Toffoli, and Fredkin are involutions Lemma
2-Local Hamiltonian is QMA-complete Theorem
Bell preparation transform and inverse Theorem
Compute-copy-uncompute restores clean workspace Theorem
Compute-copy-uncompute yields a clean coherent function query Theorem
Correctness of Gray-Path Two-Level Synthesis Theorem
CSS syndrome correction Theorem
Exact Controlled One-Qubit Unitary with Two CNOTs Theorem
Exact finite unitary synthesis from cosine-sine recursion Theorem
Exact QSD CNOT Upper Bound Theorem
Exact Three-CNOT Synthesis of Two-Qubit Unitaries Theorem
Gate, workspace, and serial-depth costs of reversible embedding Theorem

…and 7 more results.

Dependency tree · two levels

22 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)
John Preskill, Quantum Computation, Chapter 6: Quantum Algorithms (standard reference, not scraped)