SigmaLayer/DegenerateLuders: the degenerate case — the problem made precise, the boundary proved

Category: 7-SigmaLayer (the record layer — the open frontier, stated).

What changes at higher rank

At rank one, the Lüders channel is measure-and-reprepare: the post-state is the fixed basis vertex [eᵢ], whatever the preparation, and swap_luders_born delivers exactly that. At higher rank it is not: the Lüders post-state is the normalised projection [Πᵢψ], which depends on the preparation — a superposition inside the block survives, with its internal coherence intact. That ψ-dependence is the entire difficulty, and this module does three things about it:

1. states the obligation precisely (BlockLudersObligation, the §8.3 _statement pattern);
2. proves the boundary: the calibrated-swap witness — any fixed calibration — cannot satisfy it for a block of dimension ≥ 2 (swap_not_blockLuders). The fixed-calibration architecture is refuted for degenerate measurements, as a theorem rather than a scope note;
3. proves the positive half that does survive: the degenerate selector Born weights are right — the block-selector's outcome sectors carry exactly the blockField rates (degenerate_selector_born). Statistics generalise; the update is what does not.

✅ How it was closed (the route, and how the anticipated wall dissolved)

A degenerate witness must relocate the base point [ψ] ↦ [Πᵢψ] — a ψ-dependent target — while preserving measure globally. no_exact_collapse still governs: pointwise across preparations the map loses base dimensions, so the lost data must be stored, not destroyed. The natural construction is the projective join: ℂℙ^{N-1} decomposes (off a null set) as join(ℂℙ^{dᵢ-1}, ℂℙ^{N-dᵢ-1}) — block component, complement component, mixing angle, relative phase — with the update keeping the block component and banking the rest. The wall is the Fubini–Study measure decomposition under the join, which is unformalised geometry. Effort L; recorded in specs/BACKLOG.md.

Corrected 2026-08-04 (codebase audit). The sentence "nothing in this module claims progress" stood long after the construction landed. BlockLudersObligation — defined right here — is inhabited by joinWitness_blockLuders (SigmaLayer/JoinLuders.lean), packaged as degenerateMeasurementClosure (SigmaLayer/JoinClosure.lean). The anticipated wall (an FS measure decomposition under the join) was dissolved rather than crossed: the pair arena simply is the projective join ℙ(ℂ^{N+N}), the update is a permutation unitary on it, and Liouville preservation is FS unitary invariance — no disintegration needed.

References

SigmaLayer/SwapLuders.lean (swap_luders_marginal — whose preparation-independence is exactly what this module turns against the fixed-calibration architecture); SigmaLayer/OutcomeField.lean (blockField — the kinematic form of the degenerate rates this module's degenerate_selector_born makes dynamical); CONVENTIONS.md §8.3 (the _statement discipline); specs/BACKLOG.md (the ★★ row's open item (i)).

The block projector

def CSD.RecordLayer.blockProj {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : EuclideanSpace ℂ (Fin N) →ₗ[ℂ] EuclideanSpace ℂ (Fin N)

The block projector Πᵢ of a degeneracy map b: keep the coordinates whose basis directions belong to outcome i, kill the rest.

Equations

• CSD.RecordLayer.blockProj b i = { toFun := fun (ψ : EuclideanSpace ℂ (Fin N)) => WithLp.toLp 2 fun (j : Fin N) => if b j = i then ψ.ofLp j else 0, map_add' := ⋯, map_smul' := ⋯ }

theorem CSD.RecordLayer.blockProj_apply {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (ψ : EuclideanSpace ℂ (Fin N)) (j : Fin N) : ((blockProj b i) ψ).ofLp j = if b j = i then ψ.ofLp j else 0

theorem CSD.RecordLayer.blockProj_single {N K : ℕ} {b : Fin N → Fin K} {i : Fin K} {j : Fin N} (hb : b j = i) : (blockProj b i) (EuclideanSpace.single j 1) = EuclideanSpace.single j 1

A basis vertex inside the block is fixed by its block projector.

theorem CSD.RecordLayer.single_ne_zero' {N : ℕ} (j : Fin N) : EuclideanSpace.single j 1 ≠ 0

Vertex facts

theorem CSD.RecordLayer.momentMap_vertex {N : ℕ} (j k : Fin N) : LF4.momentMap (vertexPoint j) k = if k = j then 1 else 0

The moment map at a vertex is the vertex's indicator: momentMap [eⱼ] k = δⱼₖ.

theorem CSD.RecordLayer.vertexPoint_injective {N : ℕ} : Function.Injective vertexPoint

Distinct vertices are distinct projective points.

theorem CSD.RecordLayer.epistemicMeasure_injective {N : ℕ} {p q : LF4.CPN N} (h : p ≠ q) : epistemicMeasure p ≠ epistemicMeasure q

Distinct base points give distinct epistemic measures — evaluate on the base singleton.

The block selector, and its dynamical Born weights

noncomputable def CSD.RecordLayer.blockIndex {N K : ℕ} [NeZero N] (b : Fin N → Fin K) : LF4.KSigma N → Fin K

The block selector: the degenerate measurement's outcome index — read the fine-grained basin, then coarse-grain by the degeneracy map.

Equations

• CSD.RecordLayer.blockIndex b x = b (CSD.RecordLayer.basinIndex (CSD.RecordLayer.momentContext N) x)

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

theorem CSD.RecordLayer.degenerate_selector_born {N K : ℕ} [NeZero N] (b : Fin N → Fin K) (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin K) : (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) (blockIndex b ⁻¹' {i}) = ENNReal.ofReal (∑ j : Fin N with b j = i, ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2)

★ The degenerate SELECTOR Born weights. (Renamed in prose 2026-08-04: this is the kinematic selector statement — the epistemicMeasure of a selector fibre — not the protocol-level dynamical Born, which is join_sector_born in JoinClosure.lean. The distinction is the corpus's own, stated in SwapClosure.lean.) The block-selector's outcome-i sector carries exactly the coarse-grained Born weight — the sum of the fine-grained weights over the block. With momentMap_mk_eq_inner_sq this is (blockField b).rate at the preparation: the kinematic blockField of OutcomeField.lean, now realised by a selector. Statistics generalise to degenerate measurements; it is the update that does not (see the no-go below).

The obligation, and the boundary

def CSD.RecordLayer.BlockLudersObligation {N K : ℕ} (b : Fin N → Fin K) (postMarg : (ψ : EuclideanSpace ℂ (Fin N)) → ψ ≠ 0 → Fin K → MeasureTheory.Measure (LF4.KSigma N)) : Prop

What degenerate Lüders demands — statement only, the _statement pattern of CONVENTIONS.md §8.3. A family of post-measurement system marginals implements block-Lüders for the degeneracy map b when, whenever the preparation has a component in block i, the post-outcome-i marginal is the epistemic state of the normalised block projection [Πᵢψ].

★ The right-hand side depends on ψ — that is the entire content, and precisely what a fixed calibration cannot produce. A fixed ray-level calibration cannot produce it (swap_not_blockLuders, below) — but the phase-carrying join witness does: joinWitness_blockLuders (SigmaLayer/JoinLuders.lean) inhabits this for every block structure, including blocks of dimension ≥ 2. (Corrected 2026-08-04 (codebase audit). — this line read "nothing in the corpus inhabits this", which the corpus itself had already contradicted.)

Equations

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

noncomputable def CSD.RecordLayer.readyMeasure (K : ℕ) : MeasureTheory.Measure LF4.KTorus

The apparatus-ready register state: Haar conditioned on the ready arc.

Equations

• CSD.RecordLayer.readyMeasure K = MeasureTheory.volume[|CSD.RecordLayer.readyArc K]

instance CSD.RecordLayer.instIsProbabilityMeasureKTorusReadyMeasure {K : ℕ} : MeasureTheory.IsProbabilityMeasure (readyMeasure K)

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

The swap witness's post-measurement system marginal, for the block selector with calibration ν: prepare [ψ] with a ready register and calibrated bank, run the protocol, condition on the outcome, project to the system.

Equations

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

theorem CSD.RecordLayer.vertex_outcome_pos {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {i : Fin K} {j : Fin N} (hb : b j = i) : ((epistemicMeasure (vertexPoint j)).prod (readyMeasure K)) ((shearProtocol (blockIndex b) ⋯).outcomeSector i) ≠ 0

A vertex preparation inside block i gives outcome i with nonzero probability.

theorem CSD.RecordLayer.swap_not_blockLuders {N K : ℕ} [NeZero N] (b : Fin N → Fin K) {i : Fin K} {j₁ j₂ : Fin N} (hb₁ : b j₁ = i) (hb₂ : b j₂ = i) (hne : j₁ ≠ j₂) (ν : Fin K → MeasureTheory.Measure (LF4.KSigma N)) [∀ (k : Fin K), MeasureTheory.IsProbabilityMeasure (ν k)] : ¬BlockLudersObligation b (swapPostMarg b ν)

★★ The boundary theorem: no fixed calibration implements degenerate Lüders.

For any block of dimension ≥ 2 — two basis directions j₁ ≠ j₂ with b j₁ = b j₂ = i — the calibrated-swap witness fails BlockLudersObligation, whatever the calibration ν.

The proof turns swap_luders_marginal's virtue against it: the swap's post-marginal is the fixed slot state ν i, independent of the preparation, while the obligation at the two vertex preparations demands the two distinct states epistemicMeasure [eⱼ₁] and epistemicMeasure [eⱼ₂]. So the fixed-calibration architecture is refuted for degenerate measurements — as a theorem, not a scope note. A degenerate witness must make the relocation depend on the preparation's block component; see the module docstring for the projective-join route.