SigmaLayer/PhaseSlot: the phase-carrying slot — degenerate Lüders, route (ii), brick 2

Category: 7-SigmaLayer (dynamical measurement — the degenerate-Lüders construction, route (ii) of the sharpened wall).

What this proves

BlockCollapse.lean sharpened the wall: the vector-level collapse-with-storage (componentSwap) fails to descend to ray pairs because the product ℙ×ℙ quotient forgets the relative scale. Route (ii) keeps the phase: the slot carries nonzero vectors, and the preparation carries its ontic phase as an epistemically uniform circle orbit. Three pieces:

1. ★ pairSwap — the total, involutive, measurable pair dynamics on nonzero-vector pairs: fire componentSwap exactly when both outputs are nonzero, else the identity. The condition evaluated at a fired image is automatically true (componentSwap is involutive and the inputs were nonzero), which is what makes the conditional map a genuine involution (pairSwap_involutive) — reversibility, hence storage, hence no_exact_collapse respected.
2. phasePrep — the phase-orbit preparation: the uniform measure on {χ(θ)·ψ}, the image of the circle's Haar measure. The ray-level readout of the orbit is the Dirac at [ψ] (readout_phasePrep): the enrichment adds ontic phase, not epistemic content.
3. ★★ phase_slot_block_luders — the degenerate Lüders update, realised: with a fixed block-calibrated slot α (Πᵢα = α, α ≠ 0), the ray-level readout of the post-swap system is exactly δ_{[Πᵢψ]} — the blockLudersObligation_iff_relocation target — for every preparation with nonvanishing block component.

Why this evades swap_not_blockLuders, honestly

The no-go's mechanism was: the full swap makes the post-system the slot's prior content, hence preparation-independent, hence wrong at two in-block vertices. The pair swap here is partial: the block component of the system stays — the dynamics moves system-information into the slot (the complement is stored), not slot-content into the system. The slot calibration is still fixed (Measure.dirac); preparation-dependence of the post-state comes from the preparation itself. No contradiction with the no-go: its premise fails for a partial swap. And the partial swap is only well-defined because the arena is phase-enriched — on rays it was ill-defined, which is exactly what the sharpened wall said.

⚠️ Honest scope — what brick 3 still owes

This is the state-update core, not yet the full protocol: (a) the register/sector plumbing (a MeasurementProtocol on the phase-enriched arena with the record trigger, mirroring SwapWitness); (b) Liouville preservation on the enriched arena — pairSwap preserves summed norms (componentSwap_norm_sum), so the natural invariant reference measure is a unitarily-invariant one (e.g. Gaussian) on the doubled space; formalising that invariance is the recorded remaining work (specs/BACKLOG.md, effort M). Nothing here claims either.

Corrected 2026-08-04 (codebase audit). Both debts were paid the same day (2026-08-02), and (b) did not need the Gaussian route: the phase-enriched pair arena is the projective join, so Liouville preservation is FS unitary invariance (joinSwap_measurePreserving, SigmaLayer/JoinArena.lean), and the protocol plumbing (a) is SigmaLayer/JoinProtocol.lean. The paragraph above is kept as the construction record. The obligation is discharged at the level BlockLudersObligation actually demands — the post-state as a measure — for the canonical phase-orbit preparations and fixed calibration.

References

SigmaLayer/BlockCollapse.lean (componentSwap, the sharpened wall, brick 1); SigmaLayer/DegenerateLuders.lean (swap_not_blockLuders — the boundary this evades, BlockLudersObligation); SigmaLayer/MeasurementConstraints.lean (no_exact_collapse); Mathlib/LinearAlgebra/Projectivization/MeasureSpace.lean (measurable_mk'); Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean (AddCircle.toCircle); specs/BACKLOG.md.

The total conditional pair swap

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

The firing condition: both componentSwap outputs are nonzero.

Equations

• CSD.RecordLayer.pairSwapCond b i p = ((CSD.RecordLayer.componentSwap b i p).1 ≠ 0 ∧ (CSD.RecordLayer.componentSwap b i p).2 ≠ 0)

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

The total pair swap on nonzero-vector pairs: fire the component swap exactly when both outputs are nonzero, else the identity.

Equations

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

theorem CSD.RecordLayer.pairSwap_of_cond {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {p : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 } × { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }} (h : pairSwapCond b i (↑p.1, ↑p.2)) : ↑(pairSwap b i p).1 = (componentSwap b i (↑p.1, ↑p.2)).1 ∧ ↑(pairSwap b i p).2 = (componentSwap b i (↑p.1, ↑p.2)).2

The fired-branch values.

theorem CSD.RecordLayer.pairSwap_of_not_cond {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {p : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 } × { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }} (h : ¬pairSwapCond b i (↑p.1, ↑p.2)) : pairSwap b i p = p

The unfired-branch value.

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

★ The pair swap is a genuine involution — the reversibility that makes the collapse a relocation-with-storage rather than a contraction. The key: at a fired image the firing condition is automatically satisfied, because componentSwap is involutive and the original inputs were nonzero.

theorem CSD.RecordLayer.pairSwapCond_of_calibrated {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ α : EuclideanSpace ℂ (Fin N)} (hPi : (blockProj b i) ψ ≠ 0) (hα : (blockProj b i) α = α) (hα0 : α ≠ 0) : pairSwapCond b i (ψ, α)

The firing condition holds in the calibrated-measurement situation: nonzero block component, block-supported nonzero slot.

theorem CSD.RecordLayer.pairSwap_fst_calibrated {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ α : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hPi : (blockProj b i) ψ ≠ 0) (hα : (blockProj b i) α = α) (hα0 : α ≠ 0) : ↑(pairSwap b i (⟨ψ, hψ0⟩, ⟨α, hα0⟩)).1 = (blockProj b i) ψ

The calibrated fired value: the post-swap system vector is exactly the Lüders-collapsed Πᵢψ.

theorem CSD.RecordLayer.continuous_componentSwap {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Continuous (componentSwap b i)

The component swap is continuous (a linear coordinate exchange).

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

The pair swap is measurable.

The phase-orbit preparation

noncomputable def CSD.RecordLayer.phaseVec {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (θ : AddCircle 1) : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }

The phase orbit of a preparation: θ ↦ χ(θ)·ψ, a nonzero vector for every phase.

Equations

• CSD.RecordLayer.phaseVec ψ hψ0 θ = ⟨↑θ.toCircle • ψ, ⋯⟩

theorem CSD.RecordLayer.measurable_phaseVec {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : Measurable (phaseVec ψ hψ0)

noncomputable def CSD.RecordLayer.phasePrep {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : MeasureTheory.Measure { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }

The phase-orbit preparation: uniform over the ontic phase, Dirac in every other respect.

Equations

• CSD.RecordLayer.phasePrep ψ hψ0 = MeasureTheory.Measure.map (CSD.RecordLayer.phaseVec ψ hψ0) MeasureTheory.volume

instance CSD.RecordLayer.instIsProbabilityMeasureSubtypeEuclideanSpaceComplexFinNeOfNatPhasePrep {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : MeasureTheory.IsProbabilityMeasure (phasePrep ψ hψ0)

theorem CSD.RecordLayer.mk'_phaseVec {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (θ : AddCircle 1) : Projectivization.mk' ℂ (phaseVec ψ hψ0 θ) = Projectivization.mk ℂ ψ hψ0

Every point of the phase orbit reads out to the same ray.

theorem CSD.RecordLayer.readout_phasePrep {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) : MeasureTheory.Measure.map (Projectivization.mk' ℂ) (phasePrep ψ hψ0) = MeasureTheory.Measure.dirac (Projectivization.mk ℂ ψ hψ0)

The enrichment adds ontic phase, not epistemic content: the ray-level readout of the phase orbit is the Dirac at the ray.

The degenerate Lüders update, realised

theorem CSD.RecordLayer.phase_slot_block_luders {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (h : (blockProj b i) ψ ≠ 0) {α : EuclideanSpace ℂ (Fin N)} (hα : (blockProj b i) α = α) (hα0 : α ≠ 0) : MeasureTheory.Measure.map (fun (p : { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 } × { w : EuclideanSpace ℂ (Fin N) // w ≠ 0 }) => Projectivization.mk' ℂ (pairSwap b i p).1) ((phasePrep ψ hψ0).prod (MeasureTheory.Measure.dirac ⟨α, hα0⟩)) = MeasureTheory.Measure.dirac (Projectivization.mk ℂ ((blockProj b i) ψ) h)

★★ The degenerate Lüders update, realised by the phase-carrying slot. Prepare the phase orbit of ψ; calibrate the slot with a fixed block-supported α; fire the pair swap; read out the system ray. The result is exactly δ_{[Πᵢψ]} — the target blockLudersObligation_iff_relocation demands — for every preparation with nonvanishing block-i component. A fixed calibration achieves a preparation-dependent post-state because the partial swap moves system-information into the slot, not slot-content into the system; swap_not_blockLuders's premise fails, and its conclusion is evaded.