DCNOT interaction content and cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.dcnot_content_cost

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$ . Define $\mathrm{DCNOT}:|i,j\rangle\mapsto|j,i\oplus j\rangle$ , where $i,j\in\{0,1\}$ and $\oplus$ is addition modulo two. Its canonical interaction content and cost are

\beta(\mathrm{DCNOT})=\frac{\pi}{4}(1,1,0),\qquad C_H(\mathrm{DCNOT})=\frac{\pi}{2(\alpha_1+\alpha_2-|\alpha_3|)}.

The explicit basis action fixes the order of the two controlled-NOT operations.

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.7, III.D.2: DCNOT's basis action fixes the product convention; the cost
has denominator a1+a2-|a3| and numerator pi/2. -/
theorem dcnot_content_cost (H : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    HasContent dcnot ![Real.pi / 4, Real.pi / 4, 0] ∧
      interactionCost H dcnot =
        ENNReal.ofReal (Real.pi / (2 * (a 0 + a 1 - |a 2|))) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 7, III.D.2: DCNOT content and interaction cost

Read-back

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

For every complex two-qubit matrix $H$ and real triple $a$ , 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$ 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).

The matrix $D|i,j\rangle=|j,i\oplus j\rangle$ is unitary and has content $d=(\pi/4,\pi/4,0)$ : the inequalities $d_1\le d_0$ , $|d_2|\le d_1$ , $d_0\le\pi/4$ hold, and there exist four one-qubit unitaries $A',B',C',D'$ such that

D=(A'\otimes B')\exp\!\left(-i\sum_{j=0}^2d_j\sigma_j\otimes\sigma_j\right)(C'\otimes D').

Furthermore,

C_H(D)=\frac{\pi}{2(a_0+a_1-|a_2|)},

where the denominator is positive under the hypotheses and the value is regarded as an extended nonnegative real. The interaction cost $C_H(D)$ is the infimum, with empty infimum $+\infty$ , of nonnegative times $t$ for which, for every $\varepsilon>0$ , 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)$ , using one-qubit unitaries and nonnegative durations summing exactly to $t$ , differs in operator norm from $zD$ by strictly less than $\varepsilon$ for some $|z|=1$ ; zero pulses are allowed.

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