Unified Tense Pronoun Architecture

@cite{abusch-1997} @cite{heim-kratzer-1998} @cite{kratzer-1998} @cite{partee-1973} @cite{von-stechow-2009} @cite{ogihara-1989}

@cite{abusch-1997}'s insight: a tense morpheme is a temporal pronoun — a variable with a presupposed temporal constraint (Prior, reinterpreted) and a binding mode (indexical/anaphoric/bound). This single concept projects onto five representations of temporal reference in the codebase:

1. Priorean operators (PAST/PRES/FUT): constraint.constrains
2. Reichenbach frames (S, P, R, E): TensePronoun.toFrame
3. Referential variables: TensePronoun.resolve
4. Kaplan indexicals (rigid to speech time): mode =.indexical
5. Attitude binding (zero tense, @cite{ogihara-1989}): mode =.bound

The existing ad-hoc bridge theorems (referential_past_decomposition, temporallyBound_gives_simultaneous, indexical_tense_matches_opNow, ogihara_bound_tense_simultaneous) become trivial projections from this unified type.

Architecture

This module lives in Core/ because both Theories/Semantics.Montague/Sentence/Tense/ and Theories/Semantics.Intensional/Attitude/ need the shared infrastructure (GramTense, SOTParameter, TemporalAssignment, etc.) without a cross-tree import.

inductive Core.Tense.GramTense : Type

Grammatical tense: a temporal relation imposed by tense morphology.

Following the Reichenbach/Klein tradition:

• PAST: reference time before speech time
• PRESENT: reference time overlaps speech time
• FUTURE: reference time after speech time

• past : GramTense
• present : GramTense
• future : GramTense

instance Core.Tense.instDecidableEqGramTense : DecidableEq GramTense

Equations

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

instance Core.Tense.instReprGramTense : Repr GramTense

Equations

• Core.Tense.instReprGramTense = { reprPrec := Core.Tense.instReprGramTense.repr }

def Core.Tense.instReprGramTense.repr : GramTense → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Tense.instReprGramTense.repr Core.Tense.GramTense.past prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Tense.GramTense.past")).group prec✝

def Core.Tense.instBEqGramTense.beq : GramTense → GramTense → Bool

Equations

• Core.Tense.instBEqGramTense.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Tense.instBEqGramTense : BEq GramTense

Equations

• Core.Tense.instBEqGramTense = { beq := Core.Tense.instBEqGramTense.beq }

def Core.Tense.instInhabitedGramTense.default : GramTense

Equations

• Core.Tense.instInhabitedGramTense.default = Core.Tense.GramTense.past

instance Core.Tense.instInhabitedGramTense : Inhabited GramTense

Equations

• Core.Tense.instInhabitedGramTense = { default := Core.Tense.instInhabitedGramTense.default }

def Core.Tense.GramTense.toRelation : GramTense → Time.TemporalRelation

Convert tense to its corresponding temporal relation

Equations

• Core.Tense.GramTense.past.toRelation = Core.Time.TemporalRelation.before
• Core.Tense.GramTense.present.toRelation = Core.Time.TemporalRelation.overlapping
• Core.Tense.GramTense.future.toRelation = Core.Time.TemporalRelation.after

def Core.Tense.GramTense.inverseRelation : GramTense → Time.TemporalRelation

The inverse relation (for "backwards" reference)

Equations

• Core.Tense.GramTense.past.inverseRelation = Core.Time.TemporalRelation.after
• Core.Tense.GramTense.present.inverseRelation = Core.Time.TemporalRelation.overlapping
• Core.Tense.GramTense.future.inverseRelation = Core.Time.TemporalRelation.before

def Core.Tense.GramTense.constrains {Time : Type u_1} [LinearOrder Time] (t : GramTense) (refTime perspTime : Time) : Prop

The temporal constraint imposed by a grammatical tense. Past: ref < perspective. Present: ref = perspective. Future: ref > perspective. This is the core ordering that Priorean operators assert and Abusch's tense pronouns presuppose.

Equations

• Core.Tense.GramTense.past.constrains refTime perspTime = (refTime < perspTime)
• Core.Tense.GramTense.present.constrains refTime perspTime = (refTime = perspTime)
• Core.Tense.GramTense.future.constrains refTime perspTime = (refTime > perspTime)

inductive Core.Tense.SOTParameter : Type

Sequence of Tenses (SOT) parameter.

Languages differ in how embedded tense interacts with matrix tense:

• SOT languages (English): Embedded tense is relative to matrix
• Non-SOT languages (Japanese): Embedded tense is absolute

• relative : SOTParameter
• absolute : SOTParameter

instance Core.Tense.instDecidableEqSOTParameter : DecidableEq SOTParameter

Equations

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

def Core.Tense.instReprSOTParameter.repr : SOTParameter → ℕ → Std.Format

Equations

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

instance Core.Tense.instReprSOTParameter : Repr SOTParameter

Equations

• Core.Tense.instReprSOTParameter = { reprPrec := Core.Tense.instReprSOTParameter.repr }

def Core.Tense.instBEqSOTParameter.beq : SOTParameter → SOTParameter → Bool

Equations

• Core.Tense.instBEqSOTParameter.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Tense.instBEqSOTParameter : BEq SOTParameter

Equations

• Core.Tense.instBEqSOTParameter = { beq := Core.Tense.instBEqSOTParameter.beq }

@[reducible, inline]

abbrev Core.Tense.TenseInterpretation : Type

Tense interpretation modes. Tenses parallel pronouns: indexical (deictic), anaphoric (discourse-bound), and bound variable (zero tense).

This is an alias for Core.ReferentialMode.ReferentialMode, which captures Partee's insight that the same three-way classification applies to both pronouns and tenses.

Equations

• Core.Tense.TenseInterpretation = Core.ReferentialMode.ReferentialMode

theorem Core.Tense.bound_is_sot_mechanism : ReferentialMode.ReferentialMode.bound ≠ ReferentialMode.ReferentialMode.indexical ∧ ReferentialMode.ReferentialMode.bound ≠ ReferentialMode.ReferentialMode.anaphoric

Bound (zero) tense is the SOT mechanism: it must be locally bound, yielding the simultaneous reading without a deletion rule.

Temporal assignment functions are the temporal instantiation of Core.VarAssignment (VarAssignment Time = ℕ → Time). All algebraic properties (update_lookup_same, update_lookup_other, update_update_same, update_self) are inherited from the generic infrastructure.

@[reducible, inline]

abbrev Core.Tense.TemporalAssignment (Time : Type u_1) : Type u_1

Temporal assignment function: maps variable indices to times. The temporal analogue of H&K's Assignment (ℕ → Entity). Defined as VarAssignment Time from Core.VarAssignment.

Equations

• Core.Tense.TemporalAssignment Time = Core.VarAssignment.VarAssignment Time

@[reducible, inline]

abbrev Core.Tense.updateTemporal {Time : Type u_1} (g : TemporalAssignment Time) (n : ℕ) (t : Time) : TemporalAssignment Time

Modified temporal assignment g[n ↦ t]. Specializes Core.VarAssignment.updateVar.

Equations

• Core.Tense.updateTemporal g n t = Core.VarAssignment.updateVar g n t

@[reducible, inline]

abbrev Core.Tense.interpTense {Time : Type u_1} (n : ℕ) (g : TemporalAssignment Time) : Time

Temporal variable denotation: ⟦tₙ⟧^g = g(n). Specializes Core.VarAssignment.lookupVar.

Equations

• Core.Tense.interpTense n g = Core.VarAssignment.lookupVar n g

@[reducible, inline]

abbrev Core.Tense.temporalLambdaAbs {Time : Type u_1} {α : Type u_2} (n : ℕ) (body : TemporalAssignment Time → α) : TemporalAssignment Time → Time → α

Temporal lambda abstraction: bind a time variable. Specializes Core.VarAssignment.varLambdaAbs.

Partee's bound tense: "Whenever Mary phones, Sam is asleep" — present tense bound by "whenever", just as "Every farmer beats his donkey" has "his" bound by "every farmer".

Equations

• Core.Tense.temporalLambdaAbs n body = Core.VarAssignment.varLambdaAbs n body

def Core.Tense.situationToTemporal {W : Type u_1} {Time : Type u_2} (g : ℕ → Situation W Time) : TemporalAssignment Time

Project a situation assignment to a temporal assignment. This is the formal bridge between situation semantics and tense semantics: the temporal coordinate of each situation is extracted.

Equations

• Core.Tense.situationToTemporal g n = (g n).time

theorem Core.Tense.situation_temporal_commutes {W : Type u_1} {Time : Type u_2} (g : ℕ → Situation W Time) (n : ℕ) : interpTense n (situationToTemporal g) = (g n).time

Temporal interpretation via situation assignment commutes with time projection: interpTense n (π g) = (g n).time.

theorem Core.Tense.zeroTense_receives_binder_time {Time : Type u_1} (g : TemporalAssignment Time) (n : ℕ) (binderTime : Time) : interpTense n (updateTemporal g n binderTime) = binderTime

Zero tense: a bound tense variable contributes no independent temporal constraint. When an attitude verb binds it, the variable receives the matrix event time. This is the SOT mechanism: the "past" morphology on the embedded verb is agreement, not a semantic tense.

@[reducible, inline]

abbrev Core.Tense.SitProp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Type of situation-level propositions (Prop-valued, for proof-level temporal reasoning).

A temporal predicate takes a situation and returns truth value. This is what tense operators modify.

Note: a Bool-valued counterpart exists at Semantics.Attitudes.SituationDependent.SitProp for computational RSA evaluation. The split follows the Prop'/BProp pattern in Core/Proposition.lean.

Equations

• Core.Tense.SitProp W Time = (Situation W Time → Prop)

structure Core.Tense.TensePronoun : Type

@cite{abusch-1997}'s unified tense denotation.

A tense morpheme introduces a temporal variable with:

• A variable index in the temporal assignment
• A presupposed temporal constraint (past/present/future)
• A binding mode (indexical, anaphoric, or bound)

This unifies five views of tense:

• Priorean: constraint.constrains (temporal ordering)
• Reichenbach: resolve g = R, perspective time = P
• Referential: resolve g = interpTense varIndex g
• Kaplan indexical: mode =.indexical → rigid to speech time
• Attitude binding: mode =.bound → zero tense

• varIndex : ℕ
• constraint : GramTense
• mode : TenseInterpretation
• evalTimeIndex : ℕ

  Index of the evaluation time variable in the temporal assignment. Default 0 = speech time slot. Under embedding, attitude verbs update this index to point at the matrix event time. @cite{klecha-2016}: modals can also shift the eval time index.

def Core.Tense.instDecidableEqTensePronoun.decEq (x✝ x✝¹ : TensePronoun) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.Tense.instDecidableEqTensePronoun : DecidableEq TensePronoun

Equations

• Core.Tense.instDecidableEqTensePronoun = Core.Tense.instDecidableEqTensePronoun.decEq

def Core.Tense.instReprTensePronoun.repr : TensePronoun → ℕ → Std.Format

Equations

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

instance Core.Tense.instReprTensePronoun : Repr TensePronoun

Equations

• Core.Tense.instReprTensePronoun = { reprPrec := Core.Tense.instReprTensePronoun.repr }

def Core.Tense.instBEqTensePronoun.beq : TensePronoun → TensePronoun → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.Tense.instBEqTensePronoun.beq x✝¹ x✝ = false

instance Core.Tense.instBEqTensePronoun : BEq TensePronoun

Equations

• Core.Tense.instBEqTensePronoun = { beq := Core.Tense.instBEqTensePronoun.beq }

def Core.Tense.TensePronoun.resolve {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) : Time

Resolve: look up the temporal variable.

Equations

• tp.resolve g = Core.Tense.interpTense tp.varIndex g

def Core.Tense.TensePronoun.presupposition {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (resolvedTime perspectiveTime : Time) : Prop

Presupposition: the constraint applied to the resolved time.

Equations

• tp.presupposition resolvedTime perspectiveTime = tp.constraint.constrains resolvedTime perspectiveTime

def Core.Tense.TensePronoun.toFrame {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime perspectiveTime eventTime : Time) : Reichenbach.ReichenbachFrame Time

Construct the Reichenbach frame. R = g(varIndex), P = perspectiveTime.

Equations

• tp.toFrame g speechTime perspectiveTime eventTime = { speechTime := speechTime, perspectiveTime := perspectiveTime, referenceTime := tp.resolve g, eventTime := eventTime }

def Core.Tense.TensePronoun.isIndexical (tp : TensePronoun) : Bool

Equations

• tp.isIndexical = (tp.mode == Core.ReferentialMode.ReferentialMode.indexical)

def Core.Tense.TensePronoun.isBound (tp : TensePronoun) : Bool

Equations

• tp.isBound = (tp.mode == Core.ReferentialMode.ReferentialMode.bound)

def Core.Tense.TensePronoun.evalTime {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) : Time

Resolve the evaluation time from the assignment. In root clauses (evalTimeIndex = 0, g(0) = speech time), this is speech time. Under embedding, the attitude verb updates the assignment so that g(evalTimeIndex) = matrix event time.

Equations

• tp.evalTime g = Core.Tense.interpTense tp.evalTimeIndex g

def Core.Tense.TensePronoun.fullPresupposition {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (g : TemporalAssignment Time) : Prop

Full presupposition: the tense constraint checked against the resolved evaluation time (not just a bare perspective time parameter). This makes the eval time compositionally determined rather than stipulated.

Equations

• tp.fullPresupposition g = tp.constraint.constrains (tp.resolve g) (tp.evalTime g)

theorem Core.Tense.evalTime_root_is_speech {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime : Time) (hEval : tp.evalTimeIndex = 0) (hRoot : g 0 = speechTime) : tp.evalTime g = speechTime

When evalTimeIndex = 0 and g(0) = speechTime, the evaluation time is speech time. This is the root-clause default: tense is checked against speech time.

theorem Core.Tense.evalTime_shifts_under_embedding {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (matrixEventTime : Time) : tp.evalTime (updateTemporal g tp.evalTimeIndex matrixEventTime) = matrixEventTime

Updating the eval time index gives Von Stechow's perspective shift: the embedded tense is now checked against a different time (the matrix event time). This is how attitude verbs "transmit" their event time.

theorem Core.Tense.TensePronoun.bound_resolve_eq_binder {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (binderTime : Time) : tp.resolve (updateTemporal g tp.varIndex binderTime) = binderTime

Resolving a bound tense under binding yields the binder time.

theorem Core.Tense.TensePronoun.bound_present_simultaneous {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime perspTime eventTime : Time) (hBind : tp.resolve g = perspTime) (_hPres : tp.constraint = GramTense.present) : (tp.toFrame g speechTime perspTime eventTime).isPresent

A present-constraint bound tense under binding gives R = P (simultaneous). The hPres hypothesis constrains the theorem to present tenses; the frame equality follows from hBind alone (R = resolve = perspTime).

def Core.Tense.doubleAccess {Time : Type u_1} (p : Time → Prop) (speechTime matrixEventTime : Time) : Prop

Double-access: present-under-past requires the complement to hold at BOTH speech time (indexical rigidity) AND matrix event time (attitude accessibility).

Equations

• Core.Tense.doubleAccess p speechTime matrixEventTime = (p speechTime ∧ p matrixEventTime)

theorem Core.Tense.TensePronoun.indexical_present_at_speech {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (resolvedTime speechTime : Time) (hPres : tp.constraint = GramTense.present) (hPresup : tp.presupposition resolvedTime speechTime) : resolvedTime = speechTime

An indexical present tense presupposes resolution to speech time.

inductive Core.Tense.Overtness : Type

Phonological overtness of a referential expression (@cite{heim-kratzer-1998} §3).

Applies uniformly to pronouns and tenses: English has zero tense under SOT (bound present surfaces as ∅); Japanese has zero pronouns in subject position (locally bound by Agr). Persian has zero pronouns but NOT zero tense (tense is in C, outside the local agreement domain).

The distribution of overt vs. zero is governed by locality of agreement: a referential expression that is locally bound by an agreeing head surfaces as zero.

• overt : Overtness
• zero : Overtness

instance Core.Tense.instDecidableEqOvertness : DecidableEq Overtness

Equations

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

def Core.Tense.instReprOvertness.repr : Overtness → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Core.Tense.instReprOvertness.repr Core.Tense.Overtness.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Tense.Overtness.zero")).group prec✝

instance Core.Tense.instReprOvertness : Repr Overtness

Equations

• Core.Tense.instReprOvertness = { reprPrec := Core.Tense.instReprOvertness.repr }

instance Core.Tense.instBEqOvertness : BEq Overtness

Equations

• Core.Tense.instBEqOvertness = { beq := Core.Tense.instBEqOvertness.beq }

def Core.Tense.instBEqOvertness.beq : Overtness → Overtness → Bool

Equations

• Core.Tense.instBEqOvertness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Tense.instInhabitedOvertness.default : Overtness

Equations

• Core.Tense.instInhabitedOvertness.default = Core.Tense.Overtness.overt

instance Core.Tense.instInhabitedOvertness : Inhabited Overtness

Equations

• Core.Tense.instInhabitedOvertness = { default := Core.Tense.instInhabitedOvertness.default }

def Core.Tense.Overtness.fromBinding : ReferentialMode.ReferentialMode → (localDomain : Bool) → Overtness

Kratzer's locality generalization (1998, formula 26):

A referential expression that is locally bound by an agreeing head surfaces as zero. Free (indexical or anaphoric) expressions surface as overt. This unifies:

• Reflexives = locally bound entity pronouns → zero/reduced
• Simultaneous tense = locally bound temporal pronoun → zero under SOT
• Japanese subject pro = locally bound by Agr → zero
• Persian pronouns = locally bound by Agr → zero, but tense is NOT local to Agr (tense is in C) → overt

Equations

• Core.Tense.Overtness.fromBinding Core.ReferentialMode.ReferentialMode.bound true = Core.Tense.Overtness.zero
• Core.Tense.Overtness.fromBinding x✝¹ x✝ = Core.Tense.Overtness.overt

theorem Core.Tense.Overtness.free_always_overt (m : ReferentialMode.ReferentialMode) (l : Bool) (hFree : m.isFree = true) : fromBinding m l = overt

Free (indexical or anaphoric) expressions are always overt.

theorem Core.Tense.Overtness.bound_local_is_zero : fromBinding ReferentialMode.ReferentialMode.bound true = zero

Bound expressions in a local domain are zero.

theorem Core.Tense.Overtness.bound_nonlocal_is_overt : fromBinding ReferentialMode.ReferentialMode.bound false = overt

Bound expressions outside the local domain remain overt. This is the Persian case: tense is bound but not in a local agreement domain (tense is in C, Agr is in Infl).

The key bridge showing that @cite{abusch-1997}'s De Bruijn temporal indexing is already tower-style depth access. TensePronoun.evalTimeIndex is a depth-relative index into the tower: when the temporal assignment encodes tower time coordinates (g k = (tower.contextAt k).time), interpTense agrees with AccessPattern.resolve.

• tensePronounAccessPattern — converts TensePronoun.evalTimeIndex to an AccessPattern with depth :=.relative tp.evalTimeIndex
• tense_tower_bridge — when g encodes tower time coordinates, interpTense agrees with AccessPattern.resolve
• tense_root_bridge — root clause: evalTimeIndex = 0 means origin time
• von_stechow_tower — pushing a temporal shift = Von Stechow's perspective shift

def Core.Tense.tensePronounAccessPattern {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) : Context.AccessPattern (Context.KContext W E P T) T

Convert a TensePronoun's eval-time index to an AccessPattern that reads the time coordinate at the corresponding tower depth.

evalTimeIndex = 0 → origin (speech-act context time) evalTimeIndex = k → depth k (the k-th embedding's time)

This makes explicit the observation that Abusch's variable indices ARE tower depth indices for the temporal coordinate.

Equations

• Core.Tense.tensePronounAccessPattern tp = { depth := Core.Context.DepthSpec.relative tp.evalTimeIndex, project := Core.Context.KContext.time }

def Core.Tense.towerFaithful {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (g : TemporalAssignment T) (t : Context.ContextTower (Context.KContext W E P T)) : Prop

A temporal assignment that faithfully represents a tower: g k returns the time coordinate at tower depth k. This is the bridge condition connecting the variable-assignment world to the tower world.

Equations

• Core.Tense.towerFaithful g t = ∀ (k : ℕ), g k = (t.contextAt k).time

theorem Core.Tense.tense_tower_bridge {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) (g : TemporalAssignment T) (t : Context.ContextTower (Context.KContext W E P T)) (hFaithful : towerFaithful g t) : tp.evalTime g = (tensePronounAccessPattern tp).resolve t

When the temporal assignment encodes tower time coordinates, interpTense at the eval-time index agrees with resolving the tensePronounAccessPattern against the tower.

This is the central result: Abusch's De Bruijn indexing IS tower-depth access for the temporal coordinate.

theorem Core.Tense.tense_root_bridge {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) (c : Context.KContext W E P T) (hEval : tp.evalTimeIndex = 0) (g : TemporalAssignment T) (hFaithful : towerFaithful g (Context.ContextTower.root c)) : tp.evalTime g = c.time

In a root tower (no shifts), evalTimeIndex = 0 accesses the origin time. This is the root-clause default: tense is checked against speech time.

Combined with evalTime_root_is_speech, this shows that root-clause temporal evaluation is origin access — exactly Kaplan's thesis for time.

theorem Core.Tense.tensePronounAccessPattern_root_resolves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) (hEval : tp.evalTimeIndex = 0) (c : Context.KContext W E P T) : (tensePronounAccessPattern tp).resolve (Context.ContextTower.root c) = c.time

The access pattern for a root-clause tense pronoun (evalTimeIndex = 0) resolves to depth 0, which is the origin.

theorem Core.Tense.von_stechow_tower {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (g : TemporalAssignment T) (t : Context.ContextTower (Context.KContext W E P T)) (newTime : T) : updateTemporal g t.depth newTime t.depth = newTime

@cite{von-stechow-2009}'s perspective shift — the attitude verb transmits its event time to the embedded clause — corresponds to pushing a temporalShift onto the tower.

Concretely: the updated assignment at the tower depth yields the new time.

theorem Core.Tense.von_stechow_tower_preserves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (g : TemporalAssignment T) (t : Context.ContextTower (Context.KContext W E P T)) (newTime : T) (hFaithful : towerFaithful g t) (k : ℕ) (hk : k < t.depth) : updateTemporal g t.depth newTime k = (t.contextAt k).time

Under faithful encoding, layers below the push point are preserved.

theorem Core.Tense.von_stechow_tower_innermost {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Context.ContextTower (Context.KContext W E P T)) (newTime : T) : (t.push (Context.temporalShift newTime)).innermost.time = newTime

Pushing a temporal shift assigns newTime to the new depth in the extended tower, mirroring von_stechow_tower on the assignment side.