SigmaLayer/JoinClosure: the degenerate one-protocol package

Category: dynamical measurement — the degenerate counterpart of SwapMeasurementClosure/UnifiedArenaClosure, requested by the fourth external review (2026-08-03): the degenerate pieces existed as theorems on the join protocol but had never been packaged as one closure on one protocol.

★★ degenerateMeasurementClosure — for every block structure b and preparation ψ, the join protocol simultaneously carries:

• ready ⇒ no record, record created (the outcome the selector had fixed), outcomes exclusive, record persists across the operational window — the standard record architecture, all fields proved of the constructed propagator;
• Liouville preservation of the join arena measure at every time pair;
• ★ the coarse dynamical Born mass (join_sector_born, new here): the outcome-i sector of the canonical join preparation carries exactly the block Born weight ∑_{j : b j = i} ‖⟨eⱼ, ψ⟩‖² — and the mass is independent of the ancilla calibration;
• the ψ-dependent degenerate Lüders update (joinWitness_blockLuders): conditioning on outcome i relocates the system to epistemicMeasure [Πᵢψ].

The spine of join_sector_born: the preparation pulls the sector back to a cylinder over the good system fibres (preimage_sector_ae), whose Haar volume is a Dirac slice of the selector Born theorem — volume (goodTheta) = epistemicMeasure [ψ] (blockIndex⁻¹ i) (volume_goodTheta), evaluated by degenerate_selector_born.

⚠️ Honest scope. The Born mass is stated at the canonical join preparation (joinPrep: phase-orbit join point, Haar fibres, ready register) — the same preparation the Lüders theorem conditions; the calibration vector α is quantified, so the statistics provably cannot leak the calibration. The i.i.d. frequency layer is not restated: it consumes any probability measure and event and applies verbatim. The rank-one specialisation (K = N, b = id) is the swap closure's territory and is not duplicated here.

References

specs/BACKLOG.md (the degenerate one-protocol package row — this discharges it; fourth external review 2026-08-03); SigmaLayer/DegenerateLuders.lean (degenerate_selector_born, BlockLudersObligation), SigmaLayer/JoinProtocol.lean (joinProtocol, join_correlates, join_pointerInvariant, joinEvolve_measurePreserving), SigmaLayer/JoinLuders.lean (joinPrep, goodTheta, preimage_sector_ae, joinWitness_blockLuders), SigmaLayer/SwapClosure.lean (SwapMeasurementClosure, the rank-one precedent), SigmaLayer/MeasurementCapstone.lean (whose degenerate field this upgrades).

★ The coarse Born mass of the good fibres

theorem CSD.RecordLayer.volume_goodTheta {N K : ℕ} [NeZero N] {b : Fin N → Fin K} {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin K) : MeasureTheory.volume (goodTheta b ψ hψ0 i) = ENNReal.ofReal (∑ j : Fin N with b j = i, ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2)

The good-fibre volume is the block Born weight — the Dirac slice of degenerate_selector_born: epistemicMeasure [ψ] = δ_{[ψ]} ⊗ Haar, so the selector-Born mass IS the Haar volume of the good system fibres.

theorem CSD.RecordLayer.join_sector_born {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin K) : (joinPrep ψ α hψ0) ((joinProtocol b).outcomeSector i) = ENNReal.ofReal (∑ j : Fin N with b j = i, ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2)

★ The coarse dynamical Born mass on the join protocol: the canonical join preparation gives the outcome-i sector exactly the block Born weight — independently of the ancilla calibration α, which the statement quantifies.

★★ The package

structure CSD.RecordLayer.DegenerateMeasurementClosure {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ : EuclideanSpace ℂ (Fin N)) : Prop

The degenerate measurement package, on one protocol — what the fourth external review asked for: ready/record/exclusivity/persistence, Liouville preservation, the coarse dynamical Born mass, and the ψ-dependent degenerate Lüders update, all carried by the join protocol for the block structure b.

• ready_no_record (x : JoinSel N × LF4.KTorus) : x.2 ∈ readyArc K → (joinProtocol b).readout x = none

  Ready ⇒ no record.

• record_created (i : Fin K) (x : JoinSel N × LF4.KTorus) : x ∈ selReady (joinIdx b) i → (joinProtocol b).readout ((joinProtocol b).evolve 0 1 x) = some i

  A record is created, and it is the outcome the hidden selector had fixed.

• outcomes_exclusive : Pairwise (Function.onFun Disjoint (joinProtocol b).outcomeSector)

  Distinct outcomes are exclusive.

• record_persists (i : Fin K) (x : JoinSel N × LF4.KTorus) (t : SigmaLayer.OnticTime) : x ∈ (joinProtocol b).outcomeSector i → 1 ≤ t → t ≤ 1 + 1 → (joinProtocol b).readout ((joinProtocol b).evolve 0 t x) = some i

  The record persists across the operational window.

• liouville (p₀ : LF4.CPN (N + N)) (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (joinEvolve b s t) (joinArenaMeasure p₀) (joinArenaMeasure p₀)

  The full propagator preserves the join arena Liouville measure.

• sector_born (hψ0 : ψ ≠ 0) (α : EuclideanSpace ℂ (Fin N)) : ‖ψ‖ = 1 → ∀ (i : Fin K), (joinPrep ψ α hψ0) ((joinProtocol b).outcomeSector i) = ENNReal.ofReal (∑ j : Fin N with b j = i, ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2)

  ★ The coarse dynamical Born mass, calibration-independent.

• luders (α : Fin K → EuclideanSpace ℂ (Fin N)) : (∀ (i : Fin K), (blockProj b i) (α i) = α i) → ∀ (hψ0 : ψ ≠ 0) (i : Fin K) (h : (blockProj b i) ψ ≠ 0), joinPostMarg b α ψ hψ0 i = epistemicMeasure (Projectivization.mk ℂ ((blockProj b i) ψ) h)

  The ψ-dependent degenerate Lüders update, from a fixed block-supported calibration family, through Liouville-preserving dynamics.

theorem CSD.RecordLayer.degenerateMeasurementClosure {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ : EuclideanSpace ℂ (Fin N)) : DegenerateMeasurementClosure b ψ

★★ The degenerate one-protocol package holds — for every block structure and every preparation, with the correlation and pointer-invariance proved of the constructed propagator, never assumed.