Perfect one-cbit transmission criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.cbitCapability_iff

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. The receiving party may choose one fixed pure preparation suited to the gate; it need not work for every preparation. Then

U\text{ can send one perfect cbit }A\to B\quad\Longleftrightarrow\quad\beta_1=\pi/4.

The same equivalence holds with $A,B$ exchanged. This identifies the first transmission threshold in the canonical chamber.

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.9–10, IV.B.1: a single perfect classical bit is possible precisely on the
first chamber face. The receiver's preparation is existential, not universal. -/
theorem cbitCapability_iff (U : TwoMatrix) (b : Triple) (hU : HasContent U b) :
    (CanCbit U ↔ b 0 = Real.pi / 4) ∧
      (CanCbit (reverseParties U) ↔ b 0 = Real.pi / 4) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 9, IV.B.1: exact criterion 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 $U$ and real triple $b$ , assume $U$ is unitary, $b_1\le b_0$ , $|b_2|\le b_1$ , $b_0\le\pi/4$ , and there exist four one-qubit unitaries $A,B,C,D$ such that

U=(A\otimes B)\exp\!\left(-i\sum_{j=0}^2b_j\sigma_j\otimes\sigma_j\right)(C\otimes D), \qquad(\sigma_0,\sigma_1,\sigma_2)=(X,Y,Z).

For a two-qubit matrix $V$ , let $P(V)$ mean that $V$ is unitary and there exist one-qubit unitaries $E,F$ , a unit vector $v\in\mathbb C^2$ , and unit vectors $w_0,w_1\in\mathbb C^2$ , such that $V(E|i\rangle\otimes v)=w_i\otimes F|i\rangle$ for each bit $i$ . With $S|i,j\rangle=|j,i\rangle$ , the two asserted equivalences are

P(U)\Longleftrightarrow b_0=\pi/4, \qquad P(SUS)\Longleftrightarrow b_0=\pi/4.

The vectors $v,w_0,w_1$ and the unitaries in the two occurrences of $P$ are separately existentially quantified.

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