Temporal intervals

@cite{allen-1983} @cite{kamp-reyle-1993} @cite{klein-1994} @cite{pancheva-2003} @cite{rouillard-2026} @cite{sagey-1986} @cite{smith-1997}

The basic interval type and its relational algebra: containment, subinterval, overlap, precedence, meets, plus the nuclear cluster needed by aspectual semantics (proper subinterval, final subinterval, initial overlap, isAfter/isBefore).

Open/closed boundary distinctions and generalized intervals (@cite{rouillard-2026}) live in Generalized.lean.

structure Core.Time.Interval (Time : Type u_1) [LinearOrder Time] : Type u_1

Temporal interval: a pair of times [start, finish] with start ≤ finish. Following standard interval semantics.

• start : Time
• finish : Time
• valid : self.start ≤ self.finish

def Core.Time.Interval.point {Time : Type u_1} [LinearOrder Time] (t : Time) : Interval Time

Point interval: start = finish

Equations

• Core.Time.Interval.point t = { start := t, finish := t, valid := ⋯ }

def Core.Time.Interval.contains {Time : Type u_1} [LinearOrder Time] (i : Interval Time) (t : Time) : Prop

Does time t fall within interval i?

Equations

• i.contains t = (i.start ≤ t ∧ t ≤ i.finish)

def Core.Time.Interval.subinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Interval i₁ is contained in i₂

Equations

• i₁.subinterval i₂ = (i₂.start ≤ i₁.start ∧ i₁.finish ≤ i₂.finish)

def Core.Time.Interval.overlaps {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Intervals overlap

Equations

• i₁.overlaps i₂ = (i₁.start ≤ i₂.finish ∧ i₂.start ≤ i₁.finish)

def Core.Time.Interval.precedes {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ precedes i₂ (no overlap, i₁ entirely before i₂)

Equations

• i₁.precedes i₂ = (i₁.finish < i₂.start)

def Core.Time.Interval.meets {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ meets i₂ (i₁ ends exactly when i₂ starts)

Equations

• i₁.meets i₂ = (i₁.finish = i₂.start)

def Core.Time.Interval.properSubinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Proper subinterval: i₁ ⊆ i₂ with at least one strict boundary. Required for IMPF: reference time PROPERLY inside event runtime.

Equations

• i₁.properSubinterval i₂ = (i₁.subinterval i₂ ∧ (i₂.start < i₁.start ∨ i₁.finish < i₂.finish))

def Core.Time.Interval.IsPoint {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : Prop

An interval is a point iff its endpoints coincide (start = finish). The atomic case in the time dimension — used by Bennett-Partee 1972 strict subinterval property and Zhao 2025 ATOM-DIST_t at the atomic granularity.

Equations

• i.IsPoint = (i.start = i.finish)

def Core.Time.Interval.isAfter {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ is entirely after i₂ (i₁ starts at or after i₂ finishes).

Equations

• i₁.isAfter i₂ = (i₂.finish ≤ i₁.start)

def Core.Time.Interval.isBefore {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ is entirely before i₂.

Equations

• i₁.isBefore i₂ = (i₁.finish ≤ i₂.start)

theorem Core.Time.Interval.properSubinterval_implies_subinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) (h : i₁.properSubinterval i₂) : i₁.subinterval i₂

@[simp]

theorem Core.Time.Interval.subinterval_refl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : i.subinterval i

theorem Core.Time.Interval.properSubinterval_irrefl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : ¬i.properSubinterval i

No interval is properly contained in itself.

theorem Core.Time.Interval.isAfter_iff_isBefore {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : i₁.isAfter i₂ ↔ i₂.isBefore i₁

def Core.Time.Interval.finalSubinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Final subinterval: i₁ ⊆ i₂ and they share the same right endpoint. @cite{pancheva-2003}: PTS(i', i) iff i is a final subinterval of i'.

Equations

• i₁.finalSubinterval i₂ = (i₁.subinterval i₂ ∧ i₁.finish = i₂.finish)

def Core.Time.Interval.initialOverlap {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Initial overlap (∂): i₁ and i₂ overlap, and the start of i₂ is in i₁. @cite{pancheva-2003}: i ∂τ(e) — the beginning of the eventuality is included in the reference interval but the end may not be. @cite{smith-1997}: the neutral viewpoint uses the same interval relation.

Equations

• i₁.initialOverlap i₂ = (i₁.overlaps i₂ ∧ i₁.contains i₂.start)

theorem Core.Time.Interval.finalSubinterval_implies_subinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) (h : i₁.finalSubinterval i₂) : i₁.subinterval i₂

Final subinterval implies subinterval.

theorem Core.Time.Interval.finalSubinterval_refl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : i.finalSubinterval i

Every interval is a final subinterval of itself.

@[simp]

theorem Core.Time.Interval.overlaps_refl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : i.overlaps i

Overlap is reflexive: every interval overlaps itself.

theorem Core.Time.Interval.overlaps_symm {Time : Type u_1} [LinearOrder Time] {i₁ i₂ : Interval Time} (h : i₁.overlaps i₂) : i₂.overlaps i₁

Overlap is symmetric.

theorem Core.Time.Interval.overlaps_comm {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : i₁.overlaps i₂ ↔ i₂.overlaps i₁

Overlap is symmetric (iff version).

theorem Core.Time.Interval.overlaps_not_transitive : ¬∀ (i₁ i₂ i₃ : Interval ℤ), i₁.overlaps i₂ → i₂.overlaps i₃ → i₁.overlaps i₃

Overlap is NOT transitive: [0,1] overlaps [1,2] and [1,2] overlaps [2,3], but [0,1] does not overlap [2,3].

This is the cornerstone property that distinguishes overlap from simultaneity (identity) and makes the No-Crossing Constraint derivable from temporal precedence alone (@cite{sagey-1986} §5.2.3, fn. 6).

theorem Core.Time.Interval.subinterval_overlaps {Time : Type u_1} [LinearOrder Time] {i₁ i₂ : Interval Time} (h : i₁.subinterval i₂) : i₁.overlaps i₂

Subintervals overlap their containing intervals.

theorem Core.Time.Interval.precedes_irrefl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : ¬i.precedes i

Precedence is irreflexive: no interval precedes itself.

theorem Core.Time.Interval.precedes_asymm {Time : Type u_1} [LinearOrder Time] {i₁ i₂ : Interval Time} (h : i₁.precedes i₂) : ¬i₂.precedes i₁

Precedence is asymmetric.

theorem Core.Time.Interval.precedes_trans {Time : Type u_1} [LinearOrder Time] {i₁ i₂ i₃ : Interval Time} (h₁₂ : i₁.precedes i₂) (h₂₃ : i₂.precedes i₃) : i₁.precedes i₃

Precedence is transitive.

theorem Core.Time.Interval.precedes_not_overlaps {Time : Type u_1} [LinearOrder Time] {i₁ i₂ : Interval Time} (h : i₁.precedes i₂) : ¬i₁.overlaps i₂

Precedence and overlap are mutually exclusive.

inductive Core.Time.Interval.BoundaryType : Type

Whether an interval's boundary is included (closed) or excluded (open). @cite{rouillard-2026} §2.2.4: the distinction between closed and open times is central to deriving the polarity sensitivity of G-TIAs. Event runtimes are closed; PTSs are open intervals.

Consumed by GInterval (in Generalized.lean).

• closed : BoundaryType
• open_ : BoundaryType

@[implicit_reducible]

instance Core.Time.Interval.instDecidableEqBoundaryType : DecidableEq BoundaryType

Equations

• Core.Time.Interval.instDecidableEqBoundaryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Time.Interval.instReprBoundaryType.repr : BoundaryType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Time.Interval.instReprBoundaryType : Repr BoundaryType

Equations

• Core.Time.Interval.instReprBoundaryType = { reprPrec := Core.Time.Interval.instReprBoundaryType.repr }

def Core.Time.Interval.BoundaryType.toBoundedness : BoundaryType → Scale.Boundedness

Interval boundary type maps to scale boundedness. @cite{rouillard-2026}: closed runtimes correspond to closed scales (licensed); open PTSs correspond to open scales (blocked/information collapse). This is the "interval generalization": Interval.BoundaryType.closed/.open_ is isomorphic to Core.Scale.Boundedness.closed/.open_.

Equations

• Core.Time.Interval.BoundaryType.closed.toBoundedness = Core.Scale.Boundedness.closed
• Core.Time.Interval.BoundaryType.open_.toBoundedness = Core.Scale.Boundedness.open_

theorem Core.Time.Interval.closedBoundary_licensed : BoundaryType.closed.toBoundedness.isLicensed = true

theorem Core.Time.Interval.openBoundary_blocked : BoundaryType.open_.toBoundedness.isLicensed = false

@[implicit_reducible]

instance Core.Time.Interval.instLicensingPipelineBoundaryType : Scale.LicensingPipeline BoundaryType

Equations

• Core.Time.Interval.instLicensingPipelineBoundaryType = { toBoundedness := Core.Time.Interval.BoundaryType.toBoundedness }