Generalized intervals with open/closed boundaries

@cite{rouillard-2026}

GInterval extends the basic Interval with explicit open/closed annotations on each endpoint, plus the closed/open_ constructors, the toOpen/toClosed operations (eq. 99a–b), and generalized containment/subinterval relations.

Used by Rouillard 2026's account of G-TIA polarity sensitivity, where event runtimes are closed and PTSs are open.

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

A generalized interval with specified boundary types. Extends the basic Interval with open/closed annotations on each end. @cite{rouillard-2026} eq. (14a–b), (99a–b).

• left : Time

  Left endpoint

• right : Time

  Right endpoint

• leftType : BoundaryType

  Left boundary type: closed [m or open]m

• rightType : BoundaryType

  Right boundary type: closed m] or open m[

• valid : self.left ≤ self.right

  The endpoints are ordered

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

A closed interval [m₁, m₂]: both endpoints included. @cite{rouillard-2026} eq. (14a): C := {t | min(t) ⊑ᵢ t ∧ max(t) ⊑ᵢ t}.

Equations

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

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

An open interval]m₁, m₂[: both endpoints excluded. @cite{rouillard-2026} eq. (14b): O := {t | min(t) ⊄ᵢ t ∨ max(t) ⊄ᵢ t}.

Equations

• Core.Time.Interval.GInterval.open_ i = { left := i.start, right := i.finish, leftType := Core.Time.Interval.BoundaryType.open_, rightType := Core.Time.Interval.BoundaryType.open_, valid := ⋯ }

def Core.Time.Interval.GInterval.toOpen {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : GInterval Time

The o(t) operation: open counterpart of a time. @cite{rouillard-2026} eq. (99a): if t is open, o(t) = t; if t is closed, o(t) is the open interval with the same endpoints.

Equations

• gi.toOpen = { left := gi.left, right := gi.right, leftType := Core.Time.Interval.BoundaryType.open_, rightType := Core.Time.Interval.BoundaryType.open_, valid := ⋯ }

def Core.Time.Interval.GInterval.toClosed {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : GInterval Time

The c(t) operation: closed counterpart of a time. @cite{rouillard-2026} eq. (99b): if t is closed, c(t) = t; if t is open, c(t) adds the endpoints.

Equations

• gi.toClosed = { left := gi.left, right := gi.right, leftType := Core.Time.Interval.BoundaryType.closed, rightType := Core.Time.Interval.BoundaryType.closed, valid := ⋯ }

def Core.Time.Interval.GInterval.isClosed {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : Prop

Is this interval closed (both boundaries included)?

Equations

• gi.isClosed = (gi.leftType = Core.Time.Interval.BoundaryType.closed ∧ gi.rightType = Core.Time.Interval.BoundaryType.closed)

def Core.Time.Interval.GInterval.isOpen {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : Prop

Is this interval open (both boundaries excluded)?

Equations

• gi.isOpen = (gi.leftType = Core.Time.Interval.BoundaryType.open_ ∧ gi.rightType = Core.Time.Interval.BoundaryType.open_)

def Core.Time.Interval.GInterval.gcontains {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) (m : Time) : Prop

Containment for generalized intervals: m is in gi. For closed endpoints, ≤ is used; for open endpoints, <.

Equations

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

def Core.Time.Interval.GInterval.gsubinterval {Time : Type u_1} [LinearOrder Time] (gi₁ gi₂ : GInterval Time) : Prop

Generalized subinterval: gi₁ ⊆ gi₂ (every moment in gi₁ is in gi₂).

Equations

• gi₁.gsubinterval gi₂ = ∀ (m : Time), gi₁.gcontains m → gi₂.gcontains m

def Core.Time.Interval.GInterval.toInterval {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : Interval Time

Convert a closed GInterval back to the basic Interval type.

Equations

• gi.toInterval = { start := gi.left, finish := gi.right, valid := ⋯ }

@[simp]

theorem Core.Time.Interval.GInterval.toClosed_isClosed {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : gi.toClosed.isClosed

The closed counterpart of an open interval is always closed.

@[simp]

theorem Core.Time.Interval.GInterval.toOpen_isOpen {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : gi.toOpen.isOpen

The open counterpart is always open.

@[simp]

theorem Core.Time.Interval.GInterval.toClosed_idempotent {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : gi.toClosed.toClosed = gi.toClosed

toClosed is idempotent.

@[simp]

theorem Core.Time.Interval.GInterval.toOpen_idempotent {Time : Type u_1} [LinearOrder Time] (gi : GInterval Time) : gi.toOpen.toOpen = gi.toOpen

toOpen is idempotent.

@[simp]

theorem Core.Time.Interval.GInterval.closed_gcontains_start {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : (closed i).gcontains i.start

The closed counterpart of an interval contains its endpoints (definitional).

@[simp]

theorem Core.Time.Interval.GInterval.closed_gcontains_finish {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : (closed i).gcontains i.finish

theorem Core.Time.Interval.GInterval.gsubinterval_closed_open_strict {Time : Type u_1} [LinearOrder Time] (rt : Interval Time) (gi : GInterval Time) (h_open : gi.isOpen) (h_sub : (closed rt).gsubinterval gi) : gi.left < rt.start ∧ rt.finish < gi.right

A closed interval contained in an open generalized interval forces strict inequalities at both endpoints. The right hypothesis the prior MaxInfo no_smallest_open_including_closed had to assume (pts.left < runtime.start) is derivable once openness is enforced structurally — instantiate gsubinterval at the closed endpoints and unfold gcontains.