Ising and exchange interactions give different gate orderings

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.interactionDependent_examples

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

prove2quantum

Use instantaneous free local controls and the ideal interaction-cost model on exactly two qubits. Write $H_I=X\otimes X$ for unit-strength Ising interaction and $H_E=X\otimes X+Y\otimes Y+Z\otimes Z$ for unit-strength exchange interaction, where $X,Y,Z$ are the Pauli spin matrices. With CNOT, DCNOT and SWAP acting as $|i,j\rangle\mapsto|i,i\oplus j\rangle$ , $|j,i\oplus j\rangle$ and $|j,i\rangle$ , respectively,

\begin{aligned}C_{H_I}(\mathrm{CNOT})&=\pi/4<C_{H_I}(\mathrm{DCNOT})=\pi/2<C_{H_I}(\mathrm{SWAP})=3\pi/4,\\C_{H_E}(\mathrm{SWAP})&=\pi/4<C_{H_E}(\mathrm{DCNOT})=\pi/2.\end{aligned}

These examples show that the ordering by cost can change with the interaction. Hamiltonian strength one is allowed even though a gate-content coordinate is bounded by $\pi/4$ .

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.E: unit-strength Ising and exchange interactions give different gate
orderings. Strength 1 is not constrained by the gate-chamber bound pi/4. -/
theorem interactionDependent_examples :
    interactionCost (canonicalPauliInteraction ![1, 0, 0]) cnot = ENNReal.ofReal (Real.pi / 4) ∧
    interactionCost (canonicalPauliInteraction ![1, 0, 0]) dcnot = ENNReal.ofReal (Real.pi / 2) ∧
    interactionCost (canonicalPauliInteraction ![1, 0, 0]) swapGate =
      ENNReal.ofReal (3 * Real.pi / 4) ∧
    interactionCost (canonicalPauliInteraction ![1, 0, 0]) cnot <
      interactionCost (canonicalPauliInteraction ![1, 0, 0]) dcnot ∧
    interactionCost (canonicalPauliInteraction ![1, 0, 0]) dcnot <
      interactionCost (canonicalPauliInteraction ![1, 0, 0]) swapGate ∧
    interactionCost (canonicalPauliInteraction ![1, 1, 1]) swapGate = ENNReal.ofReal (Real.pi / 4) ∧
    interactionCost (canonicalPauliInteraction ![1, 1, 1]) dcnot = ENNReal.ofReal (Real.pi / 2) ∧
    interactionCost (canonicalPauliInteraction ![1, 1, 1]) swapGate <
      interactionCost (canonicalPauliInteraction ![1, 1, 1]) dcnot := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 7, III.E: interaction-dependent ordering examples

Read-back

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

Let $X,Y,Z$ be the usual Pauli matrices, let $H_x=X\otimes X$ , and let $H_{\mathrm{iso}}=X\otimes X+Y\otimes Y+Z\otimes Z$ . Let $N|i,j\rangle=|i,j\oplus i\rangle$ , $D|i,j\rangle=|j,i\oplus j\rangle$ , and $S|i,j\rangle=|j,i\rangle$ , for bits $i,j$ . For these Hermitian Hamiltonians and unitary targets, define $C_H(V)$ as the infimum in $[0,+\infty]$ , with empty infimum $+\infty$ , of nonnegative times $t$ admitting the following approximation property: for every $\varepsilon>0$ , some finite product $(A_m\otimes B_m)e^{-it_mH}\cdots(A_1\otimes B_1)e^{-it_1H}(A_0\otimes B_0)$ , using one-qubit unitaries and nonnegative durations summing exactly to $t$ , has operator-norm distance strictly less than $\varepsilon$ from $zV$ for some complex $|z|=1$ ; the pulse list can be empty. The declaration asserts all eight statements

\begin{gathered} C_{H_x}(N)=\pi/4,\qquad C_{H_x}(D)=\pi/2,\qquad C_{H_x}(S)=3\pi/4,\\ C_{H_x}(N)<C_{H_x}(D),\qquad C_{H_x}(D)<C_{H_x}(S),\\ C_{H_{\mathrm{iso}}}(S)=\pi/4,\qquad C_{H_{\mathrm{iso}}}(D)=\pi/2,\qquad C_{H_{\mathrm{iso}}}(S)<C_{H_{\mathrm{iso}}}(D), \end{gathered}

where the displayed finite values are embedded in the extended nonnegative reals.

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