Single-qubit gates and iSWAP form a universal gate set

Proved

SuperconductingQC.closure_singleQubit_iSWAP_eq_top

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

quantum-computingquantum-gates

Let $n\ge1$ and let $U(2^n)$ be the group of unitary operators on $n$ qubits. The subgroup generated by all single-qubit gates $U^{(k)}$ ( $U\in U(2)$ , $k$ any qubit) together with the iSWAP gate placed on any ordered pair of distinct qubits is all of $U(2^n)$ :

\big\langle\,\mathcal S_n\cup\mathcal G_n(\mathrm{iSWAP})\,\big\rangle=U(2^n).

Equivalently, every $n$ -qubit unitary is an exact finite product of single-qubit gates and iSWAP gates. This is the precise content of the statement that single-qubit gates combined with the two-qubit gates available on superconducting hardware form a universal gate set.

Formalization Note Universality is exact (the generated group, not its closure in the topological sense). $n=0$ is excluded for the same reason as in the CNOT version.

Preamble

import Mathlib
import Definitions.Def_SuperconductingQC_Gates

open scoped Matrix Kronecker

Formal statement

namespace SuperconductingQC

theorem closure_singleQubit_iSWAP_eq_top (n : ℕ) (hn : 1 ≤ n) :
    Subgroup.closure (singleQubitGates n ∪ twoQubitGateInstances n iSWAP) = ⊤ := by
  sorry

end SuperconductingQC

Source

Wikipedia, "Superconducting quantum computing" (PDF snapshot supplied by the mission author, retrieved 2026-10-13), https://en.wikipedia.org/wiki/Superconducting_quantum_computing; section 'Criteria for a viable quantum processor': 'single-qubit gates combined with two-qubit gates form a universal gate set', with the two-qubit gate iSWAP of section 'Quantum 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