Declerck's Tense Theory

@cite{declerck-1991} @cite{declerck-2006} @cite{reichenbach-1947}

Declerck's descriptive theory of English tense differs from @cite{reichenbach-1947} in three structural ways:

1. TO-chain architecture: Tenses express chains of binary temporal relations between adjacent Times of Orientation (TOs), not configurations of points on a single time line. A tense schema relates TS to TO_sit, TO_sit to TO₂, TO₂ to TO₁, etc. — but does NOT assert relations between non-adjacent elements. This makes the conditional tense vague (not three-ways ambiguous) about the relation between TO_sit and t₀.

2. TO/TE decomposition: Reichenbach's overloaded "R" is split into TO (Time of Orientation: the time a situation is related from) and TE (Time Established: what adverbials/context contribute). These are independent: a TO may lack a TE (narrative in medias res); a TE may not serve as a TO ("yesterday" in "John was here yesterday" frames TO_sit but doesn't orient anything).

3. Two time-spheres: The past/present time-sphere distinction is a first-class conceptual partition, not derivable from temporal relations. Both "I visited Paris" (preterit) and "I have visited Paris" (perfect) can refer to the same objective event; they differ in time-sphere membership (past vs. present).

The Eight Tense Schemata

Each English tense realizes a chain of relations from TS inward to TO₁:

Tense	Schema	Sphere
Preterit	TS simul TO_sit, TO_sit before TO₁	past
Present	TS simul TO_sit, TO_sit includes t₀	present
Present Perfect	TS simul TO_sit, TO_sit before/upto TO₁	present
Past Perfect	TS simul TO_sit, TO_sit before TO₂, TO₂ before TO₁	past
Future	TS simul TO_sit, TO_sit after TO₁	present
Future Perfect	TS simul TO_sit, TO_sit before TO₂, TO₂ after TO₁	present
Conditional	TS simul TO_sit, TO_sit after TO₂, TO₂ before TO₁	past
Conditional Perfect	TS simul TO_sit, TO_sit before TO₃, TO₃ after TO₂, TO₂ before TO₁	past

Design

We represent each schema as a DeclercianSchema — a chain of named TO links with an explicit time-sphere tag. The toFrame projection collapses a resolved schema into a ReichenbachFrame, with bridge theorems proving the correspondence.

The chain structure deliberately does NOT place all TOs on a single time line. Non-adjacent TOs have no asserted relation, which is how Declerck captures temporal vagueness (the future-perfect / conditional cases where TO_sit's relation to t₀ is genuinely underspecified).

The E = R invariant

Declerck's universal principle is TS = TO_sit (every tense represents its situation time as coinciding with some orientation time, never as standing in a non-trivial Allen relation to it). Since we map both R and E to TO_sit in the Reichenbach projection, every Declercian frame has E = R. This means isPerfect (E < R) can never hold for a Declercian projection — the "perfect" lives in the chain structure (TO_sit before TO₂), not in the Reichenbach E/R relation.

inductive Semantics.Tense.TOChain.TimeSphere : Type

The two time-spheres of English (@cite{declerck-1991}, @cite{declerck-2006}).

The tense system partitions linguistic time into two spheres:

• past: wholly before t₀, containing the preterit, past perfect, conditional, and conditional perfect
• present: includes t₀, containing the present, present perfect, future, and future perfect

This is a conceptual partition, not a temporal relation: both "I visited Paris" and "I have visited Paris" can refer to the same objective event, but differ in time-sphere membership.

• past : TimeSphere
• present : TimeSphere

@[implicit_reducible]

instance Semantics.Tense.TOChain.instDecidableEqTimeSphere : DecidableEq TimeSphere

Equations

• Semantics.Tense.TOChain.instDecidableEqTimeSphere x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Tense.TOChain.instReprTimeSphere : Repr TimeSphere

Equations

• Semantics.Tense.TOChain.instReprTimeSphere = { reprPrec := Semantics.Tense.TOChain.instReprTimeSphere.repr }

def Semantics.Tense.TOChain.instReprTimeSphere.repr : TimeSphere → ℕ → Std.Format

Equations

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

structure Semantics.Tense.TOChain.TOLink (Time : Type u_1) : Type u_1

A single link in a TO chain: a Core.Time.Orientation-labelled Time of Orientation related to the next TO inward by a temporal relation.

Example: in the past perfect schema TS simul TO_sit before TO₂ before TO₁, the link for TO₂ is ⟨.sub 0, .before, t₂⟩ — meaning TO₂ (= .sub 0, one step out from the binding TO₁ = .perspective) stands in the before relation to the next TO outward. The .situation role labels TO_sit.

• name : Core.Time.Orientation

  The orientation-time role of this link (.situation for TO_sit; .sub n for an intermediate TO).

• relation : Core.Time.Relation

  How this TO relates to the next TO inward toward TO₁. before = this TO precedes the next; after = this TO follows it; overlapping = simultaneous.

• time : Time

  The resolved time value.

structure Semantics.Tense.TOChain.DeclercianSchema (Time : Type u_1) : Type u_1

Declerck's tense schema: a chain of TOs from TO₁ outward to TO_sit, with a time-sphere classification.

The chain runs from TO₁ (innermost, adjacent to t₀) outward through intermediate TOs to TO_sit. The situation time TS is always simultaneous with TO_sit (Declerck's universal principle: every tense represents TS as coinciding with some TO), so there is no separate ts field — both E and R in the Reichenbach projection are derived from TO_sit.

The chain captures only adjacent relations. Non-adjacent TOs (e.g., TO_sit and TO₁ in the conditional tense) have no asserted relation — this is Declerck's account of temporal vagueness.

• t0 : Time

  Temporal zero-point (usually = speech time)

• to1 : Time

  Basic TO (TO₁): the starting point for temporal relations. Usually = t₀, but can be a future or past time in embedded contexts.

• chain : List (TOLink Time)

  Chain of TOs from TO₁ outward. Each link's relation connects it to the previous link (or to TO₁ for the first link). The last element is TO_sit, which TS is simultaneous with.

• timeSphere : TimeSphere

  Which time-sphere the tense belongs to

def Semantics.Tense.TOChain.DeclercianSchema.toSit {Time : Type u_1} (s : DeclercianSchema Time) : Time

The situation-TO (= TS): the TO with which the situation time coincides. This is the last element of the chain, or TO₁ if the chain is empty.

Equations

• s.toSit = match s.chain.getLast? with | some link => link.time | none => s.to1

def Semantics.Tense.TOChain.DeclercianSchema.depth {Time : Type u_1} (s : DeclercianSchema Time) : ℕ

Number of TOs in the schema (including TO₁).

Equations

• s.depth = s.chain.length + 1

def Semantics.Tense.TOChain.DeclercianSchema.toFrame {Time : Type u_1} (s : DeclercianSchema Time) : Core.Time.Reichenbach.ReichenbachFrame Time

Project a Declercian schema to a Reichenbach frame.

The mapping:

• S = t₀
• P = TO₁ (basic TO = perspective time)
• R = TO_sit (situation-TO)
• E = TO_sit (= TS, by Declerck's universal principle TS = TO_sit)

Since R = E = TO_sit, every Declercian frame has isPerfective (E = R) and can never satisfy isPerfect (E < R). The "perfect" in Declerck's system is a chain property (TO_sit before TO₂), not an E/R relation.

This is a lossy projection: the chain structure (intermediate TOs, temporal vagueness) is collapsed.

Equations

• s.toFrame = { speechTime := s.t0, perspectiveTime := s.to1, referenceTime := s.toSit, eventTime := s.toSit }

theorem Semantics.Tense.TOChain.DeclercianSchema.eventTime_eq_refTime {Time : Type u_1} (s : DeclercianSchema Time) : s.toFrame.eventTime = s.toFrame.referenceTime

Every Declercian frame has E = R (Declerck's TS = TO_sit principle).

Each schema is parameterized by concrete times so that bridge theorems can verify the structural relations.

def Semantics.Tense.TOChain.preterit {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Preterit: TS simul TO_sit, TO_sit before TO₁. Past time-sphere. Two TOs in the chain.

Example: "John was ill yesterday."

• TO₁ = t₀ (absolute use)
• TO_sit before TO₁ (past time-sphere)
• TS = TO_sit

Equations

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

def Semantics.Tense.TOChain.present {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Present tense: TS simul TO_sit, TO_sit includes t₀. Present time-sphere. Two TOs in the chain.

Declerck's key insight: the present tense does NOT assert TO_sit = t₀ but rather TO_sit includes t₀. For point times this degenerates to equality (captured by .overlapping), but for intervals "John is in London today" has TO_sit = today, which properly includes t₀. The interval-level inclusion is handled by Interval.subinterval.

Example: "John is in London."

• TO_sit includes t₀ (= overlapping for point times)
• TS = TO_sit

Equations

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

def Semantics.Tense.TOChain.presentPerfect {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Present perfect: TS simul TO_sit, TO_sit before TO₁. Present time-sphere (the crucial difference from the preterit).

Declerck's distinctive claim: the present perfect and preterit differ in time-sphere membership, not in definiteness or current relevance. Both can refer to the same event; the perfect places it in the pre-present sector of the present time-sphere.

Example: "I have visited Paris."

• TO₁ = t₀
• TO_sit before TO₁ (pre-present sector)
• TS = TO_sit
• Present time-sphere (vs. past for the preterit)

Equations

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

def Semantics.Tense.TOChain.pastPerfect {Time : Type u_1} (t0 to2 toSit : Time) : DeclercianSchema Time

Past perfect: TS simul TO_sit, TO_sit before TO₂, TO₂ before TO₁. Past time-sphere. Three TOs in the chain.

The past perfect is either "the past of the preterit" or "the past of the present perfect." In both cases TO₂ lies in the past time-sphere relative to TO₁, and TO_sit is anterior to TO₂.

Example: "John had left before we arrived."

• TO₁ = t₀
• TO₂ before TO₁ (past time-sphere)
• TO_sit before TO₂ (anterior to the past reference)
• TS = TO_sit

Equations

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

def Semantics.Tense.TOChain.future {Time : Type u_1} (t0 toSit : Time) : DeclercianSchema Time

Future tense: TS simul TO_sit, TO_sit after TO₁. Present time-sphere. Two TOs in the chain.

The future locates TO_sit either wholly after t₀ or from t₀ onwards. For point times, after suffices.

Example: "I will do it next week."

• TO₁ = t₀
• TO_sit after TO₁ (post-present sector)
• TS = TO_sit

Equations

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

def Semantics.Tense.TOChain.futurePerfect {Time : Type u_1} (t0 to2 toSit : Time) : DeclercianSchema Time

Future perfect: TS simul TO_sit, TO_sit before TO₂, TO₂ after TO₁. Present time-sphere. Three TOs in the chain.

The future perfect is vague about the relation between TO_sit and TO₁: John may have already left, may be leaving now, or may leave later. The chain captures this by NOT asserting a TO_sit–TO₁ relation.

Example: "John will have left when we arrive."

• TO₁ = t₀
• TO₂ after TO₁ (future reference point)
• TO_sit before TO₂ (anterior to the future reference)
• TS = TO_sit

Equations

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

def Semantics.Tense.TOChain.conditional {Time : Type u_1} (t0 to2 toSit : Time) : DeclercianSchema Time

Conditional tense: TS simul TO_sit, TO_sit after TO₂, TO₂ before TO₁. Past time-sphere (for TO₂). Three TOs in the chain.

The conditional is the mirror image of the future perfect: "future in the past." Like the future perfect, it is vague about TO_sit's relation to TO₁ — the situation may or may not have occurred by speech time.

Example: "The house would weather many more storms."

• TO₁ = t₀
• TO₂ before TO₁ (past time-sphere)
• TO_sit after TO₂ (posterior within the past domain)
• TS = TO_sit

Equations

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

def Semantics.Tense.TOChain.conditionalPerfect {Time : Type u_1} (t0 to2 to3 toSit : Time) : DeclercianSchema Time

Conditional perfect: TS simul TO_sit, TO_sit before TO₃, TO₃ after TO₂, TO₂ before TO₁. Past time-sphere. Four TOs in the chain.

The most intricate English tense: "past in the future in the past."

Example: "He would have left by then."

• TO₁ = t₀
• TO₂ before TO₁ (past time-sphere)
• TO₃ after TO₂ (future within the past domain)
• TO_sit before TO₃ (anterior to the future-in-past reference)
• TS = TO_sit

Equations

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

theorem Semantics.Tense.TOChain.preterit_depth {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).depth = 2

Simple tenses have depth 2 (TO₁ + TO_sit).

theorem Semantics.Tense.TOChain.present_depth {Time : Type u_1} (t0 toSit : Time) : (present t0 toSit).depth = 2

theorem Semantics.Tense.TOChain.presentPerfect_depth {Time : Type u_1} (t0 toSit : Time) : (presentPerfect t0 toSit).depth = 2

theorem Semantics.Tense.TOChain.future_depth {Time : Type u_1} (t0 toSit : Time) : (future t0 toSit).depth = 2

theorem Semantics.Tense.TOChain.pastPerfect_depth {Time : Type u_1} (t0 to2 toSit : Time) : (pastPerfect t0 to2 toSit).depth = 3

Compound tenses have depth 3 (TO₁ + TO₂ + TO_sit).

theorem Semantics.Tense.TOChain.futurePerfect_depth {Time : Type u_1} (t0 to2 toSit : Time) : (futurePerfect t0 to2 toSit).depth = 3

theorem Semantics.Tense.TOChain.conditional_depth {Time : Type u_1} (t0 to2 toSit : Time) : (conditional t0 to2 toSit).depth = 3

theorem Semantics.Tense.TOChain.conditionalPerfect_depth {Time : Type u_1} (t0 to2 to3 toSit : Time) : (conditionalPerfect t0 to2 to3 toSit).depth = 4

The conditional perfect has depth 4 (TO₁ + TO₂ + TO₃ + TO_sit).

theorem Semantics.Tense.TOChain.present_sphere {Time : Type u_1} (t0 toSit : Time) : (present t0 toSit).timeSphere = TimeSphere.present

Present time-sphere tenses: present, present perfect, future, future perfect.

theorem Semantics.Tense.TOChain.presentPerfect_sphere {Time : Type u_1} (t0 toSit : Time) : (presentPerfect t0 toSit).timeSphere = TimeSphere.present

theorem Semantics.Tense.TOChain.future_sphere {Time : Type u_1} (t0 toSit : Time) : (future t0 toSit).timeSphere = TimeSphere.present

theorem Semantics.Tense.TOChain.futurePerfect_sphere {Time : Type u_1} (t0 to2 toSit : Time) : (futurePerfect t0 to2 toSit).timeSphere = TimeSphere.present

theorem Semantics.Tense.TOChain.preterit_sphere {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).timeSphere = TimeSphere.past

Past time-sphere tenses: preterit, past perfect, conditional, conditional perfect.

theorem Semantics.Tense.TOChain.pastPerfect_sphere {Time : Type u_1} (t0 to2 toSit : Time) : (pastPerfect t0 to2 toSit).timeSphere = TimeSphere.past

theorem Semantics.Tense.TOChain.conditional_sphere {Time : Type u_1} (t0 to2 toSit : Time) : (conditional t0 to2 toSit).timeSphere = TimeSphere.past

theorem Semantics.Tense.TOChain.conditionalPerfect_sphere {Time : Type u_1} (t0 to2 to3 toSit : Time) : (conditionalPerfect t0 to2 to3 toSit).timeSphere = TimeSphere.past

Each bridge theorem shows that a Declercian schema, when resolved to concrete times satisfying the chain constraints, projects to a ReichenbachFrame satisfying the expected Reichenbach tense predicate.

This connects Declerck's chain architecture to the existing Reichenbach
infrastructure used by all other tense theories in linglib. 

theorem Semantics.Tense.TOChain.preterit_isPast (t0 toSit : ℤ) (h : toSit < t0) : (preterit t0 toSit).toFrame.isPast

Preterit projects to a frame satisfying PAST (R < P).

theorem Semantics.Tense.TOChain.present_isPresent (t0 : ℤ) : (present t0 t0).toFrame.isPresent

Present projects to a frame satisfying PRESENT (R = P) for point times.

theorem Semantics.Tense.TOChain.presentPerfect_frame_isPast (t0 toSit : ℤ) (h : toSit < t0) : (presentPerfect t0 toSit).toFrame.isPast

Present perfect projects to a frame satisfying PAST (R < P) — because TO_sit (= R) < TO₁ (= P). The present-sphere membership is tracked by timeSphere, not by the Reichenbach R/P relation.

This is Declerck's key structural claim: the perfect/preterit distinction is time-sphere, not R/P configuration. Both project to R < P.

theorem Semantics.Tense.TOChain.preterit_presentPerfect_same_frame (t0 toSit : ℤ) : (preterit t0 toSit).toFrame = (presentPerfect t0 toSit).toFrame

Preterit and present perfect produce identical Reichenbach frames for the same times — they differ ONLY in time-sphere. This is Declerck's central thesis about the perfect/preterit distinction: the contrast is sphere membership, not R/P configuration.

theorem Semantics.Tense.TOChain.preterit_presentPerfect_differ_sphere (t0 toSit : ℤ) : (preterit t0 toSit).timeSphere ≠ (presentPerfect t0 toSit).timeSphere

... but they differ in time-sphere.

theorem Semantics.Tense.TOChain.pastPerfect_isPast (t0 to2 toSit : ℤ) (h₁ : toSit < to2) (h₂ : to2 < t0) : (pastPerfect t0 to2 toSit).toFrame.isPast

Past perfect projects to PAST (R < P). The chain gives TO_sit < TO₂ < TO₁, so R (= TO_sit) < P (= TO₁).

theorem Semantics.Tense.TOChain.future_isFuture (t0 toSit : ℤ) (h : toSit > t0) : (future t0 toSit).toFrame.isFuture

Future projects to FUTURE (R > P).

theorem Semantics.Tense.TOChain.conditional_to2_before_to1 (t0 to2 toSit : ℤ) (h : to2 < t0) : to2 < (conditional t0 to2 toSit).to1

Conditional: TO₂ < TO₁ projects to PAST for the intermediate reference. The full frame has R (= TO_sit) related to P (= TO₁), but the relation is underspecified — TO_sit may be before, at, or after TO₁.

We can only prove that TO₂ < TO₁ (the chain constraint), which Reichenbach would misrepresent as three separate tense schemata.

Declerck's chain model captures temporal vagueness naturally: when a schema's chain doesn't include a direct link between two TOs, their relation is genuinely unspecified.

The future perfect and conditional tense are both vague about
the relation between TO_sit and TO₁. @cite{reichenbach-1947}
incorrectly treats this as three-way ambiguity (S–R–E, R–S–E,
R–E–S as distinct schemata for the conditional). 

theorem Semantics.Tense.TOChain.futurePerfect_vague_sit_t0 : ∃ (toSit₁ : ℤ) (toSit₂ : ℤ) (toSit₃ : ℤ), ∃ to2 > 0, toSit₁ < to2 ∧ toSit₂ < to2 ∧ toSit₃ < to2 ∧ toSit₁ < 0 ∧ toSit₂ = 0 ∧ toSit₃ > 0

The future perfect is vague about TO_sit's relation to t₀: the chain relates TO_sit to TO₂ and TO₂ to TO₁, but NOT TO_sit to TO₁. All three scenarios are consistent.

theorem Semantics.Tense.TOChain.conditional_vague_sit_t0 : ∃ (toSit₁ : ℤ) (toSit₂ : ℤ) (toSit₃ : ℤ), ∃ to2 < 0, toSit₁ > to2 ∧ toSit₂ > to2 ∧ toSit₃ > to2 ∧ toSit₁ < 0 ∧ toSit₂ = 0 ∧ toSit₃ > 0

The conditional tense is vague about TO_sit's relation to t₀: the chain relates TO_sit to TO₂ and TO₂ to TO₁, but NOT TO_sit to TO₁. All three scenarios are consistent.

@cite{reichenbach-1947}'s three separate schemata for the conditional (S–R–E, R–S–E, R–E–S) are NOT distinct tenses — they are instances of a single vague schema.

Concrete examples matching the Phenomena/Tense/Data.lean frames, showing the Declercian schemata produce the same data.

def Semantics.Tense.TOChain.exPreterit : DeclercianSchema ℤ

"John was ill yesterday" — preterit, absolute use.

Equations

• Semantics.Tense.TOChain.exPreterit = Semantics.Tense.TOChain.preterit 0 (-3)

def Semantics.Tense.TOChain.exPresent : DeclercianSchema ℤ

"It is raining" — present, point time.

Equations

• Semantics.Tense.TOChain.exPresent = Semantics.Tense.TOChain.present 0 0

def Semantics.Tense.TOChain.exPresentPerfect : DeclercianSchema ℤ

"I have visited Paris" — present perfect.

Equations

• Semantics.Tense.TOChain.exPresentPerfect = Semantics.Tense.TOChain.presentPerfect 0 (-3)

def Semantics.Tense.TOChain.exPreteritParis : DeclercianSchema ℤ

"I visited Paris" — preterit (same event, different sphere).

Equations

• Semantics.Tense.TOChain.exPreteritParis = Semantics.Tense.TOChain.preterit 0 (-3)

def Semantics.Tense.TOChain.exPastPerfect : DeclercianSchema ℤ

"John had left before we arrived" — past perfect.

Equations

• Semantics.Tense.TOChain.exPastPerfect = Semantics.Tense.TOChain.pastPerfect 0 (-2) (-4)

def Semantics.Tense.TOChain.exFuture : DeclercianSchema ℤ

"I will do it next week" — future.

Equations

• Semantics.Tense.TOChain.exFuture = Semantics.Tense.TOChain.future 0 5

def Semantics.Tense.TOChain.exFuturePerfect : DeclercianSchema ℤ

"John will have left when we arrive" — future perfect.

Equations

• Semantics.Tense.TOChain.exFuturePerfect = Semantics.Tense.TOChain.futurePerfect 0 5 3

def Semantics.Tense.TOChain.exConditional : DeclercianSchema ℤ

"The house would weather many more storms" — conditional.

Equations

• Semantics.Tense.TOChain.exConditional = Semantics.Tense.TOChain.conditional 0 (-5) (-3)

def Semantics.Tense.TOChain.exConditionalPerfect : DeclercianSchema ℤ

"He would have left by then" — conditional perfect.

Equations

• Semantics.Tense.TOChain.exConditionalPerfect = Semantics.Tense.TOChain.conditionalPerfect 0 (-5) (-3) (-4)

theorem Semantics.Tense.TOChain.exPreterit_isPast : exPreterit.toFrame.isPast

Concrete preterit satisfies PAST.

theorem Semantics.Tense.TOChain.exPresent_isPresent : exPresent.toFrame.isPresent

Concrete present satisfies PRESENT.

theorem Semantics.Tense.TOChain.exPerfect_eq_preterit_frame : exPresentPerfect.toFrame = exPreteritParis.toFrame

Present perfect and preterit project to identical Reichenbach frames.

theorem Semantics.Tense.TOChain.exPerfect_neq_preterit_sphere : exPresentPerfect.timeSphere ≠ exPreteritParis.timeSphere

But they have different time-spheres.

theorem Semantics.Tense.TOChain.exFuture_isFuture : exFuture.toFrame.isFuture

Concrete future satisfies FUTURE.

theorem Semantics.Tense.TOChain.exFuturePerfect_chain_valid : (futurePerfect 0 5 3).toSit < 5 ∧ 5 > 0

Concrete future perfect: TO_sit (3) < TO₂ (5), and TO₂ (5) > t₀ (0).

theorem Semantics.Tense.TOChain.exConditional_chain_valid : -5 < 0 ∧ exConditional.toSit > -5

Concrete conditional: TO₂ (-5) < t₀ (0), TO_sit (-3) > TO₂ (-5).

theorem Semantics.Tense.TOChain.exConditionalPerfect_chain_valid : -5 < 0 ∧ -3 > -5 ∧ exConditionalPerfect.toSit < -3

Conditional perfect: 4-deep chain is valid.

Declerck TO-Chain ↔ Context Tower

Each link in a TO-chain corresponds to a temporal shift in a context tower. The chain runs from TO₁ outward to TO_sit; each link introduces a new temporal perspective point, which is exactly what pushing a temporalShift does.

• TO₁ corresponds to the tower origin (the basic temporal reference point)
• Each subsequent TO in the chain maps to a tower push with temporalShift
• DeclercianSchema.depth = chain.length + 1 corresponds to tower depth + 1 (the tower counts shifts, while Declerck counts TOs including TO₁)

The mapping is tower.depth = schema.chain.length, and schema.depth = tower.depth + 1 (because Declerck counts TO₁ as depth 1).

def Semantics.Tense.TOChain.declercianToShifts {Time : Type u_1} {E : Type u_2} {P : Type u_3} (chain : List (TOLink Time)) : List (Core.Context.ContextShift (Core.Context.KContext Time E P Time))

Convert a Declercian TO-chain to a list of temporal shifts. Each TOLink becomes a temporalShift with .temporal label. The relation in the link is not encoded in the shift itself — it is a constraint on the times, not a transformation.

Equations

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

def Semantics.Tense.TOChain.declercianToTower {Time : Type u_1} {E : Type u_2} {P : Type u_3} (s : DeclercianSchema Time) (agent addressee : E) (world : Time) (pos : P) : Core.Context.ContextTower (Core.Context.KContext Time E P Time)

Convert a Declercian schema to a context tower. The origin context has time := to1 (the basic TO). Each chain link becomes a temporal shift.

Equations

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

theorem Semantics.Tense.TOChain.declercianToTower_depth {Time : Type u_1} {E : Type u_2} {P : Type u_3} (s : DeclercianSchema Time) (agent addr : E) (world : Time) (pos : P) : (declercianToTower s agent addr world pos).depth = s.chain.length

The tower depth equals the chain length.

theorem Semantics.Tense.TOChain.declerck_depth_is_tower_depth_plus_one {Time : Type u_1} {E : Type u_2} {P : Type u_3} (s : DeclercianSchema Time) (agent addr : E) (world : Time) (pos : P) : s.depth = (declercianToTower s agent addr world pos).depth + 1

Declerck's depth = tower depth + 1. The "+1" is because Declerck counts TO₁ as part of the depth (depth = number of TOs), while the tower counts only shifts (depth = number of pushes).

theorem Semantics.Tense.TOChain.preterit_tower_depth {Time : Type u_1} (t0 toSit : Time) {E : Type u_2} {P : Type u_3} (agent addr : E) (world : Time) (pos : P) : (declercianToTower (preterit t0 toSit) agent addr world pos).depth = 1

For simple tenses (chain length 1), the tower has depth 1.

theorem Semantics.Tense.TOChain.pastPerfect_tower_depth {Time : Type u_1} (t0 to2 toSit : Time) {E : Type u_2} {P : Type u_3} (agent addr : E) (world : Time) (pos : P) : (declercianToTower (pastPerfect t0 to2 toSit) agent addr world pos).depth = 2

For compound tenses (chain length 2), the tower has depth 2.

theorem Semantics.Tense.TOChain.conditionalPerfect_tower_depth {Time : Type u_1} (t0 to2 to3 toSit : Time) {E : Type u_2} {P : Type u_3} (agent addr : E) (world : Time) (pos : P) : (declercianToTower (conditionalPerfect t0 to2 to3 toSit) agent addr world pos).depth = 3

For the conditional perfect (chain length 3), the tower has depth 3.

Re-express DeclercianSchema via the framework-agnostic Core.Time.Domain substrate (central TO + list of sub-TOs, with Allen relations computed on demand from the underlying linear order). The toDomain builder lifts the chain structure into a Domain Time Orientation whose central TO is the utterance time (T₀) and whose sub-TOs are the perspective TO (TO₁) followed by every chain link as a point interval.

This is **additive**: the `DeclercianSchema` structure and all the
named-tense constructors stay unchanged. Domain-level tooling can
now work uniformly with
`s.toDomain.relatedByName precedesSet .situation .perspective`,
while existing Reichenbach-projecting code continues to use
`s.toFrame`. 

def Semantics.Tense.TOChain.DeclercianSchema.toDomain {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : Core.Time.Domain Time Core.Time.Orientation

The schema as a Core.Time.Domain over the universal Orientation role vocabulary: central = .utterance (T₀, the temporal zero-point), sub-TOs = .perspective (TO₁) followed by every chain link as a point interval.

The Allen relations between any pair of TOs are computed from the underlying LinearOrder Time via Interval.allenRel; nothing is stored. The chain's relation field encodes the intended Declercian temporal relation but is not consulted here — its job is to constrain admissible time assignments at the call site, not to reproduce information already implicit in the linear order.

Equations

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

@[simp]

theorem Semantics.Tense.TOChain.DeclercianSchema.toDomain_central {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : s.toDomain.central = Core.Time.NamedTO.ofPoint Core.Time.Orientation.utterance s.t0

@[simp]

theorem Semantics.Tense.TOChain.DeclercianSchema.toDomain_subTOs {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : s.toDomain.subTOs = Core.Time.NamedTO.ofPoint Core.Time.Orientation.perspective s.to1 :: List.map (fun (link : TOLink Time) => Core.Time.NamedTO.ofPoint link.name link.time) s.chain

theorem Semantics.Tense.TOChain.DeclercianSchema.toDomain_labels {Time : Type u_1} [LinearOrder Time] (s : DeclercianSchema Time) : s.toDomain.labels = Core.Time.Orientation.utterance :: Core.Time.Orientation.perspective :: List.map TOLink.name s.chain

The schema's domain labels: utterance first, then perspective, then every chain link's role. Useful for stating role-set invariants.

The Zone enum encodes Declerck's six principal temporal sectors — two time-spheres (past, present) crossed with three positions (anterior pre-, central, posterior post-). Each English tense locates its situation time in one of these zones. The DeclercianSchema.zoneOf classifier projects a schema to its zone based on (timeSphere, last chain-link relation) — the relation of TO_sit to its outer anchor, plus the sphere membership of that anchor.

For **simple tenses** (chain length 1, anchor = `TO₁` = `t₀`):
- `(past, before)` → `past` (preterit)
- `(present, before)` → `prePresent` (present perfect)
- `(present, overlapping)` → `present` (present)
- `(present, after)` → `postPresent` (future)

For **compound tenses** (chain length ≥ 2, anchor = `TO₂` etc.):
- `(past, before)` → `prePast` (past perfect, conditional perfect)
- `(past, after)` → `postPast` (conditional)
- `(present, before)` → `prePresent` (future perfect's TO_sit, anterior)
- `(present, after)` → `postPresent`

The classifier is **not** the inverse of the chain — vague tenses
(future perfect, conditional) under-determine `TO_sit`'s zone, and
the classifier returns the zone of the immediate anchor. The
`zone_of_*` `rfl`-theorems below verify each named tense classifies
to its expected zone. 

inductive Semantics.Tense.TOChain.Zone : Type

The six principal Declercian zones: two time-spheres crossed with three sphere-internal positions.

• prePast : Zone
• past : Zone
• postPast : Zone
• prePresent : Zone
• present : Zone
• postPresent : Zone

@[implicit_reducible]

instance Semantics.Tense.TOChain.instDecidableEqZone : DecidableEq Zone

Equations

• Semantics.Tense.TOChain.instDecidableEqZone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.TOChain.instReprZone.repr : Zone → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Tense.TOChain.instReprZone : Repr Zone

Equations

• Semantics.Tense.TOChain.instReprZone = { reprPrec := Semantics.Tense.TOChain.instReprZone.repr }

def Semantics.Tense.TOChain.DeclercianSchema.zoneOf {Time : Type u_1} (s : DeclercianSchema Time) : Zone

Classify a schema's TO_sit by zone, based on (timeSphere, last chain link's relation). See the section docstring for the mapping. Defaults to the sphere's center for empty chains and odd cases.

Equations

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

theorem Semantics.Tense.TOChain.preterit_zone {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).zoneOf = Zone.past

theorem Semantics.Tense.TOChain.present_zone {Time : Type u_1} (t0 toSit : Time) : (present t0 toSit).zoneOf = Zone.present

theorem Semantics.Tense.TOChain.presentPerfect_zone {Time : Type u_1} (t0 toSit : Time) : (presentPerfect t0 toSit).zoneOf = Zone.prePresent

theorem Semantics.Tense.TOChain.future_zone {Time : Type u_1} (t0 toSit : Time) : (future t0 toSit).zoneOf = Zone.postPresent

theorem Semantics.Tense.TOChain.pastPerfect_zone {Time : Type u_1} (t0 to2 toSit : Time) : (pastPerfect t0 to2 toSit).zoneOf = Zone.prePast

theorem Semantics.Tense.TOChain.conditional_zone {Time : Type u_1} (t0 to2 toSit : Time) : (conditional t0 to2 toSit).zoneOf = Zone.postPast

theorem Semantics.Tense.TOChain.futurePerfect_zone {Time : Type u_1} (t0 to2 toSit : Time) : (futurePerfect t0 to2 toSit).zoneOf = Zone.prePresent

theorem Semantics.Tense.TOChain.conditionalPerfect_zone {Time : Type u_1} (t0 to2 to3 toSit : Time) : (conditionalPerfect t0 to2 to3 toSit).zoneOf = Zone.prePast

theorem Semantics.Tense.TOChain.preterit_presentPerfect_differ_zone {Time : Type u_1} (t0 toSit : Time) : (preterit t0 toSit).zoneOf ≠ (presentPerfect t0 toSit).zoneOf

Preterit and present perfect classify to different zones (past vs prePresent) despite projecting to identical Reichenbach frames (preterit_presentPerfect_same_frame). This is exactly Declerck's central claim about the perfect/preterit distinction: the difference lives in the time-sphere/zone, not in the underlying R/P configuration. The Zone classifier surfaces what toFrame flattens.

Declerck's DeclercianSchema as a Core.Time.TenseSystem (anchor = .perspective for TO₁, situation = .situation for TO_sit) and Core.Time.AspectSystem instance. The aspect instance collapses event and reference roles both to .situation — Declerck's universal TS = TO_sit principle means E = R always holds, so any predicate of the form "event equals reference" is trivially satisfied for every Declercian schema, and "event precedes reference" can never hold. The "perfect" lives in the chain structure (TO_sit before .sub 0), not in the E/R relation — exactly Declerck's claim.

@[implicit_reducible]

instance Semantics.Tense.TOChain.declercianSchema_tenseSystem {Time : Type u_1} [LinearOrder Time] : Core.Time.TenseSystem (DeclercianSchema Time) Time Core.Time.Orientation

Equations

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

@[implicit_reducible]

instance Semantics.Tense.TOChain.declercianSchema_aspectSystem {Time : Type u_1} [LinearOrder Time] : Core.Time.AspectSystem (DeclercianSchema Time) Time Core.Time.Orientation

Equations

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