refactor(Semantics/Events): root-namespace Event, sort via Dynamicity

Linglib.lean

@@ -2344,6 +2344,7 @@ import Linglib.Studies.Krifka2004
 import Linglib.Semantics.Kinds.Subkinds
 import Linglib.Semantics.Homogeneity.Basic
 import Linglib.Semantics.ArgumentStructure.Relational
+import Linglib.Semantics.ArgumentStructure.ArgumentIntroduction
 import Linglib.Semantics.Plurality.Algebra
 import Linglib.Semantics.Plurality.Basic
 import Linglib.Semantics.Plurality.Cover

Linglib/Features/Aktionsart.lean

@@ -27,7 +27,7 @@ The CUM/QUA/DIV algebra over event predicates lives in
 `Telicity` here is the Smith-flavored derived label.
 
 Sibling formalizations of competitor lexical-aspect frameworks:
-@cite{bach-1986} `EventSort` in `Semantics/Events/Basic.lean`;
+@cite{bach-1986}; the event-token sort is this `Dynamicity` feature (`Event.sort`);
 @cite{krifka-1989}/@cite{krifka-1998} CUM/QUA/DIV in
 `Semantics/Events/CEM.lean`; @cite{dowty-1979} SIP in
 `Semantics/Tense/Aspect/SubintervalProperty.lean`;

Linglib/Fragments/Slavic/Serbian/TemporalConnectives.lean

@@ -26,7 +26,6 @@ PFV/IMPF opposition rather than Tagalog's finer-grained system.
 
 namespace Fragments.Slavic.Serbian.TemporalConnectives
 
-open Semantics.Events
 open Semantics.Aspect
 open Fragments.English.TemporalExpressions (Reading TemporalExprEntry ComplementType)
 

Linglib/Fragments/Tagalog/TemporalConnectives.lean

@@ -22,7 +22,6 @@ overt aspect markers in Tagalog.
 
 namespace Fragments.Tagalog.TemporalConnectives
 
-open Semantics.Events
 open Semantics.Aspect
 open Fragments.English.TemporalExpressions (Reading TemporalExprEntry ComplementType)
 

Linglib/Semantics/ArgumentStructure/ArgumentIntroduction.lean

@@ -0,0 +1,212 @@
+import Linglib.Semantics.ArgumentStructure.Defs
+
+/-!
+# Argument Introduction by Functional Heads
+
+@cite{kratzer-1996} @cite{pylkkanen-2008} @cite{wood-marantz-2017}
+@cite{parsons-1990} @cite{moltmann-2025} @cite{hopperdietzel-2024}
+
+Neo-Davidsonian substrate for argument-introducing heads (Voice, applicative,
+Cause), built on the canonical `ThematicRel` (`Entity → Event Time → Prop`,
+@cite{moltmann-2025}: "the preferred version of event semantics for
+syntacticians"). A verb/VP denotation is a predicate of events
+`Event Time → Prop` (this is `Set (Event Time)`; used predicatively).
+
+The central new object is `VerbDenot`: a verb denotation classified by the
+structure argument introduction is sensitive to (valence). @cite{pylkkanen-2008}'s
+high/low contrast is the `IntroMode` parameter — whether the introduced
+participant is related to the *event* (high applicative / Voice, via Event
+Identification) or to the verb's internal *theme* (low applicative, via a
+transfer relation). The transitivity restriction then falls out of the
+denotations' types rather than being stipulated, and @cite{wood-marantz-2017}'s
+contextually-interpreted single argument-introducer is its `IntroMode` reading.
+
+## Main definitions
+
+* `eventIdentification` — @cite{kratzer-1996}'s Event Identification combinator
+* `RolesExclusive` — thematic uniqueness (the principle behind eq. 103)
+* `VerbDenot` — verb denotation classified by valence
+* `IntroMode` / `IntroMode.Licenses` — high/low introduction and its licensing
+* `applToEvent` / `applToTheme` — the high / low applicative denotations
+* `causeBieventive` / `causeThetaRole` — the §3.2 Cause-is-not-a-θ-role contrast
+-/
+
+namespace Semantics.ArgumentStructure
+
+variable {Entity : Type*} {Time : Type*} [LinearOrder Time]
+
+/-! ### Event Identification and thematic uniqueness -/
+
+/-- Event Identification (@cite{kratzer-1996}): combine an argument-introducer
+`f` (a thematic relation, awaiting its participant) with a VP predicate `g`,
+conjoining at the event. The result still awaits the introduced participant. -/
+def eventIdentification (f : ThematicRel Entity Time) (g : Event Time → Prop) :
+    ThematicRel Entity Time :=
+  fun x e => f x e ∧ g e
+
+theorem eventIdentification_apply (f : ThematicRel Entity Time)
+    (g : Event Time → Prop) (x : Entity) (e : Event Time) :
+    eventIdentification f g x e ↔ f x e ∧ g e := Iff.rfl
+
+/-- Two thematic relations are role-exclusive when no participant bears both to
+the same event (thematic uniqueness). This is the principle behind
+@cite{pylkkanen-2008}'s eq. 103: a participant cannot be both agent and theme. -/
+def RolesExclusive (r₁ r₂ : ThematicRel Entity Time) : Prop :=
+  ∀ x e, r₁ x e → ¬ r₂ x e
+
+/-! ### Verb denotations classified by valence -/
+
+/-- A verb/VP denotation, classified by the structure argument introduction is
+sensitive to. The valence distinction is a genuine *type* difference, which is
+why @cite{pylkkanen-2008}'s transitivity restriction is a fact about this type
+rather than a stipulation.
+
+* `unergative` — a saturated event predicate, no internal-argument slot
+  (e.g. *run*). [Diagnostic 1 target]
+* `transitive` — awaits its internal theme argument, carrying a theme relation
+  (e.g. *send a letter*).
+* `kimianStative` — a relation over individuals with *no* event argument
+  (Kimian state, @cite{moltmann-2025} §1.4.1; e.g. *own*, *owe*). [Diagnostic 2] -/
+inductive VerbDenot (Entity : Type*) (Time : Type*) [LinearOrder Time] where
+  | unergative (body : Event Time → Prop)
+  | transitive (theme : ThematicRel Entity Time) (body : ThematicRel Entity Time)
+  | kimianStative (rel : Entity → Entity → Prop)
+
+namespace VerbDenot
+
+/-- Does this denotation supply an event-internal theme (Davidsonian transitive)?
+`unergative` (no participant slot) and `kimianStative` (no event argument) lack
+one, for two distinct structural reasons. -/
+def IsTransitive : VerbDenot Entity Time → Prop
+  | .transitive _ _ => True
+  | _ => False
+
+instance : DecidablePred (IsTransitive (Entity := Entity) (Time := Time)) := fun vd =>
+  match vd with
+  | .transitive _ _ => .isTrue trivial
+  | .unergative _ => .isFalse id
+  | .kimianStative _ => .isFalse id
+
+end VerbDenot
+
+/-! ### Introduction mode and licensing -/
+
+/-- The semantic mode of an argument introducer: whether it relates the
+introduced participant to the *event* (high applicative / Voice, via Event
+Identification) or to the verb's internal *theme* (low applicative, via a
+transfer relation). This is @cite{pylkkanen-2008}'s high/low contrast at the
+denotational level, and @cite{wood-marantz-2017}'s contextually-interpreted
+single argument-introducer. -/
+inductive IntroMode where
+  | toEvent  -- high applicative / Voice
+  | toTheme  -- low applicative
+  deriving DecidableEq, Repr
+
+/-- Which verb denotations an introducer of this mode can compose with, derived
+from the denotation's valence: an event-relating introducer composes with
+anything; a theme-relating one needs an event-internal theme. -/
+def IntroMode.Licenses : IntroMode → VerbDenot Entity Time → Prop
+  | .toEvent, _  => True
+  | .toTheme, vd => vd.IsTransitive
+
+instance (m : IntroMode) :
+    DecidablePred (IntroMode.Licenses m (Entity := Entity) (Time := Time)) := fun vd => by
+  cases m <;> unfold IntroMode.Licenses <;> infer_instance
+
+/-! ### Applicative denotations -/
+
+/-- High applicative / Voice denotation: introduce a participant related to the
+EVENT, via Event Identification. Total over any VP predicate — so it composes
+with unergatives. -/
+def applToEvent (rel : ThematicRel Entity Time) (vp : Event Time → Prop) :
+    ThematicRel Entity Time :=
+  eventIdentification rel vp
+
+/-- Low applicative denotation: relate the applied argument to the THEME of a
+transitive verb via a transfer relation. Requires the verb's internal theme
+function `ThematicRel Entity Time` (type ⟨e,⟨s,t⟩⟩) — an unergative or Kimian
+state cannot supply it. -/
+def applToTheme (themeRel : ThematicRel Entity Time)
+    (transfer : Entity → Entity → Prop) (verb : ThematicRel Entity Time)
+    (theme applied : Entity) : Event Time → Prop :=
+  fun e => verb theme e ∧ themeRel theme e ∧ transfer theme applied
+
+/-- Any low-applicative denotation entails the theme bears the theme relation —
+the theme conjunct is present by construction. -/
+theorem applToTheme_entails_theme (themeRel : ThematicRel Entity Time)
+    (transfer : Entity → Entity → Prop) (verb : ThematicRel Entity Time)
+    (theme applied : Entity) (e : Event Time)
+    (h : applToTheme themeRel transfer verb theme applied e) : themeRel theme e :=
+  h.2.1
+
+/-! ### The transitivity restriction, derived -/
+
+/-- High introduction licenses any verb, including unergatives (Luganda/Venda/
+Albanian high applicatives over unergatives, @cite{pylkkanen-2008} §2.1.2). -/
+theorem toEvent_licenses_all (vd : VerbDenot Entity Time) :
+    IntroMode.toEvent.Licenses vd := trivial
+
+/-- Diagnostic 1: low (theme-relating) introduction is blocked over an
+unergative — it has no event-internal theme. Derived from the valence type,
+not stipulated. -/
+theorem toTheme_blocks_unergative (body : Event Time → Prop) :
+    ¬ IntroMode.toTheme.Licenses (VerbDenot.unergative (Entity := Entity) body) :=
+  id
+
+/-- Diagnostic 2: low introduction is blocked over a Kimian stative — distinct
+reason from Diagnostic 1: no event argument at all (@cite{moltmann-2025}). -/
+theorem toTheme_blocks_kimian (rel : Entity → Entity → Prop) :
+    ¬ IntroMode.toTheme.Licenses (VerbDenot.kimianStative (Time := Time) rel) :=
+  id
+
+/-- Low introduction is licensed over a Davidsonian transitive (English DOC,
+Hebrew possessor datives). -/
+theorem toTheme_licenses_transitive (themeRel body : ThematicRel Entity Time) :
+    IntroMode.toTheme.Licenses (VerbDenot.transitive themeRel body) := trivial
+
+/-- @cite{pylkkanen-2008}'s eq. 103, as a theorem about the denotations:
+forcing a low (theme-relating) applicative onto an unergative binds the applied
+argument's theme relation to the external argument, yielding `agentRel x e ∧
+themeRel x e` for one participant — contradictory under thematic uniqueness.
+The transitivity restriction is thus *derived*, not stipulated. -/
+theorem low_external_arg_clash
+    (agentRel themeRel : ThematicRel Entity Time)
+    (excl : RolesExclusive agentRel themeRel)
+    (x : Entity) (e : Event Time)
+    (hAgent : agentRel x e) (hTheme : themeRel x e) : False :=
+  excl x e hAgent hTheme
+
+/-! ### Cause is not a θ-role (@cite{pylkkanen-2008} Ch. 3 §3.2) -/
+
+/-- Bieventive Cause: the causative head relates the described event to a
+causing event, introducing NO individual. `λf.λe. ∃e'. f e' ∧ cause e e'`. -/
+def causeBieventive (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop) :
+    Event Time → Prop :=
+  fun e => ∃ e', caused e' ∧ cause e e'
+
+/-- The θ-role analysis @cite{pylkkanen-2008} argues against: Cause introduces a
+causer individual. `λx.λe. causer x e ∧ ∃e'. f e' ∧ cause e e'`. -/
+def causeThetaRole (cause : Event Time → Event Time → Prop)
+    (causer : ThematicRel Entity Time) (caused : Event Time → Prop) :
+    ThematicRel Entity Time :=
+  fun x e => causer x e ∧ ∃ e', caused e' ∧ cause e e'
+
+/-- The θ-role analysis forces an external (causer) participant: its denotation
+entails `causer x e`. -/
+theorem causeThetaRole_forces_causer (cause : Event Time → Event Time → Prop)
+    (causer : ThematicRel Entity Time) (caused : Event Time → Prop)
+    (x : Entity) (e : Event Time)
+    (h : causeThetaRole cause causer caused x e) : causer x e :=
+  h.1
+
+/-- The bieventive analysis admits a causative event with NO external
+participant: given only a causing relation to some caused event,
+`causeBieventive` holds without any causer. This is the Japanese adversity
+causative (@cite{pylkkanen-2008} §3.2.2) the θ-role analysis cannot model. -/
+theorem causeBieventive_no_external_arg
+    (cause : Event Time → Event Time → Prop) (caused : Event Time → Prop)
+    (e e' : Event Time) (hc : caused e') (hcause : cause e e') :
+    causeBieventive cause caused e :=
+  ⟨e', hc, hcause⟩
+
+end Semantics.ArgumentStructure

Linglib/Semantics/ArgumentStructure/Defs.lean

@@ -28,7 +28,6 @@ type/structure declarations and the Fragment ↔ Theory bridge.
 
 namespace Semantics.ArgumentStructure
 
-open Semantics.Events
 open Core.Time
 
 /-- A thematic relation: a two-place predicate relating an entity to an event.

Linglib/Semantics/ArgumentStructure/LF.lean

@@ -26,7 +26,6 @@ forms, and adverbial modification (Davidson's key payoff).
 
 namespace Semantics.ArgumentStructure
 
-open Semantics.Events
 open Core.Time
 
 /-! ### Thematic axioms (Aktionsart selection + uniqueness) -/
@@ -41,10 +40,10 @@ class ThematicAxioms (Entity Time : Type*) [LinearOrder Time]
     (frame : ThematicFrame Entity Time) where
   /-- Agents only participate in actions (dynamic events). -/
   agent_selects_action : ∀ (x : Entity) (e : Event Time),
-    frame.agent x e → e.sort = .action
+    frame.agent x e → e.sort = .dynamic
   /-- Holders only participate in states. -/
   holder_selects_state : ∀ (x : Entity) (e : Event Time),
-    frame.holder x e → e.sort = .state
+    frame.holder x e → e.sort = .stative
   /-- Each event has at most one agent. -/
   agent_unique : ∀ (x y : Entity) (e : Event Time),
     frame.agent x e → frame.agent y e → x = y
@@ -67,19 +66,19 @@ theorem agent_holder_disjoint {Entity Time : Type*} [LinearOrder Time]
 /-! ### Adverbial modification (Davidson's key payoff) -/
 
 /-- An event modifier: a predicate on events (e.g., "quickly", "in the park"). -/
-abbrev EventModifier (Time : Type*) [LinearOrder Time] := EvPred Time
+abbrev EventModifier (Time : Type*) [LinearOrder Time] := Event Time → Prop
 
 /-- Apply a modifier to an event predicate via conjunction.
     @cite{davidson-1967}: adverbial modification is conjunction of event
     predicates. "John kicked the ball quickly" = ∃e. kick(e) ∧
     Agent(j,e) ∧ Patient(b,e) ∧ quickly(e). -/
 def modify {Time : Type*} [LinearOrder Time]
-    (P : EvPred Time) (M : EventModifier Time) : EvPred Time :=
+    (P : Event Time → Prop) (M : EventModifier Time) : Event Time → Prop :=
   λ e => P e ∧ M e
 
 /-- Modification is commutative: "quickly and loudly" = "loudly and quickly". -/
 theorem modify_comm {Time : Type*} [LinearOrder Time]
-    (P : EvPred Time) (M₁ M₂ : EventModifier Time) :
+    (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) :
     modify (modify P M₁) M₂ = modify (modify P M₂) M₁ := by
   funext e
   simp only [modify]
@@ -88,7 +87,7 @@ theorem modify_comm {Time : Type*} [LinearOrder Time]
 
 /-- Modification is associative. -/
 theorem modify_assoc {Time : Type*} [LinearOrder Time]
-    (P : EvPred Time) (M₁ M₂ : EventModifier Time) :
+    (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) :
     modify (modify P M₁) M₂ = modify P (λ e => M₁ e ∧ M₂ e) := by
   funext e
   simp only [modify]
@@ -101,22 +100,22 @@ theorem modify_assoc {Time : Type*} [LinearOrder Time]
     `intransitiveLogicalForm` but using `holder` instead of `agent`,
     reflecting that states select for holders. -/
 def stativeLogicalForm {Entity Time : Type*} [LinearOrder Time]
-    (P : EvPred Time) (frame : ThematicFrame Entity Time)
+    (P : Event Time → Prop) (frame : ThematicFrame Entity Time)
     (x : Entity) : Prop :=
   ∃ s : Event Time, P s ∧ frame.holder x s
 
 /-- "x is happy in the morning" ↦ ∃s. P(s) ∧ Holder(x, s) ∧ M(s).
     State modification = event modification applied to states. -/
 def modifiedStativeLogicalForm {Entity Time : Type*} [LinearOrder Time]
-    (P : EvPred Time) (frame : ThematicFrame Entity Time)
+    (P : Event Time → Prop) (frame : ThematicFrame Entity Time)
     (x : Entity) (M : EventModifier Time) : Prop :=
   ∃ s : Event Time, P s ∧ frame.holder x s ∧ M s
 
 /-- Modified stative = stative of modified predicate (Predicate Modification):
     state modification is an instance of Davidson's conjunction-based
     event modification. -/
 theorem modified_stative_is_pm {Entity Time : Type*} [LinearOrder Time]
-    (P : EvPred Time) (frame : ThematicFrame Entity Time)
+    (P : Event Time → Prop) (frame : ThematicFrame Entity Time)
     (x : Entity) (M : EventModifier Time) :
     modifiedStativeLogicalForm P frame x M ↔
       stativeLogicalForm (modify P M) frame x := by