LemmaStatement: 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.

Two-CNOT Synthesis up to a Migrating Terminal Diagonal

Statement

Every $U \in U (4)$ factors exactly as $U = Δ V$ , where $Δ$ is diagonal in the ordered two-qubit computational basis and $V$ has a no-ancilla circuit with at most two CNOTs and arbitrary one-qubit gates. Scalar phases are retained. Consequently, if a chronological circuit has $N \geq 1$ arbitrary two-qubit slots all on the same two wires and each separator preserves every computational label on those two wires, the slots can be synthesized using at most $2 (N - 1) + 3$ CNOTs in total, leaving the separator operations unchanged. This counts only the slots' CNOTs.

Facts & Assumptions

Given: Exact matrices, arbitrary one-qubit gates, and both orientations of CNOT. In the second assertion each separator $S$ has the form $\sum_{x \in {0, 1}^{2}} ∣ x ⟩ ⟨ x ∣ \otimes S_{x}$ after grouping the two slot wires first.

[F1]

Exact Two-Qubit Cartan Decomposition gives $U = e^{i δ} (A \otimes B) N (a, b, c) (C \otimes E)$ , with local $S U (2)$ factors and $N (a, b, c) = \exp (i (a X X + b Y Y + c Z Z))$ ; here $X X = X \otimes X$ , and similarly for $Y Y, Z Z$ .

[F2]

The Pauli matrices specifies $X, Y, Z$ ; they square to identity and satisfy $X Y = i Z$ , $Y Z = i X$ , $Z X = i Y$ by matrix multiplication.

[F3]

Pauli formula for an axis rotation gives $R_{j} (t) = \cos (t / 2) I - i \sin (t / 2) σ_{j}$ .

[F4]

CNOT and Control-Target Order gives $C ∣ a, b ⟩ = ∣ a, b \oplus a ⟩$ for first-wire control.

[F5]

Exact Three-CNOT Synthesis of Two-Qubit Unitaries gives an exact three-CNOT synthesis for the last arbitrary slot, including its scalar phase.

[F6]

Denotational semantics of a finite layered circuit places later chronological operations to the left in a matrix product.

[F7]

Finite circuit resource accounting counts the stated gate occurrences and wires.

[F8]

Every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ supplies real arguments for unit complex scalars; $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle supplies an angle for each real unit-circle pair; For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ supplies multiplicativity of determinants.

Proof

1.1givenF1F2F8algebrachoose

Normalize $U$ to $U_{0} = λ^{- 1} U \in S U (4)$ with $∣ λ ∣ = 1$ : unitarity and the determinant permutation formula give $∣ \det U ∣ = 1$ , so choose $λ = e^{i \arg (\det U) / 4}$ using [F8]. Put $J = Y Y$ and $γ (W) = W J W^{T} J$ . For a $2 \times 2$ matrix $A$ , direct multiplication gives $A Y A^{T} = (\det A) Y$ . Therefore local $K = A \otimes B$ with $A, B \in S U (2)$ satisfies $K J K^{T} = J$ . It follows by substitution and cyclicity of trace that $tr γ (K_{1} W K_{2}) = tr γ (W)$ for local $S U (2)$ matrices $K_{1}, K_{2}$ . This identity uses transpose, not adjoint.

2.1step 1.1F2F8algebrachoose

Put $P = Z Z$ and $D (t) = e^{i t P} = \cos t I + i \sin t P$ . Since $P$ is diagonal with two $+ 1$ and two $- 1$ entries, $D (t)$ is diagonal unitary with determinant one. Also $J P = P J$ and $D (t)^{T} = D (t)$ . Hence $tr γ (D (t) U_{0}) = tr (D (t)^{2} γ (U_{0})) = \cos (2 t) tr γ (U_{0}) + i \sin (2 t) tr (P γ (U_{0}))$ . Its imaginary part is $a_{0} \cos (2 t) + b_{0} \sin (2 t)$ , with real $a_{0} = Im tr γ (U_{0})$ and $b_{0} = Re tr (P γ (U_{0}))$ . If both vanish, take $t = 0$ . Otherwise choose $\cos (2 t) = b_{0} / (a_{0}^{2} + b_{0}^{2})^{1 / 2}$ , $\sin (2 t) = - a_{0} / (a_{0}^{2} + b_{0}^{2})^{1 / 2}$ , possible by [F8]. Thus $V = D (t) U_{0} \in S U (4)$ has real $tr γ (V)$ .

3.1step 1.1step 2.1F1F2F8algebra

Apply [F1] to $V$ . The determinant of each local factor and of $N (a, b, c)$ is one: the latter follows from the simultaneous Pauli eigenvalue sign lists $(+, -, +, -)$ , $(-, +, +, -)$ and $(+, +, -, -)$ in the Cartan proof, each with sum zero. Thus $e^{4 i δ} = 1$ and $e^{2 i δ} \in {1, - 1}$ . The commuting symmetric matrices $X X, Y Y, Z Z$ commute with $J$ , so $γ (N) = N^{2}$ . Expand their exponentials using [F2]. Since $X X Y Y Z Z = - I$ and all nonconstant products except this triple are traceless, $tr γ (V) = e^{2 i δ} 4 (\cos (2 a) \cos (2 b) \cos (2 c) + i \sin (2 a) \sin (2 b) \sin (2 c))$ . Its imaginary part is zero, so at least one Cartan coordinate is an integer multiple of $π / 2$ .

4.1step 3.1F2F3algebra

If, for example, $c = k π / 2$ , its factor is $e^{i c Z Z} = i^{k} (Z Z)^{k}$ , a scalar times a product of one-qubit Pauli gates. It commutes with the other Cartan factors and can be absorbed into the exterior local factors. The same applies to $a$ or $b$ . Simultaneous conjugation on both qubits by a one-qubit rotation permuting the Pauli axes moves the absent coordinate to $Z Z$ . Such permutations are obtained from $R_{x} (π / 2), R_{y} (π / 2), R_{z} (π / 2)$ in [F3]; their conjugations exchange the other two axes up to signs, and each sign is squared in a Pauli product. Thus $V$ is a scalar times exterior local gates and $N (α, β, 0)$ for real $α, β$ . All scalar factors are retained as one-qubit scalar gates.

5.1step 2.1step 4.1F2F3F4F7algebra

Let $L = R_{x} (π / 2) \otimes R_{x} (π / 2)$ and let $C$ be [F4]. Its basis action gives $C (X \otimes I) C = X X$ and $C (I \otimes Z) C = Z Z$ . Formula [F3] gives $L X X L^{*} = X X$ and $L Z Z L^{*} = Y Y$ (each rotated $Z$ is $- Y$ ). Therefore the exact identity $N (α, β, 0) = L C (R_{x} (- 2 α) \otimes R_{z} (- 2 β)) C L^{*}$ follows by exponentiating the commuting generators. This uses two CNOTs and one-qubit gates only. Combined with step 4.1 it synthesizes $V$ with two CNOTs. Since $V = D (t) λ^{- 1} U$ , the required diagonal is $Δ = λ D (t)^{- 1}$ and $U = Δ V$ exactly. No CNOT is spent implementing $Δ$ in this factorization assertion.

6.1step 5.1F5F6F7inductionalgebra∎

Write the first two chronological slots as $U_{1}, S_{1}, U_{2}$ . By step 5.1, $U_{1} = Δ_{1} V_{1}$ , so the product in [F6] is $U_{2} S_{1} Δ_{1} V_{1}$ . The separator hypothesis gives $S_{1} (Δ_{1} \otimes I) = (Δ_{1} \otimes I) S_{1}$ branch by branch, even if its $S_{1, x}$ act on several other wires. The product becomes $(U_{2} Δ_{1}) S_{1} V_{1}$ . The next slot is still an arbitrary unitary on the same two wires. Factor it again and continue. Each of the first $N - 1$ slots now uses at most two CNOTs; the final accumulated slot uses at most three by [F5]. All diagonals are absorbed, every separator is unchanged, and no wire is added. For $N = 1$ the process performs no migration and uses only the three-CNOT base case. This proves the count $2 (N - 1) + 3$ and exact equality.

Depends on

Used by

Exact QSD CNOT Upper Bound Theorem

Dependency tree · two levels

45 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, Stephen S. Bullock, and Igor L. Markov, Synthesis of Quantum Logic Circuits, Theorem 14 and Appendix A.2 (standard reference, not scraped)
Vivek V. Shende, Igor L. Markov, and Stephen S. Bullock, Smaller Two-Qubit Circuits for Quantum Communication and Computation (standard reference, not scraped)