LF1 Outcomes

Category: 3-Local (LF1 outcome regions and their weights).

Outcome regions are measurable ontic regions associated with a fixed experimental context. In LF1 they are treated abstractly as measurable sets. The realised outcome of a single trial is determined by whether the deterministic evolution of the sampled microstate lands in the corresponding outcome region.

No stochastic outcome law is postulated at this stage.

Coding choice: single region, not a partition family

The manuscript describes a measurable outcome partition {Ω_i^Σ} of the ontic state space. This file formalises one element of that partition at a time via OutcomeRegion.

This is deliberate and mathematically sufficient for LF1: the frequency theorem is proved for an arbitrary fixed O : OutcomeRegion. To obtain the joint almost-sure statement for a finite partition {O_1, ..., O_k}, apply the theorem once per element and intersect the resulting full-measure sets — a finite intersection of full-measure sets is still full-measure, so no new structure is needed.

A formalised OutcomePartition type (carrying disjointness, exhaustion, and a measurable family) would be the right object if a future layer (LF2/LF4) needs to reason about partition sums such as Σ_i weight(O_i) = 1 or POVM completeness. That extension should be built in the layer that first requires it, not here.

structure CSD.LF1.OnticSetup.OutcomeRegion {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (_S : OnticSetup SigmaSpace) : Type u_1

A single measurable outcome region in the ontic state space. Parameterized by S so that S.OutcomeRegion works as dot notation.

• Ω : Set SigmaSpace
• hΩ_meas : MeasurableSet self.Ω

noncomputable def CSD.LF1.OnticSetup.OutcomeRegion.preEvent {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : Set SigmaSpace

The pullback event of an outcome region under the deterministic flow Φ.

Equations

• O.preEvent = S.Φ ⁻¹' O.Ω

theorem CSD.LF1.OnticSetup.OutcomeRegion.measurable_preEvent {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : MeasurableSet O.preEvent

noncomputable def CSD.LF1.OnticSetup.OutcomeRegion.prepEvent {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : Set SigmaSpace

The preparation-side version of the event.

Equations

• O.prepEvent = S.Ω0 ∩ O.preEvent

theorem CSD.LF1.OnticSetup.OutcomeRegion.measurable_prepEvent {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : MeasurableSet O.prepEvent

noncomputable def CSD.LF1.OnticSetup.OutcomeRegion.weight {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : ENNReal

The outcome weight under the preparation probability measure.

Equations

• O.weight = ↑S.prepMeasure O.preEvent

noncomputable def CSD.LF1.OnticSetup.OutcomeRegion.weightReal {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : ℝ

The outcome weight as a real number, for use in convergence statements.

Equations

• O.weightReal = O.weight.toReal

theorem CSD.LF1.OnticSetup.OutcomeRegion.weight_eq_prepEvent_div {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} (O : S.OutcomeRegion) : O.weight = ↑S.μL O.prepEvent / ↑S.μL S.Ω0

The outcome weight equals the Liouville volume of prepEvent divided by μL(Ω0): weight = μL(Ω0 ∩ Φ⁻¹(O.Ω)) / μL(Ω0).

Connects the abstract weight (defined via prepMeasure) to the preparation-side initial-condition event prepEvent = Ω0 ∩ Φ⁻¹(O.Ω). The right-hand side is the fraction of the preparation region whose deterministic evolution lands in the outcome region: the volume-typicality reading of the weight.