Event Adjacency and Temporal Precedence

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

Two events are temporally adjacent (∞_E in @cite{krifka-1998}'s notation) if their runtime intervals meet; one event temporally precedes another («_E) if its runtime is entirely before the other's. These primitives are event-general — they're not specific to movement relations or any particular thematic-role analysis — and are consumed by:

• Phenomena/TenseAspect/Studies/Krifka1998.lean Part II for K98 §4 adjacency-respecting θ relations (ADJ/SMR/MR)
• InitialFinalParts.lean (initial/final parts via precedence)
• MeasureAdverbialDerivation.lean (planned, K98 §3.5 cτ minimal- convex-time derivation)

def Semantics.Events.Event.adjacent {Time : Type u_1} [LinearOrder Time] (e1 e2 : Event Time) : Prop

Two events are temporally adjacent (∞_E in @cite{krifka-1998}'s notation) if their runtime intervals meet: one's finish equals the other's start. The natural concrete instance of K98's abstract event-adjacency primitive (eq. 14) on the Event Time structure where events have runtime : Interval Time.

Equations

• e1.adjacent e2 = (e1.runtime.finish = e2.runtime.start ∨ e2.runtime.finish = e1.runtime.start)

def Semantics.Events.Event.precedes {Time : Type u_1} [LinearOrder Time] (e1 e2 : Event Time) : Prop

Event temporal precedence («_E in K98 §2.5): one event's runtime is entirely before the other's. Defined via Interval.isBefore from Core/Time/Interval/Basic.lean.

Equations

• e1.precedes e2 = e1.runtime.isBefore e2.runtime

theorem Semantics.Events.Event.adjacent_symm {Time : Type u_1} [LinearOrder Time] (e1 e2 : Event Time) : e1.adjacent e2 ↔ e2.adjacent e1

Event adjacency is symmetric.