SigmaLayer/MixedJoinLuders: degenerate outcomes on mixed preparations (D3, first half)

Category: dynamical measurement — specs/BACKLOG.md D3's first half: block Lüders composed with Bayes, the degenerate counterpart of MixedLuders.lean, riding JoinClosure exactly as that module's scope note predicted.

What is proved

• mixedJoinPrep — the eigenvalue-weighted mixture of the pure join preparations at the spectral eigenvectors: two-stage sampling on the join arena, same shape as mixedSwapPrep.
• ★ mixed_join_sector_born — the mixed block Born rule: the mixture's mass on the outcome-i sector is ∑_{k : b k = i} Tr(ρ|eₖ⟩⟨eₖ|) — the density-operator Born probability of the degenerate outcome, written as its rank-one sum. Spectral bridge: sum interchange + spectral_born_eq_traceForm, one rank-one bridge per block member.
• ★ mixed_join_post_bayes — conditioning the mixture on outcome i Bayes-updates the classical ignorance: component j's posterior weight is λⱼ · pᵢ|ⱼ / ∑ₖ…Tr(…) with likelihood pᵢ|ⱼ the block Born weight of eigenvector j. Same engine as the rank-one case (cond_finsetSum).
• ★★ mixed_join_luders — block Lüders composed with Bayes: the outcome-conditioned post-measurement system marginal of the mixture is the Bayes-posterior mixture of the per-component degenerate Lüders posts epistemicMeasure [Πᵢψⱼ]. At rank ≥ 2 the posterior components are genuinely distinct — the record does not erase the classical ignorance (contrast mixed_luders_followup, where at rank one every posterior collapses to the same vertex): what survives conditioning is precisely the density-operator update ρ ↦ Πᵢ ρ Πᵢ / Tr(ρ Πᵢ), realised as a mixture of the per-eigenvector block posts.

⚠️ Honest scope

• mixed_join_luders is stated under hproj : ∀ j, blockProj b i ψⱼ ≠ 0 — every spectral component meets block i. A component with Πᵢψⱼ = 0 has zero likelihood, hence zero Bayes weight, so nothing is lost — but its Lüders post [Πᵢψⱼ] does not exist as a ray, so the clean mixture statement needs the hypothesis. The refinement (sum over the components with nonzero block projection only) is bookkeeping over mixed_join_post_bayes and is deliberately left unstated rather than shipped as a weaker theorem wearing the same name.
• The spectral ensemble is the canonical mixture realisation; nothing depends on the choice (MixedSwap.lean). Per-protocol record facts hold under the mixture verbatim and are not restated (JoinClosure).

References

specs/BACKLOG.md D3; SigmaLayer/MixedLuders.lean (the rank-one model this transports, and whose scope note this discharges); SigmaLayer/MixedSwap.lean (eigRay, spectral_born_eq_traceForm); SigmaLayer/JoinClosure.lean (join_sector_born); SigmaLayer/JoinLuders.lean (joinPrep, joinPostMarg, joinWitness_blockLuders, sysRead); SigmaLayer/DegenerateLuders.lean (blockProj); Mathlib/Probability/ConditionalProbability.lean (cond_finsetSum).

noncomputable def CSD.RecordLayer.mixedJoinPrep {N K : ℕ} (ρ : LF2.DensityOperator N) (α : EuclideanSpace ℂ (Fin N)) : MeasureTheory.Measure (JoinSel N × LF4.KTorus)

The mixed join preparation: the eigenvalue-weighted mixture of the pure join preparations at the spectral eigenvectors — two-stage sampling on the join arena.

Equations

• CSD.RecordLayer.mixedJoinPrep ρ α = ∑ j : Fin N, ENNReal.ofReal (⋯.eigenvalues j) • CSD.RecordLayer.joinPrep (⋯.eigenvectorBasis j) α ⋯

instance CSD.RecordLayer.instIsProbabilityMeasureProdJoinSelKTorusMixedJoinPrep {N K : ℕ} (ρ : LF2.DensityOperator N) (α : EuclideanSpace ℂ (Fin N)) : MeasureTheory.IsProbabilityMeasure (mixedJoinPrep ρ α)

theorem CSD.RecordLayer.spectral_block_born_eq_traceForm {N K : ℕ} (ρ : LF2.DensityOperator N) (b : Fin N → Fin K) (i : Fin K) : ∑ j : Fin N, ⋯.eigenvalues j * ∑ k : Fin N with b k = i, ‖inner ℂ (EuclideanSpace.single k 1) (⋯.eigenvectorBasis j)‖ ^ 2 = ∑ k : Fin N with b k = i, LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single k 1) ⋯)

The block spectral bridge: the eigenvalue-weighted block Born weights of the eigenvectors are the block sum of density-operator Born probabilities — sum interchange plus one rank-one spectral bridge per block member.

theorem CSD.RecordLayer.mixed_join_sector_born {N K : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (b : Fin N → Fin K) (α : EuclideanSpace ℂ (Fin N)) (i : Fin K) : (mixedJoinPrep ρ α) ((joinProtocol b).outcomeSector i) = ENNReal.ofReal (∑ k : Fin N with b k = i, LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single k 1) ⋯))

★ The mixed block Born rule: the mixture's mass on the degenerate outcome-i sector is the block sum ∑_{k : b k = i} Tr(ρ|eₖ⟩⟨eₖ|) — the density-operator Born probability of the coarse outcome, dynamically. Calibration-independent, as for the pure case.

theorem CSD.RecordLayer.mixed_join_post_bayes {N K : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (b : Fin N → Fin K) (α : EuclideanSpace ℂ (Fin N)) (i : Fin K) : (joinProtocol b).postMeasure (mixedJoinPrep ρ α) i = ∑ j : Fin N, (ENNReal.ofReal (⋯.eigenvalues j * ∑ k : Fin N with b k = i, ‖inner ℂ (EuclideanSpace.single k 1) (⋯.eigenvectorBasis j)‖ ^ 2) / ENNReal.ofReal (∑ k : Fin N with b k = i, LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single k 1) ⋯))) • (joinProtocol b).postMeasure (joinPrep (⋯.eigenvectorBasis j) α ⋯) i

★ Bayes updating on a degenerate outcome: the outcome-conditioned post-measurement ensemble of the mixed join preparation is the Bayes-posterior mixture of the per-component post-ensembles — posterior weight λⱼ · pᵢ|ⱼ / ∑ₖ Tr(ρ|eₖ⟩⟨eₖ|) with likelihood pᵢ|ⱼ the block Born weight of eigenvector j.

noncomputable def CSD.RecordLayer.mixedJoinPostMarg {N K : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (b : Fin N → Fin K) (α : Fin K → EuclideanSpace ℂ (Fin N)) (i : Fin K) : MeasureTheory.Measure (LF4.KSigma N)

The outcome-conditioned post-measurement system marginal of the mixed join preparation — joinPostMarg's mixture counterpart, with the outcome-i calibration.

Equations

• CSD.RecordLayer.mixedJoinPostMarg ρ b α i = MeasureTheory.Measure.map CSD.RecordLayer.sysRead ((CSD.RecordLayer.joinProtocol b).postMeasure (CSD.RecordLayer.mixedJoinPrep ρ (α i)) i)

theorem CSD.RecordLayer.mixed_join_luders {N K : ℕ} [NeZero N] (ρ : LF2.DensityOperator N) (b : Fin N → Fin K) (α : Fin K → EuclideanSpace ℂ (Fin N)) (hα : ∀ (i : Fin K), (blockProj b i) (α i) = α i) (i : Fin K) (hproj : ∀ (j : Fin N), (blockProj b i) (⋯.eigenvectorBasis j) ≠ 0) : mixedJoinPostMarg ρ b α i = ∑ j : Fin N, (ENNReal.ofReal (⋯.eigenvalues j * ∑ k : Fin N with b k = i, ‖inner ℂ (EuclideanSpace.single k 1) (⋯.eigenvectorBasis j)‖ ^ 2) / ENNReal.ofReal (∑ k : Fin N with b k = i, LF2.traceForm ρ (LF2.rankOneEffect (EuclideanSpace.single k 1) ⋯))) • epistemicMeasure (Projectivization.mk ℂ ((blockProj b i) (⋯.eigenvectorBasis j)) ⋯)

★★ Block Lüders composed with Bayes — D3's first half. After degenerate outcome i on the mixed preparation, the post-measurement system marginal is the Bayes-posterior mixture of the per-component degenerate Lüders posts epistemicMeasure [Πᵢψⱼ]. At rank ≥ 2 these posteriors are genuinely distinct: the record does not erase the classical ignorance, and what survives is exactly ρ ↦ Πᵢ ρ Πᵢ / Tr(ρ Πᵢ) realised as a mixture. (Hypothesis hproj: every component meets block i — see the scope note.)