Result 2: the two-branch attained interaction cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.interactionCost_twoBranches

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. 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|$ . For real triples, $x\prec_s y$ means s-majorization: sort their absolute coordinates in descending order, give the smallest coordinate the sign of the product, and compare the first coordinate and the two sums $x_1+x_2\mp x_3$ . Put $\beta_n=\beta+(\pi/2)n$ for $n\in\mathbb Z^3$ . If $\alpha_1>0$ , there is a least feasible time $t_*$ , attained in the ideal control model, such that

C_H(U)=t_* = \min\{t\ge0:\beta\prec_s t\alpha\ \text{or}\ \beta_{(-1,0,0)}\prec_s t\alpha\}.

For zero canonical interaction, the cost is $0$ for local gates and $+\infty$ otherwise. This characterizes time cost using just two periodic branches.

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, Result 2 (abstract p.1): the two-branch minimum is attained for a nonzero
interaction. For a zero canonical interaction the extended cost is 0 on local gates and
infinity otherwise; no division by zero or empty real infimum is used. -/
theorem interactionCost_twoBranches (H U : TwoMatrix) (a b : Triple)
    (hH : HasCanonicalHamiltonian H a) (hU : HasContent U b) :
    (0 < a 0 → ∃ t : ℝ, IsLeast {s : ℝ | 0 ≤ s ∧
        (SMajorized b (s • a) ∨ SMajorized (secondShift b) (s • a))} t ∧
      IdealSimulates H U t ∧ interactionCost H U = ENNReal.ofReal t) ∧
    (a = 0 → (TwoQubitLocalEquivalent U 1 → interactionCost H U = 0) ∧
      (¬ TwoQubitLocalEquivalent U 1 → 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, Result 2: interaction cost; main result selected from the p.1 abstract

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 every pair of real triples $a,b$ , assume that $H$ is Hermitian, $a_1\le a_0$ , $|a_2|\le a_1$ , and there exist single-qubit unitary matrices $A,B$ and Hermitian single-qubit matrices $K,L$ satisfying $(A\otimes B)H(A\otimes B)^\dagger=J(a)+K\otimes I_2+I_2\otimes L$ , where $J(x)=x_0X\otimes X+x_1Y\otimes Y+x_2Z\otimes Z$ and $X,Y,Z$ are the standard Pauli matrices. Assume also that $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and $U=(A'\otimes B')e^{-iJ(b)}(C'\otimes D')$ for some single-qubit unitary matrices $A',B',C',D'$ . For a real triple $x$ , let $x_{\max}=\max_j|x_j|$ , $x_{\min}=\min_j|x_j|$ , and define

\sigma(x)=\left(x_{\max},\ \sum_{j=0}^{2}|x_j|-x_{\max}-x_{\min},\ \begin{cases}-x_{\min},&x_0x_1x_2<0,\\x_{\min},&x_0x_1x_2\ge0.\end{cases}\right).

Write $x\preceq_s y$ for the three inequalities $\sigma(x)_0\le\sigma(y)_0$ , $\sigma(x)_0+\sigma(x)_1-\sigma(x)_2\le\sigma(y)_0+\sigma(y)_1-\sigma(y)_2$ , and $\sigma(x)_0+\sigma(x)_1+\sigma(x)_2\le\sigma(y)_0+\sigma(y)_1+\sigma(y)_2$ . Say that $H$ ideally simulates $U$ at time $t$ when $H$ is Hermitian, $U$ is unitary, $t\ge0$ , and for every real $\varepsilon>0$ there exist a finite list of nonnegative durations $\tau_1,\ldots,\tau_m$ , single-qubit unitary matrices $A_j,B_j$ for $j=0,\ldots,m$ , and $z\in\mathbb C$ with $|z|=1$ , such that $\sum_{j=1}^{m}\tau_j=t$ and

\left\|(A_m\otimes B_m)e^{-i\tau_mH}\cdots (A_1\otimes B_1)e^{-i\tau_1H}(A_0\otimes B_0)-zU\right\|_{\mathrm{op}}<\varepsilon;

the empty list $m=0$ is allowed. Define $C_H(U)$ to be the infimum, in $[0,\infty]$ , of all nonnegative times at which this simulation condition holds, with infimum $+\infty$ if there are no such times. The conclusion is the conjunction of two implications: if $a_0>0$ , there exists a real $t$ which is the least element of

\left\{s\in\mathbb R:\ s\ge0,\quad b\preceq_s sa\ \text{or}\ (b_0-\pi/2,b_1,b_2)\preceq_s sa\right\},

such that $H$ ideally simulates $U$ at time $t$ and $C_H(U)=t$ , viewed as an extended nonnegative real; and if $a=(0,0,0)$ , then $C_H(U)=0$ whenever $U=(E\otimes F)(G\otimes T)$ for some single-qubit unitaries $E,F,G,T$ , whereas $C_H(U)=+\infty$ whenever no such four unitaries exist.

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