The exact restricted-chamber criterion and one-branch cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.restrictedCost

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$ . Write $\beta^- =\beta-(\pi/2,0,0)$ . For a nonzero interaction ( $\alpha_1>0$ ),

\beta\prec_s\beta^-\quad\Longleftrightarrow\quad\beta_1+|\beta_3|\le\pi/4.

Under this restriction, $C_H(U)=\min\{t\ge0:\beta\prec_s t\alpha\}$ , with the minimum attained in the ideal control model. The shifted vector is s-ordered before comparison, giving $(\pi/2-\beta_1,\beta_2,-\beta_3)$ .

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 pp.6–7, III.C: the exact criterion for dropping the second branch, and the
resulting attained one-branch interaction-cost formula. -/
theorem restrictedCost (H U : TwoMatrix) (a b : Triple)
    (hH : HasCanonicalHamiltonian H a) (hU : HasContent U b) (ha : 0 < a 0) :
    (SMajorized b (secondShift b) ↔ b 0 + |b 2| ≤ Real.pi / 4) ∧
    (b 0 + |b 2| ≤ Real.pi / 4 → ∃ t : ℝ,
      IsLeast {s : ℝ | 0 ≤ s ∧ SMajorized b (s • a)} t ∧
      IdealSimulates H U t ∧ interactionCost H U = ENNReal.ofReal t) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 6, III.C: when the second shift can be omitted

Read-back

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

For all complex two-qubit matrices $H,U$ and real triples $a,b$ , 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).

Also assume $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and $U=(A'\otimes B')\exp(-i\sum_jb_j\sigma_j\otimes\sigma_j)(C'\otimes D')$ for some four one-qubit unitaries. For any real triple $x$ , let $h=\max(|x_0|,|x_1|,|x_2|)$ , $\ell=\min(|x_0|,|x_1|,|x_2|)$ , and

o(x)=\bigl(h,\ |x_0|+|x_1|+|x_2|-h-\ell,\ \eta\bigr), \qquad \eta=\begin{cases}-\ell&x_0x_1x_2<0,\\ \ell&x_0x_1x_2\ge0.\end{cases}

Write $x\preceq_s y$ when $o(x)_0\le o(y)_0$ , $o(x)_0+o(x)_1-o(x)_2\le o(y)_0+o(y)_1-o(y)_2$ , and $o(x)_0+o(x)_1+o(x)_2\le o(y)_0+o(y)_1+o(y)_2$ . Then

b\preceq_s(b_0-\pi/2,b_1,b_2) \quad\Longleftrightarrow\quad b_0+|b_2|\le\pi/4.

Moreover, if $b_0+|b_2|\le\pi/4$ , there exists a real $t$ such that $t\ge0$ , $b\preceq_s ta$ , and $t\le s$ for every real $s\ge0$ satisfying $b\preceq_s sa$ ; at this same exact time $t$ , $U$ admits arbitrarily accurate pulse simulation under $H$ , and its interaction cost is $t$ . Here simulation at time $t$ means that for every $\varepsilon>0$ there is 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, nonnegative durations summing to $t$ , and some $|z|=1$ , whose operator-norm distance from $zU$ is strictly less than $\varepsilon$ ; zero pulses are allowed. The interaction cost is the infimum of all such nonnegative times in $[0,+\infty]$ , with empty infimum $+\infty$ .

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