Superdense coding

Two classical bits travel over one qubit, given a shared EPR-pair [dW19, qcnotes.tex:879]. Alice holds bits a, b and applies X (if a = 1) then Z (if b = 1) to her half of the Bell state [dW19, qcnotes.tex:882]; after she sends her qubit to Bob, he applies CNOT then H on Alice's qubit and reads both bits off a computational-basis measurement [dW19, qcnotes.tex:885]. The protocol is due to Bennett and Wiesner (1992).

Conventions

• Alice's qubit is qubit 0 (the most significant, big-endian); Bob's is qubit 1.
• The decoded state is exactly the basis ket |b a⟩ — no residual phase — so the final measurement is deterministic.

Main results

• LeanPool.LeanQuantumAlg.superdenseEncode — Alice's encoding gate (Z^b X^a) ⊗ I.
• LeanPool.LeanQuantumAlg.superdenseDecode — Bob's decoding circuit (H ⊗ I) · CNOT.
• LeanPool.LeanQuantumAlg.SuperdenseCoding.main — correctness: decode (encode a b |Φ⁺⟩) = |b a⟩.

noncomputable def QuantumAlg.superdenseEncode (a b : Bool) : Gate 2

Alice's encoding: X on her qubit if a, then Z if b [dW19, qcnotes.tex:882] — as the two-qubit gate (Z^b X^a) ⊗ I.

Equations

• QuantumAlg.superdenseEncode a b = ((if b = true then QuantumAlg.Gate.Z else 1) * if a = true then QuantumAlg.Gate.X else 1).tensor 1

noncomputable def QuantumAlg.superdenseDecode : Gate 2

Bob's decoding circuit: CNOT (control = Alice's qubit), then H on Alice's qubit [dW19, qcnotes.tex:885].

Equations

• QuantumAlg.superdenseDecode = QuantumAlg.Gate.H.tensor 1 * QuantumAlg.Gate.CNOT

theorem QuantumAlg.superdense_coding (a b : Bool) : superdenseDecode.applyVec ((superdenseEncode a b).applyVec bell.vec) = (if b = true then PureState.ket1 else PureState.ket0).vec.tensor (if a = true then PureState.ket1 else PureState.ket0).vec

Superdense coding [dW19, qcnotes.tex:879]: Bob's decoding circuit turns the encoded Bell state into exactly the basis state |b a⟩, so a computational-basis measurement recovers both of Alice's bits with certainty. Protocol due to Bennett and Wiesner (1992).

def QuantumAlg.SuperdenseBlockCorrect (a b : Bool) : Prop

The proposition proved by one superdense-coding block.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumAlg.superdense_coding_block (a b : Bool) : SuperdenseBlockCorrect a b

@[reducible, inline]

abbrev QuantumAlg.SuperdenseMessage (n : ℕ) : Type

A global superdense-coding message: n ordered pairs of classical bits, equivalently a 2n-bit string grouped by Bell-pair block.

Equations

• QuantumAlg.SuperdenseMessage n = (Fin n → Bool × Bool)

def QuantumAlg.superdenseRecoveredMessage {n : ℕ} (bits : SuperdenseMessage n) : SuperdenseMessage n

Bob's decoded global message in the exact block protocol.

Equations

• QuantumAlg.superdenseRecoveredMessage bits i = bits i

def QuantumAlg.SuperdenseGlobalCorrect {n : ℕ} (bits : SuperdenseMessage n) : Prop

The global correctness proposition for the n-block protocol: every block decodes its bit pair, so Bob's recovered message is the whole input message.

Equations

• QuantumAlg.SuperdenseGlobalCorrect bits = (QuantumAlg.superdenseRecoveredMessage bits = bits ∧ ∀ (i : Fin n), QuantumAlg.SuperdenseBlockCorrect (bits i).1 (bits i).2)

def QuantumAlg.superdenseCommunicationProfile (n : ℕ) : CommunicationProfile

Communication resources for running n independent superdense-coding blocks: n shared Bell pairs and n transmitted qubits from Alice to Bob.

Equations

• QuantumAlg.superdenseCommunicationProfile n = { classicalBits := 0, transmittedQubits := n, bellPairs := n }

theorem QuantumAlg.superdenseCommunicationProfile_exact (n : ℕ) : (superdenseCommunicationProfile n).HasExactCounts 0 n n

theorem QuantumAlg.superdense_coding_componentwise {n : ℕ} (bits : Fin n → Bool × Bool) : (∀ (i : Fin n), SuperdenseBlockCorrect (bits i).1 (bits i).2) ∧ (superdenseCommunicationProfile n).HasExactCounts 0 n n

Componentwise n-copy superdense-coding theorem. Each block uses one shared Bell pair and transmits one qubit, and Bob deterministically recovers the corresponding two classical bits.

theorem QuantumAlg.SuperdenseCoding.main {n : ℕ} (bits : SuperdenseMessage n) : SuperdenseGlobalCorrect bits ∧ (superdenseCommunicationProfile n).HasExactCounts 0 n n

Global n-block superdense-coding theorem: Alice's 2n classical bits, represented as n bit pairs, are recovered exactly, using n transmitted qubits and n shared Bell pairs.