CNOT interaction content and cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.cnot_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$ . The gate $\mathrm{CNOT}:|i,j\rangle\mapsto|i,i\oplus j\rangle$ , with $\oplus$ denoting addition modulo two, has canonical interaction content $(\pi/4,0,0)$ up to local unitaries and global phase, and

C_H(\mathrm{CNOT})=\frac{\pi}{4\alpha_1}.

The interaction-content assertion concerns the physical local-equivalence class; the raw CNOT matrix is not an SU(4) canonical exponential.

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.1 and p.13: CNOT content is projective local equivalence, not
literal equality of the raw CNOT matrix with an SU(4) canonical exponential. -/
theorem cnot_content_cost (H : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    HasContent cnot ![Real.pi / 4, 0, 0] ∧
      interactionCost H cnot = ENNReal.ofReal (Real.pi / (4 * a 0)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 7, III.D.1: CNOT 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$ such that

(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 CNOT matrix $N|i,j\rangle=|i,j\oplus i\rangle$ is unitary and has content $d=(\pi/4,0,0)$ : this triple satisfies $d_1\le d_0$ , $|d_2|\le d_1$ , $d_0\le\pi/4$ , and there exist four one-qubit unitaries $A',B',C',D'$ such that

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

Moreover, $C_H(N)=\pi/(4a_0)$ , with the right side regarded as an extended nonnegative real. Here $C_H(N)$ is the infimum, with empty infimum $+\infty$ , of nonnegative times $t$ for which every $\varepsilon>0$ admits 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$ , whose operator-norm distance from $zN$ is strictly less than $\varepsilon$ for some $|z|=1$ ; the pulse list may be empty.

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