SigmaLayer/MixedEnsemble: finite ensembles and the spectral ensemble decomposition (#8 A+B)

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

Extends the mixed-state layer (SigmaLayer/MixedState.lean, ledger T9) from the binary mixture mix to the two missing pieces of the mixed-state / ensemble representation flagged as open in specs/future-work.md (SL-T9 "remaining extensions"):

• A — finite ensembles. ensemble w ρ = ∑ᵢ wᵢ ρᵢ over a finite index type: a convex combination of arbitrarily many density operators is a density operator (ensemble), and the Born rule is affine over the whole ensemble, Tr((∑ᵢ wᵢ ρᵢ) E) = ∑ᵢ wᵢ Tr(ρᵢ E) (traceForm_ensemble) — the many-component generalisation of traceForm_mix.
• B — the spectral ensemble decomposition. Every density operator IS a convex ensemble of PURE states: ρ = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| where the eigenvalues λᵢ form a probability distribution and the eigenvectors eᵢ are the pure components (density_eq_eigen_ensemble, density_isPureEnsemble). Hence the Born rule for any mixed state is the eigenvalue-weighted average of the pure Born rules (traceForm_eq_pureEnsemble) — the operational content of "mixed = classical mixture of pure".

Built on Mathlib's Hermitian spectral theorem (Matrix.IsHermitian.spectral_theorem, eigenvectorBasis, eigenvectorUnitary_apply) and the repository's LF2.DensityOperator / traceForm / outerProduct / rankOneDensity. This closes #8 pieces A and B (the statistical/QM-adapter side); the ontic-side mixed representation on the unified model (#8 C) is separate.

References: SigmaLayer/MixedState.lean (mix, traceForm_mix, IsPure, maximallyMixed), LF2/BornWrapper.lean (DensityOperator, Effect, traceForm, outerProduct, rankOneDensity, born_quadratic); specs/future-work.md SL-T9.

A — finite ensembles (many-component mixtures)

noncomputable def CSD.SigmaLayer.ensemble {N : ℕ} {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hsum : ∑ i : ι, w i = 1) (ρ : ι → LF2.DensityOperator N) : LF2.DensityOperator N

A finite ensemble of density operators. For weights w : ι → ℝ forming a probability distribution (0 ≤ wᵢ, ∑ wᵢ = 1) and density operators ρ : ι → DensityOperator N, the convex combination ∑ᵢ wᵢ ρᵢ is a density operator: the classical mixture of arbitrarily many preparations. The many-component generalisation of mix.

Equations

• CSD.SigmaLayer.ensemble w hw hsum ρ = { M := ∑ i : ι, ↑(w i) • (ρ i).M, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.SigmaLayer.ensemble_M {N : ℕ} {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hsum : ∑ i : ι, w i = 1) (ρ : ι → LF2.DensityOperator N) : (ensemble w hw hsum ρ).M = ∑ i : ι, ↑(w i) • (ρ i).M

theorem CSD.SigmaLayer.traceForm_ensemble {N : ℕ} {ι : Type u_1} [Fintype ι] (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) (hsum : ∑ i : ι, w i = 1) (ρ : ι → LF2.DensityOperator N) (E : LF2.Effect N) : LF2.traceForm (ensemble w hw hsum ρ) E = ∑ i : ι, w i * LF2.traceForm (ρ i) E

The Born rule is affine over the whole ensemble. Mixing arbitrarily many preparations mixes the outcome probabilities: Tr((∑ᵢ wᵢ ρᵢ) E) = ∑ᵢ wᵢ Tr(ρᵢ E). The many-component traceForm_mix.

B — the spectral ensemble decomposition (mixed = ensemble of pure)

theorem CSD.SigmaLayer.density_eq_eigen_ensemble {N : ℕ} (ρ : LF2.DensityOperator N) : ρ.M = ∑ i : Fin N, ↑(⋯.eigenvalues i) • LF2.outerProduct (⋯.eigenvectorBasis i)

Every density operator is the eigenvalue-weighted sum of its eigenvector projectors. ρ = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| (λᵢ the eigenvalues, eᵢ the orthonormal eigenvectors). The matrix core of the spectral ensemble decomposition, from the Hermitian spectral theorem.

theorem CSD.SigmaLayer.eigenvalues_isProbability {N : ℕ} (ρ : LF2.DensityOperator N) : (∀ (i : Fin N), 0 ≤ ⋯.eigenvalues i) ∧ ∑ i : Fin N, ⋯.eigenvalues i = 1

The eigenvalues of a density operator form a probability distribution: each is ≥ 0 and they sum to 1 (nonnegativity from PSD, sum from trace one). So the spectral decomposition is a genuine convex ensemble.

theorem CSD.SigmaLayer.eigenvectorBasis_norm_one {N : ℕ} (ρ : LF2.DensityOperator N) (i : Fin N) : ‖⋯.eigenvectorBasis i‖ = 1

The eigenvectors of a density operator are unit vectors (an orthonormal basis).

theorem CSD.SigmaLayer.density_isPureEnsemble {N : ℕ} (ρ : LF2.DensityOperator N) : ∃ (w : Fin N → ℝ) (e : Fin N → EuclideanSpace ℂ (Fin N)), (∀ (i : Fin N), 0 ≤ w i) ∧ ∑ i : Fin N, w i = 1 ∧ (∀ (i : Fin N), ‖e i‖ = 1) ∧ ρ.M = ∑ i : Fin N, ↑(w i) • LF2.outerProduct (e i)

Every density operator is a convex ensemble of pure states. There is a probability distribution w and unit vectors e with ρ = ∑ᵢ wᵢ |eᵢ⟩⟨eᵢ| — the eigenvalues and eigenvectors. The precise sense in which a mixed state is a classical mixture of pure preparations.

theorem CSD.SigmaLayer.traceForm_eq_pureEnsemble {N : ℕ} (ρ : LF2.DensityOperator N) (E : LF2.Effect N) : LF2.traceForm ρ E = ∑ i : Fin N, ⋯.eigenvalues i * LF2.traceForm (LF2.rankOneDensity (⋯.eigenvectorBasis i) ⋯) E

The Born rule of a mixed state is the eigenvalue-weighted average of the pure Born rules. For any effect E, Tr(ρ E) = ∑ᵢ λᵢ Tr(|eᵢ⟩⟨eᵢ| E) — measuring E on the mixture ρ gives the classical average, over the eigen-ensemble, of measuring E on each pure eigenstate. Combines the spectral decomposition (B) with the affine Born rule (A).

theorem CSD.SigmaLayer.mixedEnsemble_capstone {N : ℕ} (ρ : LF2.DensityOperator N) (E : LF2.Effect N) : LF2.traceForm ρ E = ∑ i : Fin N, ⋯.eigenvalues i * LF2.traceForm (LF2.rankOneDensity (⋯.eigenvectorBasis i) ⋯) E

#8 A+B capstone: the mixed-state ensemble representation. Finite convex ensembles of density operators are density operators with an affine Born rule (ensemble, traceForm_ensemble); conversely every density operator is a convex ensemble of pure states (density_isPureEnsemble), so its Born rule is the eigenvalue-weighted average of pure Born rules (traceForm_eq_pureEnsemble). The pure Born rule (born_quadratic) is the single-component extreme case.