Simultaneous qubit and reverse cbit: criterion and optimal cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.hybridCapability_cost

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|$ . 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. A qubit $A\to B$ and a cbit $B\to A$ can be transmitted simultaneously exactly when $\beta_1=\beta_2=\pi/4$ , and the same is true with the parties exchanged. 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. 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. For $\alpha_1>0$ ,

C_H(\mathrm{qubit}_{A\to B}+\mathrm{cbit}_{B\to A})=\frac{\pi}{2(\alpha_1+\alpha_2)},\qquad\beta_*=\frac{\pi}{4}\left(1,1,\frac{2\alpha_3}{\alpha_1+\alpha_2}\right).

The canonical gate with content $\beta_*$ attains this cost in either orientation. Bob may use his own sent bit to select his recovery, which must then work for every unknown qubit.

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 pp.11–12, IV.B.3: a qubit plus reverse cbit has the same exact content criterion
and optimal cost. Recovery can depend on the receiver's own classical message. -/
theorem hybridCapability_cost (U H : TwoMatrix) (b a : Triple)
    (hU : HasContent U b) (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    (CanHybrid U ↔ b 0 = Real.pi / 4 ∧ b 1 = Real.pi / 4) ∧
    (CanHybrid (reverseParties U) ↔ b 0 = Real.pi / 4 ∧ b 1 = Real.pi / 4) ∧
    HasContent (contentGate (optimalTransmissionContent a)) (optimalTransmissionContent a) ∧
    OptimalTask H CanHybrid (contentGate (optimalTransmissionContent a))
      (Real.pi / (2 * (a 0 + a 1))) ∧
    OptimalTask H (fun V => CanHybrid (reverseParties V))
      (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, IV.B.3: simultaneous qubit and reverse cbit

Read-back

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

Let $U,H$ be complex matrices on $\mathbb C^2\otimes\mathbb C^2$ , and let $b=(b_0,b_1,b_2)$ and $a=(a_0,a_1,a_2)$ be real triples, indexed starting at $0$ . Write $X=\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$ , $Y=\left(\begin{smallmatrix}0&-i\\i&0\end{smallmatrix}\right)$ , $Z=\left(\begin{smallmatrix}1&0\\0&-1\end{smallmatrix}\right)$ , $J(d)=d_0X\otimes X+d_1Y\otimes Y+d_2Z\otimes Z$ , and $G(d)=e^{-iJ(d)}$ . Say that $V\sim W$ when there exist one-qubit unitary matrices $A,B,C,D$ such that $V=(A\otimes B)W(C\otimes D)$ . Assume that $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and $U\sim G(b)$ . Assume also that $H$ is Hermitian, $a_1\le a_0$ , $|a_2|\le a_1$ , and there exist one-qubit unitaries $A,B$ and Hermitian one-qubit matrices $K,L$ with

(A\otimes B)H(A\otimes B)^\dagger =J(a)+K\otimes I+I\otimes L,

and assume $a_0>0$ . For a two-qubit matrix $V$ , let $\mathcal H(V)$ mean that $V$ is unitary and there exist one-qubit unitaries $E,F,R_0,R_1$ and unit vectors $u_0,u_1\in\mathbb C^2$ , with $\langle u_0,u_1\rangle=0$ , such that, for every $j\in\{0,1\}$ and every unit vector $q\in\mathbb C^2$ ,

(I\otimes R_j)V(Eq\otimes F|j\rangle)=u_j\otimes q.

Let $S$ be the swap matrix, $S|i,j\rangle=|j,i\rangle$ . Then

\mathcal H(U)\iff b_0=b_1=\pi/4, \qquad \mathcal H(SUS)\iff b_0=b_1=\pi/4.

Set

c=\left(\frac\pi4,\frac\pi4,\frac\pi4\,\frac{2a_2}{a_0+a_1}\right), \qquad W=G(c), \qquad t_*=\frac{\pi}{2(a_0+a_1)}.

The matrix $W$ is unitary, $c_1\le c_0$ , $|c_2|\le c_1$ , $c_0\le\pi/4$ , and $W\sim G(c)$ . Moreover, $W$ has both properties $\mathcal H(W)$ and $\mathcal H(SWS)$ , and is optimal at time $t_*$ for each property in the following precise sense. Define $C_H(V)$ as the infimum, in $[0,\infty]$ , of nonnegative times $t$ for which $H$ is Hermitian, $V$ is unitary, and for every $\varepsilon>0$ there exist a finite pulse protocol and $z\in\mathbb C$ , $|z|=1$ , whose total interaction time is exactly $t$ and whose resulting matrix differs from $zV$ by operator norm less than $\varepsilon$ . Such a protocol starts at $A_0\otimes B_0$ and successively replaces its current matrix $P$ by $(A_j\otimes B_j)e^{-it_jH}P$ , where all $A_j,B_j$ are one-qubit unitaries, all $t_j\ge0$ , and $\sum_jt_j=t$ ; the pulse list may be empty, and the infimum of an empty set of admissible times is $+\infty$ . The required approximating protocols for $W$ exist at exactly $t_*$ , and, for each predicate $P(V)=\mathcal H(V)$ and $P(V)=\mathcal H(SVS)$ ,

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

The hypotheses imply $a_1\ge0$ and $a_0+a_1>0$ , so the displayed denominators are nonzero and $t_*>0$ .

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