Prove2Me

Coherent exchange under the transmon coupling Hamiltonian realises iSWAP

Proved
SuperconductingQC.coupling_evolution_eq_iSWAP_conjTranspose

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

quantum-computingquantum-gates

Let ℏ≠0\hbar\neq0 and J≠0J\neq0 be real numbers and let

H=ℏJ2(σ1xσ2x+σ1yσ2y)H=\frac{\hbar J}{2}\left(\sigma^x_1\sigma^x_2+\sigma^y_1\sigma^y_2\right)

be the Hamiltonian of two capacitively coupled transmons. Then evolving for time t=π/(2J)t=\pi/(2J) gives

exp⁡(−itℏH)∣t=π/(2J)=iSWAP†,\exp\left(-\frac{i t}{\hbar}H\right)\Big|_{t=\pi/(2J)}=\mathrm{iSWAP}^{\dagger},

the conjugate transpose of the iSWAP gate, i.e. the gate ∣00⟩↦∣00⟩|00\rangle\mapsto|00\rangle, ∣01⟩↦−i∣10⟩|01\rangle\mapsto -i|10\rangle, ∣10⟩↦−i∣01⟩|10\rangle\mapsto -i|01\rangle, ∣11⟩↦∣11⟩|11\rangle\mapsto|11\rangle.

This makes precise the statement that two-qubit gates of iSWAP type are produced by coherent exchange in the coupled-transmon Hamiltonian. Since iSWAP† and iSWAP differ by single-qubit gates (iSWAP†=(Z⊗Z) iSWAP\mathrm{iSWAP}^\dagger=(Z\otimes Z)\,\mathrm{iSWAP}), it links the physical Hamiltonian to the gate set of the goal theorem.

Formalization Note JJ may be negative (then t<0t<0); the identity holds for every nonzero JJ.

Preamble
import Mathlib
import Definitions.Def_SuperconductingQC_Gates

open scoped Matrix Kronecker
Formal statement
namespace SuperconductingQC

theorem coupling_evolution_eq_iSWAP_conjTranspose (hbar J : ℝ) (hhbar : hbar ≠ 0)
    (hJ : J ≠ 0) :
    timeEvolution hbar (Real.pi / (2 * J)) (couplingHamiltonian hbar J) = 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 'Quantum gates' (iSWAP via coherent exchange) and section 'Transmon' (two-transmon Hamiltonian H = (ħJ/2)(σ1x σ2x + σ1y σ2y))
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