SigmaLayer/RelocationObstruction: the collapse stroke is not generated

Category: dynamical measurement — the negative half of the Hamiltonian-origin question.

PointerGeneration.lean closed the record-creating half: rampedU_schrodinger exhibits the smooth witness's stroke as the flow of an explicit Hermitian generator, so record creation is dynamics rather than a map wearing a dynamical label. The collapse half was left as pointerRelocate, a case split on the readout, proved measure-preserving by a partition argument. This module shows that gap cannot be closed as posed: the bank-swap relocation is not the time-one map of any flow, and neither is the obvious non-permutation alternative.

The two horns

• ★★ pointerBankSwap_not_flow_time_one — the relocation used on the record cylinders exchanges the system factor with bank slot j. Embed a circle in the system's torus coordinate; after the exchange that coordinate reads slot j, which the embedding held constant. So the exchange collapses a section onto a non-contractible space, and not_isFlowTimeOne_of_section_collapsed applies. Note this is not the flux obstruction of PiecewiseHamiltonian.lean: flux obstructs a symplectomorphism within the identity component, whereas the exchange never reaches that component, and the H¹(ℂℙ^K) = 0 escape that saved the record stroke does not help because the obstruction lives in the bank's product structure.
• ★ pointerImprint_not_injective — the alternative that avoids permuting factors, writing the system into a slot rather than exchanging with it, is not injective, so it is not a homeomorphism, so it is not a flow map either.

What this does and does not say

It says the swap architecture's collapse stroke cannot become dynamics, and that the naive repair fails for an independent reason. Together with swap_not_blockLuders (DegenerateLuders.lean), which shows the same architecture cannot do degenerate Lüders for any fixed calibration, the swap route is a witness that cannot be generated. It does not say collapse is undynamical in general: a generated relocation must be a bijection that is not a factor exchange, which points at the join and phase-slot routes (JoinLuders.lean, PhaseSlot.lean), where state-dependence is produced by the dynamics rather than by permuting coordinates.

It also constrains record proliferation: carrier maps that relocate a record by permuting factors inherit the first horn, and imprint-style copies inherit the second.

References

SigmaLayer/PointerLuders.lean (pointerBankSwap, pointerRelocate); SigmaLayer/PointerGeneration.lean (rampedU_schrodinger, the positive half); SigmaLayer/PiecewiseHamiltonian.lean (the flux obstruction this is not); SigmaLayer/DegenerateLuders.lean (swap_not_blockLuders); Mathlib/Topology/Homotopy/FactorExchangeObstruction.lean; Mathlib/Topology/Homotopy/CircleFundamentalGroup.lean; specs/BACKLOG.md.

The exchange is continuous

theorem CSD.RecordLayer.continuous_pointerBankSwap {N : ℕ} (j : Fin N) : Continuous (pointerBankSwap j)

The bank swap is continuous: it permutes coordinates.

def CSD.RecordLayer.bankSwapCM {N : ℕ} (j : Fin N) : C(PointerLudersArena N, PointerLudersArena N)

The bank swap as a bundled continuous map.

Equations

• CSD.RecordLayer.bankSwapCM j = { toFun := CSD.RecordLayer.pointerBankSwap j, continuous_toFun := ⋯ }

The section a factor exchange collapses

noncomputable def CSD.RecordLayer.torusSection {N : ℕ} (p₀ : LF4.CPN N) (q₀ : Pointer N) : C(AddCircle 1, PointerLudersArena N)

Embed a circle in the system's first torus angle, holding every other coordinate fixed. In particular every bank slot is held at a constant point.

Equations

• CSD.RecordLayer.torusSection p₀ q₀ = { toFun := fun (θ : AddCircle 1) => (((p₀, θ, 0), q₀), fun (x : Fin N) => (p₀, 0, 0)), continuous_toFun := ⋯ }

def CSD.RecordLayer.torusReadout {N : ℕ} : C(PointerLudersArena N, AddCircle 1)

Read the system's first torus angle.

Equations

• CSD.RecordLayer.torusReadout = { toFun := fun (y : CSD.RecordLayer.PointerLudersArena N) => y.1.1.2.1, continuous_toFun := ⋯ }

theorem CSD.RecordLayer.torusReadout_comp_section {N : ℕ} (p₀ : LF4.CPN N) (q₀ : Pointer N) : torusReadout.comp (torusSection p₀ q₀) = ContinuousMap.id (AddCircle 1)

theorem CSD.RecordLayer.torusReadout_comp_swap_comp_section {N : ℕ} (j : Fin N) (p₀ : LF4.CPN N) (q₀ : Pointer N) : torusReadout.comp ((bankSwapCM j).comp (torusSection p₀ q₀)) = ContinuousMap.const (AddCircle 1) 0

After the exchange the readout reports slot j, which the section held constant. This is the collapse the obstruction consumes.

Horn one: the exchange is not homotopic to the identity

theorem CSD.RecordLayer.pointerBankSwap_not_homotopic_id {N : ℕ} (j : Fin N) (p₀ : LF4.CPN N) (q₀ : Pointer N) : ¬(bankSwapCM j).Homotopic (ContinuousMap.id (PointerLudersArena N))

★★ The bank swap is not homotopic to the identity. It collapses the circle section of torusSection onto a point, and the circle is not contractible.

theorem CSD.RecordLayer.pointerBankSwap_not_flow_time_one {N : ℕ} (j : Fin N) (p₀ : LF4.CPN N) (q₀ : Pointer N) : ¬∃ (φ : C(↑unitInterval × PointerLudersArena N, PointerLudersArena N)), (∀ (y : PointerLudersArena N), φ (0, y) = pointerBankSwap j y) ∧ ∀ (y : PointerLudersArena N), φ (1, y) = y

★★ The bank-swap relocation is not the time-one map of any flow.

So the collapse stroke of the swap architecture cannot be generated, in the sense that the record-creating stroke is generated (rampedU_schrodinger). Any jointly continuous family joining the identity to the relocation would be a homotopy, and there is none.

Horn two: the non-permutation alternative is not injective

def CSD.RecordLayer.pointerImprint {N : ℕ} (j : Fin N) (y : PointerLudersArena N) : PointerLudersArena N

The imprint: copy the system into bank slot j without removing it. This is the natural way to broadcast a record without permuting factors.

Equations

• CSD.RecordLayer.pointerImprint j y = ((y.1.1, y.1.2), Function.update y.2 j y.1.1)

theorem CSD.RecordLayer.pointerImprint_not_injective {N : ℕ} (j : Fin N) (q₀ : Pointer N) {a b : LF4.KSigma N} (hab : a ≠ b) : ¬Function.Injective (pointerImprint j)

★ The imprint is not injective, hence not a homeomorphism, hence not the time-one map of any flow. Two arena points differing only in slot j are identified, because the imprint overwrites that slot.

theorem CSD.RecordLayer.pointerImprint_not_homeomorph {N : ℕ} (j : Fin N) (q₀ : Pointer N) {a b : LF4.KSigma N} (hab : a ≠ b) : ¬∃ (e : PointerLudersArena N ≃ₜ PointerLudersArena N), ∀ (y : PointerLudersArena N), e y = pointerImprint j y

★ No flow realises the imprint at time one, since a flow map is a homeomorphism and the imprint is not injective.