LF4 general-N Slice E (Born lift): Born = Fubini–Study volume ratio on Σ

Category: 3-Local (Born = Fubini–Study volume ratio on Σ).

Glossary: https://glossary.constraintsurfacedynamics.com/born-volume-ratio/ Plain-language, CSD-role and formal statements of the Born volume ratio. ⚠️ The entry anchors fs_born_volume_ratio_N_uncond (BornRegionUncond.lean), not the form here: it says the genericity hypothesis is retired, and hpos below is exactly that hypothesis. Kept symmetric by scripts/check-glossary.sh.

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

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

The general-N analogue of fs_born_volume_ratio_qubit (qubit, N = 2), now unconditional — the qubit's h_uniform hypothesis is the Slice E headline fs_moment_joint_dirichlet_N, which is a theorem. Three steps:

• E4a fs_volume_eq_dirichlet — the Duistermaat–Heckman volume law on Σ: the Fubini–Study measure of a measurable moment-coordinate region R ⊆ openSimplexFree is M! times its Lebesgue volume.
• E4b volume_openSimplexFree — the standard simplex has volume (M!)⁻¹, forced by μ_FS being a probability measure (a simplex-volume fact derived via Kähler geometry + Gaussians).
• E4c fs_born_volume_ratio_N — for each free coordinate i : Fin M, the FS measure of the i-th barycentric region (pulled back through the moment map) equals the Born weight ‖⟨e_{castSucc i}, ψ⟩‖². No carving, no busch_effect_gleason.
• fs_born_volume_ratio_N_apex — the last coordinate (the dropped apex, index M), via the affine apex map A(x) = L(x) + b' with det L = 1 − ∑b' = b_M. Together with E4c this covers all N coordinates.

Scope

fs_born_volume_ratio_N + fs_born_volume_ratio_N_apex land Born on all N coordinates of a fully-generic preparation (the qubit gave 1 of 2). The genericity hypothesis ∀ j, 0 < ‖⟨eⱼ,ψ⟩‖² (no vanishing amplitude) makes freeBornVec ψ an interior simplex point, so each barycentric region is a homeomorphic image of the open simplex (hence open, measurable) and stays inside it.

theorem CSD.LF4.measurable_ratio_momentMap {M : ℕ} : Measurable fun (p : CPN (M + 1)) => ratioN fun (i : Fin (M + 1)) => momentMap p i

The free-coordinate moment map p ↦ ratioN (momentMap p) is measurable.

theorem CSD.LF4.fs_volume_eq_dirichlet {M : ℕ} (p₀ : CPN (M + 1)) {R : Set (Fin M → ℝ)} (hR : MeasurableSet R) (hRsub : R ⊆ openSimplexFree) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ((fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1)))) => ratioN fun (i : Fin (M + 1)) => momentMap p i) ⁻¹' R) = ↑M.factorial * MeasureTheory.volume R

E4a: the Duistermaat–Heckman volume law on Σ. For a measurable region R of the free moment simplex with R ⊆ openSimplexFree, the Fubini–Study measure of its pullback equals M! times the Lebesgue volume of R. Unconditional; the genuine general-N DH content on Σ.

theorem CSD.LF4.volume_openSimplexFree {M : ℕ} : MeasureTheory.volume openSimplexFree = (↑M.factorial)⁻¹

E4b: the standard simplex has volume (M!)⁻¹. Forced by μ_FS being a probability measure: pushing it forward gives M! · vol|_{openSimplexFree}, whose total mass is 1. A simplex-volume fact obtained via the Kähler/Gaussian route.

E4c: the barycentric region and the Born volume ratio

theorem CSD.LF4.replaceMap_apply {N : ℕ} (b : Fin N → ℝ) (i : Fin N) (t : Fin N → ℝ) (k : Fin N) : (replaceMap b i) t k = b k * t i + if k = i then 0 else t k

Coordinate formula for the vertex-replacement map: (replaceMap b i t) k = b k · t i + (t k if k ≠ i else 0).

theorem CSD.LF4.isOpen_openSimplexFree {M : ℕ} : IsOpen openSimplexFree

The open free simplex is an open set.

theorem CSD.LF4.replaceMap_image_subset {M : ℕ} (b : Fin M → ℝ) (i : Fin M) (hb : b ∈ openSimplexFree) : ⇑(replaceMap b i) '' openSimplexFree ⊆ openSimplexFree

The i-th barycentric region stays inside the simplex when b is an interior point (b ∈ openSimplexFree): the subdivision of the simplex at an interior point.

theorem CSD.LF4.fs_born_volume_ratio_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) (i : Fin M) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ((fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1)))) => ratioN fun (j : Fin (M + 1)) => momentMap p j) ⁻¹' ⇑(replaceMap (ratioN fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j) i) '' openSimplexFree) = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single i.castSucc 1) ψ‖ ^ 2)

E4c: Born weight = Fubini–Study volume ratio on Σ (general N, free coords). For a fully-generic unit preparation ψ (no vanishing amplitude), the Fubini–Study measure of the i-th barycentric region of the moment simplex (pulled back through the moment map) equals the Born weight ‖⟨e_{castSucc i}, ψ⟩‖². Unconditional — the qubit h_uniform hypothesis is now the proved headline fs_moment_joint_dirichlet_N. No carving, no busch_effect_gleason. An hpos-free form is available: fs_born_volume_ratio_N_uncond (BornRegionUncond.lean).

Apex coordinate (the dropped vertex, index M)

The free-coordinate subdivision treats coordinate M (mapped to the origin in free coordinates) asymmetrically: its barycentric region is the corner simplex with apex moved from 0 to b', the image under the affine map A(x) = L(x) + b' with linear part L(x) = x − (∑x)•b', det L = 1 − ∑b' = b_M. This closes the last coordinate left open by fs_born_volume_ratio_N.

noncomputable def CSD.LF4.apexLin {M : ℕ} (b : Fin M → ℝ) : (Fin M → ℝ) →ₗ[ℝ] Fin M → ℝ

The linear part of the apex map: L(x) = x − (∑ⱼxⱼ)•b, matrix 1 − b⊗𝟙.

Equations

• CSD.LF4.apexLin b = Matrix.toLin' (1 - Matrix.of fun (k x : Fin M) => b k)

theorem CSD.LF4.apexLin_apply {M : ℕ} (b x : Fin M → ℝ) (k : Fin M) : (apexLin b) x k = x k - (∑ j : Fin M, x j) * b k

Coordinate formula for the apex linear part: (apexLin b x) k = x k − (∑ x)·b k.

theorem CSD.LF4.apexLin_det {M : ℕ} (b : Fin M → ℝ) : LinearMap.det (apexLin b) = 1 - ∑ k : Fin M, b k

det (apexLin b) = 1 − ∑ b (matrix determinant lemma via det_one_sub_mul_comm).

theorem CSD.LF4.apexMap_image_subset {M : ℕ} (b : Fin M → ℝ) (hb : b ∈ openSimplexFree) : (fun (x : Fin M → ℝ) => (apexLin b) x + b) '' openSimplexFree ⊆ openSimplexFree

The apex region stays inside the simplex when b is an interior point: A(x) k = x k + (1 − ∑x)·b k, and ∑ A(x) = ∑x + (1 − ∑x)∑b, with 1 − ∑A(x) = (1 − ∑x)(1 − ∑b) > 0.

theorem CSD.LF4.fs_born_volume_ratio_N_apex {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) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ((fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin (M + 1)))) => ratioN fun (j : Fin (M + 1)) => momentMap p j) ⁻¹' (fun (x : Fin M → ℝ) => (apexLin (ratioN fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j)) x + ratioN fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j) '' openSimplexFree) = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single (Fin.last M) 1) ψ‖ ^ 2)

Apex coordinate of E4c. For the last coordinate (the dropped vertex, index M), the Fubini–Study measure of the apex barycentric region equals the Born weight ‖⟨e_{last M}, ψ⟩‖². Together with fs_born_volume_ratio_N this covers all N coordinates of a fully-generic preparation. Unconditional; no busch_effect_gleason. An hpos-free form is available: fs_born_volume_ratio_N_apex_uncond (BornRegionUncond.lean).