SigmaLayer/JoinProtocol: the degenerate measurement as a MeasurementProtocol

Category: 7-SigmaLayer (dynamical measurement — degenerate Lüders, brick 4: the protocol plumbing).

What this is

JoinArena.lean proved the degenerate Lüders update is a Liouville-preserving unitary with a pointwise-correct readout. This module runs that update inside the corpus's standard measurement architecture — the same two-time-propagator, ready/pointer-region, record-triggered shape as SwapWitness:

• the ontic space is Xj × T²_R: join point ℙ(ℂ^{N+N}), system fibre, ancilla fibre, pointer register;
• the selector is the coarse block index read off the join point's system ray and the system fibre (joinIdx — b ∘ basinIndex ∘ (joinFst, fibre));
• the propagator joinEvolve shears the register (record creation, as always) and, at the readout crossing, fires the record-triggered joinG: apply the join unitary to the join point and exchange the system fibre with the ancilla fibre. The fibre exchange is the degenerate analogue of the rank-one witness's fresh slot: the post-measurement system fibre is the ancilla's (fresh), while the outcome-conditioned original fibre is stored, not destroyed.

Because the arena is literally a shear arena over Xsel = Xj, the whole record apparatus — regions, readout, sectors, persistence — is inherited from shearProtocol by structure update; only the propagator cluster is new.

What is proved

• joinG_joinG — the record-triggered map is an involution (joinSwap is a permutation unitary squared to 1; the fibre exchange is its own inverse; the register is untouched).
• joinEvolve_comp — the two-time law, the same eight readout-crossing cases as swapEvolve_comp.
• joinProtocol — the MeasurementProtocol instance.
• join_correlates / join_pointerInvariant — CorrelatesOn and PointerInvariantOn discharged from the constructed propagator, never assumed.
• ★ joinEvolve_measurePreserving — the full propagator preserves the join-arena Liouville measure (μ_FS ⊗ vol ⊗ vol) ⊗ vol, at every time pair: the shear part by the generic shear theorem, the crossing part by joinSwap_measurePreserving (FS unitary invariance) + the fibre-transposition shuffle, glued by the register-arc partition.

⚠️ What brick 5 (the last one) owes

The conditioned-marginal bookkeeping: the sector-conditioned post-measurement system readout for the canonical phase-orbit preparation equals epistemicMeasure [Πᵢψ] — the BlockLudersObligation instance, mirroring SwapLuders. The pointwise input is join_block_luders; the plumbing is conditioning + pushforward (specs/BACKLOG.md).

References

SigmaLayer/JoinArena.lean (joinSwap, join_block_luders, joinFst); SigmaLayer/SwapWitness.lean (the transcribed architecture: arcIndex, the crossing propagator, the partition argument); SigmaLayer/ShearWitness.lean (shearEvolve and the generic record machinery, inherited); SigmaLayer/DegenerateLuders.lean (swap_not_blockLuders — why the rank-one architecture could not host this); specs/BACKLOG.md.

The join selector space

@[reducible, inline]

abbrev CSD.RecordLayer.JoinSel (N : ℕ) : Type

The join selector space: join point, system fibre, ancilla fibre.

Equations

• CSD.RecordLayer.JoinSel N = ((CSD.LF4.CPN (N + N) × CSD.LF4.KTorus) × CSD.LF4.KTorus)

noncomputable def CSD.RecordLayer.joinIdx {N K : ℕ} [NeZero N] (b : Fin N → Fin K) : JoinSel N → Fin K

The coarse selector: block index of the join point's system ray at the system fibre.

Equations

• CSD.RecordLayer.joinIdx b x = b (CSD.RecordLayer.basinIndex (CSD.RecordLayer.momentContext N) (CSD.RecordLayer.joinFst x.1.1, x.1.2))

theorem CSD.RecordLayer.measurable_joinIdx {N K : ℕ} [NeZero N] (b : Fin N → Fin K) : Measurable (joinIdx b)

The record-triggered join map

noncomputable def CSD.RecordLayer.joinG {N K : ℕ} (b : Fin N → Fin K) : JoinSel N × LF4.KTorus → JoinSel N × LF4.KTorus

The record-triggered join map G: if the pointer displays outcome i, apply the join unitary for block i and exchange the system fibre with the ancilla fibre; otherwise do nothing. The register is untouched.

Equations

• CSD.RecordLayer.joinG b x = match CSD.RecordLayer.arcIndex K x.2 with | none => x | some i => (((CSD.RecordLayer.joinSwap b i x.1.1.1, x.1.2), x.1.1.2), x.2)

theorem CSD.RecordLayer.joinG_register {N K : ℕ} (b : Fin N → Fin K) (x : JoinSel N × LF4.KTorus) : (joinG b x).2 = x.2

theorem CSD.RecordLayer.joinG_of_mem {N K : ℕ} (b : Fin N → Fin K) {x : JoinSel N × LF4.KTorus} {i : Fin K} (h : x.2 ∈ pointerArc K i) : joinG b x = (((joinSwap b i x.1.1.1, x.1.2), x.1.1.2), x.2)

theorem CSD.RecordLayer.joinG_of_none {N K : ℕ} (b : Fin N → Fin K) {x : JoinSel N × LF4.KTorus} (h : ∀ (i : Fin K), x.2 ∉ pointerArc K i) : joinG b x = x

theorem CSD.RecordLayer.joinMat_mul_self {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinMat b i * joinMat b i = 1

The join matrix squares to the identity — the permutation is an involution.

theorem CSD.RecordLayer.joinSwap_joinSwap {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p : LF4.CPN (N + N)) : joinSwap b i (joinSwap b i p) = p

The join swap on rays is an involution.

theorem CSD.RecordLayer.joinG_joinG {N K : ℕ} (b : Fin N → Fin K) (x : JoinSel N × LF4.KTorus) : joinG b (joinG b x) = x

G is an involution — the join unitary squares to the identity, the fibre exchange is its own inverse, and the register (the trigger) is untouched.

G preserves the join-arena Liouville measure

noncomputable def CSD.RecordLayer.joinSelMeasure {N : ℕ} (p₀ : LF4.CPN (N + N)) : MeasureTheory.Measure (JoinSel N)

The join-selector Liouville measure: Fubini–Study on the join point, Haar on both fibres.

Equations

• CSD.RecordLayer.joinSelMeasure p₀ = ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀).prod MeasureTheory.volume).prod MeasureTheory.volume

instance CSD.RecordLayer.instIsProbabilityMeasureJoinSelJoinSelMeasure {N : ℕ} (p₀ : LF4.CPN (N + N)) : MeasureTheory.IsProbabilityMeasure (joinSelMeasure p₀)

noncomputable def CSD.RecordLayer.joinArenaMeasure {N : ℕ} (p₀ : LF4.CPN (N + N)) : MeasureTheory.Measure (JoinSel N × LF4.KTorus)

The join-arena Liouville measure: selector ⊗ register Haar.

Equations

• CSD.RecordLayer.joinArenaMeasure p₀ = (CSD.RecordLayer.joinSelMeasure p₀).prod MeasureTheory.volume

theorem CSD.RecordLayer.joinArenaMeasure_def {N : ℕ} (p₀ : LF4.CPN (N + N)) : joinArenaMeasure p₀ = (joinSelMeasure p₀).prod MeasureTheory.volume

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

instance CSD.RecordLayer.instIsProbabilityMeasureProdJoinSelKTorusJoinArenaMeasure {N : ℕ} (p₀ : LF4.CPN (N + N)) : MeasureTheory.IsProbabilityMeasure (joinArenaMeasure p₀)

noncomputable def CSD.RecordLayer.joinGm {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : JoinSel N → JoinSel N

The fired-branch map on the selector: join swap on the point, fibre exchange.

Equations

• CSD.RecordLayer.joinGm b i y = ((CSD.RecordLayer.joinSwap b i y.1.1, y.2), y.1.2)

theorem CSD.RecordLayer.measurable_joinGm {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Measurable (joinGm b i)

theorem CSD.RecordLayer.measurePreserving_joinGm {N K : ℕ} (p₀ : LF4.CPN (N + N)) (b : Fin N → Fin K) (i : Fin K) : MeasureTheory.MeasurePreserving (joinGm b i) (joinSelMeasure p₀) (joinSelMeasure p₀)

def CSD.RecordLayer.joinArcPiece {N : ℕ} (K : ℕ) (o : Option (Fin K)) : Set (JoinSel N × LF4.KTorus)

The register-arc pieces of the join arena.

Equations

• CSD.RecordLayer.joinArcPiece K none = {x : CSD.RecordLayer.JoinSel N × CSD.LF4.KTorus | ∀ (i : Fin K), x.2 ∉ CSD.RecordLayer.pointerArc K i}
• CSD.RecordLayer.joinArcPiece K (some i) = {x : CSD.RecordLayer.JoinSel N × CSD.LF4.KTorus | x.2 ∈ CSD.RecordLayer.pointerArc K i}

theorem CSD.RecordLayer.measurableSet_joinArcPiece {N K : ℕ} (o : Option (Fin K)) : MeasurableSet (joinArcPiece K o)

theorem CSD.RecordLayer.joinArcPiece_disjoint {N K : ℕ} : Pairwise (Function.onFun Disjoint (joinArcPiece K))

theorem CSD.RecordLayer.joinArcPiece_cover {N K : ℕ} : ⋃ (o : Option (Fin K)), joinArcPiece K o = Set.univ

theorem CSD.RecordLayer.joinG_agree {N K : ℕ} (b : Fin N → Fin K) (o : Option (Fin K)) (x : JoinSel N × LF4.KTorus) (hx : x ∈ joinArcPiece K o) : joinG b x = (match (motive := Option (Fin K) → JoinSel N × LF4.KTorus → JoinSel N × LF4.KTorus) o with | none => id | some i => Prod.map (joinGm b i) id) x

theorem CSD.RecordLayer.measurable_joinG {N K : ℕ} (b : Fin N → Fin K) : Measurable (joinG b)

theorem CSD.RecordLayer.measurePreserving_joinG {N K : ℕ} (p₀ : LF4.CPN (N + N)) (b : Fin N → Fin K) : MeasureTheory.MeasurePreserving (joinG b) (joinArenaMeasure p₀) (joinArenaMeasure p₀)

★ The record-triggered join map preserves the arena Liouville measure — each register arc's piece map preserves it, and each piece is invariant under its own map because the trigger coordinate is untouched.

The crossing propagator

noncomputable def CSD.RecordLayer.joinEvolve {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (s t : SigmaLayer.OnticTime) : JoinSel N × LF4.KTorus → JoinSel N × LF4.KTorus

The join propagator: shear the register; fire the record-triggered join map when the window crosses readout, in either direction (G is an involution).

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.RecordLayer.joinEvolve_fwd {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {s t : SigmaLayer.OnticTime} (hs : s < 1) (ht : 1 ≤ t) : joinEvolve b s t = joinG b ∘ shearEvolve (joinIdx b) s t

theorem CSD.RecordLayer.joinEvolve_bwd {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {s t : SigmaLayer.OnticTime} (ht : t < 1) (hs : 1 ≤ s) : joinEvolve b s t = shearEvolve (joinIdx b) s t ∘ joinG b

theorem CSD.RecordLayer.joinEvolve_lo {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {s t : SigmaLayer.OnticTime} (hs : s < 1) (ht : t < 1) : joinEvolve b s t = shearEvolve (joinIdx b) s t

theorem CSD.RecordLayer.joinEvolve_hi {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {s t : SigmaLayer.OnticTime} (hs : 1 ≤ s) (ht : 1 ≤ t) : joinEvolve b s t = shearEvolve (joinIdx b) s t

theorem CSD.RecordLayer.sE_comp {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (s t u : SigmaLayer.OnticTime) (x : JoinSel N × LF4.KTorus) : shearEvolve (joinIdx b) t u (shearEvolve (joinIdx b) s t x) = shearEvolve (joinIdx b) s u x

Pointwise shear composition.

theorem CSD.RecordLayer.sE_congr {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {s t t' : SigmaLayer.OnticTime} (h : elapsed t = elapsed t') (x : JoinSel N × LF4.KTorus) : shearEvolve (joinIdx b) s t x = shearEvolve (joinIdx b) s t' x

theorem CSD.RecordLayer.sE_congr_left {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {s s' t : SigmaLayer.OnticTime} (h : elapsed s = elapsed s') (x : JoinSel N × LF4.KTorus) : shearEvolve (joinIdx b) s t x = shearEvolve (joinIdx b) s' t x

theorem CSD.RecordLayer.joinEvolve_comp {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (s t u : SigmaLayer.OnticTime) : joinEvolve b t u ∘ joinEvolve b s t = joinEvolve b s u

The two-time composition law — the same eight readout-crossing cases as swapEvolve_comp, closing on G² = id and the frozen shear.

theorem CSD.RecordLayer.measurable_joinEvolve {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (s t : SigmaLayer.OnticTime) : Measurable (joinEvolve b s t)

noncomputable def CSD.RecordLayer.joinProtocol {N K : ℕ} [NeZero N] (b : Fin N → Fin K) : MeasurementProtocol (JoinSel N × LF4.KTorus) K

The degenerate-measurement protocol on the join arena. All region and readout structure is inherited from the shear protocol; only the propagator cluster is new.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.RecordLayer.join_correlates {N K : ℕ} [NeZero N] (b : Fin N → Fin K) : (joinProtocol b).CorrelatesOn (selReady (joinIdx b))

CorrelatesOn discharged: the register dynamics is the shear's, and G never moves the register.

theorem CSD.RecordLayer.join_pointerInvariant {N K : ℕ} [NeZero N] (b : Fin N → Fin K) : (joinProtocol b).PointerInvariantOn

PointerInvariantOn discharged: right of readout the propagator is frozen.

theorem CSD.RecordLayer.joinEvolve_measurePreserving {N K : ℕ} (p₀ : LF4.CPN (N + N)) [NeZero N] (b : Fin N → Fin K) (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (joinEvolve b s t) (joinArenaMeasure p₀) (joinArenaMeasure p₀)

★ The full join propagator preserves the arena Liouville measure, at every time pair.