Result 1: necessary and sufficient fast-control simulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.simulation_iff_integerShift

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$ . For every $t\ge0$ ,

U\text{ is ideally simulable using }H\text{ for total time }t\quad\Longleftrightarrow\quad\exists n\in\mathbb Z^3,\ \beta+(\pi/2)n\prec_s t\alpha.

The protocol is an operator protocol uniform over all input states. This is a two-way feasibility characterization, including $t=0$ .

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.4–6, Result 1: exact ideal fast-control feasibility iff some integer shift is
s-majorized by the available canonical interaction-time vector, also at time zero. -/
theorem simulation_iff_integerShift (H U : TwoMatrix) (a b : Triple) (t : ℝ)
    (hH : HasCanonicalHamiltonian H a) (hU : HasContent U b) (ht : 0 ≤ t) :
    IdealSimulates H U t ↔ ∃ n : Fin 3 → ℤ, SMajorized (contentIntegerShift b n) (t • a) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 4, Result 1: necessary and sufficient gate simulation condition

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$ , real triples $a,b$ , and real $t\ge0$ , 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$ such that $(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 unitaries $A',B',C',D'$ . For any real triple $x$ , let $\sigma(x)$ have first coordinate $\max_j|x_j|$ , second coordinate $\sum_j|x_j|-\max_j|x_j|-\min_j|x_j|$ , and third coordinate $-\min_j|x_j|$ if $x_0x_1x_2<0$ , or $+\min_j|x_j|$ otherwise; define $x\preceq_s y$ by

\sigma(x)_0\le\sigma(y)_0,\qquad \sigma(x)_0+\sigma(x)_1-\sigma(x)_2\le\sigma(y)_0+\sigma(y)_1-\sigma(y)_2,\qquad \sigma(x)_0+\sigma(x)_1+\sigma(x)_2\le\sigma(y)_0+\sigma(y)_1+\sigma(y)_2.

Then the following are equivalent: for every real $\varepsilon>0$ , there exist a finite list of nonnegative durations $\tau_1,\ldots,\tau_m$ , single-qubit unitary matrices $E_j,F_j$ for $j=0,\ldots,m$ , and $z\in\mathbb C$ with $|z|=1$ , such that $\sum_j\tau_j=t$ and

\left\|(E_m\otimes F_m)e^{-i\tau_mH}\cdots (E_1\otimes F_1)e^{-i\tau_1H}(E_0\otimes F_0)-zU\right\|_{\mathrm{op}}<\varepsilon;

and there exists an integer triple $n=(n_0,n_1,n_2)\in\mathbb Z^3$ such that

\left(b_0+\frac{\pi n_0}{2},\ b_1+\frac{\pi n_1}{2},\ b_2+\frac{\pi n_2}{2}\right)\preceq_s (ta_0,ta_1,ta_2).

The finite list may be empty, the time $t=0$ is included, and there is no positivity assumption on $a_0$ beyond the stated ordering conditions.

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