LF2 Setup: Sector data

Category: 3-Local (LF2 SectorData: LF1 OnticSetup plus projective target, projection, and group action).

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

Extends the LF1 OnticSetup with:

• a measurable projection π : Σ → P onto an abstract epistemic measurable space (standing in for CP^{N-1});
• a group G acting measurably on both Σ and P;
• the compatibility hypotheses (μL-invariance of the ontic action and G-equivariance of π) that drive the LF2 measure bridge.

The projective space is left abstract — no Projectivization, no Fubini–Study measure construction. Concrete instantiation is LF4+'s job. The reference measure μFS is not a field of SectorData; it enters downstream theorems as an explicit argument, keeping SectorData μFS-agnostic.

structure CSD.LF2.SectorData (SigmaSpace : Type u_1) (P : Type u_2) (G : Type u_3) [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] : Type (max u_1 u_2)

LF2 sector data. Groups the LF1 ontic setup together with the epistemic projection π and a G-action satisfying μL-invariance and π-equivariance.

sector-posit (SO-1) structural data, not a derivation. Both π : SigmaSpace → P and the group G are taken as structural inputs. Nothing in SectorData constrains π to project onto the quantum-effective sector specifically: any measurable map with the two coherence conditions (μL-invariance of the ontic action, π-equivariance) qualifies. Similarly, G is any group acting measurably on both spaces with the two coherence conditions. The natural reading is G = U(N) acting on Σ via the lift of its action on CP^{N-1} — the group the corpus's witness (LF4/Instance.lean) instantiates; on CP^{N-1} the central phase acts trivially, so the literature's SU(N) reading is the same action — with π the standard projection, but no field forces this.

This labelling carries the sector posit (SO-1) in Paper B's framing: the physical motivation for the quantum-effective sector assumption is a load-bearing external input to the corpus, not derived in v1.00. Concrete instantiation (P := Projectivization ℂ (EuclideanSpace ℂ (Fin N)), G := Matrix.specialUnitaryGroup (Fin N) ℂ, plus the explicit π) is deferred to LF4-todo §8.

MulAction-based encoding. The G-action is encoded via Mathlib's MulAction G _ typeclasses on both SigmaSpace and P, with transitivity encoded by MulAction.IsPretransitive G P (the Mathlib-idiomatic spelling of "any two points in P are related by some group element"). This replaces the earlier onticAction : G → _ ≃ᵐ _ field encoding plus the four _one / _mul coherence fields and the epAction_transitive field: the group-action laws follow from the MulAction typeclass, and transitivity from IsPretransitive. Measurability of each action is supplied as structure fields (measurable_smul_σ, measurable_smul_P).

• toOntic : LF1.OnticSetup SigmaSpace

  Underlying LF1 ontic data (Σ, μL, Φ, Ω0, plus their measurability / nonzero-volume / measure-preservation hypotheses).

• π : SigmaSpace → P

  The epistemic projection from ontic state space to the abstract projective target.

• measurable_π : Measurable self.π

  Measurability of the projection.

• measurable_smul_σ (g : G) : Measurable fun (x : SigmaSpace) => g • x

  Measurability of each ontic action map g • · : SigmaSpace → SigmaSpace.

• measurable_smul_P (g : G) : Measurable fun (x : P) => g • x

  Measurability of each epistemic action map g • · : P → P.

• hμL_inv (g : G) : MeasureTheory.MeasurePreserving (fun (x : SigmaSpace) => g • x) ↑self.toOntic.μL ↑self.toOntic.μL

  Liouville invariance: each ontic action g • · preserves μL.

• hπ_equiv (g : G) (x : SigmaSpace) : self.π (g • x) = g • self.π x

  Equivariance: π intertwines the ontic and epistemic actions.

@[reducible, inline]

abbrev CSD.LF2.SectorData.μL {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) : MeasureTheory.Measure SigmaSpace

Convenience re-export of the ontic Liouville measure as a Measure.

Equations

• D.μL = ↑D.toOntic.μL