Event Mereology

@cite{bach-1986} @cite{champollion-2017}

Event-specific mereological infrastructure built on top of the generic Core.Mereology definitions. Specializes CUM, QUA, IsSumHom, etc. to event structures with EventCEM, thematic role homomorphisms, and Vendler class bridges.

Generic mereological definitions (CUM, DIV, QUA, Atom, AlgClosure, IsSumHom, Overlap, ExtMeasure, QMOD) live in Core.Mereology.

Event CEM (Classical Extensional Mereology)

class Semantics.Events.CEM.EventCEM (Time : Type u_1) [LinearOrder Time] extends Semantics.Events.EventMereology Time : Type u_1

Classical Extensional Mereology for events: enriches EventMereology with binary sum (⊔) via SemilatticeSup (Event Time). @cite{champollion-2017} Ch. 2: event domain forms a join semilattice.

• partOf : Event Time → Event Time → Prop
• refl (e : Event Time) : partOf e e
• antisymm (e₁ e₂ : Event Time) : partOf e₁ e₂ → partOf e₂ e₁ → e₁ = e₂
• trans (e₁ e₂ e₃ : Event Time) : partOf e₁ e₂ → partOf e₂ e₃ → partOf e₁ e₃
• τ_monotone (e₁ e₂ : Event Time) : partOf e₁ e₂ → e₁.runtime.subinterval e₂.runtime
• sort_preserved (e₁ e₂ : Event Time) : partOf e₁ e₂ → e₁.sort = e₂.sort
• evSemilatticeSup : SemilatticeSup (Event Time)

  Events form a join semilattice (binary sum ⊕ exists).

• le_eq_partOf (e₁ e₂ : Event Time) : e₁ ≤ e₂ ↔ EventMereology.partOf e₁ e₂

  ≤ from SemilatticeSup agrees with partOf.

• intervalSemilatticeSup : SemilatticeSup (Core.Time.Interval Time)

  Intervals form a join semilattice (for τ homomorphism).

• τ_hom (e₁ e₂ : Event Time) : (SemilatticeSup.sup e₁ e₂).runtime = SemilatticeSup.sup e₁.runtime e₂.runtime

  τ is a sum homomorphism: τ(e₁ ⊕ e₂) = τ(e₁) ⊕ τ(e₂). @cite{champollion-2017} §2.5.1.

@[implicit_reducible]

noncomputable instance Semantics.Events.CEM.eventCEMSemilatticeSup (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] : SemilatticeSup (Event Time)

Equations

• Semantics.Events.CEM.eventCEMSemilatticeSup Time = Semantics.Events.CEM.EventCEM.evSemilatticeSup

Lexical Cumulativity

def Semantics.Events.CEM.LexCum (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] (P : EvPred Time) : Prop

Lexical cumulativity for event predicates: the event-specific instantiation of CUM. A verb predicate V is lexically cumulative iff for any two V-events, their sum is also a V-event. @cite{champollion-2017} §3.2: activities and states are lexically cumulative.

Equations

• Semantics.Events.CEM.LexCum Time P = ∀ (e₁ e₂ : Semantics.Events.Event Time), P e₁ → P e₂ → P (SemilatticeSup.sup e₁ e₂)

theorem Semantics.Events.CEM.cum_iff_lexCum (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] (P : EvPred Time) : Mereology.CUM P ↔ LexCum Time P

LexCum is exactly CUM specialized to EvPred. This bridges the abstract and event-specific formulations.

Role Homomorphism (θ preserves ⊕)

class Semantics.Events.CEM.RoleHom (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : EventCEM Time] [SemilatticeSup Entity] : Type (max u_1 u_2)

A thematic-role sum homomorphism: the function mapping each event to its θ-role filler preserves ⊕. @cite{champollion-2017} §2.5.1 eq. 34–35: Agent(e₁ ⊕ e₂) = Agent(e₁) ⊕ Agent(e₂).

This is stated as: given a function θ : Event Time → Entity extracting the unique role-filler, θ is a sum homomorphism.

• agentOf : Event Time → Entity

  Agent extraction function (partial: only defined for events with agents).

• agent_hom : Mereology.IsSumHom agentOf

  Agent extraction preserves ⊕.

• patientOf : Event Time → Entity

  Patient extraction function.

• patient_hom : Mereology.IsSumHom patientOf

  Patient extraction preserves ⊕.

• themeOf : Event Time → Entity

  Theme extraction function.

• theme_hom : Mereology.IsSumHom themeOf

  Theme extraction preserves ⊕.

Trace Functions: τ, σ, θ as IsSumHom (@cite{champollion-2017} §2.5)

Trace functions = sum-homomorphisms on Event T

@cite{champollion-2017} §2.5 calls τ, σ, and the thematic-role extractors "trace functions" — functions that trace each event into a different domain (time, space, entities). The structural property they share is sum-homomorphism: the trace of a sum equals the sum of the traces. Linglib uses Mereology.IsSumHom as the unifying abstraction; any function f : Event Time → β that admits an IsSumHom instance qualifies as a trace function for substrate purposes.

The concrete trace functions in linglib are:

• τ (runtime): instance below, derived from EventCEM.τ_hom.
• σ (spatial extent): instIsSumHomσ in Trace.lean, derived from Trace.σ_map_sup.
• agentOf / patientOf / themeOf: instances below, derived from RoleHom.agent_hom / patient_hom / theme_hom.

This unification means SR theorems (StratifiedReference.lean) can be stated dimension-polymorphically as (d : Event T → β) [IsSumHom d] → ... and instantiate uniformly across all five trace functions, rather than per-trace.

theorem Semantics.Events.CEM.τ_is_sum_hom (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] (e₁ e₂ : Event Time) : (SemilatticeSup.sup e₁ e₂).runtime = SemilatticeSup.sup e₁.runtime e₂.runtime

τ is a sum homomorphism: follows directly from EventCEM.τ_hom. τ(e₁ ⊕ e₂) = τ(e₁) ⊕ τ(e₂). @cite{champollion-2017} §2.5.1: the runtime function preserves sums.

instance Semantics.Events.CEM.instIsSumHomRuntime (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] : Mereology.IsSumHom fun (e : Event Time) => e.runtime

τ (runtime extraction) as an IsSumHom instance, derived from EventCEM.τ_hom. Enables cum_pullback to work automatically for τ without manually threading the sum-homomorphism proof.

instance Semantics.Events.CEM.instIsSumHomAgent (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : EventCEM Time] [SemilatticeSup Entity] [rh : RoleHom Entity Time] : Mereology.IsSumHom RoleHom.agentOf

agentOf as an IsSumHom instance, derived from RoleHom.agent_hom. Parallels instIsSumHomRuntime for τ — same mathlib pattern of promoting a structure field to a resolvable typeclass instance.

instance Semantics.Events.CEM.instIsSumHomPatient (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : EventCEM Time] [SemilatticeSup Entity] [rh : RoleHom Entity Time] : Mereology.IsSumHom RoleHom.patientOf

patientOf as an IsSumHom instance, derived from RoleHom.patient_hom.

instance Semantics.Events.CEM.instIsSumHomTheme (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : EventCEM Time] [SemilatticeSup Entity] [rh : RoleHom Entity Time] : Mereology.IsSumHom RoleHom.themeOf

themeOf as an IsSumHom instance, derived from RoleHom.theme_hom.

Bridges to Existing Types

theorem Semantics.Events.CEM.vendlerClass_atelic_cases (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.atelic) : c = Features.VendlerClass.state ∨ c = Features.VendlerClass.activity ∨ c = Features.VendlerClass.semelfactive

Atelic Vendler classes are exactly states, activities, and semelfactives.

theorem Semantics.Events.CEM.vendlerClass_telic_cases (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.telic) : c = Features.VendlerClass.achievement ∨ c = Features.VendlerClass.accomplishment

Telic Vendler classes are exactly achievements and accomplishments.