Four disjoint transmission-capability classes

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.fourTransmissionClasses

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. Every gate belongs to exactly one of the following four operational profiles, equivalent to the indicated disjoint chamber stratum:

\begin{array}{c|c} \text{stratum}&\text{perfect transmission tasks}\\ \beta_1<\pi/4&\text{none}\\ \beta_1=\pi/4,\ \beta_2<\pi/4&\text{one cbit only}\\ \beta_1=\beta_2=\pi/4,\ |\beta_3|<\pi/4&\text{two cbits; qubit plus reverse cbit; no two qubits}\\ \beta_1=\beta_2=|\beta_3|=\pi/4&\text{all tasks (SWAP class)} \end{array}

One-way tasks in this table are possible in either chosen direction. The empty profile excludes a perfect full bit in one use and does not assert zero Shannon capacity.

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.12, IV.C: precisely four disjoint operational classes. Endpoints of lower
strata are excluded, and both signs of SWAP's last coefficient are included. -/
theorem fourTransmissionClasses (U : TwoMatrix) (b : Triple) (hU : HasContent U b) :
    (∀ k : Fin 4, ChamberClass b k ↔ TransmissionProfile U k) ∧
      ∃! k : Fin 4, TransmissionProfile U k := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 12, IV.C: four transmission-capability classes

Read-back

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

Let $U$ be a complex matrix on $\mathbb C^2\otimes\mathbb C^2$ and let $b=(b_0,b_1,b_2)$ be a real triple. Let $X=\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$ , $Y=\left(\begin{smallmatrix}0&-i\\i&0\end{smallmatrix}\right)$ , and $Z=\left(\begin{smallmatrix}1&0\\0&-1\end{smallmatrix}\right)$ . Assume $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and there exist one-qubit unitaries $A,B,C,D$ such that

U=(A\otimes B)e^{-i(b_0X\otimes X+b_1Y\otimes Y+b_2Z\otimes Z)}(C\otimes D).

Let $S|i,j\rangle=|j,i\rangle$ , and write $V^{\mathrm{rev}}=SVS$ . Define the following five predicates on two-qubit matrices $V$ , each of which includes the requirement that $V$ is unitary; all existentially chosen one-qubit matrices below are unitary, all existentially chosen state vectors are unit vectors in $\mathbb C^2$ , bits range over $\{0,1\}$ , and $q,r$ range over all unit vectors in $\mathbb C^2$ . The predicate $C(V)$ requires $E,D,v,w_0,w_1$ such that $V(E|i\rangle\otimes v)=w_i\otimes D|i\rangle$ for every bit $i$ . The predicate $B(V)$ requires $E,F$ and vectors $a_{ij},b_{ij}$ such that

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

The predicate $Q(V)$ requires $E,R,v,w$ such that $(I\otimes R)V(Eq\otimes v)=w\otimes q$ for every $q$ . The predicate $H(V)$ requires $E,F,R_0,R_1,a_0,a_1$ , with $\langle a_0,a_1\rangle=0$ , such that $(I\otimes R_j)V(Eq\otimes F|j\rangle)=a_j\otimes q$ for every $j,q$ . The predicate $T(V)$ requires $E,F,R,S_1$ such that $(R\otimes S_1)V(Eq\otimes Fr)=r\otimes q$ for every $q,r$ . For each $k\in\{0,1,2,3\}$ , the chamber condition in the middle column below holds if and only if the eight assertions

\bigl(C(U),C(U^{\mathrm{rev}}),B(U),Q(U),Q(U^{\mathrm{rev}}), H(U),H(U^{\mathrm{rev}}),T(U)\bigr)

have exactly the truth values in the corresponding right-hand column:

\begin{array}{c|l|c} k&\text{chamber condition}&\text{eight truth values}\\ \hline 0&b_0<\pi/4& (\mathrm F,\mathrm F,\mathrm F,\mathrm F,\mathrm F,\mathrm F,\mathrm F,\mathrm F)\\ 1&b_0=\pi/4\ \land\ b_1<\pi/4& (\mathrm T,\mathrm T,\mathrm F,\mathrm F,\mathrm F,\mathrm F,\mathrm F,\mathrm F)\\ 2&b_0=\pi/4\ \land\ b_1=\pi/4\ \land\ |b_2|<\pi/4& (\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm F)\\ 3&b_0=\pi/4\ \land\ b_1=\pi/4\ \land\ |b_2|=\pi/4& (\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T,\mathrm T) \end{array}

There exists exactly one $k\in\{0,1,2,3\}$ for which the corresponding eight-assertion profile holds.

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