Result 3: interaction-independent order in the restricted chamber

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.nonlocalOrder_iff

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

prove2quantum

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$ . Let $V$ have canonical content $\beta^V$ , and write $\beta^U=\beta$ for that of $U$ . Assume $\beta^U_1+|\beta^U_3|\le\pi/4$ and $\beta^V_1+|\beta^V_3|\le\pi/4$ . With interaction cost in the ideal free-local-control model, define $U$ to be more nonlocal than $V$ when $C_H(V)\le C_H(U)$ for every Hermitian two-qubit Hamiltonian $H$ . Then

[\,\forall H,\ C_H(V)\le C_H(U)\,]\quad\Longleftrightarrow\quad\beta^V\prec_s\beta^U.

The comparison is a preorder on gates and descends to local-equivalence classes. Local gates are included.

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.8, Result 3 (definition pp.7–8): both contents must lie in the restricted
chamber. Includes local gates without the proof's invalid C_H(U)=1 shortcut there. -/
theorem nonlocalOrder_iff (U V : TwoMatrix) (bU bV : Triple)
    (hU : HasContent U bU) (hV : HasContent V bV)
    (hRU : bU 0 + |bU 2| ≤ Real.pi / 4) (hRV : bV 0 + |bV 2| ≤ Real.pi / 4) :
    MoreNonlocal U V ↔ SMajorized bV bU := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 8, Result 3: interaction-independent order in the restricted chamber

Read-back

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

For every pair of complex two-qubit matrices $U,V$ and real triples $b^U,b^V$ , assume, for each pair $(W,b)=(U,b^U)$ and $(W,b)=(V,b^V)$ , that $W$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and there exist single-qubit unitary matrices $A,B,C,D$ such that $W=(A\otimes B)e^{-iJ(b)}(C\otimes D)$ , where $J(b)=b_0X\otimes X+b_1Y\otimes Y+b_2Z\otimes Z$ and $X,Y,Z$ are the standard Pauli matrices; assume additionally that $b^U_0+|b^U_2|\le\pi/4$ and $b^V_0+|b^V_2|\le\pi/4$ . For a Hermitian two-qubit matrix $H$ and a unitary two-qubit matrix $W$ , define $C_H(W)\in[0,\infty]$ as the infimum of all $t\ge0$ such that, 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 a complex $z$ with $|z|=1$ , satisfying $\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)-zW\right\|_{\mathrm{op}}<\varepsilon;

empty lists are allowed and the infimum of an empty set of feasible times is $+\infty$ . For any real triple $x$ , define $\sigma(x)$ to have coordinates $\max_j|x_j|$ , $\sum_j|x_j|-\max_j|x_j|-\min_j|x_j|$ , and the signed minimum absolute coordinate, negative when $x_0x_1x_2<0$ and nonnegative otherwise. The conclusion is that $C_H(V)\le C_H(U)$ for every Hermitian two-qubit matrix $H$ if and only if all three inequalities

\sigma(b^V)_0\le\sigma(b^U)_0,\qquad \sigma(b^V)_0+\sigma(b^V)_1-\sigma(b^V)_2 \le\sigma(b^U)_0+\sigma(b^U)_1-\sigma(b^U)_2,\qquad \sigma(b^V)_0+\sigma(b^V)_1+\sigma(b^V)_2 \le\sigma(b^U)_0+\sigma(b^U)_1+\sigma(b^U)_2

hold. The quantifier over $H$ includes the zero matrix and all other Hermitian two-qubit matrices.

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