SigmaLayer/MixedFrequency: the mixed-state Born FREQUENCY on the unified model (#8 C, a.s. limit)

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

FiniteQMClosure.mixed_born (mixed_ontic_born_weight) delivers the mixed Born content at the WEIGHT level: the spectral-ensemble mixture of ontic Born-region measures equals Tr(ρ Eᵢ). This module upgrades it to a genuine almost-sure FREQUENCY limit — a two-stage sampling process: each shot draws a spectral component j of ρ with probability λⱼ (its eigenvalue), then an ontic microstate from the unified model's Liouville measure μL; the outcome is the pointer readout for the drawn component's eigenvector. The frequency of outcome i over the trials converges a.s. to Tr(ρ Eᵢ).

• eigenvalueMeasure ρ — the eigenvalue probability distribution as a measure on the component index;
• mixtureMeasure — the two-stage law eigenvalueMeasure ⊗ μL on Fin(M+1) × Σ;
• mixtureRegion ρ i — the outcome-i region ⋃ⱼ {j} × π⁻¹(bornRegion(eⱼ) i);
• mixtureMeasure_region_toReal — μmix(mixtureRegion i) = Tr(ρ Eᵢ) (the two-stage region measure IS the density-operator Born weight, via mixed_ontic_born_weight);
• unified_mixed_born_frequency — the a.s. frequency limit, by born_frequency_convergence_partition.

So the unified model carries mixed-state Born statistics as certified FREQUENCIES, not only as weights — closing the last open QM item in FiniteQMClosure (its Tier-4 "mixed-state frequency LLN").

References: SigmaLayer/MixedOntic.lean (mixed_ontic_born_weight), SigmaLayer/MixedEnsemble.lean (eigenvalues_isProbability), LF4/BornFrequencyPartition.lean (the general partition LLN).

noncomputable def CSD.SigmaLayer.eigRegion {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) (j i : Fin (M + 1)) : Set (LF4.KSigma (M + 1))

The single-outcome ontic Born region of ρ's j-th eigenvector, pulled back through π.

Equations

• CSD.SigmaLayer.eigRegion H hH p₀ ρ j i = (CSD.SigmaLayer.productSector H hH p₀).pi ⁻¹' CSD.LF4.bornRegion (⋯.eigenvectorBasis j) ⋯ i

theorem CSD.SigmaLayer.eigRegion_measurable {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) (j i : Fin (M + 1)) : MeasurableSet (eigRegion H hH p₀ ρ j i)

noncomputable def CSD.SigmaLayer.eigenvalueMeasure {M : ℕ} (ρ : LF2.DensityOperator (M + 1)) : MeasureTheory.Measure (Fin (M + 1))

The eigenvalue distribution as a probability measure on the component index Fin (M+1): ∑ⱼ λⱼ · δⱼ.

Equations

• CSD.SigmaLayer.eigenvalueMeasure ρ = ∑ j : Fin (M + 1), ENNReal.ofReal (⋯.eigenvalues j) • MeasureTheory.Measure.dirac j

theorem CSD.SigmaLayer.eigenvalueMeasure_singleton {M : ℕ} (ρ : LF2.DensityOperator (M + 1)) (k : Fin (M + 1)) : (eigenvalueMeasure ρ) {k} = ENNReal.ofReal (⋯.eigenvalues k)

instance CSD.SigmaLayer.eigenvalueMeasure_isProbability {M : ℕ} (ρ : LF2.DensityOperator (M + 1)) : MeasureTheory.IsProbabilityMeasure (eigenvalueMeasure ρ)

noncomputable def CSD.SigmaLayer.mixtureMeasure {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) : MeasureTheory.Measure (Fin (M + 1) × LF4.KSigma (M + 1))

The two-stage mixture measure on Fin(M+1) × Σ: draw a spectral component ~ λ, then an ontic microstate ~ μL.

Equations

• CSD.SigmaLayer.mixtureMeasure H hH p₀ ρ = (CSD.SigmaLayer.eigenvalueMeasure ρ).prod ↑(CSD.SigmaLayer.productDynamics H hH p₀).muL

def CSD.SigmaLayer.mixtureRegion {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)) : Set (Fin (M + 1) × LF4.KSigma (M + 1))

The mixed outcome-i region: component j's eigenvector lands in the i-th ontic Born region.

Equations

• CSD.SigmaLayer.mixtureRegion H hH p₀ ρ i = ⋃ (j : Fin (M + 1)), {j} ×ˢ CSD.SigmaLayer.eigRegion H hH p₀ ρ j i

theorem CSD.SigmaLayer.mixtureRegion_measurable {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)) : MeasurableSet (mixtureRegion H hH p₀ ρ i)

theorem CSD.SigmaLayer.mixtureMeasure_region_toReal {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)) : ((mixtureMeasure H hH p₀ ρ) (mixtureRegion H hH p₀ ρ i)).toReal = LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)

The two-stage region measure IS the density-operator Born weight. μmix(mixtureRegion i).toReal = Tr(ρ Eᵢ). The mixture measure of the disjoint rectangle union is ∑ⱼ λⱼ · μL(eigRegion j i), which is the mixed_ontic_born_weight sum.

theorem CSD.SigmaLayer.unified_mixed_born_frequency {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ρ : LF2.DensityOperator (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (Y : ℕ → Ω → Fin (M + 1) × LF4.KSigma (M + 1)) (hY : ∀ (n : ℕ), Measurable (Y n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (Y n) Pr = mixtureMeasure H hH p₀ ρ) (hindep : ∀ (i : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (Y n ⁻¹' mixtureRegion H hH p₀ ρ i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin (M + 1)), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (Y k ⁻¹' mixtureRegion H hH p₀ ρ i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)))

Mixed-state Born FREQUENCY on the unified model (#8 C, a.s. limit). For i.i.d. two-stage trials Y (draw a spectral component of ρ ~ λ, then an ontic microstate ~ μL) whose law is mixtureMeasure, the frequency of outcome i — the drawn component's eigenvector landing in the i-th ontic Born region — converges almost surely to the density-operator Born weight Tr(ρ Eᵢ). So the unified model productDynamics H hH p₀ carries mixed-state Born statistics as certified frequencies, not only weights.