SWAP interaction content, branch choice, and cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.swap_content_cost

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $H$ be a Hermitian Hamiltonian on two qubits $A,B$ , with canonical interaction coefficients $\alpha=(\alpha_1,\alpha_2,\alpha_3)$ satisfying $\alpha_1\ge\alpha_2\ge|\alpha_3|$ . Local terms in $H$ are allowed. Local unitary controls are instantaneous and free, interaction intervals are nonnegative, and $\hbar=1$ . Write $C_H(U)$ for the infimum of the interaction durations of protocols implementing the gate $U$ , allowing the ideal limit of arbitrarily fine pulses at fixed total duration and disregarding global phase. This cost is an extended nonnegative real, with value $+\infty$ for an impossible simulation. Assume $\alpha_1>0$ . For $\mathrm{SWAP}:|i,j\rangle\mapsto|j,i\rangle$ , both $\frac{\pi}{4}(1,1,1)$ and $\frac{\pi}{4}(1,1,-1)$ describe its physical local-equivalence class, and

C_H(\mathrm{SWAP})=\frac{3\pi}{4(\alpha_1+\alpha_2+|\alpha_3|)}.

The positive branch attains this cost when $\alpha_3\ge0$ , and the negative branch when $\alpha_3\le0$ ; both tie at zero. A branch cost is the infimum of nonnegative times satisfying that branch of s-majorization.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P99

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P99

open scoped Matrix Kronecker NNReal ENNReal

open QAlgorithms.Papers.Independent.Information100.P10 (pauli)

open QAlgorithms.Papers.Independent.Information100.P32 (evolution)

noncomputable section

/-- PDF p.7, III.D.3: SWAP's two signed contents and cost; the positive branch is
optimal for positive a3, the negative branch for negative a3, and both tie at zero. -/
theorem swap_content_cost (H : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    HasContent swapGate ![Real.pi / 4, Real.pi / 4, Real.pi / 4] ∧
    HasContent swapGate ![Real.pi / 4, Real.pi / 4, -Real.pi / 4] ∧
    interactionCost H swapGate =
      ENNReal.ofReal (3 * Real.pi / (4 * (a 0 + a 1 + |a 2|))) ∧
    (0 ≤ a 2 → branchCost a ![Real.pi / 4, Real.pi / 4, Real.pi / 4] =
      interactionCost H swapGate) ∧
    (a 2 ≤ 0 → branchCost a ![Real.pi / 4, Real.pi / 4, -Real.pi / 4] =
      interactionCost H swapGate) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 7, III.D.3: SWAP content and interaction cost

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every complex two-qubit matrix $H$ and real triple $a$ , assume $H=H^\dagger$ , $a_1\le a_0$ , $|a_2|\le a_1$ , $a_0>0$ , and there exist one-qubit unitaries $A,B$ and Hermitian one-qubit matrices $K,L$ with

(A\otimes B)H(A\otimes B)^\dagger =\sum_{j=0}^2a_j\sigma_j\otimes\sigma_j+K\otimes I+I\otimes L, \qquad(\sigma_0,\sigma_1,\sigma_2)=(X,Y,Z).

Let $S|i,j\rangle=|j,i\rangle$ and $d_\pm=(\pi/4,\pi/4,\pm\pi/4)$ . For each of $d_+$ and $d_-$ , $S$ is unitary, the triple satisfies $d_1\le d_0$ , $|d_2|\le d_1$ , $d_0\le\pi/4$ , and some four one-qubit unitaries give $S=(A'\otimes B')\exp(-i\sum_jd_j\sigma_j\otimes\sigma_j)(C'\otimes D')$ . Its interaction cost is

C_H(S)=\frac{3\pi}{4(a_0+a_1+|a_2|)}.

Here $C_H(S)$ is the extended nonnegative infimum of times $t\ge0$ such that every $\varepsilon>0$ admits a finite product $(A_m\otimes B_m)e^{-it_mH}\cdots(A_1\otimes B_1)e^{-it_1H}(A_0\otimes B_0)$ , with one-qubit unitaries and nonnegative durations summing exactly to $t$ , whose operator-norm distance from $zS$ is strictly less than $\varepsilon$ for some $|z|=1$ ; empty pulse lists are allowed. For a real triple $x$ , define $o(x)=(h,\sum_j|x_j|-h-\ell,\eta)$ , where $h=\max_j|x_j|$ , $\ell=\min_j|x_j|$ , and $\eta=-\ell$ if $x_0x_1x_2<0$ , otherwise $\eta=\ell$ . Define $x\preceq_s y$ by the three inequalities

o(x)_0\le o(y)_0,\qquad o(x)_0+o(x)_1-o(x)_2\le o(y)_0+o(y)_1-o(y)_2,\qquad o(x)_0+o(x)_1+o(x)_2\le o(y)_0+o(y)_1+o(y)_2,

and $B_a(d)=\inf\{t\ge0:d\preceq_s ta\}$ , with the times embedded in $[0,+\infty]$ and empty infimum $+\infty$ . Then $a_2\ge0$ implies $B_a(d_+)=C_H(S)$ , and $a_2\le0$ implies $B_a(d_-)=C_H(S)$ ; both implications apply when $a_2=0$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph