Event Adjacency and Temporal Precedence

[Kri98] [Bac86] [Cha17]

Two events are temporally adjacent (∞_E in [Kri98]'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:

• Studies/Krifka1998.lean Part II for K98 §4 adjacency-respecting θ relations (ADJ/SMR/MR) and the K98 §2.5 initial/final-part / telicity predicates
• MeasureAdverbialDerivation.lean (planned, K98 §3.5 cτ minimal- convex-time derivation)

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

Two events are temporally adjacent (∞_E in [Kri98]'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.toProd.2 = e2.runtime.toProd.1 ∨ e2.runtime.toProd.2 = e1.runtime.toProd.1)

def 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 Event.adjacent_symm {Time : Type u_1} [LinearOrder Time] (e1 e2 : Event Time) : e1.adjacent e2 ↔ e2.adjacent e1

Event adjacency is symmetric.