SigmaLayer/TimeIndexedRecord: time-indexed records and their persistence under isolated evolution

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

SL-T5 final follow-on. RecordSemantics.event already takes a full RecordedFact (context, outcome AND time), but the concrete pointer semantics (vnRecordSemantics) ignored the recorded time — the event was the same pointer fibre for every t (external review 2026-07-14: "ignores the recorded time"). This module builds a genuinely TIME-INDEXED record semantics from the isolated dynamics, and proves the two physical persistence facts.

• flowedSemantics — from a base outcome-region family and the isolated flow, the event of ⟨c,i,t⟩ is the set of ontic states whose time-t isolated evolution lies in the outcome region: event ⟨c,i,t⟩ = Φ_t⁻¹'(region c i). A record asserts the outcome held at the state's time-t evolution, so it genuinely depends on t.
• flowedSemantics_event_measure — the record PROBABILITY is time-invariant: μL(event ⟨c,i,t⟩) = μL(region c i), because the isolated flow preserves μL. The Born weight of a record is conserved by isolated evolution — persistence of the record probability.
• flowedSemantics_event_flow — record COVARIANCE: the record at a later time is the flow-preimage of the record at the earlier time, event ⟨c,i,t+s⟩ = Φ_s⁻¹'(event ⟨c,i,t⟩). The time-indexed evidence transforms covariantly with the isolated dynamics (the "living history" evolves with the flow).
• flowedSemantics_persistence — bundles both.

Honest scope

This makes records genuinely time-physical: the event uses the recorded time, the record probability is conserved, and the evidence is flow-covariant. This is NOT a model of persistent apparatus MEMORY (a pointer physically latching to its value and remaining there); consistent with SigmaLayer/RecordedFact.lean, a value recorded at time t is time-indexed evidence, not required to persist as a later value. A latching-memory model would be a separate record-stability postulate.

References: specs/future-work.md (SL-T5 follow-on); SigmaLayer/RecordedFact.lean (RecordSemantics, P5), SigmaLayer/ConstraintDynamics.lean (flow_preserves, flow_add), SigmaLayer/UnifiedMeasurement.lean (the concrete pointer regions that instantiate region).

noncomputable def CSD.SigmaLayer.flowedSemantics {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (D : ConstraintDynamics Sigma) (region : (c : R.Context) → R.Outcome c → Set Sigma) (hmeas : ∀ (c : R.Context) (i : R.Outcome c), MeasurableSet (region c i)) (hexcl : ∀ (c : R.Context) (a b : R.Outcome c), ∀ y ∈ region c a, y ∈ region c b → a = b) : RecordSemantics Sigma R

A time-indexed record semantics from a base outcome-region family and the isolated flow. The event of a record ⟨c,i,t⟩ is the set of ontic states whose time-t isolated evolution lies in the outcome region: event ⟨c,i,t⟩ = Φ_t⁻¹'(region c i). Genuinely uses the recorded time t.

Equations

• CSD.SigmaLayer.flowedSemantics D region hmeas hexcl = { event := fun (r : CSD.SigmaLayer.RecordedFact R) => D.flow r.time ⁻¹' region r.context r.outcome, measurable_event := ⋯, exclusive := ⋯ }

@[simp]

theorem CSD.SigmaLayer.flowedSemantics_event {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (D : ConstraintDynamics Sigma) (region : (c : R.Context) → R.Outcome c → Set Sigma) (hmeas : ∀ (c : R.Context) (i : R.Outcome c), MeasurableSet (region c i)) (hexcl : ∀ (c : R.Context) (a b : R.Outcome c), ∀ y ∈ region c a, y ∈ region c b → a = b) (c : R.Context) (i : R.Outcome c) (t : OnticTime) : (flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t } = D.flow t ⁻¹' region c i

theorem CSD.SigmaLayer.flowedSemantics_event_measure {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (D : ConstraintDynamics Sigma) (region : (c : R.Context) → R.Outcome c → Set Sigma) (hmeas : ∀ (c : R.Context) (i : R.Outcome c), MeasurableSet (region c i)) (hexcl : ∀ (c : R.Context) (a b : R.Outcome c), ∀ y ∈ region c a, y ∈ region c b → a = b) (c : R.Context) (i : R.Outcome c) (t : OnticTime) : ↑D.muL ((flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t }) = ↑D.muL (region c i)

Record probability is time-invariant (persistence under isolated evolution). The Liouville measure of a record event does not depend on the recorded time: μL(event ⟨c,i,t⟩) = μL(region c i), because the isolated flow preserves μL. The Born weight of a record is conserved by isolated evolution.

theorem CSD.SigmaLayer.flowedSemantics_event_flow {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (D : ConstraintDynamics Sigma) (region : (c : R.Context) → R.Outcome c → Set Sigma) (hmeas : ∀ (c : R.Context) (i : R.Outcome c), MeasurableSet (region c i)) (hexcl : ∀ (c : R.Context) (a b : R.Outcome c), ∀ y ∈ region c a, y ∈ region c b → a = b) (c : R.Context) (i : R.Outcome c) (s t : OnticTime) : (flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t + s } = D.flow s ⁻¹' (flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t }

Record covariance under the flow (the living history evolves with the dynamics). The record at a later time is the flow-preimage of the record at the earlier time: event ⟨c,i,t+s⟩ = Φ_s⁻¹'(event ⟨c,i,t⟩). The time-indexed evidence transforms covariantly under isolated evolution.

theorem CSD.SigmaLayer.flowedSemantics_persistence {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (D : ConstraintDynamics Sigma) (region : (c : R.Context) → R.Outcome c → Set Sigma) (hmeas : ∀ (c : R.Context) (i : R.Outcome c), MeasurableSet (region c i)) (hexcl : ∀ (c : R.Context) (a b : R.Outcome c), ∀ y ∈ region c a, y ∈ region c b → a = b) (c : R.Context) (i : R.Outcome c) : (∀ (t : OnticTime), ↑D.muL ((flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t }) = ↑D.muL (region c i)) ∧ ∀ (s t : OnticTime), (flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t + s } = D.flow s ⁻¹' (flowedSemantics D region hmeas hexcl).event { context := c, outcome := i, time := t }

Record persistence (physical). For every context/outcome, the time-indexed record probability is conserved by isolated evolution AND the record transforms covariantly with the flow: records are genuine time-physical evidence carried consistently by the isolated dynamics.