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 (ch. 6 §1.5, ch. 7 §6–7).

The E = R invariant

Declerck's universal principle is TS = TO_sit (ch. 6 §1.4). 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} ch. 2 §3).

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

instance Semantics.Tense.TOChain.instDecidableEqTimeSphere : DecidableEq TimeSphere

Equations

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

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.

instance Semantics.Tense.TOChain.instBEqTimeSphere : BEq TimeSphere

Equations

• Semantics.Tense.TOChain.instBEqTimeSphere = { beq := Semantics.Tense.TOChain.instBEqTimeSphere.beq }

def Semantics.Tense.TOChain.instBEqTimeSphere.beq : TimeSphere → TimeSphere → Bool

Equations

• Semantics.Tense.TOChain.instBEqTimeSphere.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

A single link in a TO chain: a named 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 ⟨"TO₂",.before, t₂⟩ — meaning TO₂ stands in the before relation to the next TO outward (TO₁).

• name : String

  Identifier (e.g., "TO_sit", "TO₂", "TO₃")

• relation : Core.Time.TemporalRelation

  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 ch. 6 §1.4: 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.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 (ch. 7 §1): 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 (ch. 7 §2): 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 (ch. 7 §3): 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 (ch. 7 §4): 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 (ch. 7 §5): 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 (ch. 7 §6): 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 (ch. 7 §7): 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 (ch. 7 §8): 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 (ch. 7 §1,3).

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₁. Reichenbach incorrectly
treats this as three-way ambiguity (ch. 5 §1.2). 

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.