Rouillard 2026: Temporal in-Adverbials and the Maximal Informativity Principle

[Rou26] [FH06b] [Fox07] [BR99] [Kri89] [Kri98] [Ven57] [Lad79] [IZ21] [Hoe05] [Gaj11] [vFI19]

[Rou26] "Maximal informativity accounts for the distribution of temporal in-adverbials" (Linguistics and Philosophy 49:1–56).

Core contribution

Temporal in-adverbials (TIAs) lead a double life:

• E-TIAs ("wrote a paper in three days") measure event durations. Acceptable only with telic VPs.
• G-TIAs ("hasn't been sick in three days") measure gap durations. NPI behavior: acceptable only in negative perfects.

Both distributional restrictions follow from a single principle: the Maximal Informativity Principle (MIP). For some constituent γ containing the TIA, the numeral must be capable of being the maximally informative value of γ's derived property. Where no maximally informative numeral exists ("information collapse"), the TIA is blocked.

Main declarations

• eTIA_atelic_not_licensed: atelic E-TIAs fail MIP licensing — the subinterval property makes the derived property constant (information collapse).
• eTIA_telic_upwardMonotone / upwardMonotone_hasIsLeast_of_witness: telic E-TIAs are upward monotone, with a least-true numeral at the event duration.
• no_smallest_open_PTS_geometric: density witness — no smallest open PTS contains a given closed runtime.
• gTIAOpen_not_MIP_licensed: positive G-TIAs over dense time are not MIP-licensed (the end-to-end information-collapse discharge), with the ratLength model over ℚ witnessing satisfiability.
• downwardMonotone_hasIsGreatest_of_bound / gTIANeg_hasIsGreatest: negated G-TIAs have a greatest true numeral — the gap length.
• eTIA_all_predicted / gTIA_all_predicted / surviving_is_neg_gtia_pfv: the empirical predictions (the paper's Table 1).

def NonemptyInterval.BoundaryType.toBoundedness : BoundaryType → Core.Order.Boundedness

Interval boundary type maps to scale boundedness: closed runtimes correspond to closed scales (licensed), open PTSs to open scales (blocked/information collapse). [Rou26]'s interval generalization, consumed by the MIP licensing pipeline below.

Equations

• NonemptyInterval.BoundaryType.closed.toBoundedness = Core.Order.Boundedness.closed
• NonemptyInterval.BoundaryType.open_.toBoundedness = Core.Order.Boundedness.open_

theorem NonemptyInterval.closedBoundary_licensed : BoundaryType.closed.toBoundedness.IsLicensed

theorem NonemptyInterval.openBoundary_blocked : ¬BoundaryType.open_.toBoundedness.IsLicensed

@[implicit_reducible]

instance NonemptyInterval.instLicensingPipelineBoundaryType : Core.Order.LicensingPipeline BoundaryType

Equations

• NonemptyInterval.instLicensingPipelineBoundaryType = { toBoundedness := NonemptyInterval.BoundaryType.toBoundedness }

Time measure

class Rouillard2026.TimeMeasure (Time : Type u_4) [LinearOrder Time] {α : Type u_5} [AddCommMonoid α] [LinearOrder α] (μ : NonemptyInterval Time → α) extends Core.Order.IsIntervalContent μ : Prop

A temporal measure: an IsIntervalContent (additivity, [Rou26] eq. 6; positivity, eq. 7) together with two saturation axioms — richness of Time lets any interval be trimmed or right-anchored-extended to any target measure (PTSs are anchored at speech time). Instantiate α := ℕ for the discrete integer-numeral reading or α := ℚ≥0 over dense time for the reading that drives the G-TIA collapse (ratLength below).

• additive (a b c : Time) (hab : a ≤ b) (hbc : b ≤ c) : μ { fst := a, snd := c, fst_le_snd := ⋯ } = μ { fst := a, snd := b, fst_le_snd := hab } + μ { fst := b, snd := c, fst_le_snd := hbc }
• positive (a b : Time) (h : a < b) : 0 < μ { fst := a, snd := b, fst_le_snd := ⋯ }
• subdivisible (i : NonemptyInterval Time) (m : α) : m ≤ μ i → ∃ j ≤ i, μ j = m

  Any interval can be subdivided to a subinterval with a given smaller measure.

• extensibleLeft (i : NonemptyInterval Time) (m : α) : μ i ≤ m → ∃ (j : NonemptyInterval Time), i ≤ j ∧ j.toProd.2 = i.toProd.2 ∧ μ j = m

  Right-anchored left-extension: any interval can be extended to a given larger measure keeping its right endpoint fixed.

theorem Rouillard2026.TimeMeasure.extensible {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (i : NonemptyInterval Time) (m : α) (h : μ i ≤ m) : ∃ (j : NonemptyInterval Time), i ≤ j ∧ μ j = m

Any interval can be extended to a superinterval with a given larger measure: weakening of extensibleLeft (forget the right anchor).

Generalized intervals with open/closed boundaries

structure Rouillard2026.GInterval (Time : Type u_4) [LinearOrder Time] : Type u_4

A generalized interval with specified boundary types. Extends the basic NonemptyInterval with open/closed annotations on each end. [Rou26] eq. (14a–b), (99a–b).

• left : Time

  Left endpoint

• right : Time

  Right endpoint

• leftType : NonemptyInterval.BoundaryType

  Left boundary type: closed [m or open]m

• rightType : NonemptyInterval.BoundaryType

  Right boundary type: closed m] or open m[

• valid : self.left ≤ self.right

  The endpoints are ordered

def Rouillard2026.GInterval.closed {Time : Type u_2} [LinearOrder Time] (i : NonemptyInterval Time) : GInterval Time

A closed interval [m₁, m₂]: both endpoints included. [Rou26] eq. (14a): C := {t | min(t) ⊑ᵢ t ∧ max(t) ⊑ᵢ t}.

Equations

• Rouillard2026.GInterval.closed i = { left := i.toProd.1, right := i.toProd.2, leftType := NonemptyInterval.BoundaryType.closed, rightType := NonemptyInterval.BoundaryType.closed, valid := ⋯ }

def Rouillard2026.GInterval.open_ {Time : Type u_2} [LinearOrder Time] (i : NonemptyInterval Time) : GInterval Time

An open interval]m₁, m₂[: both endpoints excluded. [rouillard-2026] eq. (14b): O := {t | min(t) ⊄ᵢ t ∨ max(t) ⊄ᵢ t}.

Equations

• Rouillard2026.GInterval.open_ i = { left := i.toProd.1, right := i.toProd.2, leftType := NonemptyInterval.BoundaryType.open_, rightType := NonemptyInterval.BoundaryType.open_, valid := ⋯ }

def Rouillard2026.GInterval.toOpen {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : GInterval Time

The o(t) operation: open counterpart of a time. [Rou26] eq. (99a): if t is open, o(t) = t; if t is closed, o(t) is the open interval with the same endpoints.

Equations

• gi.toOpen = { left := gi.left, right := gi.right, leftType := NonemptyInterval.BoundaryType.open_, rightType := NonemptyInterval.BoundaryType.open_, valid := ⋯ }

def Rouillard2026.GInterval.toClosed {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : GInterval Time

The c(t) operation: closed counterpart of a time. [Rou26] eq. (99b): if t is closed, c(t) = t; if t is open, c(t) adds the endpoints.

Equations

• gi.toClosed = { left := gi.left, right := gi.right, leftType := NonemptyInterval.BoundaryType.closed, rightType := NonemptyInterval.BoundaryType.closed, valid := ⋯ }

def Rouillard2026.GInterval.isClosed {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : Prop

Is this interval closed (both boundaries included)?

Equations

• gi.isClosed = (gi.leftType = NonemptyInterval.BoundaryType.closed ∧ gi.rightType = NonemptyInterval.BoundaryType.closed)

def Rouillard2026.GInterval.isOpen {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : Prop

Is this interval open (both boundaries excluded)?

Equations

• gi.isOpen = (gi.leftType = NonemptyInterval.BoundaryType.open_ ∧ gi.rightType = NonemptyInterval.BoundaryType.open_)

def Rouillard2026.GInterval.gcontains {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) (m : Time) : Prop

Containment for generalized intervals: m is in gi. For closed endpoints, ≤ is used; for open endpoints, <.

Equations

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

def Rouillard2026.GInterval.gsubinterval {Time : Type u_2} [LinearOrder Time] (gi₁ gi₂ : GInterval Time) : Prop

Generalized subinterval: gi₁ ⊆ gi₂ (every moment in gi₁ is in gi₂).

Equations

• gi₁.gsubinterval gi₂ = ∀ (m : Time), gi₁.gcontains m → gi₂.gcontains m

def Rouillard2026.GInterval.toInterval {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : NonemptyInterval Time

Convert a closed GInterval back to the basic NonemptyInterval type.

Equations

• gi.toInterval = { fst := gi.left, snd := gi.right, fst_le_snd := ⋯ }

@[simp]

theorem Rouillard2026.GInterval.toClosed_isClosed {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toClosed.isClosed

The closed counterpart of an open interval is always closed.

@[simp]

theorem Rouillard2026.GInterval.toOpen_isOpen {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toOpen.isOpen

The open counterpart is always open.

@[simp]

theorem Rouillard2026.GInterval.toClosed_idempotent {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toClosed.toClosed = gi.toClosed

toClosed is idempotent.

@[simp]

theorem Rouillard2026.GInterval.toOpen_idempotent {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toOpen.toOpen = gi.toOpen

toOpen is idempotent.

@[simp]

theorem Rouillard2026.GInterval.closed_gcontains_start {Time : Type u_2} [LinearOrder Time] (i : NonemptyInterval Time) : (closed i).gcontains i.toProd.1

The closed counterpart of an interval contains its endpoints (definitional).

@[simp]

theorem Rouillard2026.GInterval.closed_gcontains_finish {Time : Type u_2} [LinearOrder Time] (i : NonemptyInterval Time) : (closed i).gcontains i.toProd.2

theorem Rouillard2026.GInterval.gsubinterval_closed_open_strict {Time : Type u_2} [LinearOrder Time] (rt : NonemptyInterval Time) (gi : GInterval Time) (h_open : gi.isOpen) (h_sub : (closed rt).gsubinterval gi) : gi.left < rt.toProd.1 ∧ rt.toProd.2 < gi.right

A closed interval contained in an open generalized interval forces strict inequalities at both endpoints: instantiate gsubinterval at the closed endpoints and unfold gcontains.

Prior time spans

def Rouillard2026.pts {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] (n : α) (μ : NonemptyInterval Time → α) [TimeMeasure Time μ] (s : Time) (gi : GInterval Time) : Prop

Prior time span: the maximal interval right-bounded by s with measure n, over GInterval so open-vs-closed boundary tags are carried structurally. [Rou26] eq. (50).

Equations

• Rouillard2026.pts n μ s gi = (gi.right = s ∧ μ gi.toInterval = n)

E-TIA semantics

def Rouillard2026.inETIA {Time : Type u_2} [LinearOrder Time] (e : Event Time) (bound : NonemptyInterval Time) : Prop

The preposition in as an event-level adverbial (E-TIA reading). The event's runtime is included in the measure-phrase's bound. [Rou26] eq. (62) instantiated at M = τ.

Equations

• Rouillard2026.inETIA e bound = (e.τ ≤ bound)

def Rouillard2026.eTIAProperty {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] (P : W → Event Time → Prop) (μ : NonemptyInterval Time → α) [TimeMeasure Time μ] (g1 : NonemptyInterval Time) : α → W → Prop

E-TIA derived property: at world w, value n is true iff there is a P-event whose runtime is included in some n-unit time, and that n-unit time falls within g1. [Rou26] eq. (77).

Equations

• Rouillard2026.eTIAProperty P μ g1 n w = ∃ (t : NonemptyInterval Time), μ t = n ∧ ∃ (e : Event Time), P w e ∧ e.τ ≤ g1 ∧ e.τ ≤ t

G-TIA semantics over open generalized intervals

def Rouillard2026.gTIAPropertyOpen {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] (P : W → Event Time → Prop) (μ : NonemptyInterval Time → α) [TimeMeasure Time μ] (s : Time) : α → W → Prop

G-TIA derived property: at world w, value n is true iff there is an OPEN PTS of measure n ending at s containing the closed runtime of a P-event. The openness of the PTS is carried structurally by GInterval. [Rou26] eq. (94) revised with eq. (101).

Equations

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

def Rouillard2026.gTIAPropertyOpenNeg {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] (P : W → Event Time → Prop) (μ : NonemptyInterval Time → α) [TimeMeasure Time μ] (s : Time) : α → W → Prop

The negation of gTIAPropertyOpen, used for G-TIAs in negative contexts (where the property "no event in the n-unit open PTS" holds iff gTIAPropertyOpen is false).

Equations

• Rouillard2026.gTIAPropertyOpenNeg P μ s n w = ¬Rouillard2026.gTIAPropertyOpen P μ s n w

theorem Rouillard2026.gTIAPropertyOpen_upwardMonotone {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (s : Time) : Degree.IsUpwardMonotone (gTIAPropertyOpen P μ s)

The positive G-TIA property is upward monotone: a wider gap window with the same right anchor still contains the event runtime, via TimeMeasure.extensibleLeft.

theorem Rouillard2026.gTIAPropertyOpenNeg_downwardMonotone {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (s : Time) : Degree.IsDownwardMonotone (gTIAPropertyOpenNeg P μ s)

The negated G-TIA property is downward monotone: if no event sits in the n-unit gap window, none sits in any narrower one. Discharges the monotonicity that gTIANeg_hasIsGreatest needs.

The MIP licensing predicate

MIP_Licensed and MIP_LicensedDown are defined in Semantics/Entailment/Extremum.lean and reused here. They combine Degree.AdmitsOptimum P (non-constancy: the atelic failure mode) with the per-world existence of a Set.IsLeast / Set.IsGreatest (mathlib): a most-informative numeral exists at some world. The two conjuncts capture two separate failure modes: information collapse (E-TIA atelic; fails AdmitsOptimum) and no-extremum (positive G-TIA; fails per-world IsLeast).

E-TIA atelic case: subinterval property → information collapse

theorem Rouillard2026.eTIA_atelic_collapse {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (g1 : NonemptyInterval Time) (hSub : Semantics.Aspect.SubintervalProperty.HasSubintervalProp P) : Degree.IsConstant (eTIAProperty P μ g1)

E-TIA information collapse for atelic VPs. When a VP has the subinterval property, the E-TIA derived property is constant: every numeral yields a true proposition at any world where any does, so no numeral is more informative than another. [Rou26] §4.1.1.

theorem Rouillard2026.eTIA_atelic_no_optimum {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (g1 : NonemptyInterval Time) (hSub : Semantics.Aspect.SubintervalProperty.HasSubintervalProp P) : ¬Degree.AdmitsOptimum (eTIAProperty P μ g1)

Atelic E-TIA fails the AdmitsOptimum half of MIP licensing.

theorem Rouillard2026.eTIA_atelic_not_licensed {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (g1 : NonemptyInterval Time) (hSub : Semantics.Aspect.SubintervalProperty.HasSubintervalProp P) : ¬Entailment.MIP_Licensed (eTIAProperty P μ g1)

Atelic E-TIA is not MIP-licensed.

E-TIA telic case: upward monotone, smallest-true at event duration

theorem Rouillard2026.eTIA_telic_upwardMonotone {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (g1 : NonemptyInterval Time) : Degree.IsUpwardMonotone (eTIAProperty P μ g1)

Quantized predicates yield upward-monotone E-TIA properties. [Rou26] §4.1.1: when P is telic, the derived E-TIA property is upward monotone — the same event witnesses larger measures via TimeMeasure.extensible.

theorem Rouillard2026.upwardMonotone_hasIsLeast_of_witness {W : Type u_4} {P : ℕ → W → Prop} (_hUp : Degree.IsUpwardMonotone P) (w : W) [DecidablePred fun (n : ℕ) => P n w] (h_witness : ∃ (n : ℕ), P n w) : ∃ (x : ℕ), IsLeast {y : ℕ | P y w} x

For an upward-monotone family with a witness at some world, the per-world set {y | P y w} has a least element via Nat.find. The statement is in mathlib idiom (IsLeast); the cross-world IsMaxInf bridge is in Extremum.lean (isMaxInf_of_isLeast_upward). Pinned to ℕ: extremum existence needs a well-founded codomain, which dense α deliberately lacks (that failure IS the G-TIA collapse below).

G-TIA geometric density: no smallest open PTS

theorem Rouillard2026.no_smallest_open_PTS_geometric {Time : Type u_2} [LinearOrder Time] [DenselyOrdered Time] (rt : NonemptyInterval Time) (ptsGI : GInterval Time) (h_open : ptsGI.isOpen) (h_sub : (GInterval.closed rt).gsubinterval ptsGI) : ∃ (ptsGI' : GInterval Time), ptsGI'.isOpen ∧ (GInterval.closed rt).gsubinterval ptsGI' ∧ ptsGI'.right = ptsGI.right ∧ ptsGI.left < ptsGI'.left

No smallest open PTS includes a closed runtime (geometric witness). [Rou26] §4.2.2: under density on Time, an open PTS containing a closed runtime always has a strictly smaller open PTS still containing it — pick a moment between the open boundary and the closed start.

gTIAOpen_no_isLeast below turns this into measure-level collapse via additivity and positivity; gTIAOpen_not_MIP_licensed is the end-to-end blocking result. (For α := ℕ over dense time the TimeMeasure axioms are unsatisfiable — positivity forces an infinite descending ℕ-chain — so the discrete reading lives on discrete Time only, where E-TIA results apply but the density argument does not.)

theorem Rouillard2026.gTIAOpen_no_isLeast {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [DenselyOrdered Time] [AddRightStrictMono α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (s : Time) (w : W) (x : α) : ¬IsLeast {y : α | gTIAPropertyOpen P μ s y w} x

Positive G-TIA: no least true value. Under dense Time, additivity and positivity let every witnessing open PTS shrink to a strictly smaller-measure open PTS still containing the runtime, so the per-world true set has no least element. [Rou26] §4.2.2.

theorem Rouillard2026.gTIAOpen_not_MIP_licensed {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {α : Type u_3} [AddCommMonoid α] [LinearOrder α] [DenselyOrdered Time] [AddRightStrictMono α] {μ : NonemptyInterval Time → α} [TimeMeasure Time μ] (P : W → Event Time → Prop) (s : Time) : ¬Entailment.MIP_Licensed (gTIAPropertyOpen P μ s)

Positive G-TIAs are not MIP-licensed over dense time: the least-true-numeral leg of MIP_Licensed fails at every world. The end-to-end discharge of the information-collapse argument ([Rou26] §4.2.2) that the ℕ-valued measure could not provide.

The rational length model

Non-vacuity witness: over Time := ℚ, interval length valued in ℚ≥0 is a TimeMeasure, so the hypotheses of gTIAOpen_not_MIP_licensed are jointly satisfiable at a concrete dense model.

def Rouillard2026.ratLength (i : NonemptyInterval ℚ) : ℚ≥0

Interval length over rational time, as a nonnegative rational.

Equations

• Rouillard2026.ratLength i = ⟨i.toProd.2 - i.toProd.1, ⋯⟩

instance Rouillard2026.instIsIntervalContentRatNNRatRatLength : Core.Order.IsIntervalContent ratLength

instance Rouillard2026.instTimeMeasureRatNNRatRatLength : TimeMeasure ℚ ratLength

Negated G-TIA: greatest true numeral at the gap length

theorem Rouillard2026.downwardMonotone_hasIsGreatest_of_bound {W : Type u_4} {P : ℕ → W → Prop} (hDown : Degree.IsDownwardMonotone P) (w : W) [DecidablePred fun (n : ℕ) => P n w] (h_witness : ∃ (n : ℕ), P n w) (h_bound : ∃ (n : ℕ), ¬P n w) : ∃ (x : ℕ), IsGreatest {y : ℕ | P y w} x

For a downward-monotone family over ℕ with a true witness and a failing bound at world w, the per-world set {y | P y w} has a greatest element. Dual of upwardMonotone_hasIsLeast_of_witness; the cross-world bridge is Extremum.isMaxInf_of_isGreatest_downward. Pinned to ℕ for the same well-foundedness reason as its dual.

theorem Rouillard2026.gTIANeg_hasIsGreatest {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {μ : NonemptyInterval Time → ℕ} [TimeMeasure Time μ] (P : W → Event Time → Prop) (s : Time) (w : W) [DecidablePred fun (n : ℕ) => gTIAPropertyOpenNeg P μ s n w] (h_witness : ∃ (n : ℕ), gTIAPropertyOpenNeg P μ s n w) (h_bound : ∃ (n : ℕ), ¬gTIAPropertyOpenNeg P μ s n w) : ∃ (x : ℕ), IsGreatest {y : ℕ | gTIAPropertyOpenNeg P μ s y w} x

Negated G-TIAs satisfy the MIP at the gap length. With a true witness and a failing bound, a greatest true numeral exists — [Rou26] eq. (104)/(110): there can be a largest open interval excluding a closed time, though never a smallest one including it. Downward monotonicity is supplied by gTIAPropertyOpenNeg_downwardMonotone (no longer hypothesis-gated).

Boundedness pipeline

The Vendler-class boundedness chain VendlerClass →.telicity Telicity →.toMereoTag MereoTag →.toBoundedness Boundedness consumed by the empirical predictions below. Codebase plumbing (Features.Aktionsart), not a claim from [Rou26].

theorem Rouillard2026.telic_predicts_licensing (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.telic) : (Core.Order.LicensingPipeline.toBoundedness c).IsLicensed

Telic VPs route through LicensingPipeline to the licensed (closed) boundedness tag.

theorem Rouillard2026.atelic_predicts_blocking (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.atelic) : ¬(Core.Order.LicensingPipeline.toBoundedness c).IsLicensed

Atelic VPs route through LicensingPipeline to the unlicensed (open) boundedness tag.

Cross-source licensing sentry

Formalizer synthesis, not attributable to [Rou26] — the paper engages only telicity/Vendler aspect and its own closed/open interval distinction. These sentries pin the bodies of every registered LicensingPipeline instance in one place, so a silent instance change is caught here; pairwise agreement between any two sources is LicensingPipeline.universal.

theorem Rouillard2026.sources_agree_closed : Core.Order.LicensingPipeline.IsLicensed Core.Order.Boundedness.closed ∧ Core.Order.LicensingPipeline.IsLicensed Core.Order.MereoTag.qua ∧ Core.Order.LicensingPipeline.IsLicensed Features.Telicity.telic ∧ Core.Order.LicensingPipeline.IsLicensed Features.VendlerClass.accomplishment ∧ Core.Order.LicensingPipeline.IsLicensed NonemptyInterval.BoundaryType.closed ∧ Core.Order.LicensingPipeline.IsLicensed Semantics.Aspect.SituationBoundedness.bounded ∧ Core.Order.LicensingPipeline.IsLicensed Core.Order.EpistemicTag.finitelyAdditive

Every registered LicensingPipeline source maps its "closed" variant to licensed.

theorem Rouillard2026.sources_agree_open : ¬Core.Order.LicensingPipeline.IsLicensed Core.Order.Boundedness.open_ ∧ ¬Core.Order.LicensingPipeline.IsLicensed Core.Order.MereoTag.cum ∧ ¬Core.Order.LicensingPipeline.IsLicensed Features.Telicity.atelic ∧ ¬Core.Order.LicensingPipeline.IsLicensed Features.VendlerClass.state ∧ ¬Core.Order.LicensingPipeline.IsLicensed NonemptyInterval.BoundaryType.open_ ∧ ¬Core.Order.LicensingPipeline.IsLicensed Semantics.Aspect.SituationBoundedness.unbounded ∧ ¬Core.Order.LicensingPipeline.IsLicensed Core.Order.EpistemicTag.qualitative

Every registered LicensingPipeline source maps its "open" variant to blocked.

Rouillard's analytical apparatus

inductive Rouillard2026.TIAType : Type

Rouillard's TIA-type classification. Paper-specific apparatus; not on Fragment entries themselves.

• eTIA : TIAType
• gTIA : TIAType

@[implicit_reducible]

instance Rouillard2026.instDecidableEqTIAType : DecidableEq TIAType

Equations

• Rouillard2026.instDecidableEqTIAType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rouillard2026.instReprTIAType.repr : TIAType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rouillard2026.instReprTIAType : Repr TIAType

Equations

• Rouillard2026.instReprTIAType = { reprPrec := Rouillard2026.instReprTIAType.repr }

inductive Rouillard2026.AdverbialPosition : Type

Rouillard's syntactic position for the in-adverbial. E-TIAs are VP-adjacent (event-level); G-TIAs are AspP-adjacent (perfect-level). [Rou26] schemata (57) (§3.2) and (61) (§3.3).

• eventLevel : AdverbialPosition
• perfectLevel : AdverbialPosition

@[implicit_reducible]

instance Rouillard2026.instDecidableEqAdverbialPosition : DecidableEq AdverbialPosition

Equations

• Rouillard2026.instDecidableEqAdverbialPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rouillard2026.instReprAdverbialPosition.repr : AdverbialPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rouillard2026.instReprAdverbialPosition : Repr AdverbialPosition

Equations

• Rouillard2026.instReprAdverbialPosition = { reprPrec := Rouillard2026.instReprAdverbialPosition.repr }

structure Rouillard2026.RouillardClassification : Type

Bundle of Rouillard's analytical labels for an in-adverbial.

• tiaType : TIAType
• position : AdverbialPosition

def Rouillard2026.instDecidableEqRouillardClassification.decEq (x✝ x✝¹ : RouillardClassification) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Rouillard2026.instDecidableEqRouillardClassification : DecidableEq RouillardClassification

Equations

• Rouillard2026.instDecidableEqRouillardClassification = Rouillard2026.instDecidableEqRouillardClassification.decEq

def Rouillard2026.instReprRouillardClassification.repr : RouillardClassification → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rouillard2026.instReprRouillardClassification : Repr RouillardClassification

Equations

• Rouillard2026.instReprRouillardClassification = { reprPrec := Rouillard2026.instReprRouillardClassification.repr }

def Rouillard2026.rouillardClassification? (e : English.TemporalExpressions.DurationExprEntry) : Option RouillardClassification

Project a DurationExprEntry to Rouillard's analytical labels. Returns none for entries outside the in-adverbial paradigm (forDur, ago).

Equations

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

E-TIA empirical data

structure Rouillard2026.ETIADatum : Type

E-TIA acceptability datum: VP class → acceptable with E-TIA? Acceptability is a decidable Prop field.

• vp : String

  Description of the VP

• vendlerClass : Features.VendlerClass

  Vendler class of the VP

• acceptable : Prop

  Whether "VP in three days" is acceptable

• acceptableDecidable : Decidable self.acceptable

def Rouillard2026.datum_1a : ETIADatum

(1a) "Mary wrote up a paper in three days." — accomplishment, ✓

Equations

• Rouillard2026.datum_1a = { vp := "write up a paper", vendlerClass := Features.VendlerClass.accomplishment, acceptable := True, acceptableDecidable := instDecidableTrue }

def Rouillard2026.datum_1b : ETIADatum

(1b) "*Mary was sick in three days." — state, ✗

Equations

• Rouillard2026.datum_1b = { vp := "be sick", vendlerClass := Features.VendlerClass.state, acceptable := False, acceptableDecidable := instDecidableFalse }

def Rouillard2026.datum_88 : ETIADatum

(88) "The climber reached the summit in three days." — achievement, ✓

Equations

• Rouillard2026.datum_88 = { vp := "reach the summit", vendlerClass := Features.VendlerClass.achievement, acceptable := True, acceptableDecidable := instDecidableTrue }

def Rouillard2026.datum_84 : ETIADatum

(84) "*The dancers waltzed in one hour." — activity, ✗

Equations

• Rouillard2026.datum_84 = { vp := "waltz", vendlerClass := Features.VendlerClass.activity, acceptable := False, acceptableDecidable := instDecidableFalse }

def Rouillard2026.eTIAData : List ETIADatum

Equations

• Rouillard2026.eTIAData = [Rouillard2026.datum_1a, Rouillard2026.datum_1b, Rouillard2026.datum_88, Rouillard2026.datum_84]

def Rouillard2026.eTIA_predicted (d : ETIADatum) : Prop

E-TIA acceptability matches the boundedness prediction: LicensingPipeline.toBoundedness d.vendlerClass is licensed iff the datum is acceptable. The pipeline routes through the Telicity → MereoTag → Boundedness chain (§ 11).

Equations

• Rouillard2026.eTIA_predicted d = ((Core.Order.LicensingPipeline.toBoundedness d.vendlerClass).IsLicensed ↔ d.acceptable)

@[implicit_reducible]

instance Rouillard2026.instDecidableETIA_predicted (d : ETIADatum) : Decidable (eTIA_predicted d)

Equations

• Rouillard2026.instDecidableETIA_predicted d = id inferInstance

theorem Rouillard2026.eTIA_all_predicted (d : ETIADatum) : d ∈ eTIAData → eTIA_predicted d

G-TIA empirical data

structure Rouillard2026.GTIADatum : Type

G-TIA acceptability datum: polarity × perfect → acceptable.

• sentence : String

  Description of the sentence

• isNegative : Prop

  Is the sentence negative?

• isNegativeDecidable : Decidable self.isNegative
• hasPerfect : Prop

  Does the sentence contain a perfect?

• hasPerfectDecidable : Decidable self.hasPerfect
• acceptable : Prop

  Whether the G-TIA is acceptable

• acceptableDecidable : Decidable self.acceptable

def Rouillard2026.datum_2a : GTIADatum

(2a) "Mary hasn't been sick in three days." — negative perfect, ✓

Equations

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

def Rouillard2026.datum_2b : GTIADatum

(2b) "*Mary has been sick in three days." — positive perfect, ✗

Equations

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

def Rouillard2026.datum_48 : GTIADatum

(48) "*Mary wasn't sick in three days." — negative, no perfect, ✗

Equations

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

def Rouillard2026.gTIAData : List GTIADatum

Equations

• Rouillard2026.gTIAData = [Rouillard2026.datum_2a, Rouillard2026.datum_2b, Rouillard2026.datum_48]

def Rouillard2026.gTIA_predicted (d : GTIADatum) : Prop

G-TIA acceptability matches the polarity ∧ perfect prediction. [Rou26] Table 1: only NEG + PFV with G-TIA reading survives MIP filtering. Stated at the surface polarity-and-perfect level; the structural halves are gTIAOpen_not_MIP_licensed (positive blocked) and gTIANeg_hasIsGreatest (negative licensed at the gap length).

Equations

• Rouillard2026.gTIA_predicted d = (d.isNegative ∧ d.hasPerfect ↔ d.acceptable)

@[implicit_reducible]

instance Rouillard2026.instDecidableGTIA_predicted (d : GTIADatum) : Decidable (gTIA_predicted d)

Equations

• Rouillard2026.instDecidableGTIA_predicted d = id inferInstance

theorem Rouillard2026.gTIA_all_predicted (d : GTIADatum) : d ∈ gTIAData → gTIA_predicted d

Table 1 (eq. 112): 8 cells with derived blocking

inductive Rouillard2026.Table1Polarity : Type

[Rou26] Table 1: readings for "Mary has been sick in three days" and its negation crossed with TIA type and aspect.

Polarity, TIA type, and aspect are enums (not Bool flags), so the table reads structurally rather than as a tuple of opaque booleans.

• positive : Table1Polarity
• negative : Table1Polarity

@[implicit_reducible]

instance Rouillard2026.instDecidableEqTable1Polarity : DecidableEq Table1Polarity

Equations

• Rouillard2026.instDecidableEqTable1Polarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Rouillard2026.instReprTable1Polarity : Repr Table1Polarity

Equations

• Rouillard2026.instReprTable1Polarity = { reprPrec := Rouillard2026.instReprTable1Polarity.repr }

def Rouillard2026.instReprTable1Polarity.repr : Table1Polarity → ℕ → Std.Format

Equations

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

inductive Rouillard2026.Table1Aspect : Type

• pfv : Table1Aspect
• impv : Table1Aspect

@[implicit_reducible]

instance Rouillard2026.instDecidableEqTable1Aspect : DecidableEq Table1Aspect

Equations

• Rouillard2026.instDecidableEqTable1Aspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rouillard2026.instReprTable1Aspect.repr : Table1Aspect → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rouillard2026.instReprTable1Aspect : Repr Table1Aspect

Equations

• Rouillard2026.instReprTable1Aspect = { reprPrec := Rouillard2026.instReprTable1Aspect.repr }

structure Rouillard2026.Table1Cell : Type

• polarity : Table1Polarity
• tiaType : TIAType
• aspect : Table1Aspect

def Rouillard2026.instDecidableEqTable1Cell.decEq (x✝ x✝¹ : Table1Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Rouillard2026.instDecidableEqTable1Cell : DecidableEq Table1Cell

Equations

• Rouillard2026.instDecidableEqTable1Cell = Rouillard2026.instDecidableEqTable1Cell.decEq

def Rouillard2026.instReprTable1Cell.repr : Table1Cell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rouillard2026.instReprTable1Cell : Repr Table1Cell

Equations

• Rouillard2026.instReprTable1Cell = { reprPrec := Rouillard2026.instReprTable1Cell.repr }

def Rouillard2026.table1Survives (c : Table1Cell) : Prop

A Table 1 cell survives MIP filtering iff it is the unique NEG + G-TIA + PFV configuration. Derived (not stipulated): every other cell is blocked by Rouillard's account, by various information-collapse mechanisms (positive cells: open-PTS density; E-TIA cells under negation: aspect mismatch with perfect; IMPV cells: U-perfect quantification mismatch).

Equations

• Rouillard2026.table1Survives c = (c.polarity = Rouillard2026.Table1Polarity.negative ∧ c.tiaType = Rouillard2026.TIAType.gTIA ∧ c.aspect = Rouillard2026.Table1Aspect.pfv)

@[implicit_reducible]

instance Rouillard2026.instDecidableTable1Survives (c : Table1Cell) : Decidable (table1Survives c)

Equations

• Rouillard2026.instDecidableTable1Survives c = id inferInstance

def Rouillard2026.table1 : List Table1Cell

All 8 Table 1 cells, generated by enumerating the three discriminators.

Equations

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

theorem Rouillard2026.surviving_is_neg_gtia_pfv : List.filter (fun (c : Table1Cell) => decide (table1Survives c)) table1 = [{ polarity := Table1Polarity.negative, tiaType := TIAType.gTIA, aspect := Table1Aspect.pfv }]

[Rou26] Table 1: exactly one cell survives — NEG + G-TIA + PFV.

Stacking constraint

[Rou26] §3.2, ex. (60). When two TIAs stack, the inner (VP-adjacent) one must be E-TIA and the outer must be G-TIA. The reverse order is ungrammatical. The position constraint follows from AdverbialPosition: E-TIA = eventLevel (VP-adjacent), G-TIA = perfectLevel (AspP-adjacent).

structure Rouillard2026.StackingDatum : Type

TIA stacking datum: inner and outer adverbial classifications.

• sentence : String
• innerType : TIAType
• innerPosition : AdverbialPosition
• outerType : TIAType
• outerPosition : AdverbialPosition
• acceptable : Prop
• acceptableDecidable : Decidable self.acceptable

def Rouillard2026.stacking_60a : StackingDatum

(60a) "Mary hasn't written up a paper in three days in two weeks." Inner E-TIA + outer G-TIA: acceptable.

Equations

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

def Rouillard2026.stacking_60b : StackingDatum

(60b) "#Mary hasn't written up a paper in two weeks in three days." Reversed order: unacceptable.

Equations

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

def Rouillard2026.stackingData : List StackingDatum

Equations

• Rouillard2026.stackingData = [Rouillard2026.stacking_60a, Rouillard2026.stacking_60b]

def Rouillard2026.stacking_predicted (d : StackingDatum) : Prop

Stacking is acceptable iff inner is event-level and outer is perfect-level. [Rou26] schemata (57) (§3.2) and (61) (§3.3).

Equations

• Rouillard2026.stacking_predicted d = (d.innerPosition = Rouillard2026.AdverbialPosition.eventLevel ∧ d.outerPosition = Rouillard2026.AdverbialPosition.perfectLevel ↔ d.acceptable)

@[implicit_reducible]

instance Rouillard2026.instDecidableStacking_predicted (d : StackingDatum) : Decidable (stacking_predicted d)

Equations

• Rouillard2026.instDecidableStacking_predicted d = id inferInstance

theorem Rouillard2026.stacking_all_predicted (d : StackingDatum) : d ∈ stackingData → stacking_predicted d

Since-when questions

[Rou26] §5.2, ex. (131): "Since when has Mary been sick?" lacks the E-perfect/U-perfect ambiguity of the corresponding declarative. Rouillard derives this via the MIP over the Hamblin sets: eq. (135) gives the U-perfect ANS, while the E-perfect set (reformulated as eq. (137)) has no maximally informative true answer (open-PTS density). The observation is originally [vFI19]'s; the density mechanism is [FH06b]'s. The datum below records the observation; the density mechanism for the blocked E-perfect reading is gTIAOpen_not_MIP_licensed (its Hamblin-set application is not formalized at this substrate level).

structure Rouillard2026.SinceWhenDatum : Type

Since-when question datum: which perfect readings are available? Observation-only (no prediction sentry): the Hamblin-set derivation is not formalized at this substrate level.

• sentence : String
• uPerfect : Prop
• uPerfectDecidable : Decidable self.uPerfect
• ePerfect : Prop
• ePerfectDecidable : Decidable self.ePerfect

def Rouillard2026.sinceWhen_131 : SinceWhenDatum

(131) "Since when has Mary been sick?" — U-perfect only.

Equations

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

Fragment bridges

theorem Rouillard2026.since_fragment_bridge : English.TemporalExpressions.since_conn.complementVeridical = true ∧ English.TemporalExpressions.since_conn.order = English.TemporalExpressions.TemporalOrder.since_

Fragment bridge: since is veridical and pins the PTS left boundary, matching the since-when question's presupposition.

theorem Rouillard2026.rouillard_classification : rouillardClassification? English.TemporalExpressions.inTelic = some { tiaType := TIAType.eTIA, position := AdverbialPosition.eventLevel } ∧ rouillardClassification? English.TemporalExpressions.inGap = some { tiaType := TIAType.gTIA, position := AdverbialPosition.perfectLevel }

The Rouillard projection assigns the expected analytical labels: E-TIA at event-level for telic-completion in; G-TIA at perfect-level for the NPI-gap in.

theorem Rouillard2026.rouillard_partial : rouillardClassification? English.TemporalExpressions.forDur = none ∧ rouillardClassification? English.TemporalExpressions.ago = none

Out-of-paradigm entries return none: for and ago are duration adverbials but not in-adverbials.