LF1 General frequency theorem (law-agnostic)

Category: 3-Local.

Glossary: https://glossary.constraintsurfacedynamics.com/typicality/ Plain-language, CSD-role and formal statements of typicality, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The law-agnostic core of LF1_main_theorem_ae. For i.i.d. Σ-valued trials X : ℕ → Ω → Σ with a common law μp (any probability measure), the empirical frequency of a measurable outcome region O ⊆ Σ converges almost surely to the ontic weight (μp O).toReal.

The preparation enters only as the probability measure μp. The Ω₀-conditional preparation (OnticSetup.prepMeasure) is one instance; a posited fibre measure μ_[ψ] for a pure-state preparation is another. This is the formal counterpart of the ambient/fibre split: ambient μL-conditionals for mixed states, fibre measures for pure states (Paper A / Σ0, revised). μ_[ψ] is posited ontic structure, so no disintegration machinery is needed here — it enters downstream simply as a probability measure pushing to a Dirac on [ψ].

The proof is the same strong-law wrapper used in Convergence.lean, with S.prepMeasure replaced by the abstract μp.

theorem CSD.LF1.freq_tendsto_of_iid {SigmaSpace : Type u_1} {Ω : Type u_2} [MeasurableSpace SigmaSpace] [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℕ → Ω → SigmaSpace} (hX : ∀ (n : ℕ), Measurable (X n)) {μp : MeasureTheory.Measure SigmaSpace} (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) P = μp) {O : Set SigmaSpace} (hO : MeasurableSet O) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g P) fun (n : ℕ) => (X n ⁻¹' O).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (N : ℕ) => (∑ i ∈ Finset.range N, (X i ⁻¹' O).indicator (fun (x : Ω) => 1) ω) / ↑N) Filter.atTop (nhds (μp O).toReal)

General repeated-trial frequency theorem. I.i.d. trials with common law μp make the empirical frequency of a measurable outcome region O converge almost surely to (μp O).toReal.