SigmaLayer/JoinArena: the projective join — Liouville-preserving degenerate Lüders

Category: 7-SigmaLayer (dynamical measurement — the degenerate-Lüders construction, brick 3: the Liouville half).

The identification that makes brick 3 cheap

PhaseSlot.lean realised the degenerate Lüders update on phase-enriched vector pairs. This module observes that the phase-enriched pair arena is the projective join: a point of ℙ(ℂᴺ ⊕ ℂᴺ) = ℙ(ℂ^{N+N}) is a system-and-slot pair quotiented only by the global phase — so the relative phase, the coordinate the sharpened wall demanded, survives in the point itself. On this arena:

• the component swap is a coordinate permutation (joinPerm), hence a permutation unitary (joinMat, joinMat_mem_unitaryGroup), acting on rays through the standard unitary action;
• ★★ Liouville preservation is Fubini–Study unitary invariance (joinSwap_measurePreserving): the measure-preservation obligation recorded as brick 3's hard half is discharged by fubiniStudyMeasure_smul_invariant, because the dynamics is a unitary;
• ★★ the Lüders update is pointwise deterministic (join_block_luders): for every join microstate [ψ ⊕ α] with nonvanishing block component and block-calibrated slot, the post-swap system readout is exactly [Πᵢψ]. Every microstate updates correctly; the PhaseSlot measure form is the orbit-averaged shadow of this.

The three-brick arc, closed at the state level

1. BlockCollapse.lean: the target is a relocation; the mechanism exists on vectors; the wall is the relative phase.
2. PhaseSlot.lean: keep the phase → the update works with fixed calibration (measure form).
3. Here: the phase-kept arena is ℙ(ℂ^{N+N}), the dynamics is unitary — Liouville-preserving by FS invariance, Lüders pointwise.

⚠️ What remains for full protocol integration (recorded, mechanical)

The register/sector plumbing: a MeasurementProtocol on ℙ(ℂ^{N+N}) × T²_R whose record trigger fires joinSwap, mirroring SwapWitness, and the conditioned-marginal bookkeeping tying join_block_luders to a BlockLudersObligation instance. Both consume only theorems proved here and machinery that already exists (specs/BACKLOG.md, effort M); neither requires new mathematics. Until that lands, swap_not_blockLuders remains the recorded boundary for the ray-pair SwapArena — the join arena is where degenerate measurements live.

References

SigmaLayer/BlockCollapse.lean (componentSwap, brick 1); SigmaLayer/PhaseSlot.lean (brick 2 — the measure form); SigmaLayer/DegenerateLuders.lean (swap_not_blockLuders, blockProj); Mathlib/LinearAlgebra/Projectivization/FubiniStudy.lean (fubiniStudyMeasure_smul_invariant — the Liouville driver); specs/BACKLOG.md.

componentSwap, entrywise

theorem CSD.RecordLayer.componentSwap_fst_apply {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p : EuclideanSpace ℂ (Fin N) × EuclideanSpace ℂ (Fin N)) (j : Fin N) : (componentSwap b i p).1.ofLp j = if b j = i then p.1.ofLp j else p.2.ofLp j

theorem CSD.RecordLayer.componentSwap_snd_apply {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p : EuclideanSpace ℂ (Fin N) × EuclideanSpace ℂ (Fin N)) (j : Fin N) : (componentSwap b i p).2.ofLp j = if b j = i then p.2.ofLp j else p.1.ofLp j

The join permutation and its unitary

def CSD.RecordLayer.swpSum {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Fin N ⊕ Fin N → Fin N ⊕ Fin N

The block-complement swap on the doubled index set: fix the block-i coordinates of both copies, exchange the complements.

Equations

• CSD.RecordLayer.swpSum b i (Sum.inl j) = if b j = i then Sum.inl j else Sum.inr j
• CSD.RecordLayer.swpSum b i (Sum.inr j) = if b j = i then Sum.inr j else Sum.inl j

theorem CSD.RecordLayer.swpSum_involutive {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Function.Involutive (swpSum b i)

def CSD.RecordLayer.joinPerm {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Fin (N + N) → Fin (N + N)

The join permutation on Fin (N + N).

Equations

• CSD.RecordLayer.joinPerm b i j = finSumFinEquiv (CSD.RecordLayer.swpSum b i (finSumFinEquiv.symm j))

theorem CSD.RecordLayer.joinPerm_involutive {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Function.Involutive (joinPerm b i)

theorem CSD.RecordLayer.joinPerm_injective {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Function.Injective (joinPerm b i)

def CSD.RecordLayer.joinMat {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Matrix (Fin (N + N)) (Fin (N + N)) ℂ

The permutation matrix of the join swap.

Equations

• CSD.RecordLayer.joinMat b i = Matrix.of fun (j k : Fin (N + N)) => if k = CSD.RecordLayer.joinPerm b i j then 1 else 0

theorem CSD.RecordLayer.joinMat_mulVec {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (w : Fin (N + N) → ℂ) : (joinMat b i).mulVec w = fun (j : Fin (N + N)) => w (joinPerm b i j)

theorem CSD.RecordLayer.joinMat_mem_unitaryGroup {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinMat b i ∈ Matrix.unitaryGroup (Fin (N + N)) ℂ

The join swap is a unitary — a permutation matrix.

noncomputable def CSD.RecordLayer.joinU {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : ↥(Matrix.unitaryGroup (Fin (N + N)) ℂ)

The join unitary.

Equations

• CSD.RecordLayer.joinU b i = ⟨CSD.RecordLayer.joinMat b i, ⋯⟩

The doubled vectors

noncomputable def CSD.RecordLayer.dblVec {N : ℕ} (v α : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin (N + N))

The doubled vector: system in the first copy, slot in the second.

Equations

• CSD.RecordLayer.dblVec v α = WithLp.toLp 2 fun (j : Fin (N + N)) => Sum.elim (fun (k : Fin N) => v.ofLp k) (fun (k : Fin N) => α.ofLp k) (finSumFinEquiv.symm j)

@[simp]

theorem CSD.RecordLayer.dblVec_inl {N : ℕ} (v α : EuclideanSpace ℂ (Fin N)) (k : Fin N) : (dblVec v α).ofLp (finSumFinEquiv (Sum.inl k)) = v.ofLp k

@[simp]

theorem CSD.RecordLayer.dblVec_inr {N : ℕ} (v α : EuclideanSpace ℂ (Fin N)) (k : Fin N) : (dblVec v α).ofLp (finSumFinEquiv (Sum.inr k)) = α.ofLp k

theorem CSD.RecordLayer.dblVec_ne_zero {N : ℕ} {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) (α : EuclideanSpace ℂ (Fin N)) : dblVec v α ≠ 0

theorem CSD.RecordLayer.toEuclideanLin_joinMat_dblVec {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) : (Matrix.toEuclideanLin (joinMat b i)) (dblVec ψ α) = dblVec (componentSwap b i (ψ, α)).1 (componentSwap b i (ψ, α)).2

The action of the join unitary on a doubled vector is exactly the component swap.

The join dynamics

noncomputable def CSD.RecordLayer.joinSwap {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : LF4.CPN (N + N) → LF4.CPN (N + N)

The join swap on rays: the unitary action of the permutation on ℙ(ℂ^{N+N}).

Equations

• CSD.RecordLayer.joinSwap b i p = CSD.RecordLayer.joinU b i • p

theorem CSD.RecordLayer.joinSwap_measurePreserving {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p₀ : LF4.CPN (N + N)) : MeasureTheory.MeasurePreserving (joinSwap b i) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

★★ Liouville preservation, discharged. The join swap is a unitary, so it preserves the Fubini–Study measure — the obligation recorded as brick 3's hard half, closed by fubiniStudyMeasure_smul_invariant.

The system readout

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

The first-copy projection, as a linear map.

Equations

• CSD.RecordLayer.fstPart = { toFun := fun (w : EuclideanSpace ℂ (Fin (N + N))) => WithLp.toLp 2 fun (k : Fin N) => w.ofLp (finSumFinEquiv (Sum.inl k)), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CSD.RecordLayer.fstPart_dblVec {N : ℕ} (v α : EuclideanSpace ℂ (Fin N)) : fstPart (dblVec v α) = v

noncomputable def CSD.RecordLayer.joinFstAux {N : ℕ} [NeZero N] (v : { w : EuclideanSpace ℂ (Fin (N + N)) // w ≠ 0 }) : { u : EuclideanSpace ℂ (Fin N) // u ≠ 0 }

The vector-level readout representative: first copy where nonzero, junk vertex otherwise.

Equations

• CSD.RecordLayer.joinFstAux v = ⟨if CSD.RecordLayer.fstPart ↑v ≠ 0 then CSD.RecordLayer.fstPart ↑v else EuclideanSpace.single 0 1, ⋯⟩

theorem CSD.RecordLayer.joinFstAux_coe_of_ne {N : ℕ} [NeZero N] {v : { w : EuclideanSpace ℂ (Fin (N + N)) // w ≠ 0 }} (h : fstPart ↑v ≠ 0) : ↑(joinFstAux v) = fstPart ↑v

On the physical branch (nonzero system component), the readout representative IS the first copy (interface lemma, §9.1 — the case split its unfold sites re-derive).

theorem CSD.RecordLayer.joinFstAux_coe_of_eq {N : ℕ} [NeZero N] {v : { w : EuclideanSpace ℂ (Fin (N + N)) // w ≠ 0 }} (h : fstPart ↑v = 0) : ↑(joinFstAux v) = EuclideanSpace.single 0 1

On the junk branch (vanishing system component), the readout representative is the documented junk vertex (interface lemma, §9.1).

noncomputable def CSD.RecordLayer.joinFst {N : ℕ} [NeZero N] : LF4.CPN (N + N) → LF4.CPN N

The system readout from the join: project a join microstate to its system ray (junk vertex where the system component vanishes — documented, off the physical set).

Equations

• CSD.RecordLayer.joinFst = Projectivization.lift (fun (v : { v : EuclideanSpace ℂ (Fin (N + N)) // v ≠ 0 }) => Projectivization.mk' ℂ (CSD.RecordLayer.joinFstAux v)) ⋯

theorem CSD.RecordLayer.joinFst_mk {N : ℕ} [NeZero N] {w : EuclideanSpace ℂ (Fin (N + N))} (hw : w ≠ 0) (h : fstPart w ≠ 0) : joinFst (Projectivization.mk ℂ w hw) = Projectivization.mk ℂ (fstPart w) h

theorem CSD.RecordLayer.measurable_joinFst {N : ℕ} [NeZero N] : Measurable joinFst

The readout is measurable — same coinduced-Borel route as blockCollapse.

The pointwise Lüders update

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

★★ Degenerate Lüders on the join arena, pointwise. For every join microstate [ψ ⊕ α] with nonvanishing block-i component and block-calibrated slot, the post-swap system readout is exactly the Lüders-collapsed ray [Πᵢψ]. Deterministic at every microstate; combined with joinSwap_measurePreserving, the update is a Liouville-preserving unitary dynamics whose readout is the Lüders update — the construction swap_not_blockLuders proved impossible on the ray-pair arena, delivered on the join.