Unknown-qubit transmission criterion and optimal cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.qubitCapability_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. An arbitrary unknown qubit can be transmitted from $A$ to $B$ exactly when $\beta_1=\beta_2=\pi/4$ , and the same criterion holds in the opposite direction. 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})=\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 the bound in either chosen direction. The same fixed recovery preserves every normalized superposition, not just the two basis states.

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: unknown-qubit transmission has the same optimal content and
cost as Result 5; its criterion includes coherence for every superposition. -/
theorem qubitCapability_cost (U H : TwoMatrix) (b a : Triple)
    (hU : HasContent U b) (hH : HasCanonicalHamiltonian H a) (ha : 0 < a 0) :
    (CanQubit U ↔ b 0 = Real.pi / 4 ∧ b 1 = Real.pi / 4) ∧
    (CanQubit (reverseParties U) ↔ b 0 = Real.pi / 4 ∧ b 1 = Real.pi / 4) ∧
    HasContent (contentGate (optimalTransmissionContent a)) (optimalTransmissionContent a) ∧
    OptimalTask H CanQubit (contentGate (optimalTransmissionContent a))
      (Real.pi / (2 * (a 0 + a 1))) ∧
    OptimalTask H (fun V => CanQubit (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: transmitting a qubit

Read-back

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

For all complex two-qubit matrices $U,H$ and real triples $b,a$ , assume $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and $U=(A'\otimes B')\exp(-i\sum_jb_j\sigma_j\otimes\sigma_j)(C'\otimes D')$ for some four one-qubit unitaries, where $(\sigma_0,\sigma_1,\sigma_2)=(X,Y,Z)$ . Assume also $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$ with

(A\otimes B)H(A\otimes B)^\dagger =\sum_{j=0}^2a_j\sigma_j\otimes\sigma_j+K\otimes I+I\otimes L.

Define $Q(V)$ to mean that $V$ is unitary and there exist one-qubit unitaries $E,R$ and unit vectors $v,w\in\mathbb C^2$ such that, for every unit vector $q\in\mathbb C^2$ , $(I\otimes R)V(Eq\otimes v)=w\otimes q$ . With $S|i,j\rangle=|j,i\rangle$ , the declaration asserts

Q(U)\Longleftrightarrow(b_0=\pi/4\ \text{and}\ b_1=\pi/4), \qquad Q(SUS)\Longleftrightarrow(b_0=\pi/4\ \text{and}\ b_1=\pi/4).

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$ . The matrix $G_d$ is unitary, $d_1\le d_0$ , $|d_2|\le d_1$ , $d_0\le\pi/4$ , and there are four one-qubit unitaries $L_1,L_2,R_1,R_2$ such that $G_d=(L_1\otimes L_2)G_d(R_1\otimes R_2)$ . Define $C_H(V)$ as the extended nonnegative infimum, with empty infimum $+\infty$ , of times $t\ge0$ for which $V$ is unitary and 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)$ , with one-qubit unitaries and nonnegative durations summing exactly to $t$ , at operator-norm distance strictly less than $\varepsilon$ from $zV$ for some $|z|=1$ ; zero pulses are allowed. For each predicate $P(V)=Q(V)$ and $P(V)=Q(SVS)$ , $P(G_d)$ holds, this arbitrarily accurate simulation is possible 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