Result 4: CNOT minimizes one-cbit transmission time

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.cbit_optimal

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. Transmission means one use of the gate with normalized pure product inputs, without ancillas or prior shared entanglement. Encoding and decoding axes are free local choices fixed before the unknown input. Classical messages are encoded in orthogonal states and decoded with certainty; qubit transmission preserves every superposition with the same encoding and recovery. In simultaneous tasks, a receiver may choose its local decoder according to its own sent classical bit. For a transmission task $T$ , write $C_H(T)=\inf\{C_H(V):V\text{ performs }T\}$ . An asserted optimal gate both performs the task and has an ideal simulation at the displayed time, and every capable gate has at least its cost. Assume $\alpha_1>0$ . The CNOT gate, whose first qubit controls the second, attains

C_H(\mathrm{cbit}_{A\to B})=C_H(\mathrm{CNOT})=\frac{\pi}{4\alpha_1}.

The same gate is a minimizer for transmission in the opposite direction after free changes of local axes. Every gate capable of the chosen one-cbit task costs at least this much; no uniqueness of the minimizer is asserted.

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.10, Result 4: CNOT attains the minimum over every gate that can send one
perfect classical bit; its being a minimizer is not a uniqueness assertion. -/
theorem cbit_optimal (H : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    OptimalTask H CanCbit cnot (Real.pi / (4 * a 0)) ∧
      OptimalTask H (fun U => CanCbit (reverseParties U)) cnot
        (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. 10, Result 4: minimum interaction time for one classical bit

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=(a_0,a_1,a_2)$ , assume $H$ is Hermitian, $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}^2 a_j\sigma_j\otimes\sigma_j+K\otimes I+I\otimes L, \qquad(\sigma_0,\sigma_1,\sigma_2)=(X,Y,Z).

Here $X,Y,Z$ are the usual Pauli matrices. Define the interaction cost $C_H(V)\in[0,+\infty]$ as the infimum of all nonnegative times $t$ for which $H$ is Hermitian, $V$ is unitary, and, for every $\varepsilon>0$ , there are a finite pulse product

P=(A_m\otimes B_m)e^{-it_mH}\cdots(A_1\otimes B_1)e^{-it_1H}(A_0\otimes B_0),

with all $A_j,B_j$ one-qubit unitaries, $t_j\ge0$ , $\sum_{j=1}^m t_j=t$ , and a complex number $z$ with $|z|=1$ , such that $\|P-zV\|_{\mathrm{op}}<\varepsilon$ ; zero pulses are allowed, and the infimum of an empty set is $+\infty$ . Let $P_{\to}(V)$ mean that $V$ is unitary and there exist one-qubit unitaries $E,D$ , a unit vector $v\in\mathbb C^2$ , and unit vectors $w_0,w_1\in\mathbb C^2$ satisfying $V(E|i\rangle\otimes v)=w_i\otimes D|i\rangle$ for both bits $i$ . Let $P_{\leftarrow}(V)=P_{\to}(SVS)$ , where $S|i,j\rangle=|j,i\rangle$ . For each of the two predicates $P_{\to}$ and $P_{\leftarrow}$ , the CNOT matrix $N|i,j\rangle=|i,j\oplus i\rangle$ satisfies that predicate, admits the stated arbitrarily accurate pulse simulation at the exact time $t_*=\pi/(4a_0)$ , and satisfies

C_H(N)=t_*, \qquad \inf_{\{V:P(V)\}}C_H(V)=t_*, \qquad \forall V,\ P(V)\Longrightarrow C_H(N)\le C_H(V).

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