SigmaLayer/LocalisedTypicality: the sector posit in the right appropriate places

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

The deep open link SO-1 (the sector-origin problem, connectivity-manifest L7) asks to DERIVE the sector's typicality measure — and hence the Born weights — from a primitive ontology / the deterministic flow. The sector posit does NOT need to hold universally, for every possible measure or state; it only needs to hold where it matters: the measure only needs to be pinned where the dynamical symmetry acts. This module makes that precise. (SO-1 is the sector-origin question, distinct from Paper C Axiom A5 — the projectability / quantum-effective condition that selects the sector, not its origin.)

LF4/KahlerVolumeForced.lean already proves the Fubini–Study volume is IsForcedKahlerVolume: the UNIQUE U(N)-invariant probability measure on ℂℙ^{N-1}. So:

• forcedVolume_unique / region_measure_symmetry_forced — any two measures carrying the sector's U(N) symmetry coincide on EVERY region. The Born weights depend only on the SYMMETRY, not on which invariant measure: one does not need to derive THE measure from the dynamics, only to know the sector carries the U(N) symmetry.
• localised_sectorPostulate_capstone — for the concrete unitary-flow sector: (i) its ray-space typicality measure is FORCED (the unique U(N)-invariant probability measure), (ii) the deterministic projected flow U t • · — a one-parameter subgroup of that symmetry — PRESERVES it, and (iii) every measure sharing the symmetry gives the same Born weights. So the sector posit is discharged AT the sectors carrying the full U(N) symmetry — the right appropriate places — WITHOUT a universal derivation.

Honest scope

This is NOT the universal sector origin. The residual (SO-1) is that the FLOW alone is a single one-parameter subgroup, which does not by itself GENERATE the full U(N) — so "invariant under the flow" is weaker than "invariant under U(N)", and forcing needs the ambient symmetry the sector CONSTRUCTION carries, not the bare flow. What is shown here: given that symmetry (which the concrete sectors have), the typicality measure and the Born weights are forced, not independently posited. The sector itself is still posited (SO-1); this localises where the forcing bites.

References: specs/connectivity-manifest.md (L7 / SO-1), specs/future-work.md (SO-1); LF4/KahlerVolumeForced.lean (IsForcedKahlerVolume, fubiniStudyMeasure_unique), LF4/ManyToOnePillars.lean (manyToOneSetup).

theorem CSD.SigmaLayer.forcedVolume_unique {N : ℕ} [NeZero N] {μ ν : MeasureTheory.Measure (LF4.CPN N)} (hμ : LF4.IsForcedKahlerVolume μ) (hν : LF4.IsForcedKahlerVolume ν) : μ = ν

Any two forced Kähler volumes coincide. A measure carrying the sector's U(N) symmetry (a IsForcedKahlerVolume) is unique — so the typicality measure is determined by Σ = ℂℙ^{N-1} + its symmetry, not chosen.

theorem CSD.SigmaLayer.region_measure_symmetry_forced {N : ℕ} [NeZero N] {μ ν : MeasureTheory.Measure (LF4.CPN N)} (hμ : LF4.IsForcedKahlerVolume μ) (hν : LF4.IsForcedKahlerVolume ν) (A : Set (LF4.CPN N)) : μ A = ν A

The Born weights are symmetry-forced (localized sector posit). Any two U(N)-invariant probability measures assign the SAME measure to every region. The Born weights (region volumes) depend only on the sector's U(N) symmetry, not on which invariant measure — so deriving THE measure from the dynamics is not needed; carrying the symmetry suffices.

theorem CSD.SigmaLayer.localised_sectorPostulate_capstone {N : ℕ} [NeZero N] (U : ℝ → ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p₀ : LF4.CPN N) : LF4.IsForcedKahlerVolume (MeasureTheory.Measure.map (LF4.manyToOneSetup U p₀).pi (LF4.manyToOneSetup U p₀).liouvilleMeasure) ∧ (∀ (t : ℝ), MeasureTheory.MeasurePreserving (fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => U t • p) (MeasureTheory.Measure.map (LF4.manyToOneSetup U p₀).pi (LF4.manyToOneSetup U p₀).liouvilleMeasure) (MeasureTheory.Measure.map (LF4.manyToOneSetup U p₀).pi (LF4.manyToOneSetup U p₀).liouvilleMeasure)) ∧ ∀ (ν : MeasureTheory.Measure (LF4.CPN N)), LF4.IsForcedKahlerVolume ν → ∀ (A : Set (Projectivization ℂ (EuclideanSpace ℂ (Fin N)))), (MeasureTheory.Measure.map (LF4.manyToOneSetup U p₀).pi (LF4.manyToOneSetup U p₀).liouvilleMeasure) A = ν A

Localized sector posit: the typicality measure is forced by the symmetry the dynamics carries. For the unitary-flow sector on Σ = ℂℙ^{N-1} × T², the ray-space typicality measure π_*(μL):

1. IS the unique U(N)-invariant probability measure — forced by Σ + its symmetry, not an independent posit;
2. is PRESERVED by the deterministic projected flow U t • · (a one-parameter subgroup of that symmetry);
3. gives the SAME measure to every region as any other measure carrying the symmetry.

So the sector posit holds AT the sectors carrying the full U(N) symmetry — the right appropriate places — without a universal derivation of the sector from the bare flow (that residual is SO-1).