Quantum teleportation

Quantum teleportation sends an unknown qubit to Bob using a shared EPR-pair, Alice's computational-basis measurement of two qubits, and two classical bits [dW19, qcnotes.tex:785]. Alice applies CNOT on her two qubits and then a Hadamard on her first qubit before measuring [dW19, qcnotes.tex:790]. The four measurement outcomes determine Bob's one-qubit branch and the classical correction table: apply X when the second bit is 1, then Z when the first bit is 1 [dW19, qcnotes.tex:804], recovering Alice's original qubit [dW19, qcnotes.tex:806].

Conventions

• Qubits are big-endian: Alice's input is qubit 0, Alice's half of the EPR-pair is qubit 1, and Bob's half is qubit 2.
• The theorem is linear in arbitrary amplitudes α β : ℂ; a physical input qubit additionally satisfies the usual normalization condition.
• teleportBranchGate a b is Bob's post-measurement branch for Alice's outcome bits ab, before Bob's correction. The common scalar 1/2 appears in teleportation_premeasurement before conditional normalization.

Main results

• LeanPool.LeanQuantumAlg.teleportBellMeasure — Alice's CNOT/H unitary before measurement.
• LeanPool.LeanQuantumAlg.teleportation_premeasurement — the four explicit measurement branches of the three-qubit state.
• LeanPool.LeanQuantumAlg.QuantumTeleportation.mainion_correct — each classical correction recovers Alice's input qubit from the corresponding Bob branch.
• LeanPool.LeanQuantumAlg.QuantumTeleportation.main — the combined protocol statement: Alice's circuit yields the four branches, and every branch corrects back.

def QuantumAlg.teleportInput (α β : ℂ) : StateVector 1

Alice's one-qubit input vector α|0⟩ + β|1⟩.

For arbitrary amplitudes this is a raw vector; a physical input qubit is a PureState only after a norm-one proof is supplied.

Equations

• QuantumAlg.teleportInput α β = α • QuantumAlg.PureState.ket0.vec + β • QuantumAlg.PureState.ket1.vec

noncomputable def QuantumAlg.teleportBellMeasure : Gate 3

Alice's unitary before measuring her two qubits: CNOT on qubits 0,1, then Hadamard on qubit 0 [dW19, qcnotes.tex:790].

Equations

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

def QuantumAlg.teleportBranchGate (a b : Bool) : Gate 1

Bob's branch before correction for Alice's classical outcome bits ab: 00 ↦ I, 01 ↦ X, 10 ↦ Z, 11 ↦ XZ.

Equations

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

def QuantumAlg.teleportCorrection (a b : Bool) : Gate 1

Bob's classical correction for Alice's outcome bits ab: apply X when b = 1, then Z when a = 1 [dW19, qcnotes.tex:804].

Equations

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

theorem QuantumAlg.teleportation_uses_bell_state_prep : Gate.CNOT.apply ((Gate.H.tensor 1).apply (PureState.ket0.tensor PureState.ket0)) = bell

The Bell-pair resource can be prepared by the already-proved Bell-state circuit. This pins teleportation's shared EPR-pair to bell_state_prep.

def QuantumAlg.teleKet3 (j : Fin (2 ^ 3)) : StateVector 3

Three-qubit computational basis vectors at the raw-vector layer.

Equations

• QuantumAlg.teleKet3 j = (QuantumAlg.PureState.ket j).vec

theorem QuantumAlg.teleportation_premeasurement_basis (α β : ℂ) : teleportBellMeasure.applyVec ((teleportInput α β).tensor bell.vec) = 2⁻¹ • (α • teleKet3 0 + β • teleKet3 1 + β • teleKet3 2 + α • teleKet3 3 + α • teleKet3 4 - β • teleKet3 5 - β • teleKet3 6 + α • teleKet3 7)

Basis-vector expansion of Alice's premeasurement state. This is the three-qubit equation displayed in de Wolf's teleportation example [dW19, qcnotes.tex:791].

theorem QuantumAlg.teleportation_premeasurement (α β : ℂ) : teleportBellMeasure.applyVec ((teleportInput α β).tensor bell.vec) = 2⁻¹ • ((PureState.ket0.vec.tensor PureState.ket0.vec).tensor ((teleportBranchGate false false).applyVec (teleportInput α β)) + (PureState.ket0.vec.tensor PureState.ket1.vec).tensor ((teleportBranchGate false true).applyVec (teleportInput α β)) + (PureState.ket1.vec.tensor PureState.ket0.vec).tensor ((teleportBranchGate true false).applyVec (teleportInput α β)) + (PureState.ket1.vec.tensor PureState.ket1.vec).tensor ((teleportBranchGate true true).applyVec (teleportInput α β)))

Alice's measurement outcomes 00, 01, 10, 11 leave Bob's qubit in I, X, Z, and XZ branches respectively, all with the common unnormalized coefficient 1/2 before conditional normalization [dW19, qcnotes.tex:791].

theorem QuantumAlg.teleportation_correction_correct (a b : Bool) (α β : ℂ) : (teleportCorrection a b).applyVec ((teleportBranchGate a b).applyVec (teleportInput α β)) = teleportInput α β

Bob's branch-local correction is exact for every measurement outcome: after Alice sends ab, Bob's X-then-Z correction recovers α|0⟩ + β|1⟩ [dW19, qcnotes.tex:806].

theorem QuantumAlg.teleportation_correct (α β : ℂ) : teleportBellMeasure.applyVec ((teleportInput α β).tensor bell.vec) = 2⁻¹ • ((PureState.ket0.vec.tensor PureState.ket0.vec).tensor ((teleportBranchGate false false).applyVec (teleportInput α β)) + (PureState.ket0.vec.tensor PureState.ket1.vec).tensor ((teleportBranchGate false true).applyVec (teleportInput α β)) + (PureState.ket1.vec.tensor PureState.ket0.vec).tensor ((teleportBranchGate true false).applyVec (teleportInput α β)) + (PureState.ket1.vec.tensor PureState.ket1.vec).tensor ((teleportBranchGate true true).applyVec (teleportInput α β))) ∧ ∀ (a b : Bool), (teleportCorrection a b).applyVec ((teleportBranchGate a b).applyVec (teleportInput α β)) = teleportInput α β

Quantum teleportation correctness: Alice's CNOT/H circuit on the input qubit and shared Bell state yields the four explicit measurement branches, and for every classical outcome ab, Bob's correction recovers Alice's input qubit exactly.

def QuantumAlg.TeleportationBlockCorrect (α β : ℂ) : Prop

The proposition proved by one teleportation block.

Equations

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

theorem QuantumAlg.teleportation_correct_block (α β : ℂ) : TeleportationBlockCorrect α β

@[reducible, inline]

abbrev QuantumAlg.TeleportationInput (n : ℕ) : Type

A global teleportation input: n ordered qubit-amplitude pairs, representing an n-qubit product input at the current parallel block boundary.

Equations

• QuantumAlg.TeleportationInput n = (Fin n → ℂ × ℂ)

def QuantumAlg.teleportationRecoveredInput {n : ℕ} (input : TeleportationInput n) : TeleportationInput n

Bob's recovered global input in the exact block protocol.

Equations

• QuantumAlg.teleportationRecoveredInput input i = input i

def QuantumAlg.TeleportationGlobalCorrect {n : ℕ} (input : TeleportationInput n) : Prop

The global correctness proposition for the n-block protocol: every block recovers the corresponding input qubit after Alice's two-bit classical message and Bob's branch correction.

Equations

• QuantumAlg.TeleportationGlobalCorrect input = (QuantumAlg.teleportationRecoveredInput input = input ∧ ∀ (i : Fin n), QuantumAlg.TeleportationBlockCorrect (input i).1 (input i).2)

def QuantumAlg.teleportationCommunicationProfile (n : ℕ) : CommunicationProfile

Communication resources for running n independent teleportation blocks: n shared Bell pairs and 2n classical bits from Alice to Bob.

Equations

• QuantumAlg.teleportationCommunicationProfile n = { classicalBits := 2 * n, transmittedQubits := 0, bellPairs := n }

theorem QuantumAlg.teleportationCommunicationProfile_exact (n : ℕ) : (teleportationCommunicationProfile n).HasExactCounts (2 * n) 0 n

theorem QuantumAlg.teleportation_componentwise_correct {n : ℕ} (input : TeleportationInput n) : (∀ (i : Fin n), TeleportationBlockCorrect (input i).1 (input i).2) ∧ (teleportationCommunicationProfile n).HasExactCounts (2 * n) 0 n

Componentwise n-copy teleportation theorem at the parallel product-state boundary: each block uses one Bell pair and two classical bits, and each Bob block recovers Alice's input qubit exactly after the branch correction.

theorem QuantumAlg.QuantumTeleportation.main {n : ℕ} (input : TeleportationInput n) : TeleportationGlobalCorrect input ∧ (teleportationCommunicationProfile n).HasExactCounts (2 * n) 0 n

Global n-block teleportation theorem: Alice's n input qubits, represented as ordered product-state amplitude pairs, are recovered exactly by Bob after n shared Bell pairs and 2n classical bits from Alice.