RecordLayer/TwoTimeLuders: records at t₁ then t₂, on one arena (Q25)

Category: 7-SigmaLayer (the record layer — the two-time composition).

The question this answers

"What happens to the OTHER regions Ω_j when outcome i is realised?" The corpus had the one-measurement dynamics complete (swap_sector_born, swap_luders_marginal) and the sequential statistics as CONDITIONAL statements about the post-measurement ensemble (csd_sequential_born, csd_repeatability). This module composes them into the two-time statement on one arena: a single composite space carrying BOTH measurements, the JOINT law of the record pair, and the first record persisting — structurally — through the second measurement.

The construction

Extend the swap arena with a second apparatus — a fresh register and a fresh bank ("one measurement consumes one bank" is the standing scope note, so a second measurement carries its own):

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

Stage 1 is the first swap propagator with the second apparatus as a spectator (stageOne). Stage 2 is the second swap propagator conjugated by the coordinate shuffle regroup that brings (system, register₂, bank₂) together while the stage-1 record coordinates ride untouched (stageTwo). Because the stage-2 evolution provably never touches register₁ or bank₁ (stageTwo_register₁, stageTwo_bank₁ — definitional, the same reason swapG_register was free), the t₁ record is still on display at t₂.

What is proved

• cond_map — conditioning commutes with a measurable pushforward. (Reusable; no CSD content.)
• two_stage_first_record — the stage-1 record marginal is untouched by composing: the second apparatus cannot retro-act on the first record's probability.
• two_stage_joint — ★★ the generic composition: the joint record probability factors as (stage-1 sector measure) × (stage-2 sector measure at the relocated state). The engine is swap_luders_marginal: the stage-2 record event never reads the stage-1 record coordinates, so only the SYSTEM marginal of the conditioned post-measurement state enters — no joint factorisation of the conditioned law is ever needed.
• two_time_born — ★★ the CSD form: for the canonical ready preparation at p, P(record i at t₁ ∧ record j at t₂) = momentMap p i · c₂.rate [eᵢ] j for ANY second context c₂. Two-time statistics are Born-then-Lüders-Born, as one number on one arena.
• two_time_repeat — ★ von Neumann repeatability in composed form: with the same context twice, the joint law is momentMap p i · δᵢⱼ.
• two_time_other_fate — ★ the row's literal question: CONDITIONED on record i at t₁, the stage-2 partition carries the collapsed weights c₂.rate [eᵢ] — for the repeated context the other Ω_j are null and Ω_i is certain; a fresh context sees the collapsed state's rates.
• two_stage_readouts — both records are on display at the end: on the joint sector the final state's first register reads some i and its second register reads some j.

⚠️ Scope

• Rank-one, nondegenerate measurements — the scope of the swap witness; the stage-1 context is the computational basis (momentContext, matching the vertex calibration), the stage-2 context is arbitrary. Degenerate first measurements remain the recorded open construction (DegenerateLuders.lean).
• The clock-glued two-epoch MeasurementProtocol on [0,2] (one propagator family through both readout crossings) is deliberately NOT built: the composed-map form here carries the physics; the gluing is presentation, recorded as gated residue in specs/two-time-luders-scoping.md.
• The entangled/composite two-time version (measure a subsystem of an entangled composite, then follow up) is Q27's mixed-tier territory — the swap witness over the composite arena with reducedDM weights — and is not scoped here.
• Hamiltonian generation of the propagators is stated, not formalised, exactly as for the shear and swap witnesses.

References

specs/two-time-luders-scoping.md (the Q25 scoping note this executes); RecordLayer/SwapLuders.lean (swap_luders_marginal, cond_prod_cylinder — the engine); RecordLayer/SwapClosure.lean (swapPrep, swap_sector_born, swap_sector_born_ctx, prep_outcome_pos); RecordLayer/SwapWitness.lean (the arena and propagator); Empirical/CSD/SequentialMeasurement.lean (the conditional tier this upgrades); specs/BACKLOG.md (Q25).

The two-stage arena and its evolutions

@[reducible, inline]

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

The two-stage arena: the swap arena of the first measurement, together with the second apparatus — a fresh register and a fresh bank.

Equations

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

def CSD.RecordLayer.regroup {Xsel : Type u_1} {K : ℕ} (x : TwoStageArena Xsel K) : TwoStageArena Xsel K

The regrouping shuffle: bring (system, register₂, bank₂) together as a swap arena, with the stage-1 record coordinates (register₁, bank₁) as spectators. An involution.

Equations

• CSD.RecordLayer.regroup x = (((x.1.1.1, x.2.1), x.2.2), x.1.1.2, x.1.2)

theorem CSD.RecordLayer.regroup_regroup {Xsel : Type u_1} {K : ℕ} (x : TwoStageArena Xsel K) : regroup (regroup x) = x

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

noncomputable def CSD.RecordLayer.stageOne {Xsel : Type u_1} {K : ℕ} (idx₁ : Xsel → Fin K) : TwoStageArena Xsel K → TwoStageArena Xsel K

Stage 1: the first swap propagator runs on its own arena; the second apparatus is a spectator.

Equations

• CSD.RecordLayer.stageOne idx₁ = Prod.map (CSD.RecordLayer.swapEvolve idx₁ 0 1) id

noncomputable def CSD.RecordLayer.stageTwo {Xsel : Type u_1} {K : ℕ} (idx₂ : Xsel → Fin K) : TwoStageArena Xsel K → TwoStageArena Xsel K

Stage 2: the second swap propagator runs on (system, register₂, bank₂); the stage-1 record coordinates are spectators. The lifted evolution, conjugated by the regrouping shuffle.

Equations

• CSD.RecordLayer.stageTwo idx₂ = CSD.RecordLayer.regroup ∘ Prod.map (CSD.RecordLayer.swapEvolve idx₂ 0 1) id ∘ CSD.RecordLayer.regroup

noncomputable def CSD.RecordLayer.twoStage {Xsel : Type u_1} {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) : TwoStageArena Xsel K → TwoStageArena Xsel K

The composed two-time propagator: stage 1, then stage 2.

Equations

• CSD.RecordLayer.twoStage idx₁ idx₂ = CSD.RecordLayer.stageTwo idx₂ ∘ CSD.RecordLayer.stageOne idx₁

theorem CSD.RecordLayer.measurable_stageOne {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ : Xsel → Fin K) (h₁ : Measurable idx₁) : Measurable (stageOne idx₁)

theorem CSD.RecordLayer.measurable_stageTwo {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₂ : Xsel → Fin K) (h₂ : Measurable idx₂) : Measurable (stageTwo idx₂)

theorem CSD.RecordLayer.measurable_twoStage {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (h₁ : Measurable idx₁) (h₂ : Measurable idx₂) : Measurable (twoStage idx₁ idx₂)

★ The first record persists — structurally

theorem CSD.RecordLayer.stageTwo_register₁ {Xsel : Type u_1} {K : ℕ} (idx₂ : Xsel → Fin K) (x : TwoStageArena Xsel K) : (stageTwo idx₂ x).1.1.2 = x.1.1.2

★ The second measurement never touches the first register. Definitional: the stage-2 evolution acts through the shuffle, and register₁ rides in the spectator slot. This is what makes the t₁ record readable at t₂.

theorem CSD.RecordLayer.stageTwo_bank₁ {Xsel : Type u_1} {K : ℕ} (idx₂ : Xsel → Fin K) (x : TwoStageArena Xsel K) : (stageTwo idx₂ x).1.2 = x.1.2

The second measurement never touches the first bank — the ontic memory of the first measurement (the relocated pre-measurement state) survives the second.

The record events

def CSD.RecordLayer.recordOneEvent {Xsel : Type u_1} {K : ℕ} (i : Fin K) : Set (TwoStageArena Xsel K)

The event "the first register displays outcome i".

Equations

• CSD.RecordLayer.recordOneEvent i = {x : CSD.RecordLayer.TwoStageArena Xsel K | x.1.1.2 ∈ CSD.RecordLayer.pointerArc K i}

def CSD.RecordLayer.recordTwoEvent {Xsel : Type u_1} {K : ℕ} (j : Fin K) : Set (TwoStageArena Xsel K)

The event "the second register displays outcome j".

Equations

• CSD.RecordLayer.recordTwoEvent j = {x : CSD.RecordLayer.TwoStageArena Xsel K | x.2.1 ∈ CSD.RecordLayer.pointerArc K j}

def CSD.RecordLayer.jointRecordSector {Xsel : Type u_1} {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (i j : Fin K) : Set (TwoStageArena Xsel K)

The joint two-record sector: the initial states destined to display record i at t₁ and record j at t₂.

Equations

• CSD.RecordLayer.jointRecordSector idx₁ idx₂ i j = CSD.RecordLayer.twoStage idx₁ idx₂ ⁻¹' (CSD.RecordLayer.recordOneEvent i ∩ CSD.RecordLayer.recordTwoEvent j)

theorem CSD.RecordLayer.recordOneEvent_eq {Xsel : Type u_1} {K : ℕ} (i : Fin K) : recordOneEvent i = {y : SwapArena Xsel K | y.1.2 ∈ pointerArc K i} ×ˢ Set.univ

The first-record event is a cylinder over the first pointer region.

theorem CSD.RecordLayer.measurableSet_recordOneEvent {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (i : Fin K) : MeasurableSet (recordOneEvent i)

Persistence at the event level

theorem CSD.RecordLayer.stageTwo_preimage_recordOne {Xsel : Type u_1} {K : ℕ} (idx₂ : Xsel → Fin K) (i : Fin K) : stageTwo idx₂ ⁻¹' recordOneEvent i = recordOneEvent i

★ Stage 2 does not move the first-record event: reading register₁ after the second measurement is reading it before. The event-level form of persistence.

theorem CSD.RecordLayer.stageTwo_preimage_recordTwo {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₂ : Xsel → Fin K) (h₂ : Measurable idx₂) (j : Fin K) : stageTwo idx₂ ⁻¹' recordTwoEvent j = regroup ⁻¹' (swapProtocol idx₂ h₂).outcomeSector j ×ˢ Set.univ

The second-record event pulls back through stage 2 to the second protocol's outcome sector, cylindered by the shuffle.

Conditioning commutes with a pushforward

theorem CSD.RecordLayer.cond_map {X : Type u_2} {Y : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) {f : X → Y} (hf : Measurable f) {A : Set Y} (hA : MeasurableSet A) : (MeasureTheory.Measure.map f μ)[|A] = MeasureTheory.Measure.map f μ[|f ⁻¹' A]

Conditioning commutes with a measurable pushforward. Reusable, no CSD content.

The generic two-stage composition

noncomputable def CSD.RecordLayer.twoStagePrep {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) (ν₁ : Fin K → MeasureTheory.Measure Xsel) (μR₂ : MeasureTheory.Measure LF4.KTorus) (ν₂ : Fin K → MeasureTheory.Measure Xsel) : MeasureTheory.Measure (TwoStageArena Xsel K)

The generic two-stage preparation: stage-1 system-and-register μ12 with bank ν₁; second apparatus register μR₂ with bank ν₂ — all independent, as fresh apparatus is.

Equations

• CSD.RecordLayer.twoStagePrep μ12 ν₁ μR₂ ν₂ = (μ12.prod (MeasureTheory.Measure.pi ν₁)).prod (μR₂.prod (MeasureTheory.Measure.pi ν₂))

instance CSD.RecordLayer.instIsProbabilityMeasureTwoStageArenaTwoStagePrepOfProdOfKTorus {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (ν₁ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₁ j)] (μR₂ : MeasureTheory.Measure LF4.KTorus) [MeasureTheory.IsProbabilityMeasure μR₂] (ν₂ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₂ j)] : MeasureTheory.IsProbabilityMeasure (twoStagePrep μ12 ν₁ μR₂ ν₂)

theorem CSD.RecordLayer.two_stage_first_record {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (h₁ : Measurable idx₁) (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (ν₁ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₁ j)] (μR₂ : MeasureTheory.Measure LF4.KTorus) [MeasureTheory.IsProbabilityMeasure μR₂] (ν₂ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₂ j)] (i : Fin K) : (twoStagePrep μ12 ν₁ μR₂ ν₂) (twoStage idx₁ idx₂ ⁻¹' recordOneEvent i) = (μ12.prod (MeasureTheory.Measure.pi ν₁)) ((swapProtocol idx₁ h₁).outcomeSector i)

The stage-1 record marginal is untouched by composing — the second apparatus cannot retro-act on the first record's probability.

theorem CSD.RecordLayer.two_stage_joint {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (h₁ : Measurable idx₁) (h₂ : Measurable idx₂) (μ12 : MeasureTheory.Measure (Xsel × LF4.KTorus)) [MeasureTheory.IsProbabilityMeasure μ12] (ν₁ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₁ j)] (μR₂ : MeasureTheory.Measure LF4.KTorus) [MeasureTheory.IsProbabilityMeasure μR₂] (ν₂ : Fin K → MeasureTheory.Measure Xsel) [∀ (j : Fin K), MeasureTheory.IsProbabilityMeasure (ν₂ j)] (i j : Fin K) (hpos : μ12 ((shearProtocol idx₁ h₁).outcomeSector i) ≠ 0) : (twoStagePrep μ12 ν₁ μR₂ ν₂) (jointRecordSector idx₁ idx₂ i j) = (μ12.prod (MeasureTheory.Measure.pi ν₁)) ((swapProtocol idx₁ h₁).outcomeSector i) * (((ν₁ i).prod μR₂).prod (MeasureTheory.Measure.pi ν₂)) ((swapProtocol idx₂ h₂).outcomeSector j)

★★ The generic two-stage composition. The joint two-record probability factors as (stage-1 sector measure) × (stage-2 sector measure at the relocated state): conditioned on the first record, the second apparatus sees the slot-i calibration as its system (swap_luders_marginal) with its own fresh register and bank, so the stage-2 record probability is the single-measurement sector probability at that input. The stage-2 record event never reads the stage-1 record coordinates — only the system marginal of the conditioned state enters.

The CSD forms

noncomputable def CSD.RecordLayer.csdTwoPrep {N : ℕ} (p : LF4.CPN N) : MeasureTheory.Measure (TwoStageArena (LF4.KSigma N) N)

The canonical two-stage preparation: system at p with ready register and vertex-calibrated bank for the first measurement, fresh ready register and vertex-calibrated bank for the second.

Equations

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

instance CSD.RecordLayer.instIsProbabilityMeasureTwoStageArenaKSigmaCsdTwoPrep {N : ℕ} (p : LF4.CPN N) : MeasureTheory.IsProbabilityMeasure (csdTwoPrep p)

theorem CSD.RecordLayer.two_time_born {N : ℕ} [NeZero N] (p : LF4.CPN N) (i : Fin N) (hpos : LF4.momentMap p i ≠ 0) (c₂ : ContextField N) (j : Fin N) : (csdTwoPrep p) (jointRecordSector (basinIndex (momentContext N)) (basinIndex c₂) i j) = ENNReal.ofReal (LF4.momentMap p i) * ENNReal.ofReal (c₂.rate (vertexPoint i) j)

★★ The two-time Born law, on one arena. For the canonical ready preparation at p, measured in the computational basis at t₁ and in an ARBITRARY context c₂ at t₂:

P(record i at t₁ ∧ record j at t₂) = momentMap p i · c₂.rate [eᵢ] j.

The first factor is the dynamical Born weight of the preparation; the second is the Born weight of the COLLAPSED state [eᵢ] in the second context — Born-then-Lüders-Born as one number, with both records on one arena and the first persisting through the second measurement. This is the composed two-time statement csd_sequential_born (a conditional) could not express.

theorem CSD.RecordLayer.two_time_repeat {N : ℕ} [NeZero N] (p : LF4.CPN N) (i : Fin N) (hpos : LF4.momentMap p i ≠ 0) (j : Fin N) : (csdTwoPrep p) (jointRecordSector (basinIndex (momentContext N)) (basinIndex (momentContext N)) i j) = ENNReal.ofReal (LF4.momentMap p i) * if j = i then 1 else 0

★ Von Neumann repeatability, in composed two-time form. Measure the computational basis twice: the joint law is momentMap p i · δᵢⱼ — the same outcome recurs, any other pair of records has probability zero, as ONE statement about the two-record sector.

theorem CSD.RecordLayer.two_time_first_record {N : ℕ} [NeZero N] (p : LF4.CPN N) (c₂ : ContextField N) (i : Fin N) : (csdTwoPrep p) (twoStage (basinIndex (momentContext N)) (basinIndex c₂) ⁻¹' recordOneEvent i) = ENNReal.ofReal (LF4.momentMap p i)

The stage-1 record marginal, in CSD form: composing does not disturb the first Born law.

theorem CSD.RecordLayer.two_time_other_fate {N : ℕ} [NeZero N] (p : LF4.CPN N) (i : Fin N) (hpos : LF4.momentMap p i ≠ 0) (c₂ : ContextField N) (j : Fin N) : (csdTwoPrep p)[twoStage (basinIndex (momentContext N)) (basinIndex c₂) ⁻¹' recordTwoEvent j | twoStage (basinIndex (momentContext N)) (basinIndex c₂) ⁻¹' recordOneEvent i] = ENNReal.ofReal (c₂.rate (vertexPoint i) j)

★ The fate of the other Ω_j — the conditioned re-partition the next context sees. CONDITIONED on record i at t₁, the probability of record j at t₂ is the collapsed state's rate c₂.rate [eᵢ] j. For the repeated context (c₂ = momentContext) this makes every other Ω_j NULL and Ω_i certain (momentMap_vertex); for a fresh context it is the Lüders-updated Born law. The post-outcome fate of the other regions, stated as a conditional probability on the composed arena.

Both records on display

theorem CSD.RecordLayer.two_stage_readouts {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx₁ idx₂ : Xsel → Fin K) (h₁ : Measurable idx₁) (h₂ : Measurable idx₂) {i j : Fin K} {x : TwoStageArena Xsel K} (hx : x ∈ jointRecordSector idx₁ idx₂ i j) : (swapProtocol idx₁ h₁).readout (twoStage idx₁ idx₂ x).1 = some i ∧ (swapProtocol idx₂ h₂).readout (regroup (twoStage idx₁ idx₂ x)).1 = some j

★ Both records are visible at t₂. On the joint sector, the final state's first register reads some i — the persisting t₁ record — and its second register reads some j, through each protocol's own readout.