LF4: pairwise disjointness of the Born regions, the per-microstate outcome map

Category: 3-Local (LF4 Born-from-Kähler-volume engine, outcome-map tranche).

This is LF5-F (engine half) of specs/lf5-plan.md: the upgrade of the LF5 layer from outcome statistics (sums of cell-indicator frequencies) to a deterministic per-microstate outcome function. The owed fact, named as the gate in LF5/Capstone.lean's docstring and noted owed since the aeece86 degenerate-witness commit, is the pairwise disjointness of the bornRegion cells — the moment-subdivision is a genuine partition, so a microstate lands in at most one cell.

What is delivered

• Image-level disjointness, unconditional (any b in the closed free simplex 0 ≤ b, ∑ b ≤ 1): replaceMap_image_disjoint_replaceMap (free i vs free j, i ≠ j) and replaceMap_image_disjoint_apexMap (free i vs apex). Division-free coordinate arguments.
• bornRegion_pairwiseDisjoint — preimages of disjoint sets are disjoint; the Born vector b = ratioN (momentMap [ψ]) is in the closed free simplex for every ψ ≠ 0 (no norm hypothesis).
• bornRegion_ae_cover — the cells cover ℂℙ^M up to an FS-null set (unit ψ): measure_iUnion over the disjoint measurable family sums to ∑ ‖⟨eᵢ,ψ⟩‖² = ‖ψ‖² = 1.
• bornOutcome — the per-microstate outcome map CPN (M+1) → Option (Fin (M+1)) (some i on cell i, none off the union); bornOutcome_eq_some_iff, bornOutcome_preimage_some, measurability, a.e.-totality bornOutcome_ae_isSome.
• indicator_iUnion_disjoint — the indicator of a disjoint finite union is the sum of indicators (a thin wrapper of Set.indicator_biUnion_apply).

Honest scope

The cells are the same ψ-indexed moment-subdivision cells as the audited volume engine; nothing is carved. The disjointness is a genuine geometric fact of the barycentric subdivision at the closed-simplex point b. Born values enter through bornRegion_fs_measure_uncond (the FS-volume = Born engine); Φ = id still (D1). This file makes the partition structure formal; it does not exercise dynamics.

Image-level pairwise disjointness (closed free simplex, unconditional)

theorem CSD.LF4.replaceMap_image_disjoint_replaceMap {M : ℕ} (b : Fin M → ℝ) (i j : Fin M) (hb0 : ∀ (k : Fin M), 0 ≤ b k) (hij : i ≠ j) : Disjoint (⇑(replaceMap b i) '' openSimplexFree) (⇑(replaceMap b j) '' openSimplexFree)

Free vs free disjointness. For b in the closed free simplex (0 ≤ b, ∑ b ≤ 1) and i ≠ j, the i-th and j-th vertex-replacement cell images are disjoint. Division-free: from cell-i membership xⱼ·bᵢ − xᵢ·bⱼ = tⱼ·bᵢ ≥ 0 and cell-j membership xᵢ·bⱼ − xⱼ·bᵢ = t'ᵢ·bⱼ ≥ 0, adding forces bᵢ = bⱼ = 0, then xᵢ = bᵢ·tᵢ = 0 contradicts xᵢ = t'ᵢ > 0.

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

Free vs apex disjointness. For b in the closed free simplex, the i-th vertex-replacement cell image and the apex cell image are disjoint. Division-free: cell-i gives (1−∑x)·bᵢ − xᵢ·(1−∑b) = (1−∑t)·bᵢ ≥ 0; apex gives xᵢ·(1−∑b) − (1−∑x)·bᵢ = t'ᵢ·(1−∑b) ≥ 0; adding forces bᵢ = 0 and ∑b = 1, then xᵢ = bᵢ·tᵢ = 0 contradicts xᵢ = t'ᵢ > 0.

Born vector closed-simplex bounds (any ψ ≠ 0, no norm)

theorem CSD.LF4.ratioN_momentMap_nonneg {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (k : Fin M) : 0 ≤ ratioN (fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j) k

The free Born vector lies in the closed free simplex: each coordinate is nonnegative. Holds for every ψ ≠ 0 (the moment ratio is a ratio of nonnegatives); no norm hypothesis.

theorem CSD.LF4.ratioN_momentMap_sum_le_one {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) : ∑ k : Fin M, ratioN (fun (j : Fin (M + 1)) => momentMap (Projectivization.mk ℂ ψ hψ0) j) k ≤ 1

The free Born vector's coordinates sum to at most one (the dropped apex weight is nonnegative). Holds for every ψ ≠ 0; no norm hypothesis.

Pairwise disjointness of the Born regions

theorem CSD.LF4.bornRegion_pairwiseDisjoint {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) : Pairwise (Function.onFun Disjoint (bornRegion ψ hψ0))

The Born regions are pairwise disjoint, every ψ ≠ 0. Preimages of disjoint sets are disjoint; the Fin.lastCases split dispatches to the two image-level disjointness lemmas, with the Born vector in the closed free simplex by ratioN_momentMap_nonneg / ratioN_momentMap_sum_le_one. No norm or genericity hypothesis.

a.e. coverage (unit ψ)

theorem CSD.LF4.sum_inner_single_sq {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) : ∑ i : Fin (M + 1), ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2 = ‖ψ‖ ^ 2

Parseval: ∑ᵢ ‖⟨eᵢ, ψ⟩‖² = ‖ψ‖².

theorem CSD.LF4.bornRegion_iUnion_fs_measure {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (⋃ (i : Fin (M + 1)), bornRegion ψ hψ0 i) = 1

The FS measure of the union of the Born regions is 1 (unit ψ): measure_iUnion over the disjoint measurable family, summing to ∑ ‖⟨eᵢ,ψ⟩‖² = ‖ψ‖² = 1. ENNReal-level form.

theorem CSD.LF4.bornRegion_ae_cover {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (⋃ (i : Fin (M + 1)), bornRegion ψ hψ0 i)ᶜ = 0

a.e. coverage: the complement of the union of the Born regions is FS-null (unit ψ). The cells partition ℂℙ^M up to a null set.

The per-microstate outcome map

@[instance_reducible]

instance CSD.LF4.instMeasurableSpaceOptionFin (n : ℕ) : MeasurableSpace (Option (Fin n))

The discrete (⊤) measurable space on Option (Fin n) — the codomain of the outcome map. Option (Fin n) is finite, hence the discrete σ-algebra is the only natural choice and every set is measurable. Mathlib provides Fin.instMeasurableSpace := ⊤ but no Option instance; this supplies it locally for the outcome-map measurability statement.

Equations

• CSD.LF4.instMeasurableSpaceOptionFin n = ⊤

instance CSD.LF4.instMeasurableSingletonClassOptionFin (n : ℕ) : MeasurableSingletonClass (Option (Fin n))

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

The per-microstate Born outcome map. some i on cell i, none off the union of cells. Total off an FS-null set (bornOutcome_ae_isSome), deterministic (the cell is unique, bornRegion_pairwiseDisjoint). The genuine realisation of the contextual outcome-map slot: the microstate fixes the outcome.

Equations

• CSD.LF4.bornOutcome ψ hψ0 p = if h : ∃ (i : Fin (M + 1)), p ∈ CSD.LF4.bornRegion ψ hψ0 i then some h.choose else none

theorem CSD.LF4.bornOutcome_eq_some_iff {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (p : CPN (M + 1)) (i : Fin (M + 1)) : bornOutcome ψ hψ0 p = some i ↔ p ∈ bornRegion ψ hψ0 i

The outcome map is some i iff the microstate is in cell i. The ← direction uses uniqueness (bornRegion_pairwiseDisjoint); the → direction uses h.choose_spec plus uniqueness to pin the chosen index.

theorem CSD.LF4.bornOutcome_preimage_some {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (i : Fin (M + 1)) : bornOutcome ψ hψ0 ⁻¹' {some i} = bornRegion ψ hψ0 i

Set-level form: the some i fibre of the outcome map is exactly cell i.

theorem CSD.LF4.bornOutcome_measurableSet_some {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (i : Fin (M + 1)) : MeasurableSet (bornOutcome ψ hψ0 ⁻¹' {some i})

The some i fibres of the outcome map are measurable (immediate from bornOutcome_preimage_some + bornRegion_measurable_uncond).

theorem CSD.LF4.bornOutcome_measurable {M : ℕ} (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) : Measurable (bornOutcome ψ hψ0)

The outcome map is measurable. The codomain Option (Fin (M+1)) is a countable measurable space (⊤ σ-algebra), so measurability reduces to measurability of every singleton preimage (measurable_to_countable'): the some i fibres are cells (measurable); the none fibre is the complement of the union of cells (measurable).

theorem CSD.LF4.bornOutcome_ae_isSome {M : ℕ} (p₀ : CPN (M + 1)) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) : ∀ᵐ (p : CPN (M + 1)) ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀, (bornOutcome ψ hψ0 p).isSome = true

a.e. totality: the outcome map is defined (isSome) off an FS-null set (unit ψ). The microstate determines an outcome almost surely.

Indicator-of-disjoint-union bridge

theorem CSD.LF4.indicator_iUnion_disjoint {α : Type u_1} {ι : Type u_2} (s : Finset ι) (t : ι → Set α) (hdisj : (↑s).PairwiseDisjoint t) (f : α → ℝ) (x : α) : (⋃ i ∈ s, t i).indicator f x = ∑ i ∈ s, (t i).indicator f x

Indicator of a disjoint finite union = sum of indicators. Thin wrapper of Finset.indicator_biUnion_apply for a pairwise-disjoint family indexed by a finset. Feeds the union-event outcome-frequency restatements.