Tense Theory Infrastructure: Shared Types

@cite{abusch-1997} @cite{deal-2020} @cite{heim-kratzer-1998} @cite{klecha-2016} @cite{kratzer-1998} @cite{ogihara-1996} @cite{sharvit-2003} @cite{von-stechow-2009} @cite{wurmbrand-2014} @cite{zeijlstra-2012} @cite{banfield-1982} @cite{comrie-1985} @cite{egressy-2026} @cite{ogihara-sharvit-2012} @cite{schlenker-2003}

Shared types and infrastructure for the tense theories formalized in Semantics.Intensional/Tense/ and Minimalism/Tense/.

Design Principle

Verdicts are derived from compositional semantics, not stipulated. Each theory file proves derivation theorems for the phenomena it handles; the comparison matrix (Comparisons/TenseTheories.lean) is assembled from what's been proven. There is no TheoryVerdict enum — whether a theory "handles" a phenomenon is witnessed by the existence (or absence) of a derivation theorem in that theory's file.

Key Types

• TensePhenomenon: the 23 temporal phenomena that distinguish theories
• TenseTheory: identity card for a theory (no verdict field)
• AttitudeTemporalSemantics: how an attitude verb shifts eval time

inductive Semantics.Tense.TensePhenomenon : Type

The 24 temporal phenomena that distinguish tense theories.

Each phenomenon represents an empirical domain where theories make different predictions or use different mechanisms. The comparison matrix is built from which derivation theorems each theory proves for each phenomenon.

The first 11 are the core comparison set. The next 7 are eventual targets documented with data frames. The final 6 are added for @cite{zeijlstra-2012}, @cite{wurmbrand-2014}, @cite{sharvit-2003}, and @cite{tsilia-zhao-2026} coverage.

• pastUnderPast_shifted : TensePhenomenon

  "John said Mary was sick" — shifted reading (sick before saying)

• pastUnderPast_simultaneous : TensePhenomenon

  "John said Mary was sick" — simultaneous reading (sick at saying)

• presentUnderPast_doubleAccess : TensePhenomenon

  "John said Mary is sick" — double-access reading

• futureUnderPast : TensePhenomenon

  "John said Mary would leave" — embedded future

• sotVsNonSOT : TensePhenomenon

  English (SOT) vs Japanese (non-SOT) parametric variation

• upperLimitConstraint : TensePhenomenon

  Abusch's upper limit constraint: no forward-shifted readings

• relativeClauseTense : TensePhenomenon

  "the man who was tall" — relative clause tense interpretation

• modalTenseInteraction : TensePhenomenon

  "John might have left" — modal scoping over past

• counterfactualTense : TensePhenomenon

  "If John were here..." — past morphology, non-temporal

• temporalDeRe : TensePhenomenon

  "John believed it was raining" — de re temporal reference

• deletionVsAmbiguity : TensePhenomenon

  Kratzer (deletion) vs Ogihara (zero tense ambiguity) debate

• sotInIndirectQuestions : TensePhenomenon

  "John asked who was sick" — SOT in indirect questions

• freeIndirectDiscourse : TensePhenomenon

  "She walked to the window. The garden was beautiful." — FID perspective shift without attitude verb

• historicalPresent : TensePhenomenon

  "Napoleon enters the room. He sees..." — present tense, past reference

• perfectTenseInteraction : TensePhenomenon

  "John said Mary had been sick" — pluperfect disambiguates to shifted only

• futureOrientedComplements : TensePhenomenon

  "John wanted/planned to leave" — future-oriented complements without standard SOT

• adjunctClauseTense : TensePhenomenon

  "Before John left, Mary was happy" — tense in temporal adjuncts

• indexicalTenseShift : TensePhenomenon

  Amharic/Zazaki: tense shifts under attitudes paralleling pronoun shift

• embeddedPresentPuzzle : TensePhenomenon

  "John will say Mary is sick" — present under future, simultaneous with future saying time

• lifetimeEffects : TensePhenomenon

  "Aristotle was a philosopher" — past tense ↔ subject no longer exists implication (@cite{musan-1995}/1997)

• fakePast : TensePhenomenon

  "If John were taller..." — past morphology, non-past semantics (@cite{iatridou-2000}, beyond Deal's counterfactual tense)

• optionalSOT : TensePhenomenon

  Hebrew-type optional SOT: "John said Mary {was/is} sick" — both possible with different readings

• dependentVsIndependentTense : TensePhenomenon

  @cite{wurmbrand-2014}: three-way classification of infinitival tense (future irrealis / propositional / restructuring)

• thenPresentIncompatibility : TensePhenomenon

  Temporal "then" is incompatible with shifted present but compatible with deleted tense — derived from tense presuppositions anchored to π

• sizeSensitiveSOT : TensePhenomenon

  Hungarian-type size-sensitive SOT: simultaneous reading available in TP complements but blocked in CP complements. Clause size determines whether [uPAST] can Agree upward across the complement boundary

@[implicit_reducible]

instance Semantics.Tense.instDecidableEqTensePhenomenon : DecidableEq TensePhenomenon

Equations

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

@[implicit_reducible]

instance Semantics.Tense.instReprTensePhenomenon : Repr TensePhenomenon

Equations

• Semantics.Tense.instReprTensePhenomenon = { reprPrec := Semantics.Tense.instReprTensePhenomenon.repr }

def Semantics.Tense.instReprTensePhenomenon.repr : TensePhenomenon → ℕ → Std.Format

Equations

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

def Semantics.Tense.instInhabitedTensePhenomenon.default : TensePhenomenon

Equations

• Semantics.Tense.instInhabitedTensePhenomenon.default = Semantics.Tense.TensePhenomenon.pastUnderPast_shifted

@[implicit_reducible]

instance Semantics.Tense.instInhabitedTensePhenomenon : Inhabited TensePhenomenon

Equations

• Semantics.Tense.instInhabitedTensePhenomenon = { default := Semantics.Tense.instInhabitedTensePhenomenon.default }

structure Semantics.Tense.TenseTheory : Type

A tense theory's identity card.

This records the structural properties of each account — what mechanisms it posits — without encoding verdicts. Whether the theory handles a given phenomenon is determined by the existence of derivation theorems in the theory's file.

Fields are Bool because they describe categorical properties of the formal system, not graded judgments.

• name : String

  Theory name (e.g., "@cite{abusch-1997}")

• citation : String

  Full citation

• hasTemporalDeRe : Bool

  Does the theory have a temporal de re mechanism?

• hasULC : Bool

  Does the theory impose an upper limit constraint?

• hasZeroTense : Bool

  Does the theory posit a zero tense (ambiguous past)?

• hasSOTDeletion : Bool

  Does the theory use SOT deletion for the simultaneous reading?

• hasAgreeBasedSOT : Bool

  Does the theory use syntactic Agree for SOT?

• hasPresuppositionalTense : Bool

  Does the theory treat tenses as presupposition triggers?

• hasSizeSensitiveSOT : Bool

  Does the theory predict size-sensitive SOT?

• simultaneousMechanism : String

  How the theory derives the simultaneous reading

def Semantics.Tense.instReprTenseTheory.repr : TenseTheory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Tense.instReprTenseTheory : Repr TenseTheory

Equations

• Semantics.Tense.instReprTenseTheory = { reprPrec := Semantics.Tense.instReprTenseTheory.repr }

structure Semantics.Tense.AttitudeTemporalSemantics (Time : Type u_1) : Type u_1

How an attitude verb shifts the evaluation time for its complement.

All six theories agree that attitude verbs modify the temporal evaluation context of their complement. They differ in the formal mechanism (eval time shift, feature checking, deletion, binding). This structure captures the shared interface.

• shiftEvalTime : Core.Time.Reichenbach.ReichenbachFrame Time → Time

  Given a matrix Reichenbach frame, compute the eval time for the embedded clause. Typically = matrix event time.

• embeddedConstraint : Time → Time → Prop

  The temporal constraint imposed on the embedded clause: embeddedRefTime must stand in this relation to the shifted eval time.

def Semantics.Tense.standardShift {Time : Type u_1} : AttitudeTemporalSemantics Time

Standard eval time shift: embedded eval time = matrix event time. This is the default across all six theories.

Equations

• Semantics.Tense.standardShift = { shiftEvalTime := fun (f : Core.Time.Reichenbach.ReichenbachFrame Time) => f.eventTime, embeddedConstraint := fun (_embR _evalT : Time) => True }

theorem Semantics.Tense.standardShift_is_eventTime {Time : Type u_1} (f : Core.Time.Reichenbach.ReichenbachFrame Time) : standardShift.shiftEvalTime f = f.eventTime

Standard shift gives matrix event time.

def Semantics.Tense.TensePhenomenon.IsCoreSOT : TensePhenomenon → Prop

A phenomenon is a core SOT phenomenon if all theories handle it.

Equations

• Semantics.Tense.TensePhenomenon.pastUnderPast_shifted.IsCoreSOT = True
• Semantics.Tense.TensePhenomenon.pastUnderPast_simultaneous.IsCoreSOT = True
• Semantics.Tense.TensePhenomenon.presentUnderPast_doubleAccess.IsCoreSOT = True
• Semantics.Tense.TensePhenomenon.sotVsNonSOT.IsCoreSOT = True
• x✝.IsCoreSOT = False

@[implicit_reducible]

instance Semantics.Tense.instDecidablePredTensePhenomenonIsCoreSOT : DecidablePred TensePhenomenon.IsCoreSOT

Equations

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

def Semantics.Tense.TensePhenomenon.IsDistinguishing : TensePhenomenon → Prop

A phenomenon is a distinguishing phenomenon if theories diverge on it.

Equations

• Semantics.Tense.TensePhenomenon.relativeClauseTense.IsDistinguishing = True
• Semantics.Tense.TensePhenomenon.modalTenseInteraction.IsDistinguishing = True
• Semantics.Tense.TensePhenomenon.counterfactualTense.IsDistinguishing = True
• Semantics.Tense.TensePhenomenon.temporalDeRe.IsDistinguishing = True
• Semantics.Tense.TensePhenomenon.deletionVsAmbiguity.IsDistinguishing = True
• x✝.IsDistinguishing = False

@[implicit_reducible]

instance Semantics.Tense.instDecidablePredTensePhenomenonIsDistinguishing : DecidablePred TensePhenomenon.IsDistinguishing

Equations

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

def Semantics.Tense.TensePhenomenon.IsEventualTarget : TensePhenomenon → Prop

A phenomenon is an eventual target — documented with data but not yet connected to derivation theorems in the theory files.

Equations

• Semantics.Tense.TensePhenomenon.sotInIndirectQuestions.IsEventualTarget = True
• Semantics.Tense.TensePhenomenon.freeIndirectDiscourse.IsEventualTarget = True
• Semantics.Tense.TensePhenomenon.historicalPresent.IsEventualTarget = True
• Semantics.Tense.TensePhenomenon.perfectTenseInteraction.IsEventualTarget = True
• Semantics.Tense.TensePhenomenon.futureOrientedComplements.IsEventualTarget = True
• Semantics.Tense.TensePhenomenon.adjunctClauseTense.IsEventualTarget = True
• Semantics.Tense.TensePhenomenon.indexicalTenseShift.IsEventualTarget = True
• x✝.IsEventualTarget = False

@[implicit_reducible]

instance Semantics.Tense.instDecidablePredTensePhenomenonIsEventualTarget : DecidablePred TensePhenomenon.IsEventualTarget

Equations

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

def Semantics.Tense.TensePhenomenon.IsExtended : TensePhenomenon → Prop

A phenomenon is in the extended set added for Zeijlstra/Wurmbrand/Sharvit.

Equations

• Semantics.Tense.TensePhenomenon.embeddedPresentPuzzle.IsExtended = True
• Semantics.Tense.TensePhenomenon.lifetimeEffects.IsExtended = True
• Semantics.Tense.TensePhenomenon.fakePast.IsExtended = True
• Semantics.Tense.TensePhenomenon.optionalSOT.IsExtended = True
• Semantics.Tense.TensePhenomenon.dependentVsIndependentTense.IsExtended = True
• Semantics.Tense.TensePhenomenon.thenPresentIncompatibility.IsExtended = True
• Semantics.Tense.TensePhenomenon.sizeSensitiveSOT.IsExtended = True
• x✝.IsExtended = False

@[implicit_reducible]

instance Semantics.Tense.instDecidablePredTensePhenomenonIsExtended : DecidablePred TensePhenomenon.IsExtended

Equations

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

theorem Semantics.Tense.phenomenon_coverage (p : TensePhenomenon) : p.IsCoreSOT ∨ p.IsDistinguishing ∨ p.IsEventualTarget ∨ p.IsExtended ∨ p = TensePhenomenon.futureUnderPast ∨ p = TensePhenomenon.upperLimitConstraint

Every phenomenon falls into exactly one of the five categories.

def Semantics.Tense.embeddedFrame {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) : Core.Time.Reichenbach.ReichenbachFrame Time

Construct the Reichenbach frame for an embedded clause under an attitude verb.

The key operation: embedded perspective time P' = matrix event time E. The embedded clause's tense locates its R' relative to P' = E_matrix, not relative to S (speech time).

embeddedR and embeddedE are the embedded clause's reference and event times, determined by its tense and aspect.

Equations

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

inductive Semantics.Tense.EmbeddedTenseReading : Type

The two available readings for embedded past under past.

When past tense appears in the complement of a past-tense attitude verb, the embedded past can be interpreted as:

• shifted: the embedded event occurred BEFORE the matrix event (R' < P' = E_matrix)
• simultaneous: the embedded event occurred AT the matrix event time (R' = P' = E_matrix), via SOT deletion (@cite{ogihara-1989}, §11.2 (83))

• shifted : EmbeddedTenseReading
• simultaneous : EmbeddedTenseReading

@[implicit_reducible]

instance Semantics.Tense.instDecidableEqEmbeddedTenseReading : DecidableEq EmbeddedTenseReading

Equations

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

@[implicit_reducible]

instance Semantics.Tense.instReprEmbeddedTenseReading : Repr EmbeddedTenseReading

Equations

• Semantics.Tense.instReprEmbeddedTenseReading = { reprPrec := Semantics.Tense.instReprEmbeddedTenseReading.repr }

def Semantics.Tense.instReprEmbeddedTenseReading.repr : EmbeddedTenseReading → ℕ → Std.Format

Equations

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

def Semantics.Tense.instInhabitedEmbeddedTenseReading.default : EmbeddedTenseReading

Equations

• Semantics.Tense.instInhabitedEmbeddedTenseReading.default = Semantics.Tense.EmbeddedTenseReading.shifted

@[implicit_reducible]

instance Semantics.Tense.instInhabitedEmbeddedTenseReading : Inhabited EmbeddedTenseReading

Equations

• Semantics.Tense.instInhabitedEmbeddedTenseReading = { default := Semantics.Tense.instInhabitedEmbeddedTenseReading.default }

def Semantics.Tense.availableReadings (param : Core.Time.Tense.SOTParameter) : List EmbeddedTenseReading

Available readings depend on the SOT parameter of the language.

SOT languages (English): both shifted and simultaneous readings. Non-SOT languages (Japanese): only shifted (absolute tense).

Equations

• Semantics.Tense.availableReadings Core.Time.Tense.SOTParameter.relative = [Semantics.Tense.EmbeddedTenseReading.shifted, Semantics.Tense.EmbeddedTenseReading.simultaneous]
• Semantics.Tense.availableReadings Core.Time.Tense.SOTParameter.absolute = [Semantics.Tense.EmbeddedTenseReading.shifted]

def Semantics.Tense.simultaneousFrame {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) : Core.Time.Reichenbach.ReichenbachFrame Time

The simultaneous reading: embedded R = matrix E.

"John said Mary was sick" (she was sick AT THE TIME of saying). The embedded reference time equals the matrix event time, so embedded tense = PRESENT relative to embedded P.

Equations

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

def Semantics.Tense.shiftedFrame {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) : Core.Time.Reichenbach.ReichenbachFrame Time

The shifted reading: embedded R < matrix E.

"John said Mary had been sick" (she was sick BEFORE the saying). The embedded reference time precedes the matrix event time, so embedded tense = PAST relative to embedded P.

Equations

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

theorem Semantics.Tense.past_under_past_shifted_is_past {Time : Type u_1} [LinearOrder Time] (S P R E R' : Time) (h_root : P = S) (h_matrix_past : R < P) (h_perfective : E ≤ R) (h_shifted : R' < E) : R' < S

In a past-under-past configuration with the shifted reading, the embedded reference time is past relative to speech time.

Derivation: R' < E_matrix ≤ R_matrix < P_matrix = S Therefore R' < S, which is PAST relative to speech time.

theorem Semantics.Tense.past_under_past_simultaneous_is_past {Time : Type u_1} [LinearOrder Time] (S P R E R' : Time) (h_root : P = S) (h_matrix_past : R < P) (h_perfective : E ≤ R) (h_simultaneous : R' = E) : R' < S

In a past-under-past configuration with the simultaneous reading, the embedded reference time is still past relative to speech time.

Derivation: R' = E_matrix ≤ R_matrix < P_matrix = S Therefore R' < S.

theorem Semantics.Tense.present_under_past_simultaneous {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) : (simultaneousFrame matrixFrame matrixFrame.eventTime).referenceTime = (simultaneousFrame matrixFrame matrixFrame.eventTime).perspectiveTime

Present-under-past with the simultaneous reading: embedded R = matrix E.

theorem Semantics.Tense.simultaneousFrame_is_present {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) : (simultaneousFrame matrixFrame embeddedE).isPresent

The simultaneous frame satisfies PRESENT (R = P) relative to embedded P.

theorem Semantics.Tense.simultaneousFrame_satisfies_time_eq {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) : (simultaneousFrame matrixFrame embeddedE).referenceTime = (simultaneousFrame matrixFrame embeddedE).perspectiveTime

The simultaneousFrame satisfies the time-equality R = P.

theorem Semantics.Tense.sot_simultaneous_available : EmbeddedTenseReading.simultaneous ∈ availableReadings Core.Time.Tense.SOTParameter.relative

In SOT languages, the simultaneous reading is available.

theorem Semantics.Tense.sot_shifted_available : EmbeddedTenseReading.shifted ∈ availableReadings Core.Time.Tense.SOTParameter.relative

In SOT languages, the shifted reading is available.

theorem Semantics.Tense.nonSOT_only_shifted : availableReadings Core.Time.Tense.SOTParameter.absolute = [EmbeddedTenseReading.shifted]

In non-SOT languages, only the shifted reading is available.

theorem Semantics.Tense.nonSOT_no_simultaneous : EmbeddedTenseReading.simultaneous ∉ availableReadings Core.Time.Tense.SOTParameter.absolute

Non-SOT languages do not have the simultaneous reading.

@cite{abusch-1997}'s Upper Limit Constraint

The Upper Limit Constraint is stated by @cite{abusch-1997} §7 (p. 25): "the now of an epistemic alternative is an upper limit for the denotation of tenses". The motivation is branching futures: at the now of an intensional context, future branches diverge across epistemic alternatives, so forward reference past the now is unsupported. The presuppositional construal — ULC as a constraint on definedness of semantic values, projecting via Karttunen-Heim — is due to @cite{heim-1994-comments}; @cite{abusch-1997} fn 20 endorses this construal.

ULC: embedded R' ≤ matrix E (= embedded P).

Note on faithfulness: the value-level reduction embeddedR ≤ matrixE strips the modal-alternative quantification Abusch's formulation carries (the "now of an epistemic alternative" quantifies over doxastic alternatives). A modal-layer formulation (over WorldHistory W Time, à la @cite{klecha-2016}'s actualHistoryBase) would be more faithful to the original; deferred future work.

@[reducible, inline]

abbrev Semantics.Tense.upperLimitConstraint {Time : Type u_1} [LE Time] (embeddedR matrixE : Time) : Prop

The Upper Limit Constraint.

Stated by @cite{abusch-1997} §7 ("the now of an epistemic alternative is an upper limit for the denotation of tenses"); presuppositional construal due to @cite{heim-1994-comments}, endorsed by Abusch 1997 fn 20. The current value-level reduction is embeddedR ≤ matrixE against bare [LE Time].

Equations

• Semantics.Tense.upperLimitConstraint embeddedR matrixE = (embeddedR ≤ matrixE)

theorem Semantics.Tense.ulc_blocks_forward_shift {Time : Type u_1} [LinearOrder Time] (embeddedR matrixE : Time) (h_ulc : upperLimitConstraint embeddedR matrixE) (h_forward : embeddedR > matrixE) : False

The ULC blocks the forward-shifted reading. If embedded R' must satisfy R' ≤ E_matrix (ULC) AND R' > E_matrix (forward shift), contradiction.

theorem Semantics.Tense.shifted_satisfies_ulc {Time : Type u_1} [Preorder Time] (embeddedR matrixE : Time) (h : embeddedR < matrixE) : upperLimitConstraint embeddedR matrixE

Shifted reading satisfies ULC: R' < E_matrix → R' ≤ E_matrix.

theorem Semantics.Tense.simultaneous_satisfies_ulc {Time : Type u_1} [Preorder Time] (embeddedR matrixE : Time) (h : embeddedR = matrixE) : upperLimitConstraint embeddedR matrixE

Simultaneous reading satisfies ULC: R' = E_matrix → R' ≤ E_matrix.

TensePronoun Projections onto SOT Frames

The TensePronoun type in Core.Time.Tense unifies the five views of tense. The following theorems show that simultaneousFrame and shiftedFrame are projections of specific tense pronouns — a bound present pronoun gives the simultaneous reading; a free past pronoun gives the shifted reading.

theorem Semantics.Tense.simultaneousFrame_from_tense_pronoun {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (g : Core.Time.Tense.TemporalAssignment Time) (n : ℕ) (embeddedE : Time) (tp : Core.Time.Tense.TensePronoun) (hIdx : tp.varIndex = n) (_hPres : tp.constraint = Core.Time.Tense.GramTense.present) (hResolve : Core.Time.Tense.interpTense n g = matrixFrame.eventTime) : tp.toFrame g matrixFrame.speechTime matrixFrame.eventTime embeddedE = simultaneousFrame matrixFrame embeddedE

The simultaneous reading = bound present tense pronoun. A present-constraint tense pronoun whose variable resolves to P (the matrix event time) produces a simultaneousFrame.

theorem Semantics.Tense.shiftedFrame_from_tense_pronoun {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (g : Core.Time.Tense.TemporalAssignment Time) (n : ℕ) (embeddedR embeddedE : Time) (tp : Core.Time.Tense.TensePronoun) (hIdx : tp.varIndex = n) (_hPast : tp.constraint = Core.Time.Tense.GramTense.past) (hResolve : Core.Time.Tense.interpTense n g = embeddedR) : tp.toFrame g matrixFrame.speechTime matrixFrame.eventTime embeddedE = shiftedFrame matrixFrame embeddedR embeddedE

The shifted reading = free past tense pronoun. A past-constraint tense pronoun whose variable resolves to some R' < P produces a shiftedFrame.

theorem Semantics.Tense.doubleAccess_present_under_past {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (_embeddedE : Time) (p : Time → Prop) (h_simul : p matrixFrame.eventTime) (h_speech : p matrixFrame.speechTime) : Core.Time.Tense.doubleAccess p matrixFrame.speechTime matrixFrame.eventTime

Double-access: present-under-past requires the complement to hold at BOTH speech time AND matrix event time.

This bridges the doubleAccess definition from Core.Time.Tense to the SOT analysis: the present-under-past frame's R = P (simultaneous), and the speech time is independently accessible via indexical rigidity.

theorem Semantics.Tense.bound_tense_simultaneous {Time : Type u_1} [LinearOrder Time] (g : Core.Time.Tense.TemporalAssignment Time) (n : ℕ) (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) : Core.Time.Tense.interpTense n (Core.Time.Tense.updateTemporal g n matrixFrame.eventTime) = matrixFrame.eventTime ∧ (simultaneousFrame matrixFrame matrixFrame.eventTime).isPresent

Ogihara's synthesis: bound tense (zero tense) + attitude binding = simultaneous reading. The zero tense variable receives the matrix event time via lambda abstraction; the Reichenbach frame has R = P.

structure Semantics.Tense.ThenAdverb : Type

A "then"-type temporal adverb. Cross-linguistically, "then" shifts the perspective time P away from the speech time S (@cite{zhao-2025}, @cite{tsilia-zhao-2026}).

• language : String

  Language name

• form : String

  Surface form

• gloss : String

  English gloss

• shiftsPerspective : Bool

  "then" shifts P away from S: P ≠ S after "then" applies.

@[implicit_reducible]

instance Semantics.Tense.instReprThenAdverb : Repr ThenAdverb

Equations

• Semantics.Tense.instReprThenAdverb = { reprPrec := Semantics.Tense.instReprThenAdverb.repr }

def Semantics.Tense.instReprThenAdverb.repr : ThenAdverb → ℕ → Std.Format

Equations

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

def Semantics.Tense.instDecidableEqThenAdverb.decEq (x✝ x✝¹ : ThenAdverb) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Tense.instDecidableEqThenAdverb : DecidableEq ThenAdverb

Equations

• Semantics.Tense.instDecidableEqThenAdverb = Semantics.Tense.instDecidableEqThenAdverb.decEq