SigmaLayer/ConstraintSurface: ontic time and the concrete constrained state space

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

This module fixes the ontic time parameter and offers an optional concrete representation of a constrained ontic state space. The generic foundations stay polymorphic over an abstract Sigma; the ConstraintSurface construction here is for concrete models only. We do not claim that every abstract Sigma has been derived from explicit constraints.

See SigmaLayer/Adapters.lean for the postulate ledger (P1 to P9, B1 to B7, T1 to T15) governing the whole SigmaLayer layer, and SigmaLayer/ConstraintDynamics.lean for the deterministic dynamics.

@[reducible, inline]

abbrev CSD.SigmaLayer.OnticTime : Type

Ontic time is a real parameter (the flow parameter of the deterministic ontic dynamics).

Equations

• CSD.SigmaLayer.OnticTime = ℝ

@[reducible, inline]

abbrev CSD.SigmaLayer.Constraint (Raw : Type u) : Type u

A constraint on a raw configuration type is a predicate selecting admissible configurations.

Equations

• CSD.SigmaLayer.Constraint Raw = (Raw → Prop)

def CSD.SigmaLayer.ConstraintSurface (Raw : Type u) (constraints : Set (Constraint Raw)) : Type u

The constrained ontic state space (concrete models only). The subtype of raw configurations satisfying every constraint in the given family. This is the explicit representation of postulate P1 "there exists a measurable ontic constraint surface" for concrete models; the generic theory keeps Sigma abstract.

Equations

• CSD.SigmaLayer.ConstraintSurface Raw constraints = { x : Raw // ∀ C ∈ constraints, C x }