SigmaLayer/MixedLuders: the outcome-conditioned mixed update

Category: dynamical measurement — MixedSwap.lean's recorded extension, delivered (the fourth external review's "mixed conditioned update" row).

Two theorems close the row:

★ mixed_post_bayes — the outcome-conditioned post-measurement ensemble of a mixed preparation is the Bayes-posterior mixture of the per-eigenray post-ensembles: the posterior weight of spectral component j after outcome i is λⱼ · pᵢ|ⱼ / Tr(ρ|eᵢ⟩⟨eᵢ|) with likelihood pᵢ|ⱼ = momentMap [ψⱼ] i — classical Bayes updating of classical ignorance, as a theorem about the protocol's postMeasure. The engine is the new staged ProbabilityTheory.cond_finsetSum (Bayes for finite mixtures).

★★ mixed_luders_followup — the record, not the pedigree, fixes the post-state: after outcome i on the mixed preparation, follow-up statistics in every context are c'.rate [eᵢ] — exactly the pure preparation's rank-one Lüders update. At rank one the posterior components all collapse to the same vertex state, so classical ignorance of the preparation is erased by the record: the conditioned mixture behaves as a fresh preparation of eᵢ. This is the density-operator update ρ ↦ Πᵢ ρ Πᵢ / Tr(ρ Πᵢ) at rank one, dynamically.

The spine: mixedSwapPrep factors — the mixture lives entirely on the system-and- register factor, with the calibrated bank common (mixedSwapPrep_eq_prod), so the pure theorem swap_luders_born (already stated for an arbitrary probability preparation) applies verbatim once the outcome has nonzero mixed Born weight (mixed_outcome_pos, licensed by Tr(ρ|eᵢ⟩⟨eᵢ|) ≠ 0 through the spectral bridge — no measure hypothesis).

⚠️ Honest scope. Degenerate outcomes on mixtures (block-Lüders composed with Bayes) would ride JoinClosure the same way and are not restated delivered 2026-08-06 (SigmaLayer/MixedJoinLuders.lean, BACKLOG D3 first half): it rides JoinClosure exactly as predicted, and at rank ≥ 2 the posterior components are proven genuinely distinct — mixed_join_luders exhibits the conditioned mixture as the Bayes mixture of the per-component block posts epistemicMeasure [Πᵢψⱼ], nothing collapsing to a vertex. The spectral ensemble is the canonical mixture realisation; nothing here depends on the choice (MixedSwap.lean).

References

specs/BACKLOG.md (the outcome-conditioned mixed update row — this discharges it; fourth external review 2026-08-03); SigmaLayer/MixedSwap.lean (mixedSwapPrep, eigRay, spectral_born_eq_traceForm, mixed_swap_sector_born), SigmaLayer/SwapClosure.lean (swapPrep, readyPrep, calibratedBank, prep_outcome_pos, swap_sector_born), SigmaLayer/SwapLuders.lean (swap_luders_born), CsdLean4/Mathlib/Probability/ConditionalProbability.lean (cond_finsetSum).

The mixture factors through the bank

noncomputable def CSD.RecordLayer.mixedReadyPrep {N : ℕ} (ρ : LF2.DensityOperator N) : MeasureTheory.Measure (LF4.KSigma N × LF4.KTorus)

The mixed system-and-register preparation: the eigenvalue mixture of the pure ready preparations — the bank is not part of the ignorance.

Equations

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

instance CSD.RecordLayer.instIsProbabilityMeasureProdKSigmaKTorusMixedReadyPrep {N : ℕ} (ρ : LF2.DensityOperator N) : MeasureTheory.IsProbabilityMeasure (mixedReadyPrep ρ)

theorem CSD.RecordLayer.mixedSwapPrep_eq_prod {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) : mixedSwapPrep ρ = (mixedReadyPrep ρ).prod (calibratedBank N)

The mixed preparation factors: the mixture lives on the system-and-register factor, with the calibrated bank common to every spectral component. This is what lets every pure-preparation theorem stated for an arbitrary μ12 apply to mixtures verbatim.

theorem CSD.RecordLayer.mixed_outcome_pos {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (i : Fin N) (hpos : LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯) ≠ 0) : (mixedReadyPrep ρ) ((shearProtocol (basinIndex (momentContext N)) ⋯).outcomeSector i) ≠ 0

hpos is a theorem for mixtures: nonzero mixed Born weight Tr(ρ|eᵢ⟩⟨eᵢ|) ≠ 0 gives the outcome sector nonzero mixed measure — through the spectral bridge, some component has both nonzero eigenvalue and nonzero pure Born weight, and prep_outcome_pos does the rest.

★ The Bayes-posterior ensemble

theorem CSD.RecordLayer.mixed_post_bayes {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (i : Fin N) : (swapProtocol (basinIndex (momentContext N)) ⋯).postMeasure (mixedSwapPrep ρ) i = ∑ j : Fin N, (ENNReal.ofReal (⋯.eigenvalues j * LF4.momentMap (eigRay ρ j) i) / ENNReal.ofReal (LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯))) • (swapProtocol (basinIndex (momentContext N)) ⋯).postMeasure (swapPrep (eigRay ρ j)) i

★ The outcome-conditioned mixed post-measurement ensemble is the Bayes-posterior mixture: after outcome i, spectral component j carries posterior weight λⱼ · pᵢ|ⱼ / Tr(ρ|eᵢ⟩⟨eᵢ|) — prior times likelihood over evidence — and the ensemble is that mixture of the per-eigenray post-ensembles. Classical Bayes updating of the classical ignorance, as a theorem about the protocol.

★★ The record fixes the post-state

theorem CSD.RecordLayer.mixed_luders_followup {N : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (i : Fin N) (hpos : LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single i 1) ⋯) ≠ 0) (c' : ContextField N) (j : Fin N) : ((swapProtocol (basinIndex (momentContext N)) ⋯).postMeasure (mixedSwapPrep ρ) i) ((fun (y : SwapArena (LF4.KSigma N) N) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (vertexPoint i) j)

★★ The record, not the pedigree, fixes the post-state: after outcome i on the mixed preparation, follow-up statistics in every context are exactly the pure rank-one Lüders update's — c'.rate [eᵢ]. At rank one every Bayes-posterior component collapses to the same vertex state, so the record erases the classical ignorance of the preparation: the conditioned mixture is dynamically indistinguishable from a fresh preparation of eᵢ. The density-operator update ρ ↦ Πᵢ ρ Πᵢ / Tr(ρ Πᵢ) at rank one.