SigmaLayer/JoinLuders: BlockLudersObligation, inhabited — the degenerate arc closed

Category: 7-SigmaLayer (dynamical measurement — degenerate Lüders, brick 5: the conditioned marginal).

The headline

★★ joinWitness_blockLuders: the join witness satisfies BlockLudersObligation — the §8.3 demand that swap_not_blockLuders proved no fixed ray-level calibration can meet is inhabited by the join protocol. For every preparation ψ with nonvanishing block-i component, the sector-conditioned post-measurement system readout is exactly epistemicMeasure [Πᵢψ] — the ψ-dependent Lüders update, from a fixed block-supported calibration family, through Liouville-preserving dynamics.

How the marginal computation runs (join_luders_marginal)

The canonical preparation is a pushforward from a parameter space (phase θ, system fibre θₛ, ancilla fibre θₐ, register r): join point = the phase-orbit point [χ(θ)ψ ⊕ α], fibres Haar, register ready. Then:

1. conditioning commutes with the pushforward (cond_map);
2. on the ready support, the outcome-i sector pulls back to a cylinder over the system fibre alone — θₛ ∈ goodTheta (the block's basin cells) — because the phase orbit has constant system ray, so the selector never sees θ;
3. conditioning the product on that cylinder conditions only the θₛ factor (cond_prod_prod);
4. on the conditioned support the evolved readout is constant in everything but θₐ: the ray is [Πᵢψ] at every phase (joinPoint_collapse, from join_block_luders), and the post-measurement system fibre is the ancilla's;
5. so the marginal is δ_{[Πᵢψ]} ⊗ Haar = epistemicMeasure [Πᵢψ]. The conditioned original fibre (the θₛ factor) integrates out — it was moved to the ancilla slot, stored.

goodTheta_vol_pos discharges the conditioning positivity from Πᵢψ ≠ 0 alone (a nonzero block coordinate has a positive-width basin cell), so the obligation carries no measure hypothesis. (The generic conditioning toolkit was extracted to CsdLean4/Mathlib/Probability/ConditionalProbability.lean on 2026-08-02.)

What this closes

The degenerate-Lüders arc, bricks 1–5: relocation target (BlockCollapse) → phase-slot mechanism (PhaseSlot) → Liouville-preserving pointwise update on the join (JoinArena) → the MeasurementProtocol (JoinProtocol) → the obligation itself (here). The rank-one and degenerate Lüders updates now stand on the same architectural footing: explicit propagators, measure-preserving, records created and persistent, post-states as pushforward theorems. swap_not_blockLuders stands as the theorem explaining why the ray-pair arena could not host this.

References

SigmaLayer/DegenerateLuders.lean (BlockLudersObligation, swap_not_blockLuders); SigmaLayer/JoinProtocol.lean (the protocol); SigmaLayer/JoinArena.lean (join_block_luders — the pointwise input); SigmaLayer/SwapLuders.lean (the rank-one precedent whose conditioning toolkit this mirrors); specs/BACKLOG.md.

Conditioning toolkit — moved to the staging tree 2026-08-02

(CsdLean4/Mathlib/Probability/ConditionalProbability.lean: ProbabilityTheory.cond_map, cond_prod_prod, cond_eq_self).

theorem CSD.RecordLayer.readyMeasure_compl (K : ℕ) : (readyMeasure K) (readyArc K)ᶜ = 0

The ready register never leaves the ready arc.

theorem CSD.RecordLayer.cond_of_ae {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {S : Set X} (hS : MeasurableSet S) (h : μ Sᶜ = 0) : μ[|S] = μ

Conditioning a probability measure on the whole space does nothing.

The sector, characterised on the ready support

theorem CSD.RecordLayer.shear_sector_iff_of_ready {K : ℕ} {Xs : Type u_1} [MeasurableSpace Xs] (idx : Xs → Fin K) (hidx : Measurable idx) (i : Fin K) {x : Xs × LF4.KTorus} (hr : x.2 ∈ readyArc K) : x ∈ (shearProtocol idx hidx).outcomeSector i ↔ idx x.1 = i

On the ready arc, the shear's outcome-i sector is exactly the selector-i fibre.

theorem CSD.RecordLayer.join_outcomeSector_eq {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (i : Fin K) : (joinProtocol b).outcomeSector i = (shearProtocol (joinIdx b) ⋯).outcomeSector i

The join protocol's outcome sector is the shear's — the record trigger never moves the register.

The canonical preparation

noncomputable def CSD.RecordLayer.joinPoint {N : ℕ} (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (θ : AddCircle 1) : LF4.CPN (N + N)

One phase-orbit join point.

Equations

• CSD.RecordLayer.joinPoint ψ α hψ0 θ = Projectivization.mk ℂ (CSD.RecordLayer.dblVec (↑θ.toCircle • ψ) α) ⋯

noncomputable def CSD.RecordLayer.dblVecFst {N : ℕ} : EuclideanSpace ℂ (Fin N) →ₗ[ℂ] EuclideanSpace ℂ (Fin (N + N))

The first-copy embedding, linearly.

Equations

• CSD.RecordLayer.dblVecFst = { toFun := fun (v : EuclideanSpace ℂ (Fin N)) => CSD.RecordLayer.dblVec v 0, map_add' := ⋯, map_smul' := ⋯ }

theorem CSD.RecordLayer.dblVec_split {N : ℕ} (α v : EuclideanSpace ℂ (Fin N)) : dblVec v α = dblVecFst v + dblVec 0 α

The doubled vector is the linear first part plus the constant slot part.

theorem CSD.RecordLayer.measurable_joinPoint {N : ℕ} (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : Measurable (joinPoint ψ α hψ0)

noncomputable def CSD.RecordLayer.paramMeasure (K : ℕ) : MeasureTheory.Measure (((AddCircle 1 × LF4.KTorus) × LF4.KTorus) × LF4.KTorus)

The parameter space of the canonical preparation: phase, system fibre, ancilla fibre, register.

Equations

• CSD.RecordLayer.paramMeasure K = ((MeasureTheory.volume.prod MeasureTheory.volume).prod MeasureTheory.volume).prod (CSD.RecordLayer.readyMeasure K)

theorem CSD.RecordLayer.paramMeasure_def (K : ℕ) : paramMeasure K = ((MeasureTheory.volume.prod MeasureTheory.volume).prod MeasureTheory.volume).prod (readyMeasure K)

The parameter measure, as its defining product (interface lemma, §9.1).

instance CSD.RecordLayer.instIsProbabilityMeasureProdAddCircleRealOfNatKTorusParamMeasure {K : ℕ} : MeasureTheory.IsProbabilityMeasure (paramMeasure K)

noncomputable def CSD.RecordLayer.jF {N : ℕ} (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (q : ((AddCircle 1 × LF4.KTorus) × LF4.KTorus) × LF4.KTorus) : JoinSel N × LF4.KTorus

The preparation map: phase-orbit join point, fibres and register threaded through.

Equations

• CSD.RecordLayer.jF ψ α hψ0 q = (((CSD.RecordLayer.joinPoint ψ α hψ0 q.1.1.1, q.1.1.2), q.1.2), q.2)

theorem CSD.RecordLayer.measurable_jF {N : ℕ} (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : Measurable (jF ψ α hψ0)

noncomputable def CSD.RecordLayer.joinPrep {N K : ℕ} (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : MeasureTheory.Measure (JoinSel N × LF4.KTorus)

The canonical preparation: phase-orbit join point, Haar fibres, ready register.

Equations

• CSD.RecordLayer.joinPrep ψ α hψ0 = MeasureTheory.Measure.map (CSD.RecordLayer.jF ψ α hψ0) (CSD.RecordLayer.paramMeasure K)

instance CSD.RecordLayer.instIsProbabilityMeasureProdJoinSelKTorusJoinPrep {N K : ℕ} (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : MeasureTheory.IsProbabilityMeasure (joinPrep ψ α hψ0)

The selector on the orbit

theorem CSD.RecordLayer.joinFst_joinPoint {N : ℕ} [NeZero N] (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (θ : AddCircle 1) : joinFst (joinPoint ψ α hψ0 θ) = Projectivization.mk ℂ ψ hψ0

The phase orbit has constant system ray.

def CSD.RecordLayer.goodTheta {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) : Set LF4.KTorus

The good system fibres: those whose basin lies in block i.

Equations

• CSD.RecordLayer.goodTheta b ψ hψ0 i = {θs : CSD.LF4.KTorus | b (CSD.RecordLayer.basinIndex (CSD.RecordLayer.momentContext N) (Projectivization.mk ℂ ψ hψ0, θs)) = i}

theorem CSD.RecordLayer.measurableSet_goodTheta {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) : MeasurableSet (goodTheta b ψ hψ0 i)

theorem CSD.RecordLayer.joinIdx_jF {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (q : ((AddCircle 1 × LF4.KTorus) × LF4.KTorus) × LF4.KTorus) : joinIdx b (jF ψ α hψ0 q).1 = b (basinIndex (momentContext N) (Projectivization.mk ℂ ψ hψ0, q.1.1.2))

The selector at a preparation point reads the system fibre alone.

The sector pulls back to a fibre cylinder

theorem CSD.RecordLayer.jF_mem_sector_iff {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) {q : ((AddCircle 1 × LF4.KTorus) × LF4.KTorus) × LF4.KTorus} (hr : q.2 ∈ readyArc K) : jF ψ α hψ0 q ∈ (joinProtocol b).outcomeSector i ↔ q.1.1.2 ∈ goodTheta b ψ hψ0 i

theorem CSD.RecordLayer.preimage_sector_ae {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) : jF ψ α hψ0 ⁻¹' (joinProtocol b).outcomeSector i =ᵐ[paramMeasure K] ((Set.univ ×ˢ goodTheta b ψ hψ0 i) ×ˢ Set.univ) ×ˢ readyArc K

The pulled-back sector agrees a.e. with the fibre cylinder.

Positivity from the block component

theorem CSD.RecordLayer.goodTheta_vol_pos {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) (hPi : (blockProj b i) ψ ≠ 0) : MeasureTheory.volume (goodTheta b ψ hψ0 i) ≠ 0

A nonzero block component gives the good-fibre set positive measure.

The readout on the sector

noncomputable def CSD.RecordLayer.sysRead {N : ℕ} [NeZero N] : JoinSel N × LF4.KTorus → LF4.KSigma N

The post-measurement system readout: system ray and system fibre of the join state.

Equations

• CSD.RecordLayer.sysRead x = (CSD.RecordLayer.joinFst x.1.1.1, x.1.1.2)

theorem CSD.RecordLayer.measurable_sysRead {N : ℕ} [NeZero N] : Measurable sysRead

theorem CSD.RecordLayer.sysRead_evolve_on_sector {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (i : Fin K) {x : JoinSel N × LF4.KTorus} (hx : x ∈ (joinProtocol b).outcomeSector i) : sysRead (joinEvolve b 0 1 x) = (joinFst (joinSwap b i x.1.1.1), x.1.2)

On the sector, the evolved readout is the collapsed ray with the ancilla's fibre.

theorem CSD.RecordLayer.joinPoint_collapse {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) (hPi : (blockProj b i) ψ ≠ 0) (hα : (blockProj b i) α = α) (θ : AddCircle 1) : joinFst (joinSwap b i (joinPoint ψ α hψ0 θ)) = Projectivization.mk ℂ ((blockProj b i) ψ) hPi

The collapsed ray at every phase.

★★ The conditioned marginal

theorem CSD.RecordLayer.join_luders_marginal {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) (hPi : (blockProj b i) ψ ≠ 0) (hα : (blockProj b i) α = α) : MeasureTheory.Measure.map sysRead ((joinProtocol b).postMeasure (joinPrep ψ α hψ0) i) = epistemicMeasure (Projectivization.mk ℂ ((blockProj b i) ψ) hPi)

★★ The degenerate Lüders marginal. For the canonical preparation, conditioned on the coarse outcome i, the post-measurement system readout is exactly the collapsed epistemic state epistemicMeasure [Πᵢψ].

★★ The obligation, inhabited

noncomputable def CSD.RecordLayer.joinPostMarg {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (α : Fin K → EuclideanSpace ℂ (Fin N)) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K) : MeasureTheory.Measure (LF4.KSigma N)

The join witness's post-measurement system marginal, for calibration family α.

Equations

• CSD.RecordLayer.joinPostMarg b α ψ hψ0 i = MeasureTheory.Measure.map CSD.RecordLayer.sysRead ((CSD.RecordLayer.joinProtocol b).postMeasure (CSD.RecordLayer.joinPrep ψ (α i) hψ0) i)

theorem CSD.RecordLayer.joinWitness_blockLuders {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (α : Fin K → EuclideanSpace ℂ (Fin N)) (hα : ∀ (i : Fin K), (blockProj b i) (α i) = α i) : BlockLudersObligation b (joinPostMarg b α)

★★ BlockLudersObligation, inhabited. With any block-supported calibration family, the join witness satisfies the §8.3 degenerate-Lüders demand — the construction swap_not_blockLuders proved impossible for every fixed ray-level calibration, delivered by the phase-carrying join arena through Liouville-preserving dynamics.