LF4: the Born-region volume/frequency engine, unconditional (genericity retired)

Category: 3-Local (LF4 Born-from-Kähler-volume engine, hpos-free upgrade).

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

Glossary: https://glossary.constraintsurfacedynamics.com/born-volume-ratio/ The published entry states the Born-weight = FS-volume-ratio identity with the genericity hypothesis retired, so it anchors fs_born_volume_ratio_N_uncond here rather than the hpos-carrying form in MomentBornN.lean. Kept symmetric by scripts/check-glossary.sh.

Glossary: https://glossary.constraintsurfacedynamics.com/typicality-volume/ The published entry claims the genericity hypotheses are retired, so it anchors born_frequency_convergence_N_uncond here rather than the hpos-carrying form in BornFrequencyN.lean. Kept symmetric by scripts/check-glossary.sh.

The general-N Born = FS-volume engine (fs_born_volume_ratio_N / _apex, bornRegion_fs_measure, born_frequency_convergence_N) and the POVM tranche wrappers (povm_born_eq_dilated_volume, povm_born_frequency_volume) carried a genericity hypothesis hpos : ∀ j, 0 < ‖⟨eⱼ, ψ⟩‖² (no vanishing amplitude). This file retires that caveat: every result is re-proved for an arbitrary unit ψ ≠ 0, with statements otherwise verbatim (_uncond suffixes). Additive: the audited originals in MomentBornN.lean / BornFrequencyN.lean / POVMVolume.lean are untouched; corpus-wide call-site migration is deferred.

The per-cell dichotomy

For any unit ψ, the free Born vector b lies in the closed free simplex (0 ≤ b k, ∑ b ≤ 1 — free, from momentMap_sum_eq_one + nonnegativity of ‖·‖²). Per cell:

• positive branch (b i > 0): det (replaceMap b i) = b i ≠ 0 per cell (no joint hypothesis), and the simplex-subdivision subset lemma survives with only the closed-simplex bounds (replaceMap_image_subset_of_closedSimplex). The audited fs_volume_eq_dirichlet + replaceMap_image_volume route then runs verbatim.
• zero branch (b i = 0): det = 0, so the cell's Lebesgue volume vanishes (Measure.addHaar_image_linearMap at |det| = 0); the joint Dirichlet law (fs_volume_eq_dirichlet_inter, no subset hypothesis) then forces the FS measure of the pulled-back cell to 0 — which is the Born weight.
• apex cell: the same dichotomy on 1 − ∑ b via apexLin (affine image = translate of a linear image).

Measurability of a degenerate (det-0) image cannot use the open-image argument; instead every cell image is measurable det-free: openSimplexFree is an open subset of ℝ^M, hence σ-compact, and continuous images of σ-compact sets are σ-compact, hence Borel (image_openSimplexFree_measurableSet).

No carving: the regions are the same ψ-indexed moment-subdivision cells as the audited engine; the zero-weight cells genuinely collapse to FS-null sets, they are not redefined to hit Born values. Gleason-free throughout (no busch_effect_gleason).

Det-free measurability of the barycentric cell images (σ-compact route)

theorem CSD.LF4.isSigmaCompact_openSimplexFree {M : ℕ} : IsSigmaCompact openSimplexFree

The open free simplex is σ-compact: it is an open subset of the locally compact, second-countable ℝ^M, hence itself a locally compact second-countable space, hence σ-compact (sigmaCompactSpace_of_locallyCompact_secondCountable).

theorem CSD.LF4.image_openSimplexFree_measurableSet {M : ℕ} {f : (Fin M → ℝ) → Fin M → ℝ} (hf : Continuous f) : MeasurableSet (f '' openSimplexFree)

Det-free measurability of continuous images of the open simplex. The continuous image of a σ-compact set is σ-compact — a countable union of compacts, each closed (T2) hence Borel. Replaces the open-image argument, which dies at det = 0.

theorem CSD.LF4.replaceMap_image_measurableSet {M : ℕ} (b : Fin M → ℝ) (i : Fin M) : MeasurableSet (⇑(replaceMap b i) '' openSimplexFree)

The i-th barycentric cell image is measurable, for every b (no determinant hypothesis).

theorem CSD.LF4.apexMap_image_measurableSet {M : ℕ} (b : Fin M → ℝ) : MeasurableSet ((fun (x : Fin M → ℝ) => (apexLin b) x + b) '' openSimplexFree)

The apex barycentric cell image is measurable, for every b (no determinant hypothesis).

The joint Dirichlet law without the subset hypothesis

theorem CSD.LF4.fs_volume_eq_dirichlet_inter {M : ℕ} (p₀ : CPN (M + 1)) {R : Set (Fin M → ℝ)} (hR : MeasurableSet R) : (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 ∩ openSimplexFree)

The Duistermaat–Heckman volume law for an arbitrary measurable region R (no R ⊆ openSimplexFree): the FS measure of the pullback is M! times the Lebesgue volume of R ∩ openSimplexFree. The zero-branch workhorse — the proof is fs_volume_eq_dirichlet's minus its final subset rewrite.

Subset lemmas under the closed-simplex bounds

theorem CSD.LF4.replaceMap_image_subset_of_closedSimplex {M : ℕ} (b : Fin M → ℝ) (i : Fin M) (hb0 : ∀ (k : Fin M), 0 ≤ b k) (hbsum : ∑ k : Fin M, b k ≤ 1) (hbi : 0 < b i) : ⇑(replaceMap b i) '' openSimplexFree ⊆ openSimplexFree

Subdivision subset lemma, closed-simplex form. The i-th barycentric cell stays inside the simplex assuming only 0 ≤ b, ∑ b ≤ 1, and the per-cell positivity 0 < b i (the only coordinate whose strict positivity the k = i coordinate of the image needs). Replaces the joint-genericity hypothesis b ∈ openSimplexFree of replaceMap_image_subset.

theorem CSD.LF4.apexMap_image_subset_of_closedSimplex {M : ℕ} (b : Fin M → ℝ) (hb0 : ∀ (k : Fin M), 0 ≤ b k) (hbsum : ∑ k : Fin M, b k < 1) : (fun (x : Fin M → ℝ) => (apexLin b) x + b) '' openSimplexFree ⊆ openSimplexFree

Apex subset lemma, closed-simplex form. The apex cell stays inside the simplex assuming only 0 ≤ b and ∑ b < 1 (which is the apex positive-branch hypothesis: the apex weight is 1 − ∑ b). Replaces b ∈ openSimplexFree of apexMap_image_subset.

Apex cell volume (any b in the closed simplex)

theorem CSD.LF4.apexMap_image_volume {M : ℕ} (b : Fin M → ℝ) (hb : 0 ≤ 1 - ∑ k : Fin M, b k) : MeasureTheory.volume ((fun (x : Fin M → ℝ) => (apexLin b) x + b) '' openSimplexFree) = ENNReal.ofReal (1 - ∑ k : Fin M, b k) * MeasureTheory.volume openSimplexFree

The apex cell's Lebesgue volume is (1 − ∑ b) times the simplex volume, for any b with ∑ b ≤ 1 — including the degenerate ∑ b = 1, where the affine image is a translate of a det = 0 linear image, hence null. (Translation invariance + Measure.addHaar_image_linearMap + apexLin_det.)

The unconditional volume headlines (per-cell dichotomy)

theorem CSD.LF4.fs_born_volume_ratio_N_uncond {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (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)

Born = FS-volume ratio, free coordinates, unconditional. Statement of fs_born_volume_ratio_N with the genericity hypothesis hpos removed: valid for every unit preparation ψ ≠ 0. Positive cells by the closed-simplex subset argument; zero cells by the det-0 null image + the joint Dirichlet law (the cell's FS volume genuinely vanishes — no carving).

theorem CSD.LF4.fs_born_volume_ratio_N_apex_uncond {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : (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)

Born = FS-volume ratio, apex coordinate, unconditional. Statement of fs_born_volume_ratio_N_apex with hpos removed: the dichotomy on the apex weight 1 − ∑ b.

The unconditional Born regions, frequency capstone, POVM wrappers

theorem CSD.LF4.bornRegion_measurable_uncond {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (i : Fin (M + 1)) : MeasurableSet (bornRegion ψ hψ0 i)

Each Born region is measurable — for every ψ ≠ 0 (no norm or genericity hypothesis; the σ-compact image argument is det-free).

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

Born = FS volume of the Born regions, unconditional (real form). bornRegion_fs_measure minus hpos.

theorem CSD.LF4.born_frequency_convergence_N_uncond {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) {Ω : 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, unconditional. born_frequency_convergence_N minus hpos: valid for every unit preparation, vanishing amplitudes included (their regions are FS-null and their frequencies converge to 0 = the Born weight). Foundational-triple-only.

theorem CSD.LF4.povm_born_eq_dilated_volume_uncond {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : ℕ} (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (i : ι) (e : Fin N × ι ≃ Fin (M + 1)) (p₀ : CPN (M + 1)) (hnorm : ‖(LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin D.V) ψ)‖ = 1) : P.weight ψ i = ∑ n : Fin N, ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (bornRegion ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin D.V) ψ)) ⋯ (e (n, i)))).toReal

POVM Born weight as a sum of FS volumes, unconditional (P.3b minus hpos). The dilated state may have vanishing amplitudes (as the von Neumann post-flow state does on every off-diagonal cell); the corresponding cells are FS-null and contribute 0 to the block sum.

theorem CSD.LF4.povm_born_frequency_volume_uncond {N : ℕ} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : ℕ} (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace ℂ (Fin N)) (e : Fin N × ι ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin D.V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : CPN (M + 1)) {Ω : Type u_2} [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 : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : ι), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin N, (∑ k ∈ Finset.range m, (X k ⁻¹' bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (P.weight ψ i))

POVM empirical frequencies → POVM Born weight, unconditional (P.4 minus hpos). Valid for every unit dilated preparation, vanishing dilated amplitudes included.