SigmaLayer/ProjectiveSector: the projective sector and its projective law

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

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

Postulates P7, P8, P9: for each finite dimension N the operational pure-state target is CP^{N-1} (ProjectiveState N), and there is a measurable projection pi : Sigma -> CP^{N-1} which need NOT be injective (many-to-one is intended). The projective probability law is the pushforward of an ontic measure under pi.

Anti-circularity

ProjectiveSector carries NO Born equality, NO Fubini-Study equality, NO unitarity. It is the projection pi and its measurability only. The Born rule, the Fubini-Study bridge and unitary projected dynamics are theorem targets or named bridge assumptions elsewhere, never fields here.

Adapters into the existing setups

kahlerConstraintDynamics and kahlerProjectiveSector recover the SigmaLayer structures from LF4.KahlerOnticSetup. The ConstraintDynamics adapter is PARTIAL: KahlerOnticSetup does not carry the one-parameter-group laws (flow_zero, flow_add), so they are taken as explicit inputs. Since the 2026-08-06 F-04 tightening, KahlerOnticSetup's Kähler-geometry fields are concrete (kahler_pointwise, liouville_isProbability — the latter an instance, so finiteness of liouvilleMeasure is automatic; see LF4/KahlerOnticSetup.lean). The projection adapter is total: pi is dynamics independent.

@[reducible, inline]

abbrev CSD.SigmaLayer.ProjectiveState (N : ℕ) : Type

The projective sector projective pure-state target (postulate P7): CP^{N-1}. Definitionally the LF4 CPN N = ℙ ℂ (EuclideanSpace ℂ (Fin N)); named here for the SigmaLayer layer.

Equations

• CSD.SigmaLayer.ProjectiveState N = Projectivization ℂ (EuclideanSpace ℂ (Fin N))

structure CSD.SigmaLayer.ProjectiveSector (N : ℕ) {Sigma : Type u} [MeasurableSpace Sigma] (_D : ConstraintDynamics Sigma) : Type u

The projective sector (postulates P8, P9). A measurable projection from the ontic state space to the projective pure-state target. It need not be injective; a many-to-one pi is intended and supported. No Born rule is placed here.

• pi : Sigma → ProjectiveState N

  P8: the measurable projection onto the projective sector.

• measurable_pi : Measurable self.pi

  The projection is measurable.

noncomputable def CSD.SigmaLayer.ProjectiveSector.projectiveLaw {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (mu : MeasureTheory.Measure Sigma) : MeasureTheory.Measure (ProjectiveState N)

The projective law of an ontic measure. The pushforward pi_* mu on the projective sector. Not identified with the Fubini-Study measure without a separate bridge (SigmaLayer/MeasureBridge.lean).

Equations

• Q.projectiveLaw mu = MeasureTheory.Measure.map Q.pi mu

theorem CSD.SigmaLayer.ProjectiveSector.projectiveLaw_apply {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (mu : MeasureTheory.Measure Sigma) {B : Set (ProjectiveState N)} (hB : MeasurableSet B) : (Q.projectiveLaw mu) B = mu (Q.pi ⁻¹' B)

The projective law evaluated on a measurable set is the ontic measure of its preimage.

noncomputable def CSD.SigmaLayer.ProjectiveSector.projectivePreparationLaw {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} [Nonempty Sigma] (Q : ProjectiveSector N D) (P : Preparation D) : MeasureTheory.Measure (ProjectiveState N)

The projective preparation law. The pushforward under pi of the normalised conditional ontic preparation measure (Preparation.conditionalMeasure).

Equations

• Q.projectivePreparationLaw P = Q.projectiveLaw ↑P.conditionalMeasure

Adapters from the existing LF4.KahlerOnticSetup

def CSD.SigmaLayer.kahlerConstraintDynamics {N : ℕ} (K : LF4.KahlerOnticSetup N) [hfin : MeasureTheory.IsFiniteMeasure K.liouvilleMeasure] (hzero : ∀ (x : K.Sigma), K.flow 0 x = x) (hadd : ∀ (s t : ℝ) (x : K.Sigma), K.flow (s + t) x = K.flow s (K.flow t x)) : ConstraintDynamics K.Sigma

Partial adapter KahlerOnticSetup -> ConstraintDynamics. Recovers the SigmaLayer canonical core from a Kähler setup, given the one-parameter-group laws (hzero, hadd) that KahlerOnticSetup does not carry and IsFiniteMeasure on its liouvilleMeasure. Measurability of the flow is derived from flow_preserves_volume; measure preservation is inherited directly.

Equations

• CSD.SigmaLayer.kahlerConstraintDynamics K hzero hadd = { muL := ⟨K.liouvilleMeasure, hfin⟩, flow := K.flow, measurable_flow := ⋯, flow_zero := hzero, flow_add := hadd, flow_preserves := ⋯ }

def CSD.SigmaLayer.kahlerProjectiveSector {N : ℕ} (K : LF4.KahlerOnticSetup N) {D : ConstraintDynamics K.Sigma} : ProjectiveSector N D

Total adapter KahlerOnticSetup -> ProjectiveSector. Recovers the projection for any ConstraintDynamics on the same Sigma (the projection pi is independent of the dynamics).

Equations

• CSD.SigmaLayer.kahlerProjectiveSector K = { pi := K.pi, measurable_pi := ⋯ }