Empirical/QM: quantum Darwinism as spectrum broadcast structure

Category: 3-Local (promotion-ready). QM-generic: density matrices and a two-outcome test, no CSD ontology.

Expert-review row E of specs/BACKLOG.md, QM side. Scoped in specs/quantum-darwinism-scoping.md; read its §2 and §4 before extending this file.

The corpus proves that records are made (the pointer strokes, the Lüders theorems) and which basis survives (Empirical/CSD/Einselection.lean). It did not say that a record is redundantly copied — the property the decoherence literature uses as its criterion for a record being objective.

Which theorem this is, and which it is not

⚠️ Not the mutual-information plateau. Zurek's redundancy is usually stated as I(S : F) ≥ (1−δ)H(S) for many disjoint fragments F. That form routes through mutual information and its monotonicity, and in this corpus Mathlib/QuantumInfo/StrongSubadditivity.lean carries SSA with hDPI as an explicit hypothesis — the unconditional version sits behind the Effros/Lieb summit, which sits behind specs/lieb-dpi-scoping.md Gate 1, an open author decision. Building the entropic form here would import that gate. It is deliberately not built.

What is here is spectrum broadcast structure (Horodecki–Korbicz–Aharonov 2015): the structural form of the same physics, which implies the plateau and does not need entropies. Each fragment holds a state ρᵢ⁽ᶠ⁾ conditioned on the outcome i, and the states of any one fragment are pairwise orthogonal, so that fragment alone identifies the outcome.

• SpectrumBroadcast — the structure: a probability vector, per-fragment conditional states, and orthogonality within each fragment;
• ★ SpectrumBroadcast.not_of_constant_fragment — the vacuity test the scoping note demands, as a theorem. A fragment whose state does not depend on the outcome — the fragment that was never coupled — cannot occur in a spectrum broadcast structure at all. So the orthogonality field is doing work: it excludes something;
• ★ successProb_eq_one_of_discriminating — the general operational lemma: a test that passes ρᵢ and rejects ρⱼ discriminates them with certainty;
• copyBroadcast — the k-fold classical copy, and ★ copyBroadcast_perfect : every one of the k fragments, on its own, identifies the outcome with probability one. That is the redundancy statement, non-vacuously realised at arbitrary k.

Honest scope

⚠️ The general "orthogonal ⇒ perfectly discriminable" theorem is NOT proved here. From ρᵢ ρⱼ = 0 alone, producing the discriminating test needs the support projection of a positive semidefinite matrix and the fact that it annihilates anything orthogonal to it. TraceDistance.lean has the ingredients (posProj, mul_posProj_eq_posPart) but not that lemma, and it is a spectral argument, not a computation. What is proved instead is the conditional lemma plus its instantiation on the copy witness, where the projection is explicit. Recorded as the residue of this module; closing it would upgrade copyBroadcast_perfect from a witness to a theorem about every SpectrumBroadcast.

⚠️ No dynamics. Nothing here derives that a physical environment couples this way; which interaction an environment realises is R-015, a permanent boundary. copyBroadcast is a modelling choice exhibited as a witness, not a claim about environments.

⚠️ No CSD content. The CSD-side twin — records as agreeing coordinates of one Σ-point, and the scope theorem that objectivity is the ontic selection rather than the redundancy — is specs/quantum-darwinism-scoping.md §5 and is not built.

References: Horodecki, Korbicz & Aharonov, Phys. Rev. A 91, 032122 (2015) (spectrum broadcast structure); Zurek, Nature Physics 5, 181 (2009) (quantum Darwinism); Blume-Kohout & Zurek, Phys. Rev. A 73, 062310 (2006) (the plateau, §2 above — not built); CsdLean4/Mathlib/QuantumInfo/Helstrom.lean; specs/quantum-darwinism-scoping.md.

The structure

structure CSD.Empirical.Darwinism.SpectrumBroadcast (N k d : ℕ) : Type

Spectrum broadcast structure. The joint state of a system with N outcomes and k environment fragments has the form ∑ᵢ pᵢ |i⟩⟨i| ⊗ ρᵢ⁽¹⁾ ⊗ ⋯ ⊗ ρᵢ⁽ᵏ⁾ with, for each fragment, the conditional states pairwise orthogonal.

The joint state is not carried as a matrix: the whole content of the definition is the per-fragment data plus orthogonal, and a k-fold Kronecker product would add index plumbing without adding a hypothesis.

• p : Fin N → ℝ

  The outcome distribution.

• p_nonneg (i : Fin N) : 0 ≤ self.p i

  Probabilities are nonnegative.

• p_sum : ∑ i : Fin N, self.p i = 1

  Probabilities sum to one.

• ρ : Fin k → Fin N → Matrix (Fin d) (Fin d) ℂ

  The state of fragment f conditioned on outcome i.

• ρ_posSemidef (f : Fin k) (i : Fin N) : (self.ρ f i).PosSemidef

  Each conditional state is positive semidefinite.

• ρ_trace (f : Fin k) (i : Fin N) : (self.ρ f i).trace = 1

  Each conditional state is normalised.

• orthogonal (f : Fin k) (i j : Fin N) : i ≠ j → self.ρ f i * self.ρ f j = 0

  The broadcast condition. Within any one fragment, distinct outcomes leave orthogonal states — which is what makes that fragment alone a record.

theorem CSD.Empirical.Darwinism.SpectrumBroadcast.trace_mul_eq_zero {N k d : ℕ} (S : SpectrumBroadcast N k d) (f : Fin k) {i j : Fin N} (h : i ≠ j) : (S.ρ f i * S.ρ f j).trace = 0

Orthogonality in trace form.

theorem CSD.Empirical.Darwinism.SpectrumBroadcast.not_of_constant_fragment {N k d : ℕ} (S : SpectrumBroadcast N k d) (hN : 1 < N) (f : Fin k) (σ : Matrix (Fin d) (Fin d) ℂ) (hconst : ∀ (i : Fin N), S.ρ f i = σ) : False

★ The vacuity test, as a theorem (specs/quantum-darwinism-scoping.md §4).

A fragment whose conditional state does not depend on the outcome — the fragment that the interaction never touched — cannot appear in a spectrum broadcast structure, as soon as there are two outcomes to tell apart. So orthogonal excludes something, and a redundancy statement resting on this structure is not true by construction.

The proof is the reason the normalisation field is there: a constant fragment would need σ * σ = 0, and a positive semidefinite matrix with σ² = 0 is zero, which has trace 0, not 1.

Discrimination from an explicit test

theorem CSD.Empirical.Darwinism.successProb_eq_one_of_discriminating {n : Type u_1} [Fintype n] [DecidableEq n] {ρ₀ ρ₁ E : Matrix n n ℂ} (h₀ : ρ₀.trace = 1) (h₁ : ρ₁.trace = 1) (hpass : ρ₀ * E = ρ₀) (hreject : ρ₁ * E = 0) : QuantumInfo.successProb ρ₀ ρ₁ E = 1

★ A test that passes ρ₀ and rejects ρ₁ discriminates them with certainty.

E * ρ₀ = ρ₀ says the test accepts the first state outright; E * ρ₁ = 0 says it never fires on the second. The Helstrom success probability is then exactly 1.

The k-fold classical copy, and redundancy at every fragment

noncomputable def CSD.Empirical.Darwinism.basisProj {N : ℕ} (i : Fin N) : Matrix (Fin N) (Fin N) ℂ

The rank-one diagonal projection |i⟩⟨i|.

Equations

• CSD.Empirical.Darwinism.basisProj i = Matrix.diagonal fun (m : Fin N) => if m = i then 1 else 0

@[simp]

theorem CSD.Empirical.Darwinism.basisProj_mul_self {N : ℕ} (i : Fin N) : basisProj i * basisProj i = basisProj i

@[simp]

theorem CSD.Empirical.Darwinism.basisProj_mul_ne {N : ℕ} {i j : Fin N} (h : i ≠ j) : basisProj i * basisProj j = 0

@[simp]

theorem CSD.Empirical.Darwinism.trace_basisProj {N : ℕ} (i : Fin N) : (basisProj i).trace = 1

theorem CSD.Empirical.Darwinism.basisProj_posSemidef {N : ℕ} (i : Fin N) : (basisProj i).PosSemidef

noncomputable def CSD.Empirical.Darwinism.copyBroadcast (k N : ℕ) (p : Fin N → ℝ) (hp : ∀ (i : Fin N), 0 ≤ p i) (hsum : ∑ i : Fin N, p i = 1) : SpectrumBroadcast N k N

The k-fold classical copy. Every fragment ends holding the pointer state |i⟩⟨i|: the interaction copied the outcome into all k of them.

Equations

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

theorem CSD.Empirical.Darwinism.copyBroadcast_perfect (k N : ℕ) (p : Fin N → ℝ) (hp : ∀ (i : Fin N), 0 ≤ p i) (hsum : ∑ i : Fin N, p i = 1) (f : Fin k) {i j : Fin N} (hij : i ≠ j) : QuantumInfo.successProb ((copyBroadcast k N p hp hsum).ρ f i) ((copyBroadcast k N p hp hsum).ρ f j) (basisProj i) = 1

★★ Redundancy. In the k-fold copy, each fragment on its own identifies the outcome with probability one: for every fragment f and every pair of distinct outcomes, the test |i⟩⟨i| applied to that fragment alone discriminates them perfectly.

This is the redundancy statement the row asked for, and it is non-vacuous in both directions: it holds for arbitrary k here, and by SpectrumBroadcast.not_of_constant_fragment it would fail outright for a fragment the interaction never touched.

theorem CSD.Empirical.Darwinism.basisProj_isTest {N : ℕ} (i : Fin N) : QuantumInfo.IsTest (basisProj i)

The discriminating test really is a two-outcome test.