SigmaLayer/OnticBornFrequency: Born as an ontic typicality volume (connectivity, G1)

Category: 7-SigmaLayer (grounding the Born frequency in the ontic typicality).

The general-N Born-frequency capstone LF4/BornFrequencyN.lean samples the projective measure μ_FS on ℂℙⁿ⁻¹ directly (hlaw : map Xₙ = fubiniStudyMeasure). That is the epistemic law, and stating it as the trial hypothesis leaves the trials floating free of the ontic substrate. This file puts the sampling where it belongs — on the ontic floor — and derives the epistemic content:

Ontic vs epistemic.

• Ontic (the floor — the only thing assumed): the space Σ, the deterministic dynamics D, and its typicality measure μ_L = D.muL (ConstraintDynamics.muL). Trials sample μ_L — repeated preparations under ontic ignorance of the microstate (Paper D). That Σ, μ_L exist and that trials are i.i.d.-μ_L is SO-1: the floor, not a derivation (deriving it from a single flow's time-ergodicity is deliberately not the CSD route; typicality is repeated-preparation ignorance).
• Epistemic (everything here is derived, not assumed): the outcome regions Ωᵢ = bornRegion ψ i on the projective base ℂℙⁿ⁻¹, the projective law μ_FS = π_* μ_L (the measure bridge HasFubiniStudyPushforward), and the Born weight.

Results:

• onticBornVolume_eq — Born = the ontic typicality volume. For any projective sector whose π pushes μ_L to μ_FS, the μ_L-measure of the ontic preimage of the epistemic outcome region is exactly the Born weight ‖⟨eᵢ, ψ⟩‖² (via the pushforward + bornRegion_fs_measure_uncond). The epistemic Born number is a theorem about the ontic typicality, not a posited projective measure.
• born_frequency_from_ontic_sampling — the Born frequency from ontic sampling. For i.i.d. trials that sample the ontic μ_L (not μ_FS), the frequency of trials whose ontic microstate lands in the preimage of Ωᵢ converges a.s. to ‖⟨eᵢ, ψ⟩‖². The projective/epistemic law is never assumed — it is derived from the ontic sampling by the measure bridge.

So the only hypothesis is ontic (hlaw : map Xₙ = D.muL, the floor's typicality); μ_FS and Born are consequences. This is the general, sector-level ontic grounding that unified_born_frequency provides only for the concrete productDynamics witness. Foundational-triple, no sorry.

References

SigmaLayer/MeasureBridge.lean (HasFubiniStudyPushforward, productSector_hasFubiniStudyPushforward); LF4/BornRegionUncond.lean (bornRegion_fs_measure_uncond, bornRegion_measurable_uncond); LF1/GeneralFrequency.lean (freq_tendsto_of_iid, the law-agnostic strong law); SigmaLayer/UnifiedFlowedRecords.lean (unified_born_frequency, the product-model instance); specs/connectivity-manifest.md (L5, the sampling caveat this addresses).

theorem CSD.SigmaLayer.onticBornVolume_eq {M : ℕ} {Sigma : Type u_1} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector (M + 1) D) (p₀ : LF4.CPN (M + 1)) (hpush : HasFubiniStudyPushforward Q p₀) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin (M + 1)) : (↑D.muL (Q.pi ⁻¹' LF4.bornRegion ψ hψ0 i)).toReal = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

Born = the ontic typicality volume. If the sector's projection π pushes the ontic typicality μ_L = D.muL forward to μ_FS (the measure bridge), then the μ_L-measure of the ontic preimage π⁻¹(Ωᵢ) of the epistemic outcome region Ωᵢ = bornRegion ψ i is exactly the Born weight ‖⟨eᵢ, ψ⟩‖². The Born number is a theorem about the ontic typicality, derived via the pushforward and bornRegion_fs_measure_uncond — no projective measure is posited.

theorem CSD.SigmaLayer.born_frequency_from_ontic_sampling {M : ℕ} {Sigma : Type u_1} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector (M + 1) D) (p₀ : LF4.CPN (M + 1)) (hpush : HasFubiniStudyPushforward Q p₀) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin (M + 1)) {Ω : Type u_2} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → Sigma) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = ↑D.muL) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' Q.pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' Q.pi ⁻¹' LF4.bornRegion ψ hψ0 i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

The Born frequency from ontic sampling. For i.i.d. trials that sample the ontic typicality μ_L = D.muL (the floor — repeated preparations under ontic ignorance), the frequency of trials whose microstate lands in the ontic preimage π⁻¹(Ωᵢ) of the epistemic outcome region converges almost surely to the Born weight ‖⟨eᵢ, ψ⟩‖². The projective law μ_FS and the Born number are derived from the ontic sampling by the measure bridge (onticBornVolume_eq); the only hypothesis is ontic.

theorem CSD.SigmaLayer.productModel_onticBornVolume {M : ℕ} (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin (M + 1)) : (↑(productDynamics H hH p₀).muL ((productSector H hH p₀).pi ⁻¹' LF4.bornRegion ψ hψ0 i)).toReal = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

Non-vacuity: the ontic Born-volume identity on the concrete product model. The hpush hypothesis is not idle — it is discharged by the proved pushforward productSector_hasFubiniStudyPushforward. On the product model Σ = KSigma, the ontic typicality μ_L = (productDynamics H hH p₀).muL of the preimage of the Born region is exactly the Born weight.