SigmaLayer/PointerLudersMarginal: the smooth horn's Lüders theorem (B3b, brick 2)

Category: dynamical measurement — specs/BACKLOG.md B3b, second (final) brick.

Glossary: https://glossary.constraintsurfacedynamics.com/luders-rule/ Plain-language, CSD-role and formal statements of the Luders rule, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

What brick 1 owed, delivered here

Brick 1 (PointerLuders.lean) built the composed arena (Σ × ℂℙ^N) × bank and defined the two-stroke composite — smooth record stroke, then record-triggered relocation — while explicitly not claiming two things. Both are proved here:

• ★ pointerRelocate_measurePreserving — the piecewise invariance. The relocation is a case split on the readout, so its invariance is the partition argument the torus witness used for swapG, with record cylinders in place of register arcs: the arena splits into the no-record piece (where the relocation is the identity) and one record cylinder per outcome (where it is the slot swap, measure-preserving by brick 1, and fixes its own piece because the relocation never moves the pointer). measurePreserving_of_partition does the rest. Corollary ★ pointerLudersStroke_measurePreserving: the whole two-stroke composite conserves Liouville measure — collapse as relocation, not contraction, on the smooth horn too.
• ★★ pointer_luders_marginal — the conditioned post-measurement marginal, the actual Lüders theorem: conditioned on the outcome-i sector, the post-stroke system marginal is the slot-i calibration, exactly the swap witness's headline (swap_luders_marginal) with the trigger read off the pointer's record region instead of a torus arc. The proof has the same three moves: the sector is a base cylinder (the bank plays no part in which outcome occurs), so conditioning never touches the bank (cond_prod_cylinder); on the sector the post-stroke system coordinate is bank slot i; and evaluation pushes the bank product to its i-th factor (Measure.map_eval_pi').
• ★ pointer_luders_born — the CSD form: slots calibrated to the vertex preparations make every follow-up outcome-j probability c'.rate [eᵢ] j — Born of the collapsed state, for any context field.
• ★★ pointer_luders_born_prep — the payoff, on the witness's own preparation pointerPrep: whenever 2ε < rate i, the ε-Born lower bound makes the conditioning non-vacuous, so the smooth witness now delivers records (ε-Born, brick 4b/B3a) and a Lüders update (this module) on one arena. B3b closes.

Why this does not contradict the no-collapse results

pointerEvolve_base_marginal_unchanged still holds: the smooth stroke does not collapse. The update is the second stroke, and it moves the system by relocation — the slot swap exchanges volume 1:1 (pointerRelocate_measurePreserving), so no_exact_collapse is not in play. After the swap, slot i holds the pre-measurement system state: a perfect ontic memory, with irreversibility priced only at erasure (collapse_accuracy_bound).

⚠️ Honest scope

• Rank-one / nondegenerate only, exactly as for the swap witness: the bank calibration is one preparation per outcome. Degenerate blocks live on the join witness (JoinClosure), not here.
• The calibration is a context-fixed epistemic posit (epistemicMeasure (vertexPoint k) depends on the basis alone, never on ψ) — A7-compatible, same status as the swap's.
• One measurement consumes one bank; resetting is erasure, outside the protocol.
• The two-stroke composite is not packaged as a MeasurementProtocol: the relocation is a triggered map, not a flow, so the composite has no two-time law to offer. The sector conditioned on is the smooth protocol's own outcome sector, cylindered over the bank — which is also the honest statement that the bank plays no part in outcome selection. Realising the relocation as a Hamiltonian stroke is the same recorded extension it is for the swap witness.
• The ε-horn price stands: the sector mass is bracketed, not pinned (pointer_born_lower/_upper), and pointer_luders_born_prep needs 2ε < rate i. The conditioned marginal, by contrast, is exact — the ε lives in which outcome occurs, not in the post-measurement state.

References

specs/BACKLOG.md B3b; SigmaLayer/PointerLuders.lean (brick 1 — arena, relocation, slot swap); SigmaLayer/SwapLuders.lean (swap_luders_marginal, cond_prod_cylinder — the torus-triggered original whose shape this transports); Mathlib/MeasureTheory/ PiecewisePreserving.lean (measurePreserving_of_partition, Measure.map_eval_pi'); SigmaLayer/PointerBorn.lean (pointerPrep, pointer_born_lower — the non-vacuity supply); SigmaLayer/GlobalBasin.lean (epistemicMeasure, globalBasin_prob); SigmaLayer/PointerGeneration.lean (pointerEvolve_base_marginal_unchanged — why the update needed a second stroke at all).

The relocation partition: record cylinders and the no-record piece

def CSD.RecordLayer.relocPiece (N : ℕ) : Option (Fin N) → Set (PointerLudersArena N)

The relocation's partition piece for label k: the record cylinder for some j, the no-record set for none.

Equations

• CSD.RecordLayer.relocPiece N none = (⋃ (j : Fin N), {y : CSD.RecordLayer.PointerLudersArena N | y.1.2 ∈ CSD.RecordLayer.recordRegion j})ᶜ
• CSD.RecordLayer.relocPiece N (some j) = {y : CSD.RecordLayer.PointerLudersArena N | y.1.2 ∈ CSD.RecordLayer.recordRegion j}

def CSD.RecordLayer.relocMap (N : ℕ) : Option (Fin N) → PointerLudersArena N → PointerLudersArena N

The relocation's piece map for label k: the slot swap on a record cylinder, the identity on the no-record piece.

Equations

• CSD.RecordLayer.relocMap N none = id
• CSD.RecordLayer.relocMap N (some j) = CSD.RecordLayer.pointerBankSwap j

theorem CSD.RecordLayer.measurableSet_relocPiece {N : ℕ} (k : Option (Fin N)) : MeasurableSet (relocPiece N k)

theorem CSD.RecordLayer.relocPiece_pairwiseDisjoint {N : ℕ} : Pairwise (Function.onFun Disjoint (relocPiece N))

theorem CSD.RecordLayer.relocPiece_cover {N : ℕ} : ⋃ (k : Option (Fin N)), relocPiece N k = Set.univ

theorem CSD.RecordLayer.pointerIndex_eq_none {N : ℕ} {q : Pointer N} (h : ¬∃ (j : Fin N), q ∈ recordRegion j) : pointerIndex q = none

The readout is none off every record region.

theorem CSD.RecordLayer.pointerRelocate_of_noRecord {N : ℕ} {y : PointerLudersArena N} (h : ¬∃ (j : Fin N), y.1.2 ∈ recordRegion j) : pointerRelocate y = y

Off every record region, the relocation does nothing.

theorem CSD.RecordLayer.pointerRelocate_agree {N : ℕ} (k : Option (Fin N)) (y : PointerLudersArena N) : y ∈ relocPiece N k → pointerRelocate y = relocMap N k y

The relocation agrees with the piece map on each piece.

theorem CSD.RecordLayer.relocMap_fixes_piece {N : ℕ} (k : Option (Fin N)) : relocMap N k ⁻¹' relocPiece N k = relocPiece N k

Each piece map fixes its own piece as a preimage — the slot swap never moves the pointer, so a record cylinder is invariant.

theorem CSD.RecordLayer.measurable_pointerBankSwap {N : ℕ} (j : Fin N) : Measurable (pointerBankSwap j)

theorem CSD.RecordLayer.measurable_relocMap {N : ℕ} (k : Option (Fin N)) : Measurable (relocMap N k)

theorem CSD.RecordLayer.measurable_pointerRelocate {N : ℕ} : Measurable pointerRelocate

The relocation is measurable — piecewise, over the record-cylinder partition.

theorem CSD.RecordLayer.pointerRelocate_measurePreserving {N : ℕ} (μs : MeasureTheory.Measure (LF4.KSigma N)) [MeasureTheory.IsProbabilityMeasure μs] (q₀ : Pointer N) : MeasureTheory.MeasurePreserving pointerRelocate (pointerLudersMeasure μs q₀) (pointerLudersMeasure μs q₀)

★ The record-triggered relocation preserves the arena measure — brick 1's explicitly-owed piecewise invariance. On each record cylinder the relocation is the slot swap (measure-preserving, pointerBankSwap_measurePreserving) and the cylinder is its own preimage (pointerRelocate_pointer: the relocation never moves the pointer); off every record region it is the identity. measurePreserving_of_partition assembles the pieces — the same argument the torus witness used for swapG, with record cylinders in place of register arcs.

The smooth stroke on the composed arena

theorem CSD.RecordLayer.pointerEvolve_measurePreserving_prod {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) (μs : MeasureTheory.Measure (LF4.KSigma N)) [MeasureTheory.SFinite μs] (q₀ : Pointer N) : MeasureTheory.MeasurePreserving (pointerEvolve c ε) (μs.prod (Matrix.UnitaryGroup.fubiniStudyMeasure q₀)) (μs.prod (Matrix.UnitaryGroup.fubiniStudyMeasure q₀))

The smooth stroke preserves μs ⊗ μ_FS for any s-finite sector measure — the skew product over the pointer factor, with each slice an FS-preserving unitary. (The brick-2b statement pointerEvolve_measurePreserving is the pointerLiouville instance.)

theorem CSD.RecordLayer.measurable_pointerLudersStroke {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) : Measurable (pointerLudersStroke c ε)

theorem CSD.RecordLayer.pointerLudersStroke_measurePreserving {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) (ε : ℝ) (μs : MeasureTheory.Measure (LF4.KSigma N)) [MeasureTheory.IsProbabilityMeasure μs] (q₀ : Pointer N) : MeasureTheory.MeasurePreserving (pointerLudersStroke c ε) (pointerLudersMeasure μs q₀) (pointerLudersMeasure μs q₀)

★ The two-stroke composite conserves Liouville measure: record stroke (skew product) then relocation (piecewise slot swap). Collapse as relocation, not contraction — no_exact_collapse is respected because volume is exchanged 1:1, on the smooth horn exactly as on the exact horns.

The conditioned post-measurement marginal

theorem CSD.RecordLayer.pointerProtocol_outcomeSector {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hδ : δ ≤ 1 / 2) (i : Fin N) : (pointerProtocol c hc ε hδ).outcomeSector i = pointerEvolve c ε ⁻¹' arenaRecord N i

The sector identification: the smooth protocol's outcome sector is the brick-2b propagator's preimage of the record cylinder. Pins down the trigger the relocation reads.

theorem CSD.RecordLayer.pointerLudersStroke_sys_on_sector {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hδ : δ ≤ 1 / 2) (i : Fin N) {y : PointerLudersArena N} (hy : y.1 ∈ (pointerProtocol c hc ε hδ).outcomeSector i) : (pointerLudersStroke c ε y).1.1 = y.2 i

On the outcome-i sector, the post-stroke system coordinate is bank slot i: the stroke lands the pointer in recordRegion i, so the relocation is the slot-i swap.

theorem CSD.RecordLayer.pointer_luders_marginal {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hδ : δ ≤ 1 / 2) (μsp : MeasureTheory.Measure (PointerArena N N)) [MeasureTheory.IsProbabilityMeasure μsp] (ν : Fin N → MeasureTheory.Measure (LF4.KSigma N)) [∀ (j : Fin N), MeasureTheory.IsProbabilityMeasure (ν j)] (i : Fin N) (hpos : μsp ((pointerProtocol c hc ε hδ).outcomeSector i) ≠ 0) : MeasureTheory.Measure.map (fun (y : PointerLudersArena N) => y.1.1) (MeasureTheory.Measure.map (pointerLudersStroke c ε) (μsp.prod (MeasureTheory.Measure.pi ν))[|(pointerProtocol c hc ε hδ).outcomeSector i ×ˢ Set.univ]) = ν i

★★ The Lüders update for the smooth horn, as a pushforward.

Initial state: system-and-pointer μsp, bank slots independently calibrated to ν j. Conditioned on the outcome-i sector — the smooth protocol's own sector, cylindered over the bank, which is the statement that the bank plays no part in which outcome occurs — the post-stroke system marginal is the slot-i calibration. Collapse as measure-preserving relocation, now on the smooth horn: the same three moves as swap_luders_marginal, with the trigger read off the pointer's record region instead of a torus arc. The conditioned marginal is exact; the ε lives only in which outcome occurs.

The CSD form: sequential statistics are Lüders on the smooth horn

theorem CSD.RecordLayer.pointer_luders_born {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hδ : δ ≤ 1 / 2) (μsp : MeasureTheory.Measure (PointerArena N N)) [MeasureTheory.IsProbabilityMeasure μsp] (i : Fin N) (hpos : μsp ((pointerProtocol c hc ε hδ).outcomeSector i) ≠ 0) (c' : ContextField N) (j : Fin N) : (MeasureTheory.Measure.map (pointerLudersStroke c ε) (μsp.prod (MeasureTheory.Measure.pi fun (k : Fin N) => epistemicMeasure (vertexPoint k)))[|(pointerProtocol c hc ε hδ).outcomeSector i ×ˢ Set.univ]) ((fun (y : PointerLudersArena N) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (vertexPoint i) j)

★ Lüders for CSD on the smooth horn: 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 — Born of the collapsed state. The system after the measurement behaves, in every subsequent measurement, exactly as a fresh preparation of eᵢ.

theorem CSD.RecordLayer.pointer_luders_born_prep {N : ℕ} (c : ContextField N) (hc : ∀ (j : Fin N), Continuous fun (p : LF4.CPN N) => c.rate p j) {ε δ : ℝ} (hε : 0 < ε) (hδpos : 0 < δ) (hδ : δ ≤ 1 / 2) (p : LF4.CPN N) (q₀ : Pointer N) (i : Fin N) (hi : 2 * ε < c.rate p i) (c' : ContextField N) (j : Fin N) : (MeasureTheory.Measure.map (pointerLudersStroke c ε) ((pointerPrep p q₀ δ).prod (MeasureTheory.Measure.pi fun (k : Fin N) => epistemicMeasure (vertexPoint k)))[|(pointerProtocol c hc ε hδ).outcomeSector i ×ˢ Set.univ]) ((fun (y : PointerLudersArena N) => y.1.1) ⁻¹' globalBasin c' j) = ENNReal.ofReal (c'.rate (vertexPoint i) j)

★★ The composite on the witness's own preparation — B3b closes. For the smooth witness's ready-conditioned preparation pointerPrep, whenever the context gives outcome i a rate above the ε-floor (2ε < rate i), the ε-Born lower bound makes the conditioning non-vacuous, and follow-up statistics after outcome i are exactly the collapsed state's Born weights. The smooth horn now delivers records (ε-Born, smoothWitnessClosure/pointer_born_frequency) and a Lüders update, on one arena.