refactor(Semantics/Events): merge Defs.lean into Basic.lean

Linglib.lean

@@ -2398,7 +2398,6 @@ import Linglib.Semantics.Aspect.ChangeOfState
 -- Theories: Semantics.Iconic (Iconological Semantics for sign language)
 import Linglib.Semantics.Iconic.Basic
 -- Theories: Semantics.Events (neo-Davidsonian)
-import Linglib.Semantics.Events.Defs
 import Linglib.Semantics.Events.Basic
 import Linglib.Semantics.ArgumentStructure.Defs
 import Linglib.Semantics.Events.CEM

Linglib/Semantics/ArgumentStructure/Defs.lean

@@ -1,4 +1,4 @@
-import Linglib.Semantics.Events.Defs
+import Linglib.Semantics.Events.Basic
 import Linglib.Core.Word
 import Linglib.Semantics.ArgumentStructure.Linking
 

Linglib/Semantics/Events/Basic.lean

@@ -1,51 +1,95 @@
-import Linglib.Semantics.Events.Defs
+import Mathlib.Order.Basic
+import Linglib.Core.Time.Interval.Basic
+import Linglib.Tactics.OntSort
 import Linglib.Features.Aktionsart
 
 /-!
-# Neo-Davidsonian Event Semantics — basic API
+# Neo-Davidsonian Event Semantics
 
-API on top of `Events/Defs.lean`'s foundational types: sort predicates over
-the `Features.Dynamicity` event sort, and concrete examples on `ℤ`-time.
-
-Files that only need to *talk about* events should import `Defs.lean`
-directly.
+Foundational types and basic API for neo-Davidsonian event semantics
+(@cite{davidson-1967}, @cite{parsons-1990}). Verbs denote predicates of
+events; thematic roles are independent two-place predicates
+(`Semantics.ArgumentStructure.ThematicRel`).
 
 ## Main definitions
 
+* `Event` — the unified event type: a runtime interval + `Features.Dynamicity` sort
+* `Event.τ` — temporal trace function
 * `Event.isAction` / `Event.isState` — decidable `Prop` sort predicates
   (the `dynamic` / `stative` poles of `Features.Dynamicity`)
+* `Event.isPunctual` / `Event.isDurative` — decidable `Prop` duration predicates
+* `Event.existsClosure` — Davidsonian existential closure
+* `Event.Mereology` — part-of typeclass with τ-monotonicity + sort-preservation
+* `Event.preorder` — Preorder instance derived from `Event.Mereology`
+* `Event.Manner` — manner ontology (@cite{liefke-2024} §4.3)
 * `exampleRun` / `exampleKnow` — concrete `Event ℤ` instances
+
+## Naming note
+
+`Event` is the unified type for linguistic events. The Bach 1981/1986
+distinction between "eventuality" (genus, sortless) and "event" (narrow
+sense, non-state) has largely collapsed in current practice —
+@cite{champollion-2017} and @cite{zhao-2025} both use "event"
+generically with sort/aktionsart as an inherent attribute. Tense-aspect
+code that doesn't care about sort simply doesn't reference `.sort`;
+sortless construction sites default to `.dynamic`.
+
+## References
+
+* @cite{davidson-1967}, @cite{parsons-1990} (neo-Davidsonian foundations)
+* @cite{bach-1986} (action/state ontology)
+* @cite{krifka-1989} (interval-valued runtimes)
+* @cite{champollion-2017}, @cite{zhao-2025} (event-as-generic)
+* @cite{liefke-2024} §4.3 (manner ontology)
 -/
 
 open Core.Time
 open Features
 
+/-- An event: a temporal individual with ontological sort. -/
+@[ont_sort] structure Event (Time : Type*) [LinearOrder Time] where
+  /-- The temporal extent of this event -/
+  runtime : Interval Time
+  /-- Ontological sort (aktionsart): `dynamic` or `stative` (@cite{bach-1986}).
+      This is the `Features.Dynamicity` feature — the action/state distinction
+      at the event-token level. -/
+  sort : Features.Dynamicity
+
+namespace Event
+
+variable {Time : Type*} [LinearOrder Time]
+
+/-! ### Temporal trace -/
+
+/-- Temporal trace function τ(e) = the runtime interval of event e. -/
+@[simp]
+def τ (e : Event Time) : Interval Time :=
+  e.runtime
+
 /-! ### Sort predicates -/
 
 /-- Is this event an action (dynamic event)? -/
-def Event.isAction {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop :=
+def isAction (e : Event Time) : Prop :=
   e.sort = .dynamic
 
 /-- Is this event a state (stative event)? -/
-def Event.isState {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop :=
+def isState (e : Event Time) : Prop :=
   e.sort = .stative
 
-instance {Time : Type*} [LinearOrder Time] :
-    DecidablePred (Event.isAction (Time := Time)) :=
+instance : DecidablePred (isAction (Time := Time)) :=
   fun e => decEq e.sort .dynamic
 
-instance {Time : Type*} [LinearOrder Time] :
-    DecidablePred (Event.isState (Time := Time)) :=
+instance : DecidablePred (isState (Time := Time)) :=
   fun e => decEq e.sort .stative
 
 /-- `isAction` and `isState` are complementary. -/
-theorem isAction_iff_not_isState {Time : Type*} [LinearOrder Time] (e : Event Time) :
+theorem isAction_iff_not_isState (e : Event Time) :
     e.isAction ↔ ¬ e.isState := by
   simp only [Event.isAction, Event.isState]
   cases e.sort <;> decide
 
 /-- `isState` and `isAction` are complementary. -/
-theorem isState_iff_not_isAction {Time : Type*} [LinearOrder Time] (e : Event Time) :
+theorem isState_iff_not_isAction (e : Event Time) :
     e.isState ↔ ¬ e.isAction := by
   simp only [Event.isAction, Event.isState]
   cases e.sort <;> decide
@@ -55,25 +99,77 @@ theorem isState_iff_not_isAction {Time : Type*} [LinearOrder Time] (e : Event Ti
 /-- Is this event punctual (instantaneous)? Its runtime is a single point.
     The temporal-extent counterpart of the dynamicity sort; derived from the
     runtime via `Interval.IsPoint`. -/
-def Event.isPunctual {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop :=
+def isPunctual (e : Event Time) : Prop :=
   e.τ.IsPoint
 
 /-- Is this event durative (temporally extended)? -/
-def Event.isDurative {Time : Type*} [LinearOrder Time] (e : Event Time) : Prop :=
+def isDurative (e : Event Time) : Prop :=
   ¬ e.isPunctual
 
-instance {Time : Type*} [LinearOrder Time] :
-    DecidablePred (Event.isPunctual (Time := Time)) :=
+instance : DecidablePred (isPunctual (Time := Time)) :=
   fun e => by unfold Event.isPunctual Interval.IsPoint; infer_instance
 
-instance {Time : Type*} [LinearOrder Time] :
-    DecidablePred (Event.isDurative (Time := Time)) :=
+instance : DecidablePred (isDurative (Time := Time)) :=
   fun e => by unfold Event.isDurative; infer_instance
 
 /-- `isDurative` and `isPunctual` are complementary. -/
-theorem isDurative_iff_not_isPunctual {Time : Type*} [LinearOrder Time] (e : Event Time) :
+theorem isDurative_iff_not_isPunctual (e : Event Time) :
     e.isDurative ↔ ¬ e.isPunctual := Iff.rfl
 
+/-! ### Existential closure -/
+
+/-- Existential closure: ∃e. P(e). The fundamental step from event
+    semantics to truth conditions. -/
+def existsClosure (P : Event Time → Prop) : Prop :=
+  ∃ e : Event Time, P e
+
+/-! ### Mereology -/
+
+/-- Axioms for event part-of structure. Part-of is a partial order on
+    events with temporal and sort constraints. -/
+class Mereology (Time : Type*) [LinearOrder Time] where
+  /-- e₁ is a part of e₂ -/
+  partOf : Event Time → Event Time → Prop
+  /-- Part-of is reflexive -/
+  refl : ∀ e, partOf e e
+  /-- Part-of is antisymmetric -/
+  antisymm : ∀ e₁ e₂, partOf e₁ e₂ → partOf e₂ e₁ → e₁ = e₂
+  /-- Part-of is transitive -/
+  trans : ∀ e₁ e₂ e₃, partOf e₁ e₂ → partOf e₂ e₃ → partOf e₁ e₃
+  /-- τ is monotone: if e₁ ⊑ e₂ then τ(e₁) ⊆ τ(e₂) -/
+  τ_monotone : ∀ e₁ e₂, partOf e₁ e₂ →
+    e₁.runtime.subinterval e₂.runtime
+  /-- Sort is preserved under part-of: parts of actions are actions,
+      parts of states are states -/
+  sort_preserved : ∀ e₁ e₂, partOf e₁ e₂ → e₁.sort = e₂.sort
+
+/-- Event mereology induces a Preorder. -/
+instance preorder (Time : Type*) [LinearOrder Time]
+    [m : Mereology Time] : Preorder (Event Time) where
+  le := m.partOf
+  le_refl := m.refl
+  le_trans := m.trans
+
+/-! ### Manner -/
+
+/-- A manner: the "how" of an event, individuated as an equivalence class
+    of events under a similarity relation (@cite{liefke-2024} §4.3).
+    Manners are to events what properties are to individuals. -/
+@[ont_sort] structure Manner (Time : Type*) [LinearOrder Time] where
+  /-- The characteristic predicate: which events exhibit this manner -/
+  exhibits : Event Time → Prop
+
+/-- The manner of an event under a similarity criterion.
+    `e.manner sim` gives the manner class of `e` under `sim`. -/
+def manner (e : Event Time) (sim : Event Time → Event Time → Prop) : Manner Time :=
+  ⟨sim e⟩
+
+/-- Two events share a manner iff both satisfy the manner predicate. -/
+def Manner.sharedBy (m : Manner Time) (e₁ e₂ : Event Time) : Prop :=
+  m.exhibits e₁ ∧ m.exhibits e₂
+
+end Event
+
 /-! ### Concrete examples (ℤ-time events) -/
 
 /-- Example: a running event from time 1 to 5. -/
@@ -96,6 +192,9 @@ theorem exampleRun_not_state : ¬ exampleRun.isState := by decide
 /-- The know event is not an action. -/
 theorem exampleKnow_not_action : ¬ exampleKnow.isAction := by decide
 
+/-- The run event is durative. -/
+theorem exampleRun_isDurative : exampleRun.isDurative := by decide
+
 /-- The run event starts at 1. -/
 theorem exampleRun_start : exampleRun.τ.start = 1 := rfl