SigmaLayer/SwapWitness: the calibrated-swap witness — collapse as relocation

Category: 7-SigmaLayer (the record layer — the second dynamical witness).

Why a second witness

shear_base_marginal_unchanged proved the shear cannot implement the Lüders update: the property that makes its correlation proof work — no back-reaction on the selector — is exactly the property that prevents collapse. And the collapse no-gos (MeasurementConstraints.lean) show the repair cannot be a contraction: no_exact_collapse kills any measure-preserving map sending a positive-measure set of states onto the (null) basis vertices, and collapse_accuracy_bound prices approximate contraction in ready-state improbability. The only shape left is relocation: a globally measure-preserving bijection that permutes null slices, moving the epistemic Dirac from [ψ] to [eᵢ] without shrinking anything.

The construction

Enlarge the arena with an ancilla bank: K reference cells inside the apparatus, one per outcome, each a full copy of the selector space —

SwapArena Xsel K = (Xsel × T²_R) × (Fin K → Xsel).

The propagator is swapG ∘ (lifted shear): run the shear, then — triggered by the record, not by the selector — exchange the system's selector coordinate with bank slot j when the pointer sits in arc j.

★ The record-trigger is forced, not stylistic. The pieces {register ∈ arc j} are invariant under the slot-j swap because the swap never touches the register — which is what makes swapG a piecewise map with invariant pieces, hence measure-preserving (measurePreserving_of_partition). Conditioning on the selector index instead would move the very coordinate the pieces are defined by, and the bookkeeping fails. The physically right causal story ("the written pointer back-acts on the system") coincides with the only version whose measure theory works.

★ The crossing propagator is symmetric, correcting the design as reviewed. The proposal defined the swap to fire on forward crossings of the readout time only; the two-time composition law Φ_{t→u} ∘ Φ_{s→t} = Φ_{s→u} is quantified over all time triples, and a forward-only flag fails it on non-monotone triples (go past readout, come back: the swap is applied and never undone). Because swapG is an involution, the repair is to fire it on crossings in either direction — G ∘ shear forward, shear ∘ G backward — and all eight side-of-readout cases then close, using G² = id and the shear being frozen right of readout.

What is proved

• swapG — the record-triggered bank swap; involutive, measurable, measure-preserving.
• swapProtocol — a genuine MeasurementProtocol on the enlarged arena.
• swapEvolve_measurePreserving — the full propagator preserves the Liouville measure at every time pair. It is a dynamics.
• swap_correlates — CorrelatesOn discharged: the correlation is inherited from the shear, since the swap never moves the register.
• swap_pointerInvariant — PointerInvariantOn discharged: after readout the propagator is the identity.
• swapG_register, swapEvolve_cross_fwd, … — the algebra the Lüders module consumes.

⚠️ Scope

• The Lüders theorem is NOT in this file — see SwapLuders.lean for the post-measurement marginal. This file supplies the witness and its protocol properties.
• The Hamiltonian generation is stated, not formalised, exactly as for the shear: the swap stage is the ontic analogue of a controlled kick applied at the readout time; the arena-level Hamiltonian statement is R-016′ (the ℂℙⁿ API exists since 2026-09-08, the arena's product form is not built; BACKLOG.md ▶ OUTSTANDING), so no claim is made that this propagator arises from an H_int.
• The bank is consumed: one measurement uses one calibration of the slots. Resetting a slot is erasure, with the Landauer cost collapse_accuracy_bound prices; the reset is deliberately outside the protocol.

References

RecordLayer/ShearWitness.lean (the shear this composes with); RecordLayer/MeasurementConstraints.lean (no_exact_collapse, collapse_accuracy_bound — why relocation is the only shape); Mathlib/MeasureTheory/PiecewisePreserving.lean (swapSlot, measurePreserving_of_partition); RecordLayer/MeasurementProtocol.lean.

The arena

@[reducible, inline]

abbrev CSD.RecordLayer.SwapArena (Xsel : Type u_2) (K : ℕ) : Type u_2

The swap arena: selector × register, together with the ancilla bank — one reference cell per outcome, each a full copy of the selector space.

Equations

• CSD.RecordLayer.SwapArena Xsel K = ((Xsel × CSD.LF4.KTorus) × (Fin K → Xsel))

Classifying the register

theorem CSD.RecordLayer.pointerArc_pairwiseDisjoint {K : ℕ} : Pairwise (Function.onFun Disjoint (pointerArc K))

noncomputable def CSD.RecordLayer.arcIndex (K : ℕ) (r : LF4.KTorus) : Option (Fin K)

Which pointer arc the register occupies, if any.

Equations

• CSD.RecordLayer.arcIndex K r = if h : ∃ (j : Fin K), r ∈ CSD.RecordLayer.pointerArc K j then some h.choose else none

theorem CSD.RecordLayer.arcIndex_eq_some_iff {K : ℕ} (r : LF4.KTorus) (j : Fin K) : arcIndex K r = some j ↔ r ∈ pointerArc K j

theorem CSD.RecordLayer.arcIndex_eq_none_iff {K : ℕ} (r : LF4.KTorus) : arcIndex K r = none ↔ ∀ (j : Fin K), r ∉ pointerArc K j

The record-triggered bank swap

def CSD.RecordLayer.bankSwap {Xsel : Type u_1} {K : ℕ} (j : Fin K) (x : SwapArena Xsel K) : SwapArena Xsel K

The slot-j swap on the arena: exchange the system's selector coordinate with bank slot j. The register is untouched.

Equations

• CSD.RecordLayer.bankSwap j x = ((x.2 j, x.1.2), Function.update x.2 j x.1.1)

noncomputable def CSD.RecordLayer.swapG {Xsel : Type u_1} {K : ℕ} : SwapArena Xsel K → SwapArena Xsel K

The record-triggered swap G: if the pointer displays outcome j, exchange the system with bank slot j; otherwise do nothing. ★ Triggered by the record — the register arc — not by the selector index; see the module docstring for why the measure theory forces this.

Equations

• CSD.RecordLayer.swapG x = match CSD.RecordLayer.arcIndex K x.1.2 with | none => x | some j => CSD.RecordLayer.bankSwap j x

theorem CSD.RecordLayer.swapG_register {Xsel : Type u_1} {K : ℕ} (x : SwapArena Xsel K) : (swapG x).1.2 = x.1.2

The swap never moves the register.

theorem CSD.RecordLayer.swapG_of_mem {Xsel : Type u_1} {K : ℕ} {x : SwapArena Xsel K} {j : Fin K} (h : x.1.2 ∈ pointerArc K j) : swapG x = bankSwap j x

theorem CSD.RecordLayer.swapG_of_none {Xsel : Type u_1} {K : ℕ} {x : SwapArena Xsel K} (h : ∀ (j : Fin K), x.1.2 ∉ pointerArc K j) : swapG x = x

theorem CSD.RecordLayer.swapG_swapG {Xsel : Type u_1} {K : ℕ} (x : SwapArena Xsel K) : swapG (swapG x) = x

G is an involution — which is what lets the crossing propagator fire it symmetrically in both time directions and still satisfy the two-time composition law.

G preserves the measure

noncomputable def CSD.RecordLayer.swapMeasure {Xsel : Type u_1} [MeasurableSpace Xsel] (μs : MeasureTheory.Measure Xsel) (K : ℕ) : MeasureTheory.Measure (SwapArena Xsel K)

The Liouville measure of the swap arena: selector ⊗ register-Haar ⊗ bank.

Equations

• CSD.RecordLayer.swapMeasure μs K = (μs.prod MeasureTheory.volume).prod (MeasureTheory.Measure.pi fun (x : Fin K) => μs)

instance CSD.RecordLayer.instIsProbabilityMeasureSwapArenaSwapMeasure {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (μs : MeasureTheory.Measure Xsel) [MeasureTheory.IsProbabilityMeasure μs] : MeasureTheory.IsProbabilityMeasure (swapMeasure μs K)

theorem CSD.RecordLayer.measurePreserving_bankSwap {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (μs : MeasureTheory.Measure Xsel) [MeasureTheory.IsProbabilityMeasure μs] (j : Fin K) : MeasureTheory.MeasurePreserving (bankSwap j) (swapMeasure μs K) (swapMeasure μs K)

The slot swap preserves the arena measure — by conjugating swapSlot through the shuffle that brings the register out front.

theorem CSD.RecordLayer.measurable_bankSwap {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (j : Fin K) : Measurable (bankSwap j)

def CSD.RecordLayer.arcPiece {Xsel : Type u_1} (K : ℕ) (o : Option (Fin K)) : Set (SwapArena Xsel K)

The pieces of the swap: which arc the register occupies (or none).

Equations

• CSD.RecordLayer.arcPiece K none = {x : CSD.RecordLayer.SwapArena Xsel K | ∀ (j : Fin K), x.1.2 ∉ CSD.RecordLayer.pointerArc K j}
• CSD.RecordLayer.arcPiece K (some j) = {x : CSD.RecordLayer.SwapArena Xsel K | x.1.2 ∈ CSD.RecordLayer.pointerArc K j}

theorem CSD.RecordLayer.measurableSet_arcPiece {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (o : Option (Fin K)) : MeasurableSet (arcPiece K o)

theorem CSD.RecordLayer.arcPiece_disjoint {Xsel : Type u_1} {K : ℕ} : Pairwise (Function.onFun Disjoint (arcPiece K))

theorem CSD.RecordLayer.arcPiece_cover {Xsel : Type u_1} {K : ℕ} : ⋃ (o : Option (Fin K)), arcPiece K o = Set.univ

theorem CSD.RecordLayer.swapG_agree {Xsel : Type u_1} {K : ℕ} (o : Option (Fin K)) (x : SwapArena Xsel K) (hx : x ∈ arcPiece K o) : swapG x = (match (motive := Option (Fin K) → SwapArena Xsel K → SwapArena Xsel K) o with | none => id | some j => bankSwap j) x

theorem CSD.RecordLayer.measurable_swapG {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} : Measurable swapG

theorem CSD.RecordLayer.measurePreserving_swapG {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (μs : MeasureTheory.Measure Xsel) [MeasureTheory.IsProbabilityMeasure μs] : MeasureTheory.MeasurePreserving swapG (swapMeasure μs K) (swapMeasure μs K)

★ The record-triggered swap preserves the Liouville measure. Each piece's map preserves the measure, and each piece is invariant under its own map — because the swap never moves the register, which is the coordinate the pieces are defined by. This is where the record-trigger design choice pays.

The crossing propagator

noncomputable def CSD.RecordLayer.liftShear {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t : SigmaLayer.OnticTime) : SwapArena Xsel K → SwapArena Xsel K

The shear, lifted to the arena: it acts on selector × register and leaves the bank alone.

Equations

• CSD.RecordLayer.liftShear idx s t = Prod.map (CSD.RecordLayer.shearEvolve idx s t) id

theorem CSD.RecordLayer.liftShear_comp {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t u : SigmaLayer.OnticTime) (x : SwapArena Xsel K) : liftShear idx t u (liftShear idx s t x) = liftShear idx s u x

theorem CSD.RecordLayer.liftShear_frozen {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t : SigmaLayer.OnticTime} (hs : 1 ≤ s) (ht : 1 ≤ t) (x : SwapArena Xsel K) : liftShear idx s t x = x

theorem CSD.RecordLayer.liftShear_congr {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t t' : SigmaLayer.OnticTime} (h : elapsed t = elapsed t') (x : SwapArena Xsel K) : liftShear idx s t x = liftShear idx s t' x

theorem CSD.RecordLayer.liftShear_congr_left {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s s' t : SigmaLayer.OnticTime} (h : elapsed s = elapsed s') (x : SwapArena Xsel K) : liftShear idx s t x = liftShear idx s' t x

noncomputable def CSD.RecordLayer.swapEvolve {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t : SigmaLayer.OnticTime) : SwapArena Xsel K → SwapArena Xsel K

The swap propagator: run the shear; fire the record-triggered swap G when the time window crosses the readout time 1 — in either direction, G being an involution.

★ The symmetric firing is a correction to the reviewed design, which fired forward only: the two-time law Φ_{t→u} ∘ Φ_{s→t} = Φ_{s→u} is quantified over all triples, and a forward-only flag fails on go-past-and-come-back paths.

Equations

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

theorem CSD.RecordLayer.swapEvolve_fwd {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t : SigmaLayer.OnticTime} (hs : s < 1) (ht : 1 ≤ t) : swapEvolve idx s t = swapG ∘ liftShear idx s t

theorem CSD.RecordLayer.swapEvolve_bwd {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t : SigmaLayer.OnticTime} (ht : t < 1) (hs : 1 ≤ s) : swapEvolve idx s t = liftShear idx s t ∘ swapG

theorem CSD.RecordLayer.swapEvolve_lo {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t : SigmaLayer.OnticTime} (hs : s < 1) (ht : t < 1) : swapEvolve idx s t = liftShear idx s t

theorem CSD.RecordLayer.swapEvolve_hi {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t : SigmaLayer.OnticTime} (hs : 1 ≤ s) (ht : 1 ≤ t) : swapEvolve idx s t = liftShear idx s t

theorem CSD.RecordLayer.swapEvolve_comp {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t u : SigmaLayer.OnticTime) : swapEvolve idx t u ∘ swapEvolve idx s t = swapEvolve idx s u

The two-time composition law, all eight side-of-readout cases. Closes on G² = id and the shear being frozen right of readout.

The protocol

theorem CSD.RecordLayer.measurable_liftShear {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (s t : SigmaLayer.OnticTime) : Measurable (liftShear idx s t)

theorem CSD.RecordLayer.measurable_swapEvolve {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (s t : SigmaLayer.OnticTime) : Measurable (swapEvolve idx s t)

noncomputable def CSD.RecordLayer.swapProtocol {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) : MeasurementProtocol (SwapArena Xsel K) K

The calibrated-swap witness as a MeasurementProtocol. Ready and pointer regions are read off the register, exactly as for the shear.

Equations

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

theorem CSD.RecordLayer.swapEvolve_measurePreserving {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (μs : MeasureTheory.Measure Xsel) [MeasureTheory.IsProbabilityMeasure μs] (idx : Xsel → Fin K) (hidx : Measurable idx) (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (swapEvolve idx s t) (swapMeasure μs K) (swapMeasure μs K)

The propagator preserves the Liouville measure at every time pair — shear stage and swap stage separately, composed per branch. It is a dynamics, not a relabelling.

The hypotheses discharged

def CSD.RecordLayer.selReadyBank {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (i : Fin K) : Set (SwapArena Xsel K)

The selector-and-ready sector on the arena: the bank is unconstrained.

Equations

• CSD.RecordLayer.selReadyBank idx i = {x : CSD.RecordLayer.SwapArena Xsel K | idx x.1.1 = i ∧ x.1.2 ∈ CSD.RecordLayer.readyArc K}

theorem CSD.RecordLayer.swap_correlates {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) : (swapProtocol idx hidx).CorrelatesOn (selReadyBank idx)

★ CorrelatesOn discharged for the swap witness. Inherited from the shear: the swap stage never moves the register, so the outcome sector is read off the sheared register exactly as before.

theorem CSD.RecordLayer.swap_pointerInvariant {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) : (swapProtocol idx hidx).PointerInvariantOn

★ PointerInvariantOn discharged for the swap witness: right of readout, no crossing fires and the shear is frozen, so the propagator is the identity.