Three finite interaction intervals suffice for a pure interaction

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.threeSteps_suffice

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$ and $H=\sum_{i,j=1}^3 c_{ij}\sigma_i\otimes\sigma_j$ with real $c_{ij}$ and Pauli matrices $\sigma_1=X,\sigma_2=Y,\sigma_3=Z$ , so there are no local or scalar terms. For every two-qubit gate $U$ there is a finite protocol with local controls and nonnegative intervals $t_1,\ldots,t_m$ such that

m\le3,\qquad U_{\rm protocol}=e^{i\theta}U,\qquad \sum_{j=1}^{m}t_j=C_H(U).

Here $\theta$ is a real global phase. Zero intervals and local target gates are allowed. For a pure interaction, an optimal protocol needs no infinitesimal simulation.

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.6, III.C: for a pure interaction every gate has an optimal finite exact
protocol with at most three nonnegative interaction intervals (zero durations allowed). -/
theorem threeSteps_suffice (H U : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (hPure : PureInteraction H)
    (ha : 0 < a 0) (hU : IsGate U) :
    ∃ p : PulseProtocol, p.pulses.length ≤ 3 ∧
      SamePhysicalGate (protocolMatrix H p) U ∧
      (protocolTime p : ℝ≥0∞) = interactionCost H U := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 6, III.C: three finite interaction steps for a pure interaction

Read-back

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

For every pair of complex two-qubit matrices $H,U$ and real triple $a$ , assume $H=H^\dagger$ , $U$ is unitary, $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$ satisfying

(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).

Assume additionally that there are real coefficients $c_{ij}$ , for $i,j\in\{0,1,2\}$ , with $H=\sum_i\sum_jc_{ij}\sigma_i\otimes\sigma_j$ . Define $C_H(U)$ to be the extended nonnegative infimum of times $t\ge0$ such that, for every $\varepsilon>0$ , some finite pulse 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, durations $t_j\ge0$ summing exactly to $t$ , and a scalar $z$ of modulus one, has operator-norm distance strictly less than $\varepsilon$ from $zU$ ; the empty infimum is $+\infty$ . Then there exist an integer $m$ with $0\le m\le3$ , one-qubit unitaries $A_0,B_0,\ldots,A_m,B_m$ , nonnegative real durations $t_1,\ldots,t_m$ , and a complex number $z$ with $|z|=1$ , such that

(A_m\otimes B_m)e^{-it_mH}\cdots(A_1\otimes B_1)e^{-it_1H}(A_0\otimes B_0)=zU, \qquad \sum_{j=1}^m t_j=C_H(U).

The time equality is taken in $[0,+\infty]$ ; zero durations and an empty pulse list are included.

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