SigmaLayer/MixedOntic: the ontic-side mixed-state representation on the unified model (#8 C)

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

FiniteQMClosure carries the Born content for PURE states only (born_frequency for a single ψ). This module represents a MIXED state on the SAME ontic model productDynamics H hH p₀ as a classical mixture over ontic pure-preparations, and proves that the mixture reproduces the density-operator Born rule.

The state enters the ontic model only through the pointer/outcome structure (the ψ-dependent Born region), not through the Liouville law μL (which is fixed). So a mixed state ρ is represented by classical randomness over WHICH pure component ψⱼ = eⱼ (eigenvector) is in effect, weighted by the eigenvalues λⱼ — the spectral ensemble of SigmaLayer/MixedEnsemble.lean (density_isPureEnsemble). The resulting mixed Born WEIGHT for pointer outcome i is

∑ⱼ λⱼ · μL(π⁻¹ bornRegion(eⱼ) i) (classical mixture of ontic Born-region measures)

and mixed_ontic_born_weight proves this equals Tr(ρ Eᵢ) (traceForm ρ (rankOneEffect eᵢ)) — the density-operator Born probability of the standard-basis outcome i. So the unified model represents mixed states, not only pure ones: mixing ontic pure-preparations by the spectral weights gives EXACTLY the Born rule of ρ.

This is stated at the WEIGHT (probability) level — the same granularity as the conditioning=Lüders correspondence (conditioning_luders_effect_equivalence), which is also a weight/ratio statement rather than an LLN. A genuine mixed-state frequency LLN (redrawing the component each shot on a two-stage mixture space) is the remaining refinement of #8 C.

Proof = the ontic weight agreement onticRegion_measure_eq_born (SigmaLayer/ConditioningLuders.lean, μL(π⁻¹ bornRegion ψ i) = ‖⟨eᵢ,ψ⟩‖²) composed with the spectral affine Born rule traceForm_eq_pureEnsemble (SigmaLayer/MixedEnsemble.lean) and the pure Born quadratic form born_quadratic (LF2/BornWrapper.lean), matched up by conjugate symmetry of the inner product.

References: SigmaLayer/ConditioningLuders.lean (onticRegion_measure_eq_born), SigmaLayer/MixedEnsemble.lean (traceForm_eq_pureEnsemble, eigenvectorBasis_norm_one, density_isPureEnsemble), LF2/BornWrapper.lean (traceForm, rankOneEffect, born_quadratic); specs/future-work.md SL-T9.

theorem CSD.SigmaLayer.eigenvectorBasis_ne_zero {M : ℕ} (ρ : LF2.DensityOperator (M + 1)) (j : Fin (M + 1)) : ⋯.eigenvectorBasis j ≠ 0

The eigenvectors of a density operator are nonzero (they are unit vectors).

theorem CSD.SigmaLayer.single_norm_one {M : ℕ} (i : Fin (M + 1)) : ‖EuclideanSpace.single i 1‖ = 1

The standard basis vector eᵢ has unit norm.

theorem CSD.SigmaLayer.mixed_ontic_born_weight {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) (i : Fin (M + 1)) : ∑ j : Fin (M + 1), ⋯.eigenvalues j * (↑(productDynamics H hH p₀).muL ((productSector H hH p₀).pi ⁻¹' LF4.bornRegion (⋯.eigenvectorBasis j) ⋯ i)).toReal = LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)

The ontic mixed-state Born weight (#8 C). For any density operator ρ and pointer outcome i, the classical mixture — over ρ's spectral ensemble (λⱼ, eⱼ) — of the ontic Born-region measures equals the density-operator Born probability Tr(ρ |eᵢ⟩⟨eᵢ|):

∑ⱼ λⱼ · μL(π⁻¹ bornRegion(eⱼ) i) = traceForm ρ (rankOneEffect eᵢ).

So the unified model productDynamics H hH p₀ represents mixed states: mixing its ontic pure-preparations by the spectral weights reproduces exactly the Born rule of ρ. Composes the ontic weight agreement onticRegion_measure_eq_born with the spectral affine Born rule traceForm_eq_pureEnsemble and the pure born_quadratic, matched by conjugate symmetry of the inner product.