Result 5: optimal simultaneous bidirectional cbits

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.twoCbits_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$ . A gate with interaction content $\beta_*=\frac{\pi}{4}(1,1,2\alpha_3/(\alpha_1+\alpha_2))$ attains the simultaneous bidirectional-cbit cost

C_H(\mathrm{cbit}_{A\leftrightarrow B})=\frac{\pi}{2(\alpha_1+\alpha_2)}.

The displayed content lies in the gate chamber. The bound applies to every capable gate and scales inversely with the strength of $H$ .

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.11, Result 5: an attaining content and the minimum over all simultaneous
bidirectional classical-bit gates. Arbitrary nonzero Hamiltonian strength is allowed. -/
theorem twoCbits_optimal (H : TwoMatrix) (a : Triple)
    (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    HasContent (contentGate (optimalTransmissionContent a)) (optimalTransmissionContent a) ∧
      OptimalTask H CanTwoCbits (contentGate (optimalTransmissionContent a))
        (Real.pi / (2 * (a 0 + a 1))) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 11, Result 5: time-optimal bidirectional classical transmission

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).

Put $d=(\pi/4,\pi/4,(\pi/4)\,2a_2/(a_0+a_1))$ , $G_d=\exp(-i\sum_jd_j\sigma_j\otimes\sigma_j)$ , and $t_*=\pi/(2(a_0+a_1))$ ; the assumptions imply $a_0+a_1>0$ . A matrix $V$ has content $d$ when it is unitary, $d_1\le d_0$ , $|d_2|\le d_1$ , $d_0\le\pi/4$ , and $V=(A'\otimes B')G_d(C'\otimes D')$ for some four one-qubit unitaries. The assertion includes that $G_d$ has content $d$ . Define $P(V)$ to mean that $V$ is unitary and there exist one-qubit unitaries $E,F$ and unit vectors $u_{ij},v_{ij}\in\mathbb C^2$ , for bits $i,j$ , such that

\langle u_{i0},u_{i1}\rangle=0\ \text{for every }i,\qquad \langle v_{0j},v_{1j}\rangle=0\ \text{for every }j,\qquad V(E|i\rangle\otimes F|j\rangle)=u_{ij}\otimes v_{ij}.

Define $C_H(V)$ as the extended nonnegative infimum, with empty infimum $+\infty$ , of nonnegative times $t$ admitting arbitrarily accurate simulation of the unitary $V$ up to a scalar of modulus one: 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)$ , with one-qubit unitary factors, $t_j\ge0$ , and $\sum_jt_j=t$ , differs from $zV$ in operator norm by strictly less than $\varepsilon$ for some $|z|=1$ ; zero pulses are permitted. Then $P(G_d)$ holds, this simulation condition holds at the exact time $t_*$ , and

C_H(G_d)=t_*, \qquad \inf_{\{V:P(V)\}}C_H(V)=t_*, \qquad \forall V,\ P(V)\Longrightarrow C_H(G_d)\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