Empirical/QM: Quantum teleportation (E5)

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

Quantum teleportation (Bennett et al. 1993): Alice transmits an unknown qubit |ψ⟩ = α|0⟩ + β|1⟩ to Bob using one shared Bell pair |Φ⁺⟩ and two classical bits. Alice performs a Bell-basis measurement on her input qubit together with her half of the entangled pair; the two-bit outcome tells Bob which of the four Pauli corrections {I, Z, X, ZX} to apply to his half to recover |ψ⟩.

This file delivers the algebraic core — the branch-conditional form (§0.1 QM-validity layer, branch-conditional reading; see specs/qm-empirical-tests.md):

1. teleState_factorises — the three-qubit input state is genuinely |ψ⟩₁ ⊗ |Φ⁺⟩₂₃ (amplitude factorisation Ψ(a,b,c) = ψ(a)·Φ⁺(b,c)).
2. teleportation_bell_expansion — the teleportation identity: re-expanding in Alice's Bell basis on qubits (1,2), Ψ = ½ Σₖ |Bellₖ⟩₁₂ ⊗ (Cₖ|ψ⟩)₃, with Cₖ ∈ {I, Z, X, XZ} the Pauli image in branch k. So in each Bell-measurement branch Bob holds a Pauli image of |ψ⟩.
3. teleportation_branch_recovers_input — applying the branch correction recovers |ψ⟩ exactly in all four branches (branch-conditional; the measurement-collapse / ¼-branch-probability layer is out of scope, see the honesty note below).

The three qubits live in EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2) (matching Empirical/QM/Multipartite/GHZ.lean), with qubit 1 = Alice's input, qubit 2 = Alice's half of the pair, qubit 3 = Bob's half. This is the dual of superdense coding (Resources/SuperdenseCoding.lean): there one entangled qubit carries two classical bits; here two classical bits + one entangled qubit carry one quantum state.

Honesty note

This is the QM-validity layer in branch-conditional form: it proves the Bell-basis expansion and per-branch recovery as exact algebraic identities. The measurement step proper — collapsing the four-branch superposition to a single classical outcome with probability ¼ each — is the measurement-update notion the corpus does not yet have (the same LF5 obligation that gates BB84). The no-signalling content ("Bob's marginal is I/2 independent of the branch before he learns the outcome") likewise needs the reduced-state / partial-trace machinery absent from Mathlib; it is not asserted here.

Source

Bennett, Brassard, Crépeau, Jozsa, Peres, Wootters 1993, Phys. Rev. Lett. 70, 1895. Experimental: Bouwmeester et al. 1997, Nature 390, 575.

States

noncomputable def CSD.Empirical.QM.Teleportation.teleInput (α β : ℂ) : EuclideanSpace ℂ (Fin 2)

The input qubit |ψ⟩ = α|0⟩ + β|1⟩ : EuclideanSpace ℂ (Fin 2).

Equations

• CSD.Empirical.QM.Teleportation.teleInput α β = EuclideanSpace.single 0 α + EuclideanSpace.single 1 β

noncomputable def CSD.Empirical.QM.Teleportation.bellPhiPlus : EuclideanSpace ℂ (Fin 2 × Fin 2)

The Bell state |Φ⁺⟩ = (|00⟩ + |11⟩)/√2 on qubits (2,3).

Equations

• CSD.Empirical.QM.Teleportation.bellPhiPlus = (↑√2)⁻¹ • (EuclideanSpace.single (0, 0) 1 + EuclideanSpace.single (1, 1) 1)

noncomputable def CSD.Empirical.QM.Teleportation.bellPhiMinus : EuclideanSpace ℂ (Fin 2 × Fin 2)

|Φ⁻⟩ = (|00⟩ − |11⟩)/√2.

Equations

• CSD.Empirical.QM.Teleportation.bellPhiMinus = (↑√2)⁻¹ • (EuclideanSpace.single (0, 0) 1 - EuclideanSpace.single (1, 1) 1)

noncomputable def CSD.Empirical.QM.Teleportation.bellPsiPlus : EuclideanSpace ℂ (Fin 2 × Fin 2)

|Ψ⁺⟩ = (|01⟩ + |10⟩)/√2.

Equations

• CSD.Empirical.QM.Teleportation.bellPsiPlus = (↑√2)⁻¹ • (EuclideanSpace.single (0, 1) 1 + EuclideanSpace.single (1, 0) 1)

noncomputable def CSD.Empirical.QM.Teleportation.bellPsiMinus : EuclideanSpace ℂ (Fin 2 × Fin 2)

|Ψ⁻⟩ = (|01⟩ − |10⟩)/√2.

Equations

• CSD.Empirical.QM.Teleportation.bellPsiMinus = (↑√2)⁻¹ • (EuclideanSpace.single (0, 1) 1 - EuclideanSpace.single (1, 0) 1)

noncomputable def CSD.Empirical.QM.Teleportation.teleState (α β : ℂ) : EuclideanSpace ℂ (Fin 2 × Fin 2 × Fin 2)

The full three-qubit input |ψ⟩₁ ⊗ |Φ⁺⟩₂₃, written out in components: (1/√2)(α|000⟩ + α|011⟩ + β|100⟩ + β|111⟩). (The tensor structure is verified by teleState_factorises.)

Equations

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

Bob's conditional vectors (the Pauli images of |ψ⟩)

noncomputable def CSD.Empirical.QM.Teleportation.bobPhiPlus (α β : ℂ) : EuclideanSpace ℂ (Fin 2)

Branch |Φ⁺⟩: Bob holds I|ψ⟩ = |ψ⟩.

Equations

• CSD.Empirical.QM.Teleportation.bobPhiPlus α β = CSD.Empirical.QM.Teleportation.teleInput α β

noncomputable def CSD.Empirical.QM.Teleportation.bobPhiMinus (α β : ℂ) : EuclideanSpace ℂ (Fin 2)

Branch |Φ⁻⟩: Bob holds Z|ψ⟩ = α|0⟩ − β|1⟩.

Equations

• CSD.Empirical.QM.Teleportation.bobPhiMinus α β = EuclideanSpace.single 0 α + EuclideanSpace.single 1 (-β)

noncomputable def CSD.Empirical.QM.Teleportation.bobPsiPlus (α β : ℂ) : EuclideanSpace ℂ (Fin 2)

Branch |Ψ⁺⟩: Bob holds X|ψ⟩ = β|0⟩ + α|1⟩.

Equations

• CSD.Empirical.QM.Teleportation.bobPsiPlus α β = EuclideanSpace.single 0 β + EuclideanSpace.single 1 α

noncomputable def CSD.Empirical.QM.Teleportation.bobPsiMinus (α β : ℂ) : EuclideanSpace ℂ (Fin 2)

Branch |Ψ⁻⟩: Bob holds XZ|ψ⟩ = −β|0⟩ + α|1⟩.

Equations

• CSD.Empirical.QM.Teleportation.bobPsiMinus α β = EuclideanSpace.single 0 (-β) + EuclideanSpace.single 1 α

Pauli correction matrices

noncomputable def CSD.Empirical.QM.Teleportation.teleX : Matrix (Fin 2) (Fin 2) ℂ

Pauli X = !![0, 1; 1, 0]. (Not in Gates/SingleQubit.lean, which has only H, S, T, Z.)

Equations

• CSD.Empirical.QM.Teleportation.teleX = !![0, 1; 1, 0]

noncomputable def CSD.Empirical.QM.Teleportation.teleZ : Matrix (Fin 2) (Fin 2) ℂ

Pauli Z = !![1, 0; 0, −1].

Equations

• CSD.Empirical.QM.Teleportation.teleZ = !![1, 0; 0, -1]

noncomputable def CSD.Empirical.QM.Teleportation.teleZX : Matrix (Fin 2) (Fin 2) ℂ

The |Ψ⁻⟩-branch correction ZX = !![0, 1; −1, 0] (apply X then Z).

Equations

• CSD.Empirical.QM.Teleportation.teleZX = !![0, 1; -1, 0]

Faithfulness: the input state is genuinely |ψ⟩ ⊗ |Φ⁺⟩

theorem CSD.Empirical.QM.Teleportation.teleState_factorises (α β : ℂ) (a b c : Fin 2) : (teleState α β).ofLp (a, b, c) = (teleInput α β).ofLp a * bellPhiPlus.ofLp (b, c)

The three-qubit amplitude factorises as Ψ(a,b,c) = ψ(a)·Φ⁺(b,c), i.e. teleState is the tensor product |ψ⟩₁ ⊗ |Φ⁺⟩₂₃.

The teleportation identity (Bell-basis expansion)

theorem CSD.Empirical.QM.Teleportation.teleportation_bell_expansion (α β : ℂ) (a b c : Fin 2) : (teleState α β).ofLp (a, b, c) = 1 / 2 * (bellPhiPlus.ofLp (a, b) * (bobPhiPlus α β).ofLp c + bellPhiMinus.ofLp (a, b) * (bobPhiMinus α β).ofLp c + bellPsiPlus.ofLp (a, b) * (bobPsiPlus α β).ofLp c + bellPsiMinus.ofLp (a, b) * (bobPsiMinus α β).ofLp c)

Teleportation identity. Re-expanding the input |ψ⟩₁ ⊗ |Φ⁺⟩₂₃ in Alice's Bell basis on qubits (1,2): Ψ(a,b,c) = ½ ( Φ⁺(a,b)·(I|ψ⟩)(c) + Φ⁻(a,b)·(Z|ψ⟩)(c) + Ψ⁺(a,b)·(X|ψ⟩)(c) + Ψ⁻(a,b)·(XZ|ψ⟩)(c) ). So a Bell measurement on qubits (1,2) collapses Bob's qubit 3 to a Pauli image of |ψ⟩, the image determined by the two-bit outcome.

Per-branch recovery

theorem CSD.Empirical.QM.Teleportation.mulVec_fin2 (M : Matrix (Fin 2) (Fin 2) ℂ) (v : EuclideanSpace ℂ (Fin 2)) (i : Fin 2) : M.mulVec v.ofLp i = M i 0 * v.ofLp 0 + M i 1 * v.ofLp 1

The matrix-vector image collapses to a Fin 2 sum (helper for recovery).

theorem CSD.Empirical.QM.Teleportation.recover_phiPlus (α β : ℂ) : (Matrix.toEuclideanLin 1) (bobPhiPlus α β) = teleInput α β

Branch |Φ⁺⟩ recovery: I · (I|ψ⟩) = |ψ⟩.

theorem CSD.Empirical.QM.Teleportation.recover_phiMinus (α β : ℂ) : (Matrix.toEuclideanLin teleZ) (bobPhiMinus α β) = teleInput α β

Branch |Φ⁻⟩ recovery: Z · (Z|ψ⟩) = |ψ⟩.

theorem CSD.Empirical.QM.Teleportation.recover_psiPlus (α β : ℂ) : (Matrix.toEuclideanLin teleX) (bobPsiPlus α β) = teleInput α β

Branch |Ψ⁺⟩ recovery: X · (X|ψ⟩) = |ψ⟩.

theorem CSD.Empirical.QM.Teleportation.recover_psiMinus (α β : ℂ) : (Matrix.toEuclideanLin teleZX) (bobPsiMinus α β) = teleInput α β

Branch |Ψ⁻⟩ recovery: ZX · (XZ|ψ⟩) = |ψ⟩.

theorem CSD.Empirical.QM.Teleportation.teleportation_branch_recovers_input (α β : ℂ) : (Matrix.toEuclideanLin 1) (bobPhiPlus α β) = teleInput α β ∧ (Matrix.toEuclideanLin teleZ) (bobPhiMinus α β) = teleInput α β ∧ (Matrix.toEuclideanLin teleX) (bobPsiPlus α β) = teleInput α β ∧ (Matrix.toEuclideanLin teleZX) (bobPsiMinus α β) = teleInput α β

Teleportation recovers the input in every branch. Bundles the four per-branch corrections: with the two-bit Bell-measurement outcome, Bob's Pauli correction returns |ψ⟩ exactly.

Input normalisation

theorem CSD.Empirical.QM.Teleportation.teleInput_norm (α β : ℂ) (h : ‖α‖ ^ 2 + ‖β‖ ^ 2 = 1) : ‖teleInput α β‖ = 1

The input qubit is a unit vector when ‖α‖² + ‖β‖² = 1.