Empirical/QM: Superdense coding

Category: 3-Local (promotion-ready to 2-Framework on demand).

Superdense coding (Bennett-Wiesner 1992): two classical bits are transmitted by sending a single qubit, provided the sender and receiver share one half each of a Bell pair. The sender applies one of four single-qubit operations {I, X, Z, XZ} to her half of |Φ⁺⟩; the four results are the four mutually orthogonal Bell states, so the receiver recovers the two-bit message by a Bell-basis measurement.

This file delivers the algebraic core: the four encoding maps carry |Φ⁺⟩ to the four Bell states (up to a phase on the last), and the four Bell states are an orthonormal family — hence perfectly distinguishable, i.e. exactly two classical bits.

Basis and conventions

Two qubits live in EuclideanSpace ℂ (Fin 4) with the ordering |00⟩ = e₀, |01⟩ = e₁, |10⟩ = e₂, |11⟩ = e₃ (matching Empirical/QM/Gates/BellPrep.lean). The four Bell states:

• |Φ⁺⟩ = (e₀ + e₃)/√2 (imported as qmKetPhiPlus),
• |Ψ⁺⟩ = (e₁ + e₂)/√2,
• |Φ⁻⟩ = (e₀ − e₃)/√2,
• |Ψ⁻⟩ = (e₁ − e₂)/√2.

The encodings act on the first (high-bit) qubit; X ⊗ I, Z ⊗ I, XZ ⊗ I are the explicit 4×4 matrices. (XZ ⊗ I)|Φ⁺⟩ = −|Ψ⁻⟩ (phase −1), which does not affect orthogonality.

Source

Bennett and Wiesner 1992, Phys. Rev. Lett. 69, 2881.

The remaining three Bell states

noncomputable def CSD.Empirical.QM.SuperdenseCoding.qmKetPsiPlus : EuclideanSpace ℂ (Fin 4)

|Ψ⁺⟩ = (e₁ + e₂)/√2.

Equations

• CSD.Empirical.QM.SuperdenseCoding.qmKetPsiPlus = (↑√2)⁻¹ • (EuclideanSpace.single 1 1 + EuclideanSpace.single 2 1)

noncomputable def CSD.Empirical.QM.SuperdenseCoding.qmKetPhiMinus : EuclideanSpace ℂ (Fin 4)

|Φ⁻⟩ = (e₀ − e₃)/√2.

Equations

• CSD.Empirical.QM.SuperdenseCoding.qmKetPhiMinus = (↑√2)⁻¹ • (EuclideanSpace.single 0 1 - EuclideanSpace.single 3 1)

noncomputable def CSD.Empirical.QM.SuperdenseCoding.qmKetPsiMinus : EuclideanSpace ℂ (Fin 4)

|Ψ⁻⟩ = (e₁ − e₂)/√2.

Equations

• CSD.Empirical.QM.SuperdenseCoding.qmKetPsiMinus = (↑√2)⁻¹ • (EuclideanSpace.single 1 1 - EuclideanSpace.single 2 1)

The three nontrivial single-qubit encodings (on the first qubit)

noncomputable def CSD.Empirical.QM.SuperdenseCoding.pauliX_tensor_I : Matrix (Fin 4) (Fin 4) ℂ

X ⊗ I: bit flip on the high qubit. Swaps |00⟩↔|10⟩, |01⟩↔|11⟩.

Equations

• CSD.Empirical.QM.SuperdenseCoding.pauliX_tensor_I = Matrix.of fun (i j : Fin 4) => match i, j with | 0, 2 => 1 | 1, 3 => 1 | 2, 0 => 1 | 3, 1 => 1 | x, x_1 => 0

noncomputable def CSD.Empirical.QM.SuperdenseCoding.pauliZ_tensor_I : Matrix (Fin 4) (Fin 4) ℂ

Z ⊗ I: phase flip on the high qubit. diag(1, 1, −1, −1).

Equations

• CSD.Empirical.QM.SuperdenseCoding.pauliZ_tensor_I = Matrix.of fun (i j : Fin 4) => match i, j with | 0, 0 => 1 | 1, 1 => 1 | 2, 2 => -1 | 3, 3 => -1 | x, x_1 => 0

noncomputable def CSD.Empirical.QM.SuperdenseCoding.pauliXZ_tensor_I : Matrix (Fin 4) (Fin 4) ℂ

XZ ⊗ I on the high qubit, where XZ = [[0, −1], [1, 0]].

Equations

• CSD.Empirical.QM.SuperdenseCoding.pauliXZ_tensor_I = Matrix.of fun (i j : Fin 4) => match i, j with | 0, 2 => -1 | 1, 3 => -1 | 2, 0 => 1 | 3, 1 => 1 | x, x_1 => 0

Component extraction for |Φ⁺⟩

qmKetPhiPlus.ofLp is (1/√2) at indices 0, 3 and 0 elsewhere (re-derived locally; BellPrep's versions are private).

theorem CSD.Empirical.QM.SuperdenseCoding.phiPlus_ofLp_zero : Gates.qmKetPhiPlus.ofLp 0 = (↑√2)⁻¹

theorem CSD.Empirical.QM.SuperdenseCoding.phiPlus_ofLp_one : Gates.qmKetPhiPlus.ofLp 1 = 0

theorem CSD.Empirical.QM.SuperdenseCoding.phiPlus_ofLp_two : Gates.qmKetPhiPlus.ofLp 2 = 0

theorem CSD.Empirical.QM.SuperdenseCoding.phiPlus_ofLp_three : Gates.qmKetPhiPlus.ofLp 3 = (↑√2)⁻¹

theorem CSD.Empirical.QM.SuperdenseCoding.mulVec_phiPlus (M : Matrix (Fin 4) (Fin 4) ℂ) (k : Fin 4) : M.mulVec Gates.qmKetPhiPlus.ofLp k = (↑√2)⁻¹ * (M k 0 + M k 3)

For any row k, applying a matrix M to |Φ⁺⟩ collapses to (M[k,0] + M[k,3]) / √2.

Image identities: the four encodings produce the four Bell states

theorem CSD.Empirical.QM.SuperdenseCoding.encode_X : (Matrix.toEuclideanLin pauliX_tensor_I) Gates.qmKetPhiPlus = qmKetPsiPlus

(X ⊗ I)|Φ⁺⟩ = |Ψ⁺⟩.

theorem CSD.Empirical.QM.SuperdenseCoding.encode_Z : (Matrix.toEuclideanLin pauliZ_tensor_I) Gates.qmKetPhiPlus = qmKetPhiMinus

(Z ⊗ I)|Φ⁺⟩ = |Φ⁻⟩.

theorem CSD.Empirical.QM.SuperdenseCoding.encode_XZ : (Matrix.toEuclideanLin pauliXZ_tensor_I) Gates.qmKetPhiPlus = -qmKetPsiMinus

(XZ ⊗ I)|Φ⁺⟩ = −|Ψ⁻⟩ (phase −1; orthogonality is unaffected).

theorem CSD.Empirical.QM.SuperdenseCoding.encode_I : (Matrix.toEuclideanLin 1) Gates.qmKetPhiPlus = Gates.qmKetPhiPlus

(I ⊗ I)|Φ⁺⟩ = |Φ⁺⟩ (the trivial encoding).

The Bell basis is orthonormal (perfect distinguishability)

theorem CSD.Empirical.QM.SuperdenseCoding.bell_basis_orthonormal : inner ℂ Gates.qmKetPhiPlus qmKetPsiPlus = 0 ∧ inner ℂ Gates.qmKetPhiPlus qmKetPhiMinus = 0 ∧ inner ℂ Gates.qmKetPhiPlus qmKetPsiMinus = 0 ∧ inner ℂ qmKetPsiPlus qmKetPhiMinus = 0 ∧ inner ℂ qmKetPsiPlus qmKetPsiMinus = 0 ∧ inner ℂ qmKetPhiMinus qmKetPsiMinus = 0 ∧ inner ℂ Gates.qmKetPhiPlus Gates.qmKetPhiPlus = 1 ∧ inner ℂ qmKetPsiPlus qmKetPsiPlus = 1 ∧ inner ℂ qmKetPhiMinus qmKetPhiMinus = 1 ∧ inner ℂ qmKetPsiMinus qmKetPsiMinus = 1

The four Bell states form an orthonormal family: distinct states are orthogonal and each is a unit vector. Combined with the image identities above, the four single-qubit encodings carry |Φ⁺⟩ to a perfectly distinguishable family — exactly two classical bits.

Stated as the six pairwise-orthogonality identities plus the four unit-norm identities.