Exchanging arbitrary qubits characterizes the SWAP class

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.twoQubitsCapability_cost

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

prove2quantum

For a two-qubit unitary $U$ , let $\beta$ be an actual interaction-content witness: $U$ is locally equivalent, up to global phase, to $U_\beta=\exp[-i\sum_{k=1}^3\beta_k\sigma_k\otimes\sigma_k]$ , where $\sigma_1,\sigma_2,\sigma_3$ are the Pauli matrices $X,Y,Z$ and $\pi/4\ge\beta_1\ge\beta_2\ge|\beta_3|$ . Transmission means one use of the gate with normalized pure product inputs, without ancillas or prior shared entanglement. Encoding and decoding axes are free local choices fixed before the unknown input. Classical messages are encoded in orthogonal states and decoded with certainty; qubit transmission preserves every superposition with the same encoding and recovery. In simultaneous tasks, a receiver may choose its local decoder according to its own sent classical bit. Simultaneous exchange of arbitrary unknown qubits is equivalent to membership in the SWAP local-equivalence class, where SWAP exchanges the two tensor factors. Precisely,

U\text{ exchanges two arbitrary qubits}\quad\Longleftrightarrow\quad U\sim_{\rm LU}\mathrm{SWAP}\quad\Longleftrightarrow\quad\beta_1=\beta_2=|\beta_3|=\pi/4.

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. For a transmission task $T$ , write $C_H(T)=\inf\{C_H(V):V\text{ performs }T\}$ . An asserted optimal gate both performs the task and has an ideal simulation at the displayed time, and every capable gate has at least its cost. For $\alpha_1>0$ , SWAP attains $C_H(\mathrm{qubit}_{A\leftrightarrow B})=3\pi/[4(\alpha_1+\alpha_2+|\alpha_3|)]$ . The characterization concerns free local axes, not literal equality of unprocessed matrices.

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.12, IV.B.4: only the SWAP local-equivalence class exchanges arbitrary qubits;
its two signed chamber endpoints and the minimum task interaction cost are retained. -/
theorem twoQubitsCapability_cost (U H : TwoMatrix) (b a : Triple)
    (hU : HasContent U b) (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    (CanTwoQubits U ↔ TwoQubitLocalEquivalent U swapGate) ∧
    (CanTwoQubits U ↔ b 0 = Real.pi / 4 ∧ b 1 = Real.pi / 4 ∧ |b 2| = Real.pi / 4) ∧
    OptimalTask H CanTwoQubits swapGate
      (3 * Real.pi / (4 * (a 0 + a 1 + |a 2|))) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 12, IV.B.4: exchanging arbitrary qubits

Read-back

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

Let $U,H$ be complex matrices on $\mathbb C^2\otimes\mathbb C^2$ , and let $b=(b_0,b_1,b_2)$ and $a=(a_0,a_1,a_2)$ be real triples. Let $X=\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$ , $Y=\left(\begin{smallmatrix}0&-i\\i&0\end{smallmatrix}\right)$ , $Z=\left(\begin{smallmatrix}1&0\\0&-1\end{smallmatrix}\right)$ , $J(d)=d_0X\otimes X+d_1Y\otimes Y+d_2Z\otimes Z$ , and $G(d)=e^{-iJ(d)}$ . Define $V\sim W$ to mean that $V=(A\otimes B)W(C\otimes D)$ for some one-qubit unitaries $A,B,C,D$ . Assume $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and $U\sim G(b)$ . Assume $H$ is Hermitian, $a_1\le a_0$ , $|a_2|\le a_1$ , and, for some one-qubit unitaries $A,B$ and Hermitian one-qubit matrices $K,L$ ,

(A\otimes B)H(A\otimes B)^\dagger=J(a)+K\otimes I+I\otimes L,

and assume $a_0>0$ . For a two-qubit matrix $V$ , let $\mathcal T(V)$ mean that $V$ is unitary and there exist one-qubit unitaries $E,F,R,S_1$ such that, for every pair of unit vectors $q,r\in\mathbb C^2$ ,

(R\otimes S_1)V(Eq\otimes Fr)=r\otimes q.

Let $S$ denote the swap matrix, $S|i,j\rangle=|j,i\rangle$ . Then

\mathcal T(U)\iff U\sim S, \qquad \mathcal T(U)\iff b_0=\frac\pi4\ \land\ b_1=\frac\pi4\ \land\ |b_2|=\frac\pi4.

Furthermore, $S$ has property $\mathcal T$ and is optimal for this property at time

t_*=\frac{3\pi}{4(a_0+a_1+|a_2|)}

in the following exact sense. Let $C_H(V)$ be the infimum in $[0,\infty]$ of nonnegative $t$ such that $H$ is Hermitian, $V$ is unitary, and for every $\varepsilon>0$ there are a finite pulse protocol of total interaction time exactly $t$ and a complex number $z$ with $|z|=1$ for which the protocol matrix is within operator norm strictly less than $\varepsilon$ of $zV$ . A pulse protocol starts at a product $A_0\otimes B_0$ of one-qubit unitaries and successively replaces its current matrix $P$ by $(A_j\otimes B_j)e^{-it_jH}P$ , with one-qubit unitaries $A_j,B_j$ , nonnegative durations $t_j$ , and $\sum_jt_j=t$ ; an empty pulse list is allowed, and an empty set of admissible times has infimum $+\infty$ . Such approximating protocols for $S$ exist at exactly $t_*$ , and

C_H(S)=t_*=\inf_{\{V:\mathcal T(V)\}}C_H(V), \qquad \forall V,\quad \mathcal T(V)\Longrightarrow C_H(S)\le C_H(V).

Here $a_0+a_1+|a_2|>0$ follows from the hypotheses, so $t_*>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