LF2: Mixed-state Born rule and spectral ensemble on the indexed density type

Category: 3-Local (the operational density-operator layer).

The mixed-state ensemble content (SigmaLayer/MixedEnsemble.lean) was proved for DensityOperator N (indexed by Fin N). This module ports it to the composite index-parametric density type DensityOperatorIx ι (LF2/ReducedDensity.lean, indexed by an arbitrary [Fintype ι] [DecidableEq ι]) — the type the bipartite / composite interface (SigmaLayer/CompositeInterface.lean, target T9) uses via reduced / reducedLeft partial traces. This closes the reported density-matrix gap: mixed-state Born on the composite indexed type, not only on Fin N.

Main results

• DensityOperatorIx.traceForm : the Born pairing Tr(ρ E) on the indexed type.
• DensityOperatorIx.ensemble + traceForm_ensemble : finite convex ensembles of indexed densities are indexed densities, with an affine Born rule.
• DensityOperatorIx.eq_eigen_ensemble + eigenvalues_isProbability : every indexed density is ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| for a probability distribution λ (spectral theorem).
• DensityOperatorIx.mixedEnsemble_capstone : the mixed Born rule is the eigenvalue-weighted average of the pure Born rules — on the composite indexed type.

The proofs are the faithful ι-generalisation of the Fin N originals; every underlying lemma (Matrix.posSemidef_sum, the Hermitian spectral theorem, trace_eq_sum_eigenvalues, eigenvalues_nonneg) is stated for a general Fintype index.

noncomputable def CSD.LF2.DensityOperatorIx.traceForm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) (E : Matrix ι ι ℂ) : ℝ

Born pairing on the indexed density type. Tr(ρ E) as a real number.

Equations

• ρ.traceForm E = RCLike.re (ρ.M * E).trace

A — the affine convex ensemble

noncomputable def CSD.LF2.DensityOperatorIx.ensemble {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] (w : κ → ℝ) (hw : ∀ (k : κ), 0 ≤ w k) (hsum : ∑ k : κ, w k = 1) (ρ : κ → DensityOperatorIx ι) : DensityOperatorIx ι

Finite convex ensemble of indexed densities. For a probability distribution w and indexed densities ρ : κ → DensityOperatorIx ι, the convex combination ∑ₖ wₖ ρₖ is an indexed density.

Equations

• CSD.LF2.DensityOperatorIx.ensemble w hw hsum ρ = { M := ∑ k : κ, ↑(w k) • (ρ k).M, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.LF2.DensityOperatorIx.ensemble_M {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] (w : κ → ℝ) (hw : ∀ (k : κ), 0 ≤ w k) (hsum : ∑ k : κ, w k = 1) (ρ : κ → DensityOperatorIx ι) : (ensemble w hw hsum ρ).M = ∑ k : κ, ↑(w k) • (ρ k).M

theorem CSD.LF2.DensityOperatorIx.traceForm_ensemble {ι : Type u_1} [Fintype ι] [DecidableEq ι] {κ : Type u_2} [Fintype κ] (w : κ → ℝ) (hw : ∀ (k : κ), 0 ≤ w k) (hsum : ∑ k : κ, w k = 1) (ρ : κ → DensityOperatorIx ι) (E : Matrix ι ι ℂ) : (ensemble w hw hsum ρ).traceForm E = ∑ k : κ, w k * (ρ k).traceForm E

The Born rule is affine over the ensemble (indexed type): mixing preparations mixes the outcome probabilities, Tr((∑ₖ wₖ ρₖ) E) = ∑ₖ wₖ Tr(ρₖ E).

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

noncomputable def CSD.LF2.DensityOperatorIx.rankOne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) : DensityOperatorIx ι

Rank-one (pure) indexed density |ψ⟩⟨ψ| for a unit vector ψ — the DensityOperatorIx twin of rankOneDensity, on the shared outerProduct (LF2/BornWrapper.lean).

Equations

• CSD.LF2.DensityOperatorIx.rankOne ψ hψ = { M := CSD.LF2.outerProduct ψ, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.LF2.DensityOperatorIx.rankOne_M {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) : (rankOne ψ hψ).M = outerProduct ψ

theorem CSD.LF2.DensityOperatorIx.traceForm_rankOne_outerProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ φ : EuclideanSpace ℂ ι) (hψ : ‖ψ‖ = 1) : (rankOne ψ hψ).traceForm (outerProduct φ) = ‖inner ℂ ψ φ‖ ^ 2

The Born quadratic form on the indexed type: at a pure preparation |ψ⟩⟨ψ| the trace form of a rank-one projector |φ⟩⟨φ| is |⟨ψ, φ⟩|² — the DensityOperatorIx twin of born_quadratic, from the shared matrix core outerProduct_mul_outerProduct_trace.

theorem CSD.LF2.DensityOperatorIx.eq_eigen_ensemble {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) : ρ.M = ∑ i : ι, ↑(⋯.eigenvalues i) • outerProduct (⋯.eigenvectorBasis i)

Every indexed density is the eigenvalue-weighted sum of its eigenvector projectors: ρ = ∑ᵢ λᵢ |eᵢ⟩⟨eᵢ| — the DensityOperatorIx instance of IsHermitian.eq_eigen_outer (the Hermitian spectral theorem, expanded entrywise).

theorem CSD.LF2.DensityOperatorIx.eigenvalues_isProbability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) : (∀ (i : ι), 0 ≤ ⋯.eigenvalues i) ∧ ∑ i : ι, ⋯.eigenvalues i = 1

The eigenvalues of an indexed density form a probability distribution.

theorem CSD.LF2.DensityOperatorIx.mixedEnsemble_capstone {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ρ : DensityOperatorIx ι) (E : Matrix ι ι ℂ) : ρ.traceForm E = ∑ i : ι, ⋯.eigenvalues i * RCLike.re (outerProduct (⋯.eigenvectorBasis i) * E).trace

The mixed Born rule is the eigenvalue-weighted average of the pure Born rules (composite indexed type): Tr(ρ E) = ∑ᵢ λᵢ Tr(|eᵢ⟩⟨eᵢ| E). Combines the spectral decomposition with the affine Born rule — closing T9 on DensityOperatorIx.