Spatiotemporal Distance @cite{koev-2017}

@cite{cumming-2026}

@cite{koev-2017}:1–38) argues that the Bulgarian evidential introduces a learning event — the event through which the speaker acquired the reported information — that must be spatiotemporally distant (△) from the described event. The key predicate (Definition 24):

△(e, e') iff τ(e) ∩ τ(e') = ∅ ∨ loc(e) ≠ loc(e')

Two events satisfy △ when either their temporal traces don't overlap (standard indirect evidence: the speaker learned about the event after it happened) or they occur at different locations (the smoke-from-chimney scenario: the speaker perceives the event's effects from a distance, at the same time but a different place).

Architectural Note

Events (Ev Time) currently lack a location field. Rather than extending the core event type (which would affect ~20 files), this module defines △ parameterized over an external location function loc : Ev Time → L. The temporal component (temporallyDisjoint) is self-contained and connects to @cite{cumming-2026}'s downstream evidence constraint (T ≤ A) via disjoint_earlier_implies_isBefore.

def Semantics.Events.SpatiotemporalDistance.temporallyDisjoint {Time : Type u_1} [LinearOrder Time] (e₁ e₂ : Ev Time) : Prop

Two events are temporally disjoint when their temporal traces do not overlap (@cite{koev-2017}, first disjunct of Definition 24). This rules out direct perception: if the speaker was present for the event, the evidential is infelicitous.

Equations

• Semantics.Events.SpatiotemporalDistance.temporallyDisjoint e₁ e₂ = ¬e₁.τ.overlaps e₂.τ

def Semantics.Events.SpatiotemporalDistance.spatiotemporallyDistant {Time : Type u_1} [LinearOrder Time] {L : Type u_2} [DecidableEq L] (loc : Ev Time → L) (e₁ e₂ : Ev Time) : Prop

Spatiotemporal distance △ (@cite{koev-2017}, Definition 24). Two events are spatiotemporally distant if either their temporal traces don't overlap or they occur at different locations. Parameterized over a location function loc : Ev Time → L since Ev lacks a built-in location field.

Equations

• Semantics.Events.SpatiotemporalDistance.spatiotemporallyDistant loc e₁ e₂ = (Semantics.Events.SpatiotemporalDistance.temporallyDisjoint e₁ e₂ ∨ loc e₁ ≠ loc e₂)

theorem Semantics.Events.SpatiotemporalDistance.temporallyDisjoint_of_precedes {Time : Type u_1} [LinearOrder Time] (e₁ e₂ : Ev Time) (h : e₁.τ.precedes e₂.τ) : temporallyDisjoint e₁ e₂

If e₁ temporally precedes e₂ (no overlap, e₁ strictly before e₂), then they are temporally disjoint. This is the standard indirect evidence case: the described event finished before the learning event started.

theorem Semantics.Events.SpatiotemporalDistance.disjoint_earlier_implies_isBefore {Time : Type u_1} [LinearOrder Time] (e₁ e₂ : Ev Time) (hd : temporallyDisjoint e₁ e₂) (hearlier : e₁.τ.start ≤ e₂.τ.start) : e₁.τ.isBefore e₂.τ

If two events are temporally disjoint and the first starts no later than the second, then the first is temporally before the second: e₁.τ.finish ≤ e₂.τ.start. This bridges Koev's event-based △ to Cumming's point-based T ≤ A constraint.

theorem Semantics.Events.SpatiotemporalDistance.overlapping_not_disjoint {Time : Type u_1} [LinearOrder Time] (e₁ e₂ : Ev Time) (h : e₁.τ.overlaps e₂.τ) : ¬temporallyDisjoint e₁ e₂

If two events' temporal traces overlap, they are not temporally disjoint. Direct perception (overlapping runtimes) is incompatible with temporal distance.

theorem Semantics.Events.SpatiotemporalDistance.spatiotemporallyDistant_of_different_location {Time : Type u_1} [LinearOrder Time] {L : Type u_2} [DecidableEq L] (loc : Ev Time → L) (e₁ e₂ : Ev Time) (h : loc e₁ ≠ loc e₂) : spatiotemporallyDistant loc e₁ e₂

Spatial distance alone suffices for △, regardless of temporal overlap (@cite{koev-2017}, ex. 25b: smoke from chimney).

theorem Semantics.Events.SpatiotemporalDistance.spatiotemporallyDistant_of_temporallyDisjoint {Time : Type u_1} [LinearOrder Time] {L : Type u_2} [DecidableEq L] (loc : Ev Time → L) (e₁ e₂ : Ev Time) (h : temporallyDisjoint e₁ e₂) : spatiotemporallyDistant loc e₁ e₂

Temporal disjointness alone suffices for △.