Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Perfect bidirectional-cbit transmission criterion

Open
QAlgorithms.Papers.Independent.Intakethird100.P99.twoCbitsCapability_iff

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For a two-qubit unitary UUU, let β\betaβ be an actual interaction-content witness: UUU is locally equivalent, up to global phase, to Uβ=exp⁡[−i∑k=13βkσk⊗σk]U_\beta=\exp[-i\sum_{k=1}^3\beta_k\sigma_k\otimes\sigma_k]Uβ​=exp[−i∑k=13​βk​σk​⊗σk​], where σ1,σ2,σ3\sigma_1,\sigma_2,\sigma_3σ1​,σ2​,σ3​ are the Pauli matrices X,Y,ZX,Y,ZX,Y,Z and π/4≥β1≥β2≥∣β3∣\pi/4\ge\beta_1\ge\beta_2\ge|\beta_3|π/4≥β1​≥β2​≥∣β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. Then

U can send one perfect cbit each way simultaneously⟺β1=β2=π/4.U\text{ can send one perfect cbit each way simultaneously}\quad\Longleftrightarrow\quad\beta_1=\beta_2=\pi/4.U can send one perfect cbit each way simultaneously⟺β1​=β2​=π/4.

The third coordinate is unrestricted within the canonical chamber, ∣β3∣≤π/4|\beta_3|\le\pi/4∣β3​∣≤π/4. The two input encodings are chosen before either bit; each receiver may use the sent bit to select a decoding observable.

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.10–11, IV.B.2, (16)–(19): simultaneous perfect cbits are possible precisely
on the edge with the first two coordinates pi/4. Decoding may depend on the sent bit. -/
theorem twoCbitsCapability_iff (U : TwoMatrix) (b : Triple) (hU : HasContent U b) :
    CanTwoCbits U ↔ b 0 = Real.pi / 4 ∧ b 1 = Real.pi / 4 := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99
Source
Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 10, IV.B.2: gates enabling one classical bit each way
Read-back

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

For every complex two-qubit matrix UUU and real triple bbb, assume UUU is unitary, b1≤b0b_1\le b_0b1​≤b0​, ∣b2∣≤b1|b_2|\le b_1∣b2​∣≤b1​, b0≤π/4b_0\le\pi/4b0​≤π/4, and there are four one-qubit unitaries A,B,C,DA,B,C,DA,B,C,D with

U=(A⊗B)exp⁡ ⁣(−i∑j=02bjσj⊗σj)(C⊗D),(σ0,σ1,σ2)=(X,Y,Z).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).U=(A⊗B)exp(−ij=0∑2​bj​σj​⊗σj​)(C⊗D),(σ0​,σ1​,σ2​)=(X,Y,Z).

Then the existence of one-qubit unitaries E,FE,FE,F and unit vectors uij,vij∈C2u_{ij},v_{ij}\in\mathbb C^2uij​,vij​∈C2, for every pair of bits i,ji,ji,j, satisfying

U(E∣i⟩⊗F∣j⟩)=uij⊗vij,∀i, ⟨ui0,ui1⟩=0,∀j, ⟨v0j,v1j⟩=0,U(E|i\rangle\otimes F|j\rangle)=u_{ij}\otimes v_{ij},\qquad \forall i,\ \langle u_{i0},u_{i1}\rangle=0,\qquad \forall j,\ \langle v_{0j},v_{1j}\rangle=0,U(E∣i⟩⊗F∣j⟩)=uij​⊗vij​,∀i, ⟨ui0​,ui1​⟩=0,∀j, ⟨v0j​,v1j​⟩=0,

together with unitarity of UUU, is equivalent to the conjunction b0=π/4b_0=\pi/4b0​=π/4 and b1=π/4b_1=\pi/4b1​=π/4.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me