The sector measure is forced, not chosen

Category: 3-CSD. The (b) half of the A1 ontic-sector row in specs/BACKLOG.md — "exhibit the fibre measure as Liouville rather than merely Haar".

Glossary: https://glossary.constraintsurfacedynamics.com/fibre/ The published entry records this result in plain language, with this module as one of its Lean anchors. Kept symmetric by scripts/check-glossary.sh.

The gap this closes

LF4.KahlerOnticSetup carries a field liouvilleMeasure : Measure Sigma together with liouville_isProbability. The name says Liouville; the type says only probability measure. Nothing in the structure forced the sector's measure to be the canonical one, so kMuL = μ_FS ⊗ Haar read as a choice, and a reviewer was entitled to ask why that measure rather than another.

★★ kMuL_unique answers it: kMuL p₀ is the only probability measure on Σ = ℂℙ^{N-1} × T² invariant under the sector's own symmetry — unitaries on the base, translations on the fibre. The measure is forced by the symmetry, not selected.

⚠️ Why this is the right reading of "Liouville"

The textbook definition is the top exterior power of the Kähler form, and it is not available and will not be: specs/connectivity-manifest.md L1 records that manifold residual (dω = 0, the top-power volume identity) as blocked on Mathlib, with Q8 rating the fix XL.

Symmetry-uniqueness is the formalisable content of the same fact — on a homogeneous space the Liouville measure is the invariant one — and it is the reading the corpus already uses for the base (invariant_measure_uniqueness_cpn). This extends that reading to the whole fibred sector.

The proof, in two independent halves

• The fibre (fst_prod_volume_of_fibreShift_invariant). For each measurable base set A, push μ restricted to A ×ˢ univ forward to the fibre: a finite translation-invariant measure on T². ★ Because T² is compact, isAddInvariant_eq_smul_of_compactSpace pins it to a multiple of Haar with no regularity side conditions. Compactness of the fibre is load-bearing here, not decoration — and it is exactly what TorusFibre/GlobalRecordClosure bought in July, when the record layer moved off the non-compact ℝ fibre.
• The base. The marginal is U(N)-invariant, so invariant_measure_uniqueness_cpn pins it to a multiple of μ_FS; total mass one fixes the multiplier.

Measure.prod_eq joins them: agreement on rectangles suffices.

⚠️ Scope

The measure is forced given the symmetry group. This does not derive the group, and Σ remains the floor — deriving Σ is a non-question (specs/CSD-CHARTER.md). Nor does it touch the record layer's other open item: no H_int(M) produces the basins.

Reference: specs/BACKLOG.md (the A1 ontic-sector row, item (b)); specs/connectivity-manifest.md L1; specs/CSD-CHARTER.md; specs/future-work.md.

instance CSD.LF4.instIsAddHaarMeasureKTorusVolume : MeasureTheory.volume.IsAddHaarMeasure

Haar measure on the fibre torus, reached through the product form.

noncomputable def CSD.LF4.fibreShift {N : ℕ} (v : KTorus) (p : KSigma N) : KSigma N

The fibre shift: translate the torus coordinate, fix the base ray.

Equations

• CSD.LF4.fibreShift v p = (p.1, v + p.2)

noncomputable def CSD.LF4.baseRotate {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : KSigma N) : KSigma N

The base rotation: move the ray, fix the fibre.

Equations

• CSD.LF4.baseRotate U p = (U • p.1, p.2)

@[simp]

theorem CSD.LF4.fibreShift_apply {N : ℕ} (v : KTorus) (p : KSigma N) : fibreShift v p = (p.1, v + p.2)

@[simp]

theorem CSD.LF4.baseRotate_apply {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p : KSigma N) : baseRotate U p = (U • p.1, p.2)

theorem CSD.LF4.measurable_fibreShift {N : ℕ} (v : KTorus) : Measurable (fibreShift v)

theorem CSD.LF4.measurable_baseRotate {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : Measurable (baseRotate U)

theorem CSD.LF4.fibreShift_preimage_prod_univ {N : ℕ} (v : KTorus) (A : Set (CPN N)) : fibreShift v ⁻¹' A ×ˢ Set.univ = A ×ˢ Set.univ

The fibre shift leaves every base cylinder set where it is.

The fibre half

noncomputable def CSD.LF4.fibreSlice {N : ℕ} (μ : MeasureTheory.Measure (KSigma N)) (A : Set (CPN N)) : MeasureTheory.Measure KTorus

The fibre marginal of μ above a base set A.

Equations

• CSD.LF4.fibreSlice μ A = MeasureTheory.Measure.map Prod.snd (μ.restrict (A ×ˢ Set.univ))

theorem CSD.LF4.fibreSlice_apply {N : ℕ} (μ : MeasureTheory.Measure (KSigma N)) {A : Set (CPN N)} {B : Set KTorus} (_hA : MeasurableSet A) (hB : MeasurableSet B) : (fibreSlice μ A) B = μ (A ×ˢ B)

instance CSD.LF4.instIsFiniteMeasureFibreSlice {N : ℕ} (μ : MeasureTheory.Measure (KSigma N)) [MeasureTheory.IsFiniteMeasure μ] (A : Set (CPN N)) : MeasureTheory.IsFiniteMeasure (fibreSlice μ A)

theorem CSD.LF4.isAddLeftInvariant_fibreSlice {N : ℕ} (μ : MeasureTheory.Measure (KSigma N)) (hT : ∀ (v : KTorus), MeasureTheory.MeasurePreserving (fibreShift v) μ μ) (A : Set (CPN N)) (hA : MeasurableSet A) : (fibreSlice μ A).IsAddLeftInvariant

★ The fibre slice is translation-invariant. The shift moves only the torus coordinate, so it preserves every base cylinder, and measure preservation on Σ descends to the slice.

theorem CSD.LF4.fst_prod_volume_of_fibreShift_invariant {N : ℕ} (μ : MeasureTheory.Measure (KSigma N)) [MeasureTheory.IsFiniteMeasure μ] (hT : ∀ (v : KTorus), MeasureTheory.MeasurePreserving (fibreShift v) μ μ) : μ.fst.prod MeasureTheory.volume = μ

★★ Invariance under the fibre shift forces a product with Haar.

T² is compact, so isAddInvariant_eq_smul_of_compactSpace applies with no regularity side conditions, and the scalar is read off at univ.

The base half, and the uniqueness statement

theorem CSD.LF4.measurePreserving_fst_of_baseRotate {N : ℕ} (μ : MeasureTheory.Measure (KSigma N)) (hU : ∀ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), MeasureTheory.MeasurePreserving (baseRotate U) μ μ) (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : MeasureTheory.MeasurePreserving (fun (p : CPN N) => U • p) μ.fst μ.fst

The base marginal inherits unitary invariance.

theorem CSD.LF4.kMuL_unique {N : ℕ} [NeZero N] (p₀ : CPN N) (μ : MeasureTheory.Measure (KSigma N)) [MeasureTheory.IsProbabilityMeasure μ] (hU : ∀ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), MeasureTheory.MeasurePreserving (baseRotate U) μ μ) (hT : ∀ (v : KTorus), MeasureTheory.MeasurePreserving (fibreShift v) μ μ) : μ = kMuL p₀

★★★ The sector measure is forced by its symmetry.

kMuL p₀ is the unique probability measure on Σ = ℂℙ^{N-1} × T² invariant under U(N) acting on the base and T² acting on the fibre. So the record layer's Liouville measure is not a modelling choice — it is the only measure compatible with the sector's own symmetry.

⚠️ Forced given the group. This does not derive the symmetry, and Σ stays the floor.