CNOT from two iSWAP gates and single-qubit gates

Proved

SuperconductingQC.cnot_eq_locals_two_iSWAP

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

quantum-computingquantum-gates

There exist single-qubit unitaries $A,B,C,D,E,F\in U(2)$ such that

\mathrm{CNOT}=(A\otimes B)\,\mathrm{iSWAP}\,(C\otimes D)\,\mathrm{iSWAP}\,(E\otimes F),

where CNOT has the first qubit as control.

The equality is exact (no global phase is discarded; a phase can be absorbed into $A$ ). This is the bridge from the CNOT-based universality theorem to the iSWAP gate natively available on coupled transmons.

Preamble

import Mathlib
import Definitions.Def_SuperconductingQC_Gates

open scoped Matrix Kronecker

Formal statement

namespace SuperconductingQC

theorem cnot_eq_locals_two_iSWAP :
    ∃ A B C D E F : Matrix (Fin 2) (Fin 2) ℂ,
      A ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ B ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧
      C ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ D ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧
      E ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ F ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧
      CNOT = (A ⊗ₖ B) * iSWAP * (C ⊗ₖ D) * iSWAP * (E ⊗ₖ F) := by
  sorry

end SuperconductingQC

Source

N. Schuch, J. Siewert, Natural two-qubit gate for quantum computation using the XY interaction, Phys. Rev. A 67, 032301 (2003), https://doi.org/10.1103/PhysRevA.67.032301 (CNOT from two iSWAP gates)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph