LF1 Trials

Category: 3-Local (LF1 repeated-trial probability space and i.i.d. preparation sampling).

This file introduces the repeated-preparation model used in LF1. Each trial begins from a fresh initial microstate sampled from the conditional preparation measure on the preparation region. The resulting product measure models repetition of preparation, not stochastic dynamics of a single trial.

Single-trial evolution remains deterministic at the ontic level.

structure CSD.LF1.OnticSetup.TrialModel {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) (Ω : Type u_2) [MeasurableSpace Ω] : Type (max u_1 u_2)

A repeated-trial model for LF1.

Ω is the external sample space indexing repeated experimental runs. P is the probability law on that sample space. X n is the ontic initial microstate used on the n-th trial.

Each X n is measurable and has law equal to the preparation probability measure S.prepMeasure. Independence and identical distribution are declared as explicit hypotheses in Convergence.lean, where the law of large numbers is applied.

• P : MeasureTheory.ProbabilityMeasure Ω
• X : ℕ → Ω → SigmaSpace
• hX_measurable (n : ℕ) : Measurable (self.X n)
• hLaw (n : ℕ) : MeasureTheory.Measure.map (self.X n) ↑self.P = ↑S.prepMeasure

theorem CSD.LF1.OnticSetup.TrialModel.measurable_X {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (n : ℕ) : Measurable (T.X n)

def CSD.LF1.OnticSetup.TrialModel.trialEvent {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : Set Ω

The event on the external sample space that the n-th trial lands in the pulled-back outcome region associated with O.

Equations

• T.trialEvent O n = T.X n ⁻¹' O.preEvent

theorem CSD.LF1.OnticSetup.TrialModel.measurable_trialEvent {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : MeasurableSet (T.trialEvent O n)

theorem CSD.LF1.OnticSetup.TrialModel.trialEvent_eq_comp_preimage {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : T.trialEvent O n = S.Φ ∘ T.X n ⁻¹' O.Ω

The trial event is the preimage of the outcome region under the composition Φ ∘ X n.

This makes the deterministic structure explicit: a sample point ω is in the trial event if and only if the n-th initial microstate X n ω, after evolving under the ontic flow Φ, lands in the outcome region O.Ω.

noncomputable def CSD.LF1.OnticSetup.TrialModel.trialProb {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : ENNReal

The probability of the n-th trial landing in outcome region O, computed on the external sample space.

Equations

• T.trialProb O n = ↑T.P (T.trialEvent O n)

theorem CSD.LF1.OnticSetup.TrialModel.trialProb_eq_weight {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : T.trialProb O n = O.weight

The trial probability agrees with the preparation weight of O.

theorem CSD.LF1.OnticSetup.TrialModel.trialProb_eq_trialProb_zero {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] {S : OnticSetup SigmaSpace} {Ω : Type u_2} [MeasurableSpace Ω] (T : S.TrialModel Ω) (O : S.OutcomeRegion) (n : ℕ) : T.trialProb O n = T.trialProb O 0

All trial probabilities agree, because each trial has the same law.