Lean 4 Verified — 1 result, 2 Lean theorems
The results below have been independently checked in Lean 4, a proof assistant that mechanically verifies every logical step. Click a result name to jump to it in the derivation.
bell_matrix_detbell_expansion
Overview
This derivation addresses the question: how can a quantum state be transferred between distant parties without physically sending it, and why does this not allow faster-than-light communication?
Quantum teleportation — experimentally demonstrated many times since 1997 — allows Alice to transmit an unknown quantum state to Bob using only a shared entangled pair and a classical message. The state is destroyed at Alice’s end and recreated at Bob’s, with perfect fidelity. Standard quantum mechanics describes how teleportation works but leaves the “why” somewhat opaque.
The argument. The framework recasts teleportation as a structured redistribution of coherence across three observers:
- Alice and Bob share a pre-existing relational invariant (their entangled resource). Alice also holds the unknown state, encoded as a separate relational invariant with the system.
- Alice performs a joint measurement on her system and her half of the entangled pair. This measurement consumes both her relational invariants — the one with the system and the one with Bob — producing a classical outcome (two bits of information).
- Bob’s particle is now in a state that differs from the original by a known, simple correction. Once Alice sends him the two classical bits, he applies the correction and recovers the original state exactly.
- Coherence conservation enforces every constraint: the original state must be destroyed (no cloning), the entangled resource must be consumed (one-time use), and without the classical message Bob’s state carries no information (no faster-than-light signaling).
The result. Teleportation is a coherence channel transfer — the relational invariant moves from one observer pair to another, with the entangled state serving as the channel and classical communication as the key. No new physics is invoked; it is a direct consequence of entanglement, measurement, and coherence conservation.
Why this matters. Teleportation is often presented as one of quantum mechanics’ most counterintuitive phenomena. The coherence framework shows it is structurally inevitable once you have entanglement and conservation — there is nothing mysterious about it beyond the unfamiliarity of the underlying rules.
An honest caveat. The overview omits the detailed algebraic manipulations (Bell basis expansion, Pauli corrections) that make the protocol precise. The explanation also focuses on the simplest case of a single qubit; the generalization to higher-dimensional systems is straightforward but technically richer.
Note on status. This derivation is provisional because its central claims depend on preferred-basis S1 (interaction-invariant correspondence) (see Preferred Basis). If those postulates are promoted to theorems, this derivation would be upgraded to rigorous.
Statement
Theorem. Quantum teleportation — the transfer of an unknown quantum state from Alice to Bob using a shared entangled state and classical communication — is a coherence channel transfer in the observer-centric framework. The relational invariant between Alice and a system is transferred to a relational invariant between Bob and , mediated by the pre-existing relational invariant (the entangled resource). Coherence conservation (Axiom 1) guarantees that the original is destroyed and is consumed: no cloning occurs and the entanglement resource is depleted.
Derivation
Structural postulates: None. This derivation requires no assumptions beyond the axioms and previously derived results.
Step 1: The Setup — Three Observers and Their Relational Invariants
Definition 1.1 (Teleportation configuration). The teleportation protocol involves three observers:
- (Alice): holds system in an unknown state
- (Bob): spatially separated from Alice
- (the system): whose state is to be teleported
and the following initial relational invariant structure:
| Pair | Relational invariant | Status |
|---|---|---|
| – | exists (entangled resource) | Shared prior to protocol |
| – | exists (unknown state) | To be transferred |
| – | does not exist | To be created |
Proposition 1.2 (Hilbert space description). In the Hilbert space picture (Entanglement, Step 1), the initial state is:
where is the unknown state of (encoding the relational invariant ), and is the maximally entangled Bell state (encoding the relational invariant ).
Proof. The unknown state encodes Alice’s relational invariant with : specifically, the coherence distribution across the eigenbasis of (Measurement, Proposition 1.3). The Bell state encodes the relational invariant between Alice and Bob (Entanglement, Proposition 1.3), with maximal relational coherence (Entanglement, Theorem 2.1). Bob has no relational invariant with , so and are in a product state.
Step 2: Alice’s Bell Measurement — A Type III Interaction
Definition 2.1 (Bell measurement). Alice performs a joint measurement on and her half of the entangled pair . This is a Type III interaction (Three Interaction Types, Definition 4.4) between the composite system and Alice’s measuring apparatus, generating a new relational invariant in the Bell basis.
Theorem 2.2 (Bell basis expansion). The initial state, rewritten in the Bell basis for the subsystem, is:
where and are the four Bell states.
Proof. This is a standard algebraic identity. Expand in the three-qubit computational basis and re-express the subsystem in the Bell basis. The four Bell states form a complete orthonormal basis for , so the expansion is unique.
Proposition 2.3 (Measurement generates a classical relational invariant). Alice’s Bell measurement is a Type III interaction that generates a relational invariant between Alice and the pair. The measurement outcome — one of — is a classical relational invariant (2 bits of information) that can be communicated to Bob.
Proof. By Measurement (Theorem 2.2), the measurement interaction correlates Alice’s detector state with the Bell-basis eigenstate of . The outcome labels a definite eigenvalue of . This is a classical relational invariant: it is conserved, locally definite, and can be encoded in classical bits.
Step 3: Coherence Redistribution
Theorem 3.1 (Post-measurement state). After Alice obtains outcome , Bob’s conditional state is:
| Alice’s outcome | Bob’s state |
|---|---|
Each of Bob’s conditional states is related to the original by a known unitary: respectively.
Proof. This follows directly from the Bell basis expansion (Theorem 2.2). Conditioning on Alice’s outcome projects the subsystem onto the -th Bell state, leaving Bob’s qubit in the corresponding state from the expansion. Each such state differs from by a Pauli matrix, which is a known unitary operator.
Proposition 3.2 (Coherence accounting). The coherence budget before and after Alice’s measurement:
Before:
After:
where is the coherence content of and is the coherence of Bob’s conditional state (which equals since Bob’s state is unitarily related to ). The total coherence is conserved.
Proof. Alice’s measurement generates 2 bits () of classical relational invariant. The entangled resource (carrying of relational coherence) is consumed: after the measurement, Alice’s half of the entangled pair is part of the Bell-state projection, no longer entangled with Bob. The original relational invariant is also consumed (the system is now part of the Bell-state measurement outcome). The coherence that was in and has been redistributed into: (i) the classical measurement outcome , and (ii) the coherence content of Bob’s conditional state. By Axiom 1, the total is conserved.
Step 4: Bob’s Correction — Completing the Transfer
Theorem 4.1 (Teleportation completion). Upon receiving Alice’s classical measurement outcome (2 bits), Bob applies the corresponding Pauli correction:
| Alice’s outcome | Bob’s correction |
|---|---|
| (do nothing) | |
| (phase flip) | |
| (bit flip) | |
| (bit + phase flip) |
After the correction, Bob’s state is — identical to the original state of relative to Alice.
Proof. Each correction is the inverse of the Pauli operator relating Bob’s conditional state to (Theorem 3.1). Since the Pauli matrices are self-inverse (), the correction restores :
After the correction, the relational invariant is established: Bob has a definite relationship with the state , encoding the same coherence distribution as Alice’s original .
Corollary 4.2 (Classical communication is necessary). Without Alice’s 2-bit classical message, Bob cannot determine which correction to apply. His unconditional state (averaged over Alice’s outcomes) is:
which is maximally mixed and carries no information about . Classical communication is therefore essential — teleportation cannot be used for faster-than-light signaling.
Proof. The four Pauli matrices form a basis for Hermitian matrices. Averaging over all four Pauli rotations gives for any . This is a standard result (the Pauli twirl).
Step 5: Relational Invariant Transfer — Summary
Theorem 5.1 (Teleportation as coherence channel transfer). The net effect of the teleportation protocol on the relational invariant structure is:
| Pair | Before | After |
|---|---|---|
| – | (entangled) | Consumed |
| – | (unknown state) | Consumed |
| – | None | (transferred state) |
| – | None | (classical, 2 bits) |
The protocol transfers the relational invariant from Alice– to Bob–, consuming the entangled resource in the process.
Proof. This summarizes the results of Steps 2–4. The key structural features:
-
No cloning: is destroyed when Alice performs the Bell measurement. The coherence that was in is redistributed, not duplicated. This is consistent with the no-cloning theorem (Entanglement, Theorem 3.1).
-
Resource consumption: is consumed — after the protocol, Alice and Bob are no longer entangled. The entangled state served as a coherence channel, and that channel is depleted after one use.
-
Classical bottleneck: The 2-bit classical message is the information that “unlocks” Bob’s conditional state. Without it, the coherence is present but inaccessible (Bob’s unconditional state is maximally mixed). This is the no-signaling constraint.
-
Coherence conservation: The total coherence before () equals the total coherence after (). No coherence is created or destroyed.
Corollary 5.2 (Teleportation fidelity). The teleportation is exact: encodes exactly the same coherence distribution as . The fidelity . This is not an approximation but a structural consequence of unitarity and coherence conservation.
Step 6: Generalizations
Proposition 6.1 (Higher-dimensional teleportation). The protocol generalizes to -dimensional systems. A maximally entangled state and a generalized Bell measurement (in the basis of maximally entangled states) transfers the state, consuming bits of classical communication and ebits of entanglement.
Proof. The argument of Steps 2–4 extends by replacing the four Bell states with the generalized Bell states (where and are the generalized Pauli operators in dimension ). The Bell basis expansion, measurement, and correction proceed identically. The coherence accounting generalizes: the entangled resource carries of relational coherence, and the classical message carries of classical information.
Proposition 6.2 (Entanglement swapping as iterated transfer). Entanglement swapping — creating entanglement between two parties who have never interacted — is an immediate consequence: Alice shares with Bob and with Charlie. By teleporting her half of to Bob (using as the resource), a new relational invariant is established between Bob and Charlie, who have never directly interacted.
Proof. Apply Theorem 5.1 with = Alice’s half of the pair. The teleportation transfers the relational invariant from Alice– to Bob–. Since was entangled with Charlie, the net effect is that Bob inherits Alice’s relational invariant with Charlie. The result is entanglement between Bob and Charlie, created without direct interaction, mediated by Alice’s measurements and classical communication.
Consistency Model
Theorem 7.1. The standard quantum circuit for teleportation provides a consistency model for all results of this derivation.
Verification. Take with , (an arbitrary non-trivial state).
- Proposition 1.2: Initial state .
- Theorem 2.2: Bell basis expansion verified by direct calculation (6-term → 4-term regrouping).
- Theorem 3.1: If Alice measures , Bob’s state is .
- Theorem 4.1: Bob applies : .
- Corollary 4.2: Without classical communication, (maximally mixed). Confirmed: for all .
- Proposition 3.2: Coherence accounting: initial entanglement + state coherence = post-measurement classical information + Bob’s state coherence. Balance verified.
- Theorem 5.1: After the protocol, Alice–Bob entanglement is consumed (verified: the subsystem is in a product state), and Bob holds .
Rigor Assessment
Fully rigorous:
- Proposition 1.2: Hilbert space setup from Entanglement (Theorem 2.1) and Measurement (Proposition 1.3)
- Theorem 2.2: Bell basis expansion (standard linear algebra identity)
- Proposition 2.3: Measurement as Type III interaction (direct application of Measurement, Theorem 2.2)
- Theorem 3.1: Post-measurement states (conditioning on measurement outcomes)
- Proposition 3.2: Coherence accounting (direct application of Axiom 1)
- Theorem 4.1: Pauli correction (self-inverse property of Pauli matrices)
- Corollary 4.2: No-signaling (Pauli twirl averaging)
- Theorem 5.1: Relational invariant transfer summary (synthesis of Steps 2–4)
- Corollary 5.2: Exact fidelity (unitarity + coherence conservation)
- Proposition 6.1: Higher-dimensional generalization (generalized Pauli operators)
- Proposition 6.2: Entanglement swapping (iterated application of Theorem 5.1)
- Theorem 7.1: Consistency model verified on explicit quantum circuit
No structural postulates required. The derivation builds entirely on Entanglement, Measurement, and Three Interaction Types.
Assessment: Rigorous. The teleportation protocol is a direct synthesis of entanglement (relational invariants between observers), measurement (Type III interaction generating classical relational invariants), and coherence conservation (no cloning, resource consumption). Every step is either a standard quantum information result or a direct application of previously derived framework results.
Open Gaps
- Quantum key distribution: The teleportation channel can be repurposed for quantum key distribution (BB84, E91). Derive the security of QKD from coherence conservation — specifically, that any eavesdropper must create a relational invariant with the channel, which is detectable via the monogamy of entanglement.
- Continuous-variable teleportation: Extend from qubits to continuous-variable systems (Braunstein-Kimble protocol). The relational invariants become continuous, and the Bell measurement becomes a homodyne detection. The coherence accounting should generalize via the continuous entropy.
- Teleportation as a resource theory: Formalize the resource-theoretic aspects: entanglement as the resource, classical communication as the catalyst, and coherence conservation as the resource monotone. This connects to the broader resource theory of quantum entanglement.