Empirical/QM: No-communication theorem (E3a, marginal form)

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

The no-communication (no-signalling) theorem: a local operation performed by Alice on her half of a shared bipartite state cannot change any measurement statistic Bob computes on his half. This is the relativistic-causality guarantee underlying entanglement — entanglement gives correlations but no faster-than-light signalling.

We deliver the marginal form (E3a), which avoids the reduced-density / partial-trace machinery (absent from Mathlib): for a bipartite state ψ ∈ ℂ^m ⊗ ℂ^n, any unitary Alice-side operation U (Uᴴ U = I), and any Bob-side operator Q,

⟨(U ⊗ I) ψ, (I ⊗ Q) (U ⊗ I) ψ⟩ = ⟨ψ, (I ⊗ Q) ψ⟩.

The left side is the expectation of Bob's observable Q after Alice applies U; the right side is the expectation with Alice doing nothing. Taking Q a projector gives Bob's outcome probabilities; taking Q Hermitian gives his expectation values (bob_expectation_invariant). Either way Alice's choice of U does not enter.

This is strictly stronger than the singlet-specific Bell-marginal no-signalling already in Empirical/QM/Bell.lean (no_signalling_alice/bob, which are about the fixed singlet and specific Pauli settings): it holds for an arbitrary shared state ψ, an arbitrary unitary Alice operation, and an arbitrary Bob observable.

Scope (E3a vs E3b)

This is the amplitude / marginal form, needing only the Kronecker mixed-product identity (A ⊗ B)(C ⊗ D) = (AC) ⊗ (BD). The reduced-density form (E3b) — "Alice's local CPTP map leaves Tr_A(ρ) invariant" — is now also proved here (no_communication_reduced, channel_no_communication), on the Mathlib/LinearAlgebra/Matrix/PartialTrace.lean infrastructure that landed with the K2 channel tranche; the earlier "deferred" note is superseded.

Source

Standard; the relativistic no-signalling property of quantum mechanics (Ghirardi-Rimini-Weber 1980; Eberhard 1978). Cf. the PR-box / no-signalling literature (Popescu-Rohrlich 1994).

noncomputable def CSD.Empirical.QM.NoCommunication.aliceOp {m n : ℕ} (U : Matrix (Fin m) (Fin m) ℂ) : Matrix (Fin m × Fin n) (Fin m × Fin n) ℂ

Alice's local operation U ⊗ I on the bipartite space ℂ^m ⊗ ℂ^n (Fin m × Fin n-indexed).

Equations

• CSD.Empirical.QM.NoCommunication.aliceOp U = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) U 1

noncomputable def CSD.Empirical.QM.NoCommunication.bobOp {m n : ℕ} (Q : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin m × Fin n) (Fin m × Fin n) ℂ

Bob's observable I ⊗ Q on the bipartite space.

Equations

• CSD.Empirical.QM.NoCommunication.bobOp Q = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 Q

theorem CSD.Empirical.QM.NoCommunication.aliceOp_conjugate {m n : ℕ} (U : Matrix (Fin m) (Fin m) ℂ) (Q : Matrix (Fin n) (Fin n) ℂ) (hU : U.conjTranspose * U = 1) : (aliceOp U).conjTranspose * (bobOp Q * aliceOp U) = bobOp Q

Matrix core. Conjugating Bob's operator by Alice's unitary leaves it unchanged: (U ⊗ I)ᴴ · (I ⊗ Q) · (U ⊗ I) = I ⊗ Q, because the Alice factor collapses through Uᴴ U = I and the Bob factor through I·Q·I = Q.

theorem CSD.Empirical.QM.NoCommunication.no_communication {m n : ℕ} (U : Matrix (Fin m) (Fin m) ℂ) (Q : Matrix (Fin n) (Fin n) ℂ) (hU : U.conjTranspose * U = 1) (ψ : EuclideanSpace ℂ (Fin m × Fin n)) : inner ℂ ((Matrix.toEuclideanLin (aliceOp U)) ψ) ((Matrix.toEuclideanLin (bobOp Q)) ((Matrix.toEuclideanLin (aliceOp U)) ψ)) = inner ℂ ψ ((Matrix.toEuclideanLin (bobOp Q)) ψ)

No-communication theorem (marginal form). For a bipartite state ψ, a unitary Alice-side operation U, and any Bob-side operator Q, Bob's expectation ⟨φ, (I ⊗ Q) φ⟩ is the same whether or not Alice applies U (φ = (U ⊗ I) ψ vs φ = ψ). Alice cannot signal to Bob.

Proof. Move U ⊗ I across the inner product as an adjoint (adjoint_inner_right + toEuclideanLin_conjTranspose_eq_adjoint), compose the three matrices into one (toLpLin_mul_same), and collapse the conjugate by aliceOp_conjugate.

theorem CSD.Empirical.QM.NoCommunication.bob_expectation_invariant {m n : ℕ} (U : Matrix (Fin m) (Fin m) ℂ) (Q : Matrix (Fin n) (Fin n) ℂ) (hU : U.conjTranspose * U = 1) (ψ : EuclideanSpace ℂ (Fin m × Fin n)) : (inner ℂ ((Matrix.toEuclideanLin (aliceOp U)) ψ) ((Matrix.toEuclideanLin (bobOp Q)) ((Matrix.toEuclideanLin (aliceOp U)) ψ))).re = (inner ℂ ψ ((Matrix.toEuclideanLin (bobOp Q)) ψ)).re

Bob's expectation/probability is invariant. The real-valued form of no_communication: Bob's measured expectation of Q (and, for Q a projector, his outcome probability) does not depend on Alice's local unitary.

E3b: reduced-density form

The full operator-state statement, now that partial trace is available (CsdLean4/Mathlib/LinearAlgebra/Matrix/PartialTrace.lean): Alice's local unitary leaves Bob's reduced density operator invariant — the strongest no-signalling form short of a general CPTP map. Alice acts on factor 1 (aliceOp U = U ⊗ I), so Bob's reduced state is the partial trace over the first factor, traceLeft.

theorem CSD.Empirical.QM.NoCommunication.no_communication_reduced {m n : ℕ} (U : Matrix (Fin m) (Fin m) ℂ) (hU : U.conjTranspose * U = 1) (ρ : Matrix (Fin m × Fin n) (Fin m × Fin n) ℂ) : (aliceOp U * ρ * (aliceOp U).conjTranspose).traceLeft = ρ.traceLeft

No-communication, reduced-density form (E3b). For a bipartite density operator ρ on ℂ^m ⊗ ℂ^n and a unitary Alice-side operation U, conjugating by U ⊗ I leaves Bob's reduced state Tr_A ρ = traceLeft ρ unchanged. Specialises the partial-trace cyclicity lemma Matrix.traceLeft_conjTranspose_kronecker_one to aliceOp U = U ⊗ₖ I.

theorem CSD.Empirical.QM.NoCommunication.channel_no_communication {A : Type u_1} {A' : Type u_2} {B : Type u_3} {ι : Type u_4} [Fintype A] [Fintype A'] [Fintype B] [Fintype ι] [DecidableEq A] [DecidableEq B] (Φ : QuantumInfo.Channel A A' ι) (ρ : Matrix (A × B) (A × B) ℂ) : ((Φ.tensorRight B).apply ρ).traceLeft = ρ.traceLeft

No-communication, CPTP form (E3, retires the CPTP gap). For any quantum channel Φ (an arbitrary local CPTP map, not merely a unitary) applied on Alice's subsystem while Bob is idle (Φ ⊗ id), Bob's reduced state Tr_A is unchanged: traceLeft ((Φ ⊗ id) ρ) = traceLeft ρ. This is the strongest no-signalling form — it covers measurement, decoherence, and any noise Alice's lab applies. The Kraus operators recombine through the channel's trace-preserving identity ∑ᵢ Kᵢᴴ Kᵢ = 1, via Matrix.traceLeft_sum_conjTranspose_kronecker_one. Generalises no_communication_reduced (the single-unitary case).

theorem CSD.Empirical.QM.NoCommunication.reducedLeft_aliceConj_eq {m n : ℕ} (U : Matrix (Fin m) (Fin m) ℂ) (hU : U.conjTranspose * U = 1) (ρ : LF2.DensityOperatorIx (Fin m × Fin n)) : (aliceOp U * ρ.M * (aliceOp U).conjTranspose).traceLeft = ρ.reducedLeft.M

No-communication on a density operator (E3b, structured). Stated on the LF2 DensityOperatorIx: Alice's local unitary U ⊗ I leaves Bob's reduced density operator (reducedLeft, the partial trace over Alice's factor) unchanged at the matrix level.