Sequence of tense: the cross-cutting licensing interface

[KZ18] [Ogi19] [Egr26]

Past-under-past embeddings have a simultaneous and a backward-shifted reading (and, with an intervening future, a forward-shifted one). Rival accounts — relational/feature ([KZ18]), deletion ([Ogi19]), res-movement de re, clause-size ([Egr26]) — disagree only about when each reading is licensed, not about what a reading is. This file is the seam.

What a reading is (no enum)

A reading is which comparison atom the embedded reference time bears to its anchor. Tense.embeddedFrame puts the anchor at the matrix event time, so the three readings are exactly the overhaul's frame predicates: .lt/isPast = back-shifted, .eq/isPresent = simultaneous, .gt/isFuture = forward.

What a theory provides

A theory is one LocalLicense — a relation reading, off an immediately containing clause and the clause it contains, which atoms are licensed. Both syntactic and semantic theories emit the same Finset Ordering, so they are peers; profile folds the relation pairwise along the c-command chain (adjacency-local, so an intervening tense re-anchors). Clause size enters only through the framework-neutral Clause.Size (Syntax/Clause), never Minimalist machinery.

Double-access (a two-anchor present) and modal-base orientation (Klecha) do not fit one cell against one anchor; they are deliberately out of this interface and handled by separate substrate.

structure SequenceOfTense.Node : Type

A node in an embedding chain: a clause's morphological tense as a relative comparison cell (past = notAfter, the ≤ of [KZ18]) and its framework-neutral Clause.Size. Not a Minimalist.ComplementSize — a Minimalist clause provides its size via ComplementSize.toClauseSize.

• tense : Finset Ordering

  The clause's tense as a relative comparison cell to its anchor.

• size : Clause.Size

  The clause's framework-neutral size (Clause.Size).

@[reducible, inline]

abbrev SequenceOfTense.LocalLicense : Type

The cross-cutting interface: given a containing clause and the clause it immediately contains, which comparison atoms hold between the contained reference time and its anchor. A theory is a value of this type.

Equations

• SequenceOfTense.LocalLicense = (SequenceOfTense.Node → SequenceOfTense.Node → Finset Ordering)

def SequenceOfTense.profile (L : LocalLicense) : Node → List Node → List (Finset Ordering)

Compose a license pairwise along the c-command chain (matrix first): the licensed reading-set at each embedding level. Adjacency-local — not a fold or product — so an intervening tense re-anchors and blocking propagates ([Ogi96]'s past-under-will-under-past).

Equations

• SequenceOfTense.profile L x✝ [] = []
• SequenceOfTense.profile L x✝ (c :: rest) = L x✝ c :: SequenceOfTense.profile L c rest

Reading availability (the atoms — no Reading enum)

def SequenceOfTense.Simultaneous (s : Finset Ordering) : Prop

The simultaneous reading is licensed iff the eq atom is.

Equations

• SequenceOfTense.Simultaneous s = (Ordering.eq ∈ s)

def SequenceOfTense.Backshifted (s : Finset Ordering) : Prop

The backward-shifted reading is licensed iff the lt atom is.

Equations

• SequenceOfTense.Backshifted s = (Ordering.lt ∈ s)

def SequenceOfTense.ForwardShifted (s : Finset Ordering) : Prop

The forward-shifted reading is licensed iff the gt atom is.

Equations

• SequenceOfTense.ForwardShifted s = (Ordering.gt ∈ s)

@[implicit_reducible]

instance SequenceOfTense.instDecidableSimultaneous (s : Finset Ordering) : Decidable (Simultaneous s)

Equations

• SequenceOfTense.instDecidableSimultaneous s = SequenceOfTense.instDecidableSimultaneous._aux_1 s

@[implicit_reducible]

instance SequenceOfTense.instDecidableBackshifted (s : Finset Ordering) : Decidable (Backshifted s)

Equations

• SequenceOfTense.instDecidableBackshifted s = SequenceOfTense.instDecidableBackshifted._aux_1 s

@[implicit_reducible]

instance SequenceOfTense.instDecidableForwardShifted (s : Finset Ordering) : Decidable (ForwardShifted s)

Equations

• SequenceOfTense.instDecidableForwardShifted s = SequenceOfTense.instDecidableForwardShifted._aux_1 s

Realization: the atoms are the overhaul's frame predicates

For an embedded frame whose perspective time is the matrix event time (Tense.embeddedFrame), the licensed atom is its R-vs-P comparison, and the three named readings are exactly ReichenbachFrame.isPast/isPresent/isFuture.

theorem SequenceOfTense.isPast_iff_atom {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : f.isPast ↔ compare f.referenceTime f.perspectiveTime = Ordering.lt

theorem SequenceOfTense.isPresent_iff_atom {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : f.isPresent ↔ compare f.referenceTime f.perspectiveTime = Ordering.eq

theorem SequenceOfTense.isFuture_iff_atom {T : Type u_1} [LinearOrder T] (f : Time.ReichenbachFrame T) : f.isFuture ↔ compare f.referenceTime f.perspectiveTime = Ordering.gt

License schemas

Reusable LocalLicense constructors that the rival accounts instantiate. The specific boundary (e.g. Egressy's Say) is a study's commitment; the schemas are shared.

def SequenceOfTense.relationalLicense : LocalLicense

Relational schema ([KZ18]): the clause's own relative tense, size-blind. Past = notAfter (≤) yields {lt, eq} = back-shift ∨ sim.

Equations

• SequenceOfTense.relationalLicense x✝ c = c.tense

def SequenceOfTense.sizeGatedLicense (boundary : Clause.Size) : LocalLicense

Generic size gate: an opaque clause (size not below boundary) loses the simultaneous (eq) atom; a transparent one keeps the full relative tense. This is the size half of a clause-size SOT account; it is not by itself the [Egr26] license, which also requires an agreeing past (see LocalLicense.gate and Studies.Egressy2026). On uniformly past-under-past data the two coincide; they diverge once an intervening future appears.

Equations

• SequenceOfTense.sizeGatedLicense boundary x✝ c = if Clause.transparentTo c.size boundary then c.tense else c.tense.erase Ordering.eq

def SequenceOfTense.LocalLicense.gate (L : LocalLicense) (g : Node → Node → Bool) : LocalLicense

Refine a license by an extra gate: keep its reading set, but drop the simultaneous atom .eq wherever the gate fails. A theory composes its licensing conditions as successive gates — the SOT rule is a size gate refined by an agreeing-past gate, i.e. (sizeGatedLicense b).gate agreeingPast.

Equations

• L.gate g a c = if g a c = true then L a c else (L a c).erase Ordering.eq

Pragmatic narrowing (layer 2: a constraint on the grammatical reading set)

Grammar (a LocalLicense) emits the grammatically available reading set; a pragmatic inference then narrows it — direct perception (one cannot perceive a past event), a cessation implicature (a past stative implicates non-overlap with now), etc. A narrowing is intersection with a context-conditioned constraint (a further point-algebra relation), so it can only remove readings, never license a new one — the grammar/pragmatics boundary, free from Finset.inter_subset_left rather than a stipulated law. The context C is whatever the inference consults (polarity, perception-directness, …).

@[reducible, inline]

abbrev SequenceOfTense.Narrowing (C : Type u_2) : Type u_2

A pragmatic narrowing: the point-algebra constraint it imposes, as a function of the context the inference consults.

Equations

• SequenceOfTense.Narrowing C = (C → Finset Ordering)

def SequenceOfTense.Narrowing.apply {C : Type u_2} (n : Narrowing C) (ctx : C) (s : Finset Ordering) : Finset Ordering

Narrow a grammatically-licensed reading set: intersect with the constraint.

Equations

• n.apply ctx s = s ∩ n ctx

theorem SequenceOfTense.Narrowing.apply_subset {C : Type u_2} (n : Narrowing C) (ctx : C) (s : Finset Ordering) : n.apply ctx s ⊆ s

Pragmatics filters, never licenses: narrowing only removes readings.

Worked example: the schemas diverge on an opaque past clause

A concrete demonstration that the interface carries weight: on an opaque past clause (grade 5, boundary 5), the relational schema licenses the simultaneous reading but the size-gated one does not.

def SequenceOfTense.exMatrix : Node

A matrix past clause (size below any boundary used here).

Equations

• SequenceOfTense.exMatrix = { tense := Core.Order.notAfter, size := 0 }

def SequenceOfTense.exOpaquePast : Node

An opaque past complement: grade 5, not below boundary 5.

Equations

• SequenceOfTense.exOpaquePast = { tense := Core.Order.notAfter, size := 5 }

def SequenceOfTense.exTransparentPast : Node

A transparent past complement: grade 0, below boundary 5.

Equations

• SequenceOfTense.exTransparentPast = { tense := Core.Order.notAfter, size := 0 }