LF4 §14 states obligation: mixed states / density operators as ontic eigen-mixtures

Category: 3-Local (LF4 §14 discharge — the density-operator / mixed-state case of the states obligation).

This module discharges the mixed-state part of the §14 states obligation, completing the states-side realisation begun for pure states / rank-one projectors in LF4/ObservableCorrespondenceN.lean (pure_state_born_prob_eq_volume).

A density operator ρ is realised as an ontic eigen-mixture: its Born probability Tr(ρ · |φ⟩⟨φ|) of a projective outcome |φ⟩ is the ρ-eigenvalue-weighted sum of the ontic Fubini–Study volumes of ρ's pure eigenstates (mixed_state_born_eq_ensemble_volume). This composes three existing pieces:

• the spectral ensemble Tr(ρ · E) = ∑ᵢ λᵢ · Tr(|eᵢ⟩⟨eᵢ| · E) (SigmaLayer.mixedEnsemble_capstone);
• the pure Born rule Tr(|eᵢ⟩⟨eᵢ| · |φ⟩⟨φ|) = ‖⟨eᵢ, φ⟩‖² (LF2.born_quadratic);
• the pure-state ontic realisation ‖⟨φ, eᵢ⟩‖² = vol(bornRegionN (Wᴴ eᵢ) 0) (LF4.pure_state_born_prob_eq_volume), with W a unitary sending e₀ ↦ φ.

Genericity hpos is on each transported eigenvector Wᴴ eᵢ (i.e. the outcome φ overlaps every eigenvector of ρ). This realises the density operator (mixed state) as an ontic object — the state-side content underlying the resource bundle NoBroadcasting (a bipartite ρ confined to a pure marginal). Foundational triple; carving-free, Gleason-free.

References: LF4/ObservableCorrespondenceN.lean (pure_state_born_prob_eq_volume, bornRegionN); SigmaLayer/MixedEnsemble.lean (mixedEnsemble_capstone, eigenvectorBasis_norm_one); LF2/BornWrapper.lean (born_quadratic, rankOneEffect, traceForm); specs/LF4-todo.md §14; BRIDGE-OBLIGATIONS.md (the §14 states bundle fields).

theorem CSD.LF4.mixed_state_born_eq_ensemble_volume {M : ℕ} (p₀ : CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) (φ : EuclideanSpace ℂ (Fin (M + 1))) (hφ : ‖φ‖ = 1) (W : ↥(Matrix.unitaryGroup (Fin (M + 1)) ℂ)) (hW : (Matrix.toEuclideanLin ↑W) (EuclideanSpace.single 0 1) = φ) (hφ0 : ∀ (i : Fin (M + 1)), (Matrix.toEuclideanLin (star ↑W)) (⋯.eigenvectorBasis i) ≠ 0) (hpos : ∀ (i j : Fin (M + 1)), 0 < ‖inner ℂ (EuclideanSpace.single j 1) ((Matrix.toEuclideanLin (star ↑W)) (⋯.eigenvectorBasis i))‖ ^ 2) : LF2.traceForm ρ (LF2.rankOneEffect φ hφ) = ∑ i : Fin (M + 1), ⋯.eigenvalues i * ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (bornRegionN ((Matrix.toEuclideanLin (star ↑W)) (⋯.eigenvectorBasis i)) ⋯ 0)).toReal

§14 states obligation — the mixed-state / density-operator case. A density operator ρ is realised as an ontic eigen-mixture: the Born probability Tr(ρ · |φ⟩⟨φ|) of a projective outcome |φ⟩ is the ρ-eigenvalue-weighted sum of the ontic Fubini–Study volumes of ρ's pure eigenstates. Composes the spectral ensemble (mixedEnsemble_capstone), the pure Born rule (born_quadratic), and the pure-state realisation (pure_state_born_prob_eq_volume). Genericity hpos is on each transported eigenvector Wᴴ eᵢ. Foundational triple.

This realises the density operator (mixed state) as an ontic object — the state-side content underlying NoBroadcasting (a bipartite ρ confined to a pure marginal).