Rich Context

@cite{aikhenvald-2004} @cite{condoravdi-2002} @cite{cumming-2026} @cite{iatridou-2000}

RichContext extends KContext with a domain of accessible worlds and an evidential source. This supports two phenomena that plain KContext cannot express:

1. Domain expansion (@cite{condoravdi-2002}, Mizuno): backward temporal shifts expand the set of historical alternatives because more futures branch from earlier times.

2. Evidential perspective: the evidence grounding an assertion has a source type (direct, hearsay, inference) that interacts with tense morphology.

Key Types

• RichContext W E P T — KContext + domain : Set W + evidence : EvidentialSource
• KContext.toRich — lift with trivial domain (Set.univ) and default evidence
• DomainExpanding — property of a shift: it expands the domain
• hpShift — historical present temporal shift (backward time + domain expansion)

structure Core.Context.RichContext (W : Type u_1) (E : Type u_2) (P : Type u_3) (T : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A rich context: a Kaplanian context extended with a modal domain (the set of worlds accessible for modal evaluation) and an evidential source (how the speaker knows what they assert).

The domain field tracks the set of possible worlds available for modal/temporal quantification. Under branching time, moving backward in time expands this set (more futures branch from earlier times).

The evidence field tracks the evidential source for the assertion, connecting to @cite{cumming-2026}'s tense-evidential constraints.

• base : KContext W E P T

  The underlying Kaplanian context

• domain : Set W

  The set of accessible worlds (modal domain)

• evidence : Evidence.EvidentialSource

  The evidential source for the current assertion

def Core.Context.RichContext.toKContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : KContext W E P T

Project back to a KContext (forget domain and evidence).

Equations

• rc.toKContext = rc.base

def Core.Context.RichContext.agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : E

Agent of the rich context.

Equations

• rc.agent = rc.base.agent

def Core.Context.RichContext.world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : W

World of the rich context.

Equations

• rc.world = rc.base.world

def Core.Context.RichContext.time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : T

Time of the rich context.

Equations

• rc.time = rc.base.time

def Core.Context.RichContext.addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : E

Addressee of the rich context.

Equations

• rc.addressee = rc.base.addressee

def Core.Context.RichContext.position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : P

Position of the rich context.

Equations

• rc.position = rc.base.position

def Core.Context.RichContext.toSituation {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (rc : RichContext W E P T) : Situation W T

Project a RichContext to a Situation (world + time pair).

Equations

• rc.toSituation = rc.base.toSituation

def Core.Context.KContext.toRich {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) : RichContext W E P T

Lift a KContext to a RichContext with the trivial (universal) domain and default direct evidence. This is the root-clause default: no modal restriction, speaker has direct evidence.

Equations

• c.toRich = { base := c, domain := Set.univ, evidence := Core.Evidence.EvidentialSource.direct }

theorem Core.Context.KContext.toRich_domain {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) : c.toRich.domain = Set.univ

The trivial lift has universal domain.

theorem Core.Context.KContext.toRich_base {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : KContext W E P T) : c.toRich.base = c

The trivial lift preserves the base context.

def Core.Context.DomainExpanding {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (σ : ContextShift (RichContext W E P T)) : Prop

A context shift is domain-expanding if it can only enlarge the accessible-world set, never shrink it.

This captures @cite{condoravdi-2002}'s observation: backward temporal shifts expand the historical alternatives because more futures branch from earlier times.

Equations

• Core.Context.DomainExpanding σ = ∀ (rc : Core.Context.RichContext W E P T), rc.domain ⊆ (σ.apply rc).domain

def Core.Context.hpShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (expandedDomain : Set W) : ContextShift (RichContext W E P T)

Historical present (HP) temporal shift: moves time backward and expands the domain to include a superset of the original worlds.

The expandedDomain parameter makes the expansion explicit: the caller provides the larger domain, and the shift installs it. In the branching-time setting, this would be historicalBase at the earlier time.

Equations

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

theorem Core.Context.hpShift_expanding {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (expandedDomain : Set W) (h : ∀ (rc : RichContext W E P T), rc.domain ⊆ expandedDomain) : DomainExpanding (hpShift newTime expandedDomain)

The HP shift is domain-expanding when the provided domain is a superset of the original.

@[simp]

theorem Core.Context.hpShift_preserves_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (expandedDomain : Set W) (rc : RichContext W E P T) : ((hpShift newTime expandedDomain).apply rc).agent = rc.agent

HP shift preserves the agent.

@[simp]

theorem Core.Context.hpShift_changes_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newTime : T) (expandedDomain : Set W) (rc : RichContext W E P T) : ((hpShift newTime expandedDomain).apply rc).time = newTime

HP shift changes the time.

def Core.Context.xMarkingShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (pastTime : T) (cfWorld : W) (expandedDomain : Set W) : ContextShift (RichContext W E P T)

X-marking shift: the morphological "fake past" on counterfactual conditionals, reanalyzed as a domain-expanding shift.

Iatridou's insight: subjunctive/past morphology on conditionals doesn't locate the event in the past — it signals exclusion from the actual world. Under branching time, this exclusion IS domain expansion: the X-marked conditional quantifies over a wider set of historical alternatives than the indicative, because the past morphology shifts the evaluation time backward, expanding the branch set.

xMarkingShift combines backward time shift with domain expansion, unifying Iatridou's morphological observation with Condoravdi's semantic mechanism. The hpShift handles the same operation for the historical present; xMarkingShift adds world shift (to a counterfactual world) and labels as .mood rather than .temporal.

Equations

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

theorem Core.Context.xMarkingShift_expanding {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (pastTime : T) (cfWorld : W) (expandedDomain : Set W) (h : ∀ (rc : RichContext W E P T), rc.domain ⊆ expandedDomain) : DomainExpanding (xMarkingShift pastTime cfWorld expandedDomain)

X-marking is domain-expanding when the provided domain is a superset.

@[simp]

theorem Core.Context.xMarkingShift_changes_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (pastTime : T) (cfWorld : W) (expandedDomain : Set W) (rc : RichContext W E P T) : ((xMarkingShift pastTime cfWorld expandedDomain).apply rc).time = pastTime

@[simp]

theorem Core.Context.xMarkingShift_changes_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (pastTime : T) (cfWorld : W) (expandedDomain : Set W) (rc : RichContext W E P T) : ((xMarkingShift pastTime cfWorld expandedDomain).apply rc).world = cfWorld

@[simp]

theorem Core.Context.xMarkingShift_preserves_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (pastTime : T) (cfWorld : W) (expandedDomain : Set W) (rc : RichContext W E P T) : ((xMarkingShift pastTime cfWorld expandedDomain).apply rc).agent = rc.agent

def Core.Context.evidentialSourceShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (newSource : Evidence.EvidentialSource) : ContextShift (RichContext W E P T)

Shift the evidential source. Used when an embedding operator changes the evidence type (e.g., hearsay report changes direct → hearsay).

Equations

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

theorem Core.Context.evidentialSourceShift_preserves_domain {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (src : Evidence.EvidentialSource) (rc : RichContext W E P T) : ((evidentialSourceShift src).apply rc).domain = rc.domain

Evidential source shift preserves the domain.