LF4 general-N capstone: Busch-free frequency → Born for all N coordinates

Category: 3-Local (Busch-free frequency → Born for all N coordinates).

Glossary: https://glossary.constraintsurfacedynamics.com/typicality-volume/ Plain-language, CSD-role and formal statements of the typicality volume. ⚠️ The entry anchors born_frequency_convergence_N_uncond (BornRegionUncond.lean), not the form here: the published text says the genericity hypotheses are retired, and hpos below is exactly such a hypothesis. Kept symmetric by scripts/check-glossary.sh.

The headline empirical payoff of the general-N Duistermaat–Heckman / Born-from-Kähler- volume programme. The qubit had qubit_born_frequency_convergence_uncond (single outcome, N = 2); this is the joint, general-N, unconditional, Busch-free form:

For i.i.d. trials drawn from the genuine Fubini–Study measure on ℂℙ^M, the empirical frequencies of the N barycentric moment-outcome regions converge — on a single almost-sure event — to the Born weights ‖⟨eᵢ, ψ⟩‖² of a fully-generic preparation ψ.

The Born values enter through fs_born_volume_ratio_N (free coordinates) and fs_born_volume_ratio_N_apex (the dropped apex), which are theorems (the qubit h_uniform is the proved headline fs_moment_joint_dirichlet_N). So the whole chain is foundational-triple-only: deterministic repeated-trial typicality (LF1) + Born = Kähler volume (the moment-map cluster) ⟹ frequencies → Born, with Born derived from the symplectic geometry, never imported via Gleason/busch_effect_gleason.

Genericity hypothesis ∀ j, 0 < ‖⟨eⱼ, ψ⟩‖² (no vanishing amplitude): makes the free Born vector an interior simplex point, so every barycentric region is a homeomorphic image of the open simplex (open, measurable) and stays inside it.

Reusable openness (ψ-agnostic)

theorem CSD.LF4.replaceMap_image_isOpen {M : ℕ} (b : Fin M → ℝ) (i : Fin M) (h : LinearMap.det (replaceMap b i) ≠ 0) : IsOpen (⇑(replaceMap b i) '' openSimplexFree)

The image of the open simplex under a det ≠ 0 vertex-replacement map is open.

theorem CSD.LF4.apexLin_image_isOpen {M : ℕ} (b : Fin M → ℝ) (h : LinearMap.det (apexLin b) ≠ 0) : IsOpen ((fun (x : Fin M → ℝ) => (apexLin b) x + b) '' openSimplexFree)

The image of the open simplex under the det ≠ 0 affine apex map is open.

Free Born vector coordinates

theorem CSD.LF4.ratioN_momentMap_castSucc {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (k : Fin M) : ratioN (fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j) k = ‖inner ℂ (EuclideanSpace.single k.castSucc 1) ψ‖ ^ 2

The k-th free Born coordinate is the Born weight at castSucc k.

theorem CSD.LF4.one_sub_sum_ratioN_momentMap {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : 1 - ∑ k : Fin M, ratioN (fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j) k = ‖inner ℂ (EuclideanSpace.single (Fin.last M) 1) ψ‖ ^ 2

1 − ∑(free Born coords) is the Born weight at the apex (Fin.last M).

The Born outcome regions and the capstone

noncomputable def CSD.LF4.bornRegion {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) : Fin (M + 1) → Set (CPN (M + 1))

The N = M+1 barycentric Born outcome regions on ℂℙ^M: the replaceMap sub-simplices for the free coordinates and the affine apex region for the last, pulled back through the moment map.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF4.bornRegion_measurable {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (hpos : ∀ (j : Fin (M + 1)), 0 < ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2) (i : Fin (M + 1)) : MeasurableSet (bornRegion ψ hψ0 i)

Each Born region is measurable (an open image pulled back through a measurable map). An hpos-free form is available: bornRegion_measurable_uncond (BornRegionUncond.lean).

theorem CSD.LF4.bornRegion_fs_measure {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (hpos : ∀ (j : Fin (M + 1)), 0 < ‖inner ℂ (EuclideanSpace.single j 1) ψ‖ ^ 2) (i : Fin (M + 1)) : ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (bornRegion ψ hψ0 i)).toReal = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

The Fubini–Study measure of the i-th Born region is the Born weight ‖⟨eᵢ, ψ⟩‖² (real form). The "Born = ontic volume" content, supplied by the volume route — fs_born_volume_ratio_N / _apex, no Busch. An hpos-free form is available: bornRegion_fs_measure_uncond (BornRegionUncond.lean).

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

General-N Busch-free joint frequency → Born convergence. For i.i.d. trials drawn from the Fubini–Study measure on ℂℙ^M, the empirical frequencies of the N barycentric Born regions converge, on a single almost-sure event, to the Born weights ‖⟨eᵢ, ψ⟩‖² of a fully-generic preparation ψ. Foundational-triple-only; no busch_effect_gleason. The CSD thesis realised end-to-end for general N: deterministic typicality + Born = Kähler volume ⟹ frequencies → Born. An hpos-free form is available: born_frequency_convergence_N_uncond (BornRegionUncond.lean).