SigmaLayer/MixedSwap: mixed preparations in the dynamical model

Category: dynamical measurement — the recorded "mixed preparations" extension of the swap closure.

A mixed preparation is, ontically, a two-stage sampling: draw a spectral index j with probability λⱼ (the eigenvalue), then prepare the pure eigenray [ψⱼ] and run the measurement dynamics unchanged. This module makes that the definition —

mixedSwapPrep ρ = ∑ⱼ λⱼ • swapPrep [ψⱼ]

— a probability measure on the swap arena because the eigenvalues are a probability distribution (eigenvalues_isProbability), and derives the mixed dynamical Born rule:

★ mixed_swap_sector_born — the mixed preparation's mass on the outcome sector of the measurement protocol is exactly the density-operator Born probability:

mixedSwapPrep ρ (outcomeSector i) = Tr(ρ |eᵢ⟩⟨eᵢ|).

The dynamics is untouched: the same propagator, the same sectors, the same protocol. What mixing adds is classical ignorance of the preparation, and the theorem says the dynamical outcome statistics respond exactly as Tr(ρ ·) demands — the spectral bridge is spectral_born_eq_traceForm, composing the ontic sector weights (swap_sector_born, one per eigenray) with the affine Born rule of the spectral ensemble (traceForm_eq_pureEnsemble).

⚠️ Honest scope. Record creation, exclusivity, persistence, and no-record-when-ready are per-protocol facts independent of the preparation — they hold under mixedSwapPrep verbatim and are not restated. The i.i.d. frequency layer consumes a probability measure and an event and applies as everywhere (arena_mixed_born_frequency is the two-stage LLN precedent on the unified arena). The conditional post-measurement analysis of a mixture — Bayes-updating the ensemble weights on the outcome and composing with the rank-one Lüders posts — is a recorded extension, not claimed here delivered 2026-08-03: SigmaLayer/MixedLuders.lean (mixed_post_bayes, mixed_luders_followup). The spectral decomposition is the canonical ensemble; the mixture realisation is of course not unique (density_isPureEnsemble states existence, not uniqueness), and nothing here depends on the choice.

References

specs/BACKLOG.md (the mixed-preparations row — this discharges it); SigmaLayer/SwapClosure.lean (swapPrep, swap_sector_born), SigmaLayer/MixedEnsemble.lean (eigenvalues_isProbability, traceForm_eq_pureEnsemble), SigmaLayer/MixedOntic.lean (the kinematic counterpart, mixed_ontic_born_weight), LF2/BornWrapper.lean (born_quadratic, rankOneEffect).

theorem CSD.RecordLayer.single_norm_one' {N : ℕ} (i : Fin N) : ‖EuclideanSpace.single i 1‖ = 1

Unit standard-basis vectors, at every dimension.

theorem CSD.RecordLayer.eigenvectorBasis_ne_zero' {N : ℕ} (ρ : LF2.DensityOperator N) (j : Fin N) : ⋯.eigenvectorBasis j ≠ 0

The eigenvectors of a density operator are nonzero, at every dimension.

noncomputable def CSD.RecordLayer.eigRay {N : ℕ} (ρ : LF2.DensityOperator N) (j : Fin N) : LF4.CPN N

The j-th spectral eigenray of a density operator.

Equations

• CSD.RecordLayer.eigRay ρ j = Projectivization.mk ℂ (⋯.eigenvectorBasis j) ⋯

noncomputable def CSD.RecordLayer.mixedSwapPrep {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) : MeasureTheory.Measure (SwapArena (LF4.KSigma N) N)

The mixed preparation: the eigenvalue-weighted mixture of the pure swap preparations at the spectral eigenrays — two-stage sampling as a measure.

Equations

• CSD.RecordLayer.mixedSwapPrep ρ = ∑ j : Fin N, ENNReal.ofReal (⋯.eigenvalues j) • CSD.RecordLayer.swapPrep (CSD.RecordLayer.eigRay ρ j)

instance CSD.RecordLayer.instIsProbabilityMeasureSwapArenaKSigmaMixedSwapPrep {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) : MeasureTheory.IsProbabilityMeasure (mixedSwapPrep ρ)

theorem CSD.RecordLayer.spectral_born_eq_traceForm {N : ℕ} (ρ : LF2.DensityOperator N) (i : Fin N) : ∑ j : Fin N, ⋯.eigenvalues j * LF4.momentMap (eigRay ρ j) i = LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯)

The spectral bridge: the eigenvalue-weighted moment-map weights of the eigenrays are the density-operator Born probability.

theorem CSD.RecordLayer.mixed_swap_sector_born {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (i : Fin N) : (mixedSwapPrep ρ) ((swapProtocol (basinIndex (momentContext N)) ⋯).outcomeSector i) = ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯))

★ The mixed dynamical Born rule: the mixed preparation's mass on the measurement protocol's outcome sector is exactly Tr(ρ |eᵢ⟩⟨eᵢ|) — the same propagator, the same sectors, with classical ignorance of the preparation responding precisely as the density-operator Born rule demands.