Dynamic tense as eliminative update of static tense

[Vel96] [GSV96] [dG06] [Cha21] [Hei82]

dynPAST/dynPRES/dynFUT are the dynamic-context-update counterparts of the static PAST/PRES/FUT operators in Tense/Compositional.lean. Each is the spine's test filter lift (test ·) at the tense cell (Tense/Defs.lean) between two dref lookups — so the static and dynamic operators are the same cell, lifted from a state-level predicate to a context-level filter, and the temporal algebra (partition, contradiction, chaining) is the cells' Boolean algebra (Core.Order.holds_or_holds₃, Core.Order.not_holds_and_holds) through the generic filter algebra of Update.lean (lift_test_cover₃, lift_test_disjoint).

Contexts are level-0 states over Index.Possibility — the world coordinate is the current evaluation index, drefs are indices.

Theoretical anchor

• [Hei82] principle (A) — file change for a static condition is intersection with the satisfaction set — is the prototype "static condition lifts to context filter"; [Vel96] formalizes it as the test, and [GSV96] generalize to eliminative updates (CCP.IsEliminative).
• [dG06] recovers static readings from dynamic ones by the trivial continuation; [Cha21] recasts the lift monadically. The dynPAST = lift (test (holds past · ·)) factoring below is the tense fragment of that lift.

Main results

• dynPAST_iff_PAST_with_true (and PRES/FUT): a context entry survives the dynamic filter iff the static operator holds at its event/reference indices — the "wrapper actually wraps" check.
• temporal_partition, the contradictory-pair lemmas, and dynPAST_transitive: the temporal algebra, derived from the cells' Boolean algebra through the spine's filter algebra.

Sibling of Tense/Compositional.lean (the static operators) and Mood/Dynamic.lean (the parallel pattern for SUBJ/IND). Used by Studies/Mendes2025.lean's analysis of the Subordinate Future.

def Tense.dynPAST {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (eventVar refVar : ℕ) : Set (Intensional.Index.Possibility W Time) → Set (Intensional.Index.Possibility W Time)

Dynamic PAST: the spine's test filter at the past cell. A context entry survives iff its event-variable index precedes its reference-variable index in time.

Equations

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

def Tense.dynPRES {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (eventVar refVar : ℕ) : Set (Intensional.Index.Possibility W Time) → Set (Intensional.Index.Possibility W Time)

Dynamic PRES: the test filter at the present cell.

Equations

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

def Tense.dynFUT {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (eventVar refVar : ℕ) : Set (Intensional.Index.Possibility W Time) → Set (Intensional.Index.Possibility W Time)

Dynamic FUT: the test filter at the future cell.

Equations

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

Membership characterizations

@[simp]

theorem Tense.mem_dynPAST {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (e r : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) : p ∈ dynPAST e r c ↔ p ∈ c ∧ (p.assignment e).time < (p.assignment r).time

@[simp]

theorem Tense.mem_dynPRES {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (e r : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) : p ∈ dynPRES e r c ↔ p ∈ c ∧ (p.assignment e).time = (p.assignment r).time

@[simp]

theorem Tense.mem_dynFUT {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (e r : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) : p ∈ dynFUT e r c ↔ p ∈ c ∧ (p.assignment r).time < (p.assignment e).time

Static realization: dynamic IS the eliminative update of static

For each tense, the static operator (with the trivial propositional payload fun _ => True) holds at the entry's event/reference indices iff the dynamic filter retains the entry — the [dG06] sense in which static and dynamic tense are the same operator at different layers.

theorem Tense.dynPAST_iff_PAST_with_true {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (e r : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) : p ∈ dynPAST e r c ↔ p ∈ c ∧ PAST (fun (x : Intensional.Index W Time) => True) (p.assignment e) (p.assignment r)

theorem Tense.dynPRES_iff_PRES_with_true {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (e r : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) : p ∈ dynPRES e r c ↔ p ∈ c ∧ PRES (fun (x : Intensional.Index W Time) => True) (p.assignment e) (p.assignment r)

theorem Tense.dynFUT_iff_FUT_with_true {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (e r : ℕ) (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) : p ∈ dynFUT e r c ↔ p ∈ c ∧ FUT (fun (x : Intensional.Index W Time) => True) (p.assignment e) (p.assignment r)

Temporal algebra (cell algebra through the filter algebra)

theorem Tense.temporal_partition {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (c : Set (Intensional.Index.Possibility W Time)) (v₁ v₂ : ℕ) : dynPAST v₁ v₂ c ∪ dynPRES v₁ v₂ c ∪ dynFUT v₁ v₂ c = c

PAST ∪ PRES ∪ FUT = identity: lift_test_cover₃ at the cells' cover past ⊔ present ⊔ future = ⊤.

theorem Tense.dynPAST_dynFUT_empty {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (c : Set (Intensional.Index.Possibility W Time)) (v₁ v₂ : ℕ) : dynPAST v₁ v₂ (dynFUT v₁ v₂ c) = ∅

PAST and FUT are contradictory on the same variables: lift_test_disjoint at the disjoint cells past ⊓ future = ⊥.

theorem Tense.dynPAST_dynPRES_empty {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (c : Set (Intensional.Index.Possibility W Time)) (v₁ v₂ : ℕ) : dynPAST v₁ v₂ (dynPRES v₁ v₂ c) = ∅

PAST and PRES are contradictory on the same variables.

theorem Tense.dynPRES_dynFUT_empty {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (c : Set (Intensional.Index.Possibility W Time)) (v₁ v₂ : ℕ) : dynPRES v₁ v₂ (dynFUT v₁ v₂ c) = ∅

PRES and FUT are contradictory on the same variables.

theorem Tense.dynPAST_transitive {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (c : Set (Intensional.Index.Possibility W Time)) (p : Intensional.Index.Possibility W Time) (e r s : ℕ) (h : p ∈ dynPAST r s (dynPAST e r c)) : (p.assignment e).time < (p.assignment s).time

Chained PAST constraints compose: e < r ∧ r < s → e < s.