Perfect bidirectional-cbit transmission criterion
OpenQAlgorithms.Papers.Independent.Intakethird100.P99.twoCbitsCapability_iffFor a two-qubit unitary , let be an actual interaction-content witness: is locally equivalent, up to global phase, to , where are the Pauli matrices and . 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
The third coordinate is unrestricted within the canonical chamber, . The two input encodings are chosen before either bit; each receiver may use the sent bit to select a decoding observable.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P99
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
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For every complex two-qubit matrix and real triple , assume is unitary, , , , and there are four one-qubit unitaries with
Then the existence of one-qubit unitaries and unit vectors , for every pair of bits , satisfying
together with unitarity of , is equivalent to the conjunction and .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.