SigmaLayer/ConstraintDynamics: deterministic, measure-preserving ontic dynamics

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

ConstraintDynamics Sigma is the canonical SigmaLayer core (postulates P2, P3, P4): a finite Liouville reference measure muL on the ontic state space, together with a deterministic real-parameter flow that forms a one-parameter group and preserves muL. This is the group-law refinement of the existing LF1.OnticSetup (single map, no group law) and LF4.KahlerOnticSetup (time flow, no group law); the adapters into those live in SigmaLayer/IsolationPreparation.lean and SigmaLayer/ProjectiveSector.lean.

Anti-circularity

ConstraintDynamics carries NO Born weight, NO frequency claim, NO Fubini-Study equality, NO unitary projected dynamics, NO Schrödinger equation. It is deterministic dynamics and a reference measure only. The projective sector pi is a separate structure (ProjectiveSector); all quantum content is a theorem target or a named bridge assumption, never a field here.

structure CSD.SigmaLayer.ConstraintDynamics (Sigma : Type u) [MeasurableSpace Sigma] : Type u

Deterministic, measure-preserving ontic dynamics (postulates P2, P3, P4). A finite Liouville reference measure muL, a deterministic flow forming a one-parameter group (flow_zero, flow_add), each time-t map measurable and preserving muL. No quantum content.

• muL : MeasureTheory.FiniteMeasure Sigma

  P2: the finite Liouville reference measure.

• flow : OnticTime → Sigma → Sigma

  P3: the deterministic ontic flow.

• measurable_flow (t : OnticTime) : Measurable (self.flow t)

  Each time-t map is measurable.

• flow_zero (x : Sigma) : self.flow 0 x = x

  The flow at time 0 is the identity (one-parameter group identity).

• flow_add (s t : OnticTime) (x : Sigma) : self.flow (s + t) x = self.flow s (self.flow t x)

  The flow composes additively in time (one-parameter group law).

• flow_preserves (t : OnticTime) : MeasureTheory.MeasurePreserving (self.flow t) ↑self.muL ↑self.muL

  P4: each time-t map preserves the Liouville measure (Liouville's theorem).

def CSD.SigmaLayer.trivialDynamics {Sigma : Type u} [MeasurableSpace Sigma] (μ : MeasureTheory.FiniteMeasure Sigma) : ConstraintDynamics Sigma

The trivial (identity-flow) dynamics with a given finite reference measure. The isolated evolution is the identity; useful when the physical content of a model is a de-isolation interaction (DeisolationModel) rather than a nontrivial isolated flow.

Equations

• CSD.SigmaLayer.trivialDynamics μ = { muL := μ, flow := fun (x : CSD.SigmaLayer.OnticTime) => id, measurable_flow := ⋯, flow_zero := ⋯, flow_add := ⋯, flow_preserves := ⋯ }

theorem CSD.SigmaLayer.ConstraintDynamics.flow_neg_left {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (t : OnticTime) (x : Sigma) : D.flow (-t) (D.flow t x) = x

Reversing the flow undoes it on the left: flow (-t) (flow t x) = x. Derived from the group law, so reversibility is not a separate postulate.

theorem CSD.SigmaLayer.ConstraintDynamics.flow_neg_right {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (t : OnticTime) (x : Sigma) : D.flow t (D.flow (-t) x) = x

Reversing the flow undoes it on the right: flow t (flow (-t) x) = x.

theorem CSD.SigmaLayer.ConstraintDynamics.flow_bijective {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (t : OnticTime) : Function.Bijective (D.flow t)

Each time-t flow map is a bijection, with inverse flow (-t) (derived from the real-flow group laws, not postulated separately).

theorem CSD.SigmaLayer.ConstraintDynamics.flow_neg_leftInverse {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (t : OnticTime) : Function.LeftInverse (D.flow (-t)) (D.flow t)

flow (-t) is the two-sided inverse of flow t.

theorem CSD.SigmaLayer.ConstraintDynamics.flow_neg_rightInverse {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (t : OnticTime) : Function.RightInverse (D.flow (-t)) (D.flow t)

flow (-t) is a right inverse of flow t.