Empirical/QM: No-broadcasting — pure-marginal confinement core (E2)

Category: 3-Local.

No-broadcasting (Barnum-Caves-Fuchs-Jozsa-Schumacher 1996) generalises no-cloning to mixed states: a set of states can be broadcast (each marginal of a joint output equals the corresponding input) iff the states mutually commute. The full iff is relative-entropy-monotonicity content and is out of scope here: BCFJS run the argument through D(ρ₁‖ρ₂) ≥ 2D(ρ₁‖ρ₂) against channel monotonicity, so the gate is the hDPI hypothesis of QuantumInfo.strong_subadditivity_of_relEntropy_monotone (specs/operator-convexity-plan.md). The corpus does carry relEntropy with Klein's inequality (Mathlib/QuantumInfo/Subadditivity.lean) and the Kraus Channel layer (Mathlib/QuantumInfo/Channel.lean); what it does not carry is DPI, nor fidelity.

What the partial-trace infrastructure (CsdLean4/Mathlib/LinearAlgebra/Matrix/PartialTrace.lean) does deliver is the structural squeeze that makes broadcasting of a pure state impossible:

Pure-marginal confinement. If a bipartite (PSD, Hermitian) operator ρ on ℂ^N ⊗ ℂ^n has a pure first-factor marginal traceRight ρ = |ψ⟩⟨ψ|, then ρ is confined to that pure sector: (P ⊗ I) · ρ · (P ⊗ I) = ρ, where P = |ψ⟩⟨ψ|.

A pure marginal leaves the joint state no freedom outside the P-sector — the operative fact behind "broadcasting pure states = cloning them." The proof is the positive-semidefinite block-vanishing technique (mirroring LF2.rankOneDensity_unique_of_certainty): the complementary block (Q ⊗ I) · ρ · (Q ⊗ I) (with Q = I − P) is PSD with trace zero — its trace is Tr(traceRight ρ · Q) = Tr(P · Q) = 0 via the partial-trace module laws — hence zero, which pins ρ to the P-sector.

Source

Barnum, Caves, Fuchs, Jozsa, Schumacher 1996, Phys. Rev. Lett. 76, 2818 (the full no-broadcasting theorem; only the pure-marginal core is formalised here).

theorem CSD.Empirical.QM.NoBroadcasting.traceForm_complement_block_zero {N n : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (ρ : Matrix (Fin N × Fin n) (Fin N × Fin n) ℂ) (hmarg : ρ.traceRight = LF2.outerProduct ψ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (1 - LF2.outerProduct ψ) 1 * ρ * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (1 - LF2.outerProduct ψ) 1).trace = 0

Trace of the complementary-block conjugation vanishes. With P = |ψ⟩⟨ψ|, Q = I − P, and a bipartite operator ρ whose first-factor marginal is P, the trace of (Q ⊗ I) · ρ · (Q ⊗ I) is zero: Tr = Tr(ρ · (Q ⊗ I)) = Tr(traceRight ρ · Q) = Tr(P · Q) = 0 (since P·Q = 0).

theorem CSD.Empirical.QM.NoBroadcasting.pure_marginal_confinement {N n : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (ρ : Matrix (Fin N × Fin n) (Fin N × Fin n) ℂ) (hρ : ρ.PosSemidef) (hmarg : ρ.traceRight = LF2.outerProduct ψ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct ψ) 1 * ρ * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct ψ) 1 = ρ

Pure-marginal confinement (E2 core). A bipartite positive-semidefinite operator ρ whose first-factor marginal is the pure state P = |ψ⟩⟨ψ| is confined to the P-sector: (P ⊗ I) · ρ · (P ⊗ I) = ρ.

This is the structural obstruction to broadcasting a pure state: the joint output of any prospective broadcaster, having |ψ⟩⟨ψ| as a marginal, has no support outside the one-dimensional ψ-sector — leaving no room for an independent second copy (which would require support on |φ⟩ for a distinct φ). The proof: the complementary block (Q ⊗ I)·ρ·(Q ⊗ I) is PSD (sandwich of PSD by Hermitian) with trace zero (traceForm_complement_block_zero), hence zero; standard PSD reasoning then collapses ρ to its P-sector.