LF4: pure-state ontic Born rule as a frequency limit

Category: 3-Local.

Composes the law-agnostic frequency theorem freq_tendsto_of_iid (LF1) with the operational Born derivation pure_state_born_weights_of_certainty (LF2, via the Busch axiom) to obtain the pure-state ontic Born rule: empirical frequencies of a measurement outcome converge almost surely to |⟨ψ,φ⟩|².

Posits and honest scope

The preparation law μψ is the posited fibre measure over the pure state [ψ] (Paper A / Σ0, revised: pure-state preparation is the conditional measure on the fibre, posited ontic structure, not an ambient μL-conditional). The theorem is conditional on:

• OP + h_certain — operational consistency, the package being certain at ψ (Paper B Def 5.1; Born form then follows by the Busch/Gleason axiom);
• h_bridge — the eq-12 identification of the ontic outcome weight (μψ O).toReal with the operational weight OP.p (rankOneEffect φ).

These are exactly Paper B's posits. The Born form |⟨ψ,φ⟩|² is derived (pure_state_born_weights_of_certainty), not assumed.

Non-vacuity. Because μψ is a posited probability measure (the trial law), not a μL-conditional on a μL-null fibre, the hypotheses are jointly satisfiable. This repairs the inhabitability defect of the LF3 PureSingletPreparation bundle, whose push_dirac-via-μL-conditional form is incompatible with the continuous measure bridge π∗μL = c·μFS (a single quantum state's fibre is μL-null). See LF4-todo §8.

theorem CSD.LF4.ontic_born_frequency {N : ℕ} (hN : 2 ≤ N) {SigmaSpace : Type u_1} {Ω : Type u_2} [MeasurableSpace SigmaSpace] [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : ℕ → Ω → SigmaSpace} (hX : ∀ (n : ℕ), Measurable (X n)) {μψ : MeasureTheory.Measure SigmaSpace} (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) 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)) (OP : LF2.OperationalPackage N) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) (h_certain : OP.p (LF2.rankOneEffect ψ hψ) = 1) {φ : EuclideanSpace ℂ (Fin N)} (hφ : ‖φ‖ = 1) (h_bridge : (μψ O).toReal = OP.p (LF2.rankOneEffect φ hφ)) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' O).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (‖inner ℂ ψ φ‖ ^ 2))

Pure-state ontic Born rule (conditional, non-vacuous). For i.i.d. trials with preparation law μψ, an outcome region O whose ontic weight equals the operational Born weight (h_bridge), and an operational package OP certain at the pure state ψ, the empirical frequencies converge almost surely to |⟨ψ,φ⟩|².