SigmaLayer/RecordedFact: physical records as measurable contextual ontic events

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

This is the genuinely new SigmaLayer content: physical records represented as measurable, contextual, time-indexed ontic events (postulate P5), and a finite record history whose compatible region is the intersection of the corresponding events. Isolation (postulate P6) is then conditioning muL on this compatible region; see SigmaLayer/IsolationPreparation.lean.

Scientific reading

A RecordedFact states that a contextual property had a specified value at a specified time. The property may subsequently change; the historical record is not thereby invalidated. So the compatible region records time-indexed evidence, and we do NOT require a value measured at time t to persist at later times. Exclusivity is asserted only within a single context at a single time.

structure CSD.SigmaLayer.RecordSignature : Type (max (u + 1) (v + 1))

A record signature (postulate P5 data). A type of measurement contexts, and for each context a type of possible outcomes.

The two universes are deliberate: contexts and outcomes are independent data with no theorem in the corpus relating their sizes, so neither is forced into the other's universe. The checkUnivs linter flags the resulting max as possibly accidental generality; here it is intended, and every in-tree instantiation lives in Type 0.

• Context : Type u

  The type of measurement contexts.

• Outcome : self.Context → Type v

  For each context, the type of possible outcomes.

structure CSD.SigmaLayer.RecordedFact (R : RecordSignature) : Type (max u_1 u_2)

A recorded fact. A contextual property (context) had value outcome at time time.

• context : R.Context

  The measurement context of the record.

• outcome : R.Outcome self.context

  The recorded outcome (in the context's outcome type).

• time : OnticTime

  The ontic time at which the record was established.

structure CSD.SigmaLayer.RecordSemantics (Sigma : Type w) [MeasurableSpace Sigma] (R : RecordSignature) : Type (max (max u_1 u_2) w)

Record semantics (postulate P5). Each recorded fact is interpreted as a measurable ontic event (the region of Sigma compatible with that record), and within a single context at a single time the events for distinct outcomes are mutually exclusive. No exclusivity is asserted across contexts.

⚠️ This structure is TRIVIALLY INHABITED, and exhibiting an instance therefore proves nothing on its own (noted 2026-07-28, Tier-0 review). Take event := fun _ => ∅: every event is measurable, and exclusive holds vacuously because no state lies in any event. The structure constrains how records may be interpreted; it does not assert that anything is ever recorded.

So a phrase like "a genuine postulate-P5 RecordSemantics" names the interface, not an achievement. The content lives in the accompanying non-vacuity results, which must be supplied separately and are what actually rule out the empty semantics — e.g. RecordLayerClosure.ae_total, Measurement.bornMeasurement_ae_total, DeIsolationFlow.fibreTypicality_uncovered (the record set has full typicality measure), and the Born-weight identities fibreTypicality_bornRecord / fubiniStudy_projRecord. When citing an instance, cite those too.

• event : RecordedFact R → Set Sigma

  The measurable ontic event associated with a recorded fact.

• measurable_event (r : RecordedFact R) : MeasurableSet (self.event r)

  Each record event is measurable.

• exclusive (c : R.Context) (a b : R.Outcome c) (t : OnticTime) (x : Sigma) : x ∈ self.event { context := c, outcome := a, time := t } → x ∈ self.event { context := c, outcome := b, time := t } → a = b

  Within one context at one time, distinct outcomes have disjoint events (membership form): a state cannot simultaneously record two different outcomes of the same context at the same time.

@[reducible, inline]

abbrev CSD.SigmaLayer.RecordHistory (R : RecordSignature) : Type (max u_2 u_1)

A finite record history is a list of recorded facts (the time-indexed evidence).

Equations

• CSD.SigmaLayer.RecordHistory R = List (CSD.SigmaLayer.RecordedFact R)

def CSD.SigmaLayer.compatibleSet {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) : RecordHistory R → Set Sigma

The compatible region of a record history. The set of ontic states consistent with every record in the history: univ for the empty history, and the intersection of the head event with the tail's compatible region for a cons. This is the epistemic support during isolation.

Equations

• CSD.SigmaLayer.compatibleSet S [] = Set.univ
• CSD.SigmaLayer.compatibleSet S (r :: H) = S.event r ∩ CSD.SigmaLayer.compatibleSet S H

@[simp]

theorem CSD.SigmaLayer.compatibleSet_nil {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) : compatibleSet S [] = Set.univ

@[simp]

theorem CSD.SigmaLayer.compatibleSet_cons {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) (r : RecordedFact R) (H : RecordHistory R) : compatibleSet S (r :: H) = S.event r ∩ compatibleSet S H

theorem CSD.SigmaLayer.compatibleSet_measurable {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) (H : RecordHistory R) : MeasurableSet (compatibleSet S H)

The compatible region is measurable (intersection of measurable record events).

theorem CSD.SigmaLayer.mem_compatibleSet {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) (H : RecordHistory R) (x : Sigma) : x ∈ compatibleSet S H ↔ ∀ r ∈ H, x ∈ S.event r

Membership in the compatible region is compatibility with every record in the history.

theorem CSD.SigmaLayer.mem_event_of_mem_compatibleSet {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) {H : RecordHistory R} {x : Sigma} (hx : x ∈ compatibleSet S H) {r : RecordedFact R} (hr : r ∈ H) : x ∈ S.event r

Every record in the history holds on the compatible region.

theorem CSD.SigmaLayer.compatibleSet_append_subset {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) (H : RecordHistory R) (r : RecordedFact R) : compatibleSet S (H ++ [r]) ⊆ compatibleSet S H

Appending a record shrinks the compatible region. More evidence never enlarges the compatible support: compatibleSet S (H ++ [r]) ⊆ compatibleSet S H.

theorem CSD.SigmaLayer.compatibleSet_append_singleton {Sigma : Type w} [MeasurableSpace Sigma] {R : RecordSignature} (S : RecordSemantics Sigma R) (H : RecordHistory R) (r : RecordedFact R) : compatibleSet S (H ++ [r]) = compatibleSet S H ∩ S.event r

The compatible region of an appended history is the prior region intersected with the new event.