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

Generic No-Ancilla CNOT Lower Bound

Statement

Assume AC $_{ω}$ to form normalized Frobenius volume. For $n \geq 1$ , almost every $n$ -qubit unitary with respect to that measure requires at least $⌈ \frac{4^{n} - 3 n - 1}{4} ⌉$ CNOT gates in an exact circuit with arbitrary one-qubit gates and no ancillas. Under full AC, normalized Frobenius volume is normalized Haar measure, so the same is a Haar-almost-everywhere bound. This is a generic lower bound and is not a per-unitary assertion.

Facts & Assumptions

Given: AC $_{ω}$ , fixed $n$ , exact matrix equality, no ancillas, and the stated one-qubit/CNOT gate model.

[F1]

Parameter Count for a Fixed CNOT Skeleton: each fixed $m$ -CNOT skeleton has a normalized-Frobenius-volume-null image whenever $3 n + 4 m + 1 < 4^{n}$ ; under AC this is Haar-null.

[A1]

Assume AC $_{ω}$ for normalized Frobenius volume; the Haar wording assumes full AC (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice, The Axiom of Choice implies countable choice).

Proof

1.1givenalgebraalgebra

If $n = 1$ , the claimed lower bound is $⌈ (4 - 3 - 1) / 4 ⌉ = 0$ and holds because gate counts are nonnegative. Suppose $n \geq 2$ and put $M = ⌈ (4^{n} - 3 n - 1) / 4 ⌉$ , which is positive. For every integer $m < M$ , the ceiling property gives $4 m < 4^{n} - 3 n - 1$ , hence $3 n + 4 m + 1 < 4^{n}$ .

2.1step 1.1F1A1algebra

For fixed $n, m$ , only finitely many CNOT skeletons exist: at each of the $m$ positions one chooses an ordered pair of distinct wires from a finite set. By [F1], each skeleton image is null for normalized Frobenius volume; a finite union is null. For $n \geq 2$ , the finite union over $m = 0, \dots, M - 1$ remains null. Under full AC, [A1] and [F1] identify this as a Haar-null union.

3.1step 1.1step 2.1algebra∎

For $n \geq 2$ , outside the null union in step 2.1 no exact circuit with fewer than $M$ CNOTs exists, so almost every unitary needs at least $M$ CNOTs. For $n = 1$ , step 1.1 proves the zero bound directly. Since a null exceptional set may contain individual unitaries, the conclusion does not assert a positive lower bound for every unitary.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Vivek V. Shende, Igor L. Markov, and Stephen S. Bullock, Minimal Universal Two-Qubit CNOT-Based Circuits, arXiv:quant-ph/0308033v3 (standard reference, not scraped)