SigmaLayer/SwapLuders: the Lüders update as a pushforward theorem

Category: 7-SigmaLayer (the record layer — the collapse theorem).

The chain, and its exact status

The chain is: a record fixes the state (the collapse — the post-measurement marginal is the slot-i calibration), Born gives the next volume fractions at that state, and repeat. Each repetition consumes a fresh bank.

⚠️ Status, and it changed on 2026-09-05 — do not repeat the older wording. Iteration beyond two steps used to be an argument from self-similarity. It is now a theorem: csd_nstep_born (RecordLayer/NStepChain.lean) proves the depth-n law for every sequence of contexts and outcomes, by induction, with csd_nstep_repeatable for non-vacuity. What is still an argument is one level up: that an n-stage arena assembles to give it. two_stage_joint builds that arena for n = 2; the general construction is not done. So the honest split is — the chain law is proved to arbitrary depth given n banks; the chain arena is built for two.

⚠️ The calibration this rests on is a named posit: specs/POSITS.md Posit 5, defined at calibratedBank (RecordLayer/SwapClosure.lean). Scope conditions travel with it — a rank-one computational-basis first measurement (degenerate ones are the open construction, RecordLayer/DegenerateLuders.lean), and the §2a-scoped Hamiltonian origin of the propagator.

The headline

For the calibrated-swap witness, conditioned on outcome i, the post-measurement system marginal IS the slot-i calibration:

map projSys (postMeasure μ_in i) = ν i.

With the CSD instantiation — slots calibrated to epistemicMeasure [eⱼ] — the system state after outcome i is literally epistemicMeasure [eᵢ], the same object the corpus uses for a fresh isolated preparation of eᵢ. Not "concentrates near": equals. Every existing single-measurement theorem then applies to the follow-up unchanged, which is what makes sequential statistics Lüders.

Why this does not contradict the no-collapse results

• shear_base_marginal_unchanged said the shear cannot move the system. The swap stage is what moves it — by relocation, not contraction: the involution swapG exchanges the system's selector coordinate with a bank slot, so Liouville volume is exchanged 1:1 and no_exact_collapse is not in play. What moves is which null slice the epistemic measure occupies.
• After the swap, slot i holds the pre-measurement system state and the depleted fibre — a perfect ontic memory. Collapse is conservation plus relocation; irreversibility enters only when a slot is reset (erasure, priced by collapse_accuracy_bound).

What is proved

• swap_outcomeSector_cylinder — the outcome sector is a base cylinder: the bank plays no part in which outcome occurs.
• cond_prod_cylinder — conditioning a product measure on a first-factor event conditions the first factor. (Reusable; no CSD content.)
• swap_luders_marginal — ★★ the headline above, for arbitrary calibrations ν.
• swap_luders_iff_calibrated — ★ the minimal calibration theorem (F-05 discharge, 2026-08-06): post-marginal = τ ⟺ ν i = τ. The scope note below ("the calibration is a posit") is thereby a theorem in both directions: calibration ⇒ Lüders AND Lüders ⇒ that exact calibration — the update is calibration-encoded, provably, not an artifact of one construction.
• swap_luders_born — the CSD form: the post-outcome-i system marginal is epistemicMeasure [eᵢ], so for any context field c' the follow-up outcome-j probability is c'.rate [eᵢ] j — the Born weight of the collapsed state. Sequential statistics are Lüders.

⚠️ Scope

• Nondegenerate case only. For rank-one projectors the Lüders channel is measure-and-reprepare (a standard quantum-information fact); for degenerate projectors it is not, and this witness does not cover them. That different mechanism has since landed: the boundary is the theorem swap_not_blockLuders (RecordLayer/DegenerateLuders.lean), the witness is joinWitness_blockLuders (RecordLayer/JoinLuders.lean), packaged as degenerateMeasurementClosure (RecordLayer/JoinClosure.lean).
• The calibration is a context-fixed epistemic posit, exactly parallel to pointer-readiness: slot j is prepared in epistemicMeasure [eⱼ], which depends on the measurement basis alone, never on ψ — so it is A7-compatible. Its Liouville-nullity is forced by no_exact_collapse, not chosen for convenience.
• One measurement consumes one bank. Sequential measurements need fresh banks; resetting is erasure and is deliberately outside the protocol. (The composed two-measurement statement, with its fresh second apparatus, is RecordLayer/TwoTimeLuders.lean — Q25, 2026-08-21.)
• The Hamiltonian generation of the swap stage is stated, not formalised — as for the shear.

References

RecordLayer/SwapWitness.lean (the witness); RecordLayer/MeasurementConstraints.lean (no_exact_collapse — why relocation is the only shape); RecordLayer/GlobalBasin.lean (epistemicMeasure, globalBasin_prob); RecordLayer/ShearWitness.lean (shear_base_marginal_unchanged — the defect this repairs).

The outcome sector is a base cylinder

theorem CSD.RecordLayer.swap_outcomeSector_cylinder {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (i : Fin K) : (swapProtocol idx hidx).outcomeSector i = (shearProtocol idx hidx).outcomeSector i ×ˢ Set.univ

The bank plays no part in which outcome occurs: the swap witness's outcome sector is the shear's outcome sector, cylindered over the bank.

theorem CSD.RecordLayer.swap_evolve_sys_on_sector {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (i : Fin K) {x : SwapArena Xsel K} (hx : x ∈ (swapProtocol idx hidx).outcomeSector i) : (swapEvolve idx 0 1 x).1.1 = x.2 i

On the outcome-i sector, the post-evolution system coordinate is bank slot i.

Conditioning a product on a first-factor event

theorem CSD.RecordLayer.cond_prod_cylinder {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.IsProbabilityMeasure ν] (C : Set X) : (μ.prod ν)[|C ×ˢ Set.univ] = μ[|C].prod ν

Conditioning a product measure on a first-factor cylinder conditions the first factor. Reusable, no CSD content.

★★ The Lüders theorem

theorem CSD.RecordLayer.swap_luders_marginal {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (ν : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν j)] (i : Fin K) (hpos : μ12 ((shearProtocol idx hidx).outcomeSector i) ≠ 0) : MeasureTheory.Measure.map (fun (y : SwapArena Xsel K) => y.1.1) ((swapProtocol idx hidx).postMeasure (μ12.prod (MeasureTheory.Measure.pi ν)) i) = ν i

★★ The Lüders update, as a pushforward.

Initial state: system-and-register μ12, bank slots independently calibrated to ν j. Conditioned on outcome i, the post-measurement system marginal is the slot-i calibration — collapse as measure-preserving relocation. The proof is a computation: on the outcome sector the evolved system coordinate is bank slot i, the sector is a base cylinder so conditioning never touches the bank, and evaluation pushes the bank product to its i-th factor.

★ The minimal calibration theorem (F-05 discharge, 2026-08-06)

theorem CSD.RecordLayer.swap_luders_iff_calibrated {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (ν : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν j)] (i : Fin K) (hpos : μ12 ((shearProtocol idx hidx).outcomeSector i) ≠ 0) (τ : MeasureTheory.Measure Xsel) : MeasureTheory.Measure.map (fun (y : SwapArena Xsel K) => y.1.1) ((swapProtocol idx hidx).postMeasure (μ12.prod (MeasureTheory.Measure.pi ν)) i) = τ ↔ ν i = τ

★ The apparatus hypothesis exactly equivalent to Lüders behavior is the calibration. For the swap witness, the post-outcome-i system marginal equals a target state τ iff bank slot i is calibrated to τ:

map projSys (postMeasure (μ12 ⊗ Π ν) i) = τ  ↔  ν i = τ.

The forward direction is swap_luders_marginal (calibration ⇒ Lüders); the converse is what makes the scope note "the Lüders map is encoded in the apparatus calibration, not forced by record creation alone" a THEOREM: no choice of calibration other than ν i = epistemicMeasure [eᵢ] produces the Lüders post-state, and any calibration produces its own post-state. This is the minimal calibration theorem the 2026-08-06 external review (F-05) asked for — the update is calibration-encoded, provably, in both directions.

The CSD form: sequential statistics are Lüders

noncomputable def CSD.RecordLayer.vertexPoint {N : ℕ} (j : Fin N) : LF4.CPN N

The vertex preparation [eⱼ] as a projective point.

Equations

• CSD.RecordLayer.vertexPoint j = Projectivization.mk ℂ (EuclideanSpace.single j 1) ⋯

theorem CSD.RecordLayer.swap_luders_born {N : ℕ} [NeZero N] (μ12 : MeasureTheory.Measure (LF4.KSigma N × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (i : Fin N) (hpos : μ12 ((shearProtocol (basinIndex (momentContext N)) ⋯).outcomeSector i) ≠ 0) (c' : ContextField N) (j : Fin N) : ((swapProtocol (basinIndex (momentContext N)) ⋯).postMeasure (μ12.prod (MeasureTheory.Measure.pi fun (k : Fin N) => epistemicMeasure (vertexPoint k))) i) ((fun (y : SwapArena (LF4.KSigma N) N) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (vertexPoint i) j)

★★ Lüders for CSD: after outcome i, follow-up statistics are the collapsed state's Born weights. With the bank calibrated to the vertex preparations, the post-outcome-i system marginal is epistemicMeasure (vertexPoint i) — so for any context field c', the follow-up outcome-j probability is c'.rate [eᵢ] j. The system state after the measurement behaves, in every subsequent measurement, exactly as a fresh preparation of eᵢ: that is the Lüders update ρ ↦ Πᵢ ρ Πᵢ / Tr(ρ Πᵢ) at rank one.