SigmaLayer/BlockCollapse: the degenerate-Lüders target as a relocation — the join route, brick 1

Category: 7-SigmaLayer (dynamical measurement — the degenerate-Lüders construction, first brick of the projective-join route).

Where this sits

swap_not_blockLuders (DegenerateLuders.lean) proved the boundary: no fixed calibration implements the degenerate Lüders update, because the demanded post-state [Πᵢψ] depends on the preparation. The recorded route forward is the projective join. This module builds the route's first brick — the object every witness must implement, and the vector-level mechanism that implements it one level above the rays:

1. ★ blockCollapse — the measurable ray-level collapse map [ψ] ↦ [Πᵢψ] (junk = identity where the block component vanishes), constructed by quotient descent (Projectivization.lift) with measurability through measurable_iff_measurable_comp_mk'.
2. ★ luders_target_eq_relocation — collapse as relocation, at the epistemic level: the degenerate-Lüders target epistemicMeasure [Πᵢψ] is the pushforward of the preparation under the deterministic system-side relocation ludersRelocation (collapse the base ray, keep the fibre). blockLudersObligation_iff_relocation restates the §8.3 obligation accordingly: what a witness must realise is exactly this pushforward, as the conditioned trace of its dynamics.
3. ★ componentSwap — the vector-level witness core: on the doubled space ℂᴺ ⊕ ℂᴺ (system ⊕ slot), exchange the block-i complements and keep the block parts. It is involutive (componentSwap_involutive) and preserves summed norms (componentSwap_norm_sum) — the content of unitarity — and with a slot calibrated inside the block it performs exactly the collapse with the residual stored (componentSwap_collapse, componentSwap_stores): (ψ, α) ↦ (Πᵢψ, Πᵢα + (ψ − Πᵢψ)). No information is destroyed; no_exact_collapse is respected by storage, exactly as in the rank-one swap.

⚠️ The wall, sharpened

The witness therefore exists one level above the rays. What blocks the descent to the SwapArena is now precisely diagnosed: componentSwap acts on vectors, and its ray-pair version is ill-defined — [Πᵢα + (ψ − Πᵢψ)] depends on the relative scale of the two inputs, which the product ℙ(ℂᴺ) × ℙ(ℂᴺ) forgets (the product quotient kills a U(1) × U(1), the join needs a surviving relative U(1)). Two recorded repair routes (specs/BACKLOG.md): (i) the Fubini–Study disintegration under join coordinates (the originally recorded wall); (ii) a phase-carrying slot — run the bank at sphere level (or ℙ × S¹) so the relative scale survives, and quotient at readout. Route (ii) is new with this diagnosis and is likely the cheaper one. Until one lands, swap_not_blockLuders remains the honest boundary; nothing here claims a ray-level witness.

References

SigmaLayer/DegenerateLuders.lean (blockProj, BlockLudersObligation, swap_not_blockLuders — the boundary); SigmaLayer/MeasurementConstraints.lean (no_exact_collapse — why storage is forced); SigmaLayer/SwapWitness.lean (the rank-one precedent); Mathlib/LinearAlgebra/Projectivization/MeasureSpace.lean (measurable_iff_measurable_comp_mk'); specs/BACKLOG.md.

blockProj algebra

theorem CSD.RecordLayer.blockProj_idem {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (ψ : EuclideanSpace ℂ (Fin N)) : (blockProj b i) ((blockProj b i) ψ) = (blockProj b i) ψ

theorem CSD.RecordLayer.blockProj_compl {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (ψ : EuclideanSpace ℂ (Fin N)) : (blockProj b i) (ψ - (blockProj b i) ψ) = 0

The vector-level witness core: the component swap

def CSD.RecordLayer.componentSwap {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : EuclideanSpace ℂ (Fin N) × EuclideanSpace ℂ (Fin N) → EuclideanSpace ℂ (Fin N) × EuclideanSpace ℂ (Fin N)

The component swap on the doubled space (system ⊕ slot): keep the block-i parts, exchange the complements. Linear in each coordinate slot by construction; the unitary content is componentSwap_involutive + componentSwap_norm_sum.

Equations

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

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

theorem CSD.RecordLayer.componentSwap_norm_sum {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p : EuclideanSpace ℂ (Fin N) × EuclideanSpace ℂ (Fin N)) : ‖(componentSwap b i p).1‖ ^ 2 + ‖(componentSwap b i p).2‖ ^ 2 = ‖p.1‖ ^ 2 + ‖p.2‖ ^ 2

The summed-norm identity: the swap redistributes entries, so the total square-norm over the two slots is conserved — the isometry half of unitarity.

theorem CSD.RecordLayer.componentSwap_collapse {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ α : EuclideanSpace ℂ (Fin N)} (hα : (blockProj b i) α = α) : (componentSwap b i (ψ, α)).1 = (blockProj b i) ψ

★ The collapse, with a block-calibrated slot. If the slot state lies inside the block (Πᵢα = α), the swap delivers exactly the Lüders-collapsed system vector.

theorem CSD.RecordLayer.componentSwap_stores {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (ψ α : EuclideanSpace ℂ (Fin N)) : (componentSwap b i (ψ, α)).2 = (blockProj b i) α + (ψ - (blockProj b i) ψ)

…and the residual is stored, not destroyed: the slot receives the complement of the system state (on top of its own block part). no_exact_collapse is respected by storage.

The ray-level collapse map

noncomputable def CSD.RecordLayer.blockCollapseAux {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (v : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }) : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }

The vector-level representative map: collapse to the block component where it is nonzero, identity otherwise (junk branch, documented).

Equations

• CSD.RecordLayer.blockCollapseAux b i v = ⟨if (CSD.RecordLayer.blockProj b i) ↑v ≠ 0 then (CSD.RecordLayer.blockProj b i) ↑v else ↑v, ⋯⟩

theorem CSD.RecordLayer.blockCollapseAux_coe_of_ne {N K : ℕ} {b : Fin N → Fin K} {i : Fin K} {v : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }} (h : (blockProj b i) ↑v ≠ 0) : ↑(blockCollapseAux b i v) = (blockProj b i) ↑v

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

theorem CSD.RecordLayer.blockCollapseAux_coe_of_eq {N K : ℕ} {b : Fin N → Fin K} {i : Fin K} {v : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }} (h : (blockProj b i) ↑v = 0) : ↑(blockCollapseAux b i v) = ↑v

On the junk branch (vanishing block component), the representative is the identity (interface lemma, §9.1).

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

★ The ray-level collapse map [ψ] ↦ [Πᵢψ] (identity where the block component vanishes), by quotient descent. This is the object any degenerate-Lüders witness must realise as the conditioned trace of its dynamics.

Equations

• CSD.RecordLayer.blockCollapse b i = Projectivization.lift (fun (v : { v : EuclideanSpace ℂ (Fin N) // v ≠ 0 }) => Projectivization.mk' ℂ (CSD.RecordLayer.blockCollapseAux b i v)) ⋯

theorem CSD.RecordLayer.blockCollapse_mk {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (h : (blockProj b i) ψ ≠ 0) : blockCollapse b i (Projectivization.mk ℂ ψ hψ0) = Projectivization.mk ℂ ((blockProj b i) ψ) h

The value lemma: where the block component is nonzero, blockCollapse is [ψ] ↦ [Πᵢψ].

theorem CSD.RecordLayer.blockCollapse_idem {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (h : (blockProj b i) ψ ≠ 0) : blockCollapse b i (blockCollapse b i (Projectivization.mk ℂ ψ hψ0)) = blockCollapse b i (Projectivization.mk ℂ ψ hψ0)

Collapsed states are fixed points: idempotence on the good set.

theorem CSD.RecordLayer.blockCollapse_vertex {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {i : Fin K} {j : Fin N} (hb : b j = i) : blockCollapse b i (vertexPoint j) = vertexPoint j

Block-supported vertices are fixed: consistency with the rank-one story.

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

blockCollapse is measurable — through the coinduced-Borel coincidence (measurable_iff_measurable_comp_mk').

Collapse as relocation: the obligation, reformulated

noncomputable def CSD.RecordLayer.ludersRelocation {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : LF4.KSigma N → LF4.KSigma N

The system-side relocation on KSigma: collapse the base ray, keep the fibre.

Equations

• CSD.RecordLayer.ludersRelocation b i x = (CSD.RecordLayer.blockCollapse b i x.1, x.2)

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

theorem CSD.RecordLayer.luders_target_eq_relocation {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (h : (blockProj b i) ψ ≠ 0) : epistemicMeasure (Projectivization.mk ℂ ((blockProj b i) ψ) h) = MeasureTheory.Measure.map (ludersRelocation b i) (epistemicMeasure (Projectivization.mk ℂ ψ hψ0))

★ Collapse as relocation, at the epistemic level. The degenerate-Lüders target — the post-measurement state epistemicMeasure [Πᵢψ] demanded by the §8.3 obligation — is exactly the pushforward of the preparation under the deterministic relocation map. Nothing stochastic: the update is a measurable relocation of the epistemic Dirac slice, fibre untouched.

theorem CSD.RecordLayer.blockLudersObligation_iff_relocation {N K : ℕ} (b : Fin N → Fin K) (post : (ψ : EuclideanSpace ℂ (Fin N)) → ψ ≠ 0 → Fin K → MeasureTheory.Measure (LF4.KSigma N)) : BlockLudersObligation b post ↔ ∀ (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (i : Fin K), (blockProj b i) ψ ≠ 0 → post ψ hψ0 i = MeasureTheory.Measure.map (ludersRelocation b i) (epistemicMeasure (Projectivization.mk ℂ ψ hψ0))

The obligation is a relocation demand. BlockLudersObligation holds for a post-measurement assignment iff, at every preparation with nonvanishing block weight, the assignment is the pushforward of the preparation under ludersRelocation. What a witness must realise is exactly this pushforward, as the conditioned trace of measure-preserving dynamics.