SigmaLayer/MeasurementRecord: de-isolating measurement and record establishment

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

Bridge assumptions B4, B5. A DeisolationModel is a physical interaction (measure-preserving, per context) together with preparation-dependent outcome regions and a partial readout. De-isolation is a deterministic interaction followed by a contextual readout that establishes a new RecordedFact (establishedFact). The outcome regions may depend on the preparation, as the LF5 pointer-outcome construction requires. Totality is not required everywhere (boundaries may have measure zero); the AETotalReadout predicate states almost-everywhere completeness for a given preparation measure.

We do NOT assume that later ontic states retain the measured value: a record states that a value held at its time, not for all later times. Persistent apparatus memory would be a separate record-stability model.

structure CSD.SigmaLayer.DeisolationModel {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (R : RecordSignature) (S : RecordSemantics Sigma R) (Prep : Type w) : Type (max (max (max u u_1) u_2) w)

A de-isolating measurement model (B4, B5 interface). A measure-preserving interaction per context, preparation-dependent measurable pairwise-disjoint outcome regions, and a partial readout whose some i values are exactly membership in the i-th outcome region.

• interaction : OnticTime → (c : R.Context) → Sigma → Sigma

  The measurement interaction at a time and context.

• measurable_interaction (t : OnticTime) (c : R.Context) : Measurable (self.interaction t c)

  Each interaction is measurable.

• interaction_preserves (t : OnticTime) (c : R.Context) : MeasureTheory.MeasurePreserving (self.interaction t c) ↑D.muL ↑D.muL

  Each interaction preserves the Liouville measure.

• outcomeRegion : Prep → (c : R.Context) → R.Outcome c → Set Sigma

  The preparation-dependent outcome regions.

• measurable_outcomeRegion (p : Prep) (c : R.Context) (i : R.Outcome c) : MeasurableSet (self.outcomeRegion p c i)

  Each outcome region is measurable.

• pairwise_disjoint (p : Prep) (c : R.Context) : Set.univ.PairwiseDisjoint (self.outcomeRegion p c)

  Distinct outcomes have disjoint regions.

• readout : Prep → (c : R.Context) → Sigma → Option (R.Outcome c)

  The partial contextual readout.

• readout_eq_some_iff (p : Prep) (c : R.Context) (x : Sigma) (i : R.Outcome c) : self.readout p c x = some i ↔ x ∈ self.outcomeRegion p c i

  The readout returns some i exactly on the i-th outcome region.

def CSD.SigmaLayer.DeisolationModel.establishedFact {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} {Prep : Type w} (Mdl : DeisolationModel D R S Prep) (p : Prep) (c : R.Context) (t : OnticTime) (x : Sigma) : Option (RecordedFact R)

The established fact. De-isolation with preparation p, context c, at time t: interact, then read out; a some i readout establishes the record ⟨c, i, t⟩.

Equations

• Mdl.establishedFact p c t x = Option.map (fun (i : R.Outcome c) => { context := c, outcome := i, time := t }) (Mdl.readout p c (Mdl.interaction t c x))

def CSD.SigmaLayer.DeisolationModel.AETotalReadout {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} {Prep : Type w} (Mdl : DeisolationModel D R S Prep) (p : Prep) (c : R.Context) (t : OnticTime) (mu : MeasureTheory.Measure Sigma) : Prop

Almost-everywhere total readout (a form of B4). For a given preparation measure the readout is defined for almost every initial ontic state after the interaction. Boundaries of measure zero are permitted.

Equations

• Mdl.AETotalReadout p c t mu = ∀ᵐ (x : Sigma) ∂mu, (Mdl.readout p c (Mdl.interaction t c x)).isSome = true

def CSD.SigmaLayer.DeisolationModel.RecordsEstablishedOutcome {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} {Prep : Type w} (Mdl : DeisolationModel D R S Prep) : Prop

The post-measurement record is compatible with the realised outcome region (B5). If the readout after the interaction is some i, the post-interaction state lies in the record event S.event ⟨c,i,t⟩. Stated as a predicate; proved for concrete models where the record semantics matches the outcome regions.

Equations

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

Record-history update

def CSD.SigmaLayer.appendEstablishedFact {R : RecordSignature} (Hist : RecordHistory R) (r : RecordedFact R) : RecordHistory R

Append an established fact to a record history.

Equations

• CSD.SigmaLayer.appendEstablishedFact Hist r = Hist ++ [r]

theorem CSD.SigmaLayer.compatibleSet_appendEstablishedFact {Sigma : Type u} [MeasurableSpace Sigma] {R : RecordSignature} {S : RecordSemantics Sigma R} (Hist : RecordHistory R) (r : RecordedFact R) : compatibleSet S (appendEstablishedFact Hist r) = compatibleSet S Hist ∩ S.event r

The post-measurement compatible region. Appending the new record intersects the prior compatible region with the new record's event: compatibleSet S (appendEstablishedFact Hist r) = compatibleSet S Hist ∩ S.event r. This is the conditional update of the epistemic support (ordinary conditioning; not called Lüders update until an equality with the Lüders rule is proved).