Spatial trace function σ

The spatial trace σ maps events to the paths they traverse ([Zwa05], [Gaw09]): the spatial member of [Kri98]'s family of trace dimensions, alongside the temporal trace τ (Event.runtime) and the thematic dimension θ. Following the mixin convention of Semantics/Events/CEM.lean, Trace carries only the function σ; its structural assumptions — sum homomorphism (Mereology.IsSumHom) and injectivity — are stated at use sites.

Main declarations

• Trace: the spatial trace σ of an event theory.
• Trace.bounded_path_telic: QUA path predicates pull back through an injective sum-homomorphic σ — walk to the store is telic because to the store denotes a QUA set of paths ([Zwa05]).
• Trace.unbounded_path_atelic: CUM path predicates pull back through a sum-homomorphic σ — walk towards the store is atelic.

class Spatial.Trace (Loc : Type u_1) (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

The spatial trace σ assigns each event the path it traverses ([Zwa05], [Gaw09]), parallel to the temporal trace τ (Event.runtime). Structural assumptions on σ are stated as mixins at use sites, per Semantics/Events/CEM.lean: [Mereology.IsSumHom st.σ] for sum preservation, Function.Injective st.σ where QUA pullback needs it.

• σ : Event Time → Path Loc

  The path traversed in an event.

Telicity transfer through σ

theorem Spatial.Trace.bounded_path_telic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Path Loc)] [st : Trace Loc Time] {P : Path Loc → Prop} [hσ : Mereology.IsSumHom σ] (hinj : Function.Injective σ) (hP : Mereology.QUA P) : Mereology.QUA (P ∘ σ)

QUA path predicates pull back through an injective sum-homomorphic σ to QUA (telic) VP predicates — [Kri98]'s quantization route to telicity, stated for paths. [Zwa05] argues bounded PPs are not in fact quantized (bounded = non-cumulative instead; see Studies/Zwarts2005.lean), so this records the Krifka-style analysis, applicable when a path predicate is QUA.

theorem Spatial.Trace.unbounded_path_atelic {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Path Loc)] [st : Trace Loc Time] {P : Path Loc → Prop} [hσ : Mereology.IsSumHom σ] (hP : Mereology.CUM P) : Mereology.CUM (P ∘ σ)

CUM path predicates pull back through a sum-homomorphic σ to CUM (atelic) VP predicates: walk towards the store is atelic because towards the store denotes a cumulative set of paths ([Zwa05]).