SigmaLayer/IsolationPreparation: preparations and isolation as conditioning on a record history

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

Glossary: https://glossary.constraintsurfacedynamics.com/psi-epistemic/ Plain-language, CSD-role and formal statements of the ψ-epistemic reading, with this module — conditional_not_mutuallySingular — as the Lean anchor for finite-resolution preparation overlap. ⚠️ The Harrigan–Spekkens classification of the EXACT sharp interface is a different claim and is anchored elsewhere (RecordLayer/PBRPreparation.lean, where it comes out ψ-ontic). Kept symmetric by scripts/check-glossary.sh.

A Preparation restricts the ontic state to a measurable region of nonzero Liouville measure. The LF1 adapter (Preparation.toOnticSetup) turns a preparation plus a time into an existing LF1.OnticSetup, so the isolated epistemic law reuses LF1's normalised conditional measure prepMeasure rather than a second independent normalisation.

Postulate P6: during isolation no new record is established, and the probability law is conditional uncertainty over Sigma given the existing record history. HistoryPreparation realises this: its region is the compatible region of the history (compatibleSet), and its conditional measure is the ordinary conditioning muH(A) = muL(A ∩ compatible) / muL(compatible). This is the epistemic law conditional on the record history, not an additional ontic state.

structure CSD.SigmaLayer.Preparation {Sigma : Type w} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) : Type w

A preparation. A measurable ontic region of nonzero Liouville measure.

• region : Set Sigma

  The preparation region.

• measurable_region : MeasurableSet self.region

  The region is measurable.

• nonzero_region : ↑D.muL self.region ≠ 0

  The region has nonzero Liouville measure, so normalisation is well defined.

def CSD.SigmaLayer.Preparation.toOnticSetup {Sigma : Type w} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (P : Preparation D) (t : OnticTime) : LF1.OnticSetup Sigma

The LF1 adapter (fixed time step). A preparation and a time t yield an existing LF1.OnticSetup: muL to μL, flow t to Φ, flow_preserves t to hΦ_pres, region to Ω0.

Equations

• P.toOnticSetup t = { μL := D.muL, Φ := D.flow t, hΦ_pres := ⋯, Ω0 := P.region, hΩ0_meas := ⋯, hΩ0_nonzero := ⋯ }

noncomputable def CSD.SigmaLayer.Preparation.conditionalMeasure {Sigma : Type w} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (P : Preparation D) : MeasureTheory.ProbabilityMeasure Sigma

The isolated (conditional) preparation law. Reuses LF1's normalised conditional measure prepMeasure; it depends only on muL and region, so t = 0 instantiates the adapter. This is the epistemic law conditional on the preparation region, not an additional ontic state.

Equations

• P.conditionalMeasure = (P.toOnticSetup 0).prepMeasure

theorem CSD.SigmaLayer.Preparation.conditionalMeasure_apply {Sigma : Type w} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (P : Preparation D) (A : Set Sigma) (hA : MeasurableSet A) : ↑P.conditionalMeasure A = ↑D.muL (A ∩ P.region) / ↑D.muL P.region

The conditional preparation law is the LF1 normalised conditional measure: for measurable A, muH(A) = muL(A ∩ region) / muL(region) (reusing LF1.OnticSetup.prepMeasure_apply).

theorem CSD.SigmaLayer.Preparation.measure_inter_region_eq_zero_of_conditionalMeasure_eq_zero {Sigma : Type w} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (P : Preparation D) {A : Set Sigma} (hA : MeasurableSet A) (h : ↑P.conditionalMeasure A = 0) : ↑D.muL (A ∩ P.region) = 0

A conditional-measure null set meets the preparation region in a Liouville-null set: muH(A) = 0 forces muL (A ∩ region) = 0. The division cannot hide mass because the Liouville measure is finite.

theorem CSD.SigmaLayer.Preparation.conditional_not_mutuallySingular {Sigma : Type w} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (P Q : Preparation D) (h : ↑D.muL (P.region ∩ Q.region) ≠ 0) : ¬(↑P.conditionalMeasure).MutuallySingular ↑Q.conditionalMeasure

★★ Finite-resolution preparation overlap (Q28 item 4). If two preparation regions share Liouville-positive overlap, their normalised conditional measures cannot be separated onto disjoint supports.

⚠️ Interpretation corrected 2026-08-25. This was described as "the formal content of 'CSD is ψ-epistemic'". It is not. It is a statement about positive-volume REGION preparations, a different preparation class from exact pure states, and it does not classify exact pure-state preparations as ψ-epistemic in the Harrigan–Spekkens sense. On the exact sharp interface the corpus proves the opposite — distinct exact pure states have mutually singular ontic measures, i.e. ψ-ONTICITY — in RecordLayer.sharp_preparations_mutuallySingular.

The argument is a density argument, NOT a shared-support one — two measures can both charge a common set and still be mutually singular. On the overlap both conditionals are normalised restrictions of the same Liouville measure: a singularity witness S would make muL (S ∩ Ω_Q) null, hence muL (S ∩ Ω_P ∩ Ω_Q) null, while Sᶜ is P-null, making muL (Sᶜ ∩ Ω_P) null — and the overlap would be covered by two null sets.

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

An isolation preparation from a record history (postulate P6). No new record is established; the compatible region of the existing history has nonzero Liouville measure.

• history : RecordHistory R

  The existing record history.

• nonzero_compatible : ↑D.muL (compatibleSet S self.history) ≠ 0

  The compatible region of the history has nonzero Liouville measure.

def CSD.SigmaLayer.HistoryPreparation.toPreparation {Sigma : Type w} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} (HP : HistoryPreparation D R S) : Preparation D

The isolation preparation as an SigmaLayer Preparation, with region the compatible region of the history.

Equations

• HP.toPreparation = { region := CSD.SigmaLayer.compatibleSet S HP.history, measurable_region := ⋯, nonzero_region := ⋯ }

theorem CSD.SigmaLayer.HistoryPreparation.conditionalMeasure_apply {Sigma : Type w} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} (HP : HistoryPreparation D R S) (A : Set Sigma) (hA : MeasurableSet A) : ↑HP.toPreparation.conditionalMeasure A = ↑D.muL (A ∩ compatibleSet S HP.history) / ↑D.muL (compatibleSet S HP.history)

The isolated epistemic law. For measurable A, muH(A) = muL(A ∩ compatibleSet history) / muL(compatibleSet history): ordinary conditioning on the record history, reusing the LF1 normalised conditional measure.