Rouillard 2026: temporal in-adverbials and maximal informativity

A temporal in-adverbial measures either an event, as in Mary wrote up a paper in three days (an E-TIA), or a gap in which no event occurs, as in Mary hasn't been sick in three days (a G-TIA). E-TIAs take telic but not atelic VPs, and G-TIAs are polarity items confined to negated perfects. Rouillard derives both from the Maximal Informativity Principle: the numeral must be able to be the maximally informative value of the property of numbers its constituent denotes. An atelic VP has the subinterval property, so its E-TIA property does not depend on the numeral. The perfect quantifies over open spans ending at speech time while run times are closed, so over dense time no open span including a run time is smallest, though one excluding it is largest; of the eight readings of Mary has been sick in three days and its negation, exactly one survives.

Main definitions

• IsTimeMeasure: an additive content on the spans of time, positive and onto the positive numbers on the spans ending at any time.
• duration: the measure of a closed time.
• IsMIPLicensed: licensing by maximal informativity, after Fox and Hackl.
• eTIA: the E-TIA property.
• gTIA: the G-TIA property.

Main results

• IsTimeMeasure.exists_Ioc_eq_of_ge, IsTimeMeasure.exists_Ioc_eq_of_le: (13), and the surjectivity of a measure onto the positive numbers.
• not_isMIPLicensed_eTIA: an atelic VP does not license an E-TIA.
• not_isMIPLicensed_gTIA: a positive G-TIA is not licensed over dense time.
• isMIPLicensed_gTIANeg: a negated G-TIA is licensed.
• table1_survivor: the one reading of Table 1 that survives.

Implementation notes

• A measure of time is an AddContent on the half-open spans Set.Ioc a b of a linearly ordered time T, so the additivity over non-overlapping times of (6) is the finite additivity of the content. A closed time [a, b] is measured by its half-open counterpart, as §2.2.4 allows for open intervals. The span of a moment is empty and measures 0, where the paper leaves moments outside the domain of μ.
• Numerals form a canonically ordered cancellative monoid, the paper's positive reals with 0.
• Positivity on nondegenerate spans is the axiom, and (7) follows (IsTimeMeasure.strictAntiOn); the paper derives positivity from (7).
• The paper assumes (13) and the surjectivity of μ onto the positive reals. Both follow from one stronger axiom, that pts(n, φ, s) of (50) is defined for every positive n and every s, and (13) then holds with a final part.
• The subinterval property is the closed one of Aspect/SubintervalProperty.lean, the paper's (111).

References

• [Rou26]
• [FH06b]

Measuring times (§2.2)

def Rouillard2026.duration {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (i : NonemptyInterval T) : α

The duration of a closed time is the measure of its half-open counterpart (§2.2.4).

Equations

• Rouillard2026.duration μ i = μ (Set.Ioc i.toProd.1 i.toProd.2)

theorem Rouillard2026.duration_mono {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [CanonicallyOrderedAdd α] : Monotone (duration μ)

A longer time has a longer duration.

class Rouillard2026.IsTimeMeasure {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) : Prop

An additive content on the half-open spans is a temporal measure when it is positive on nondegenerate spans and maps the spans ending at any time onto the positive numbers, so that pts(n, φ, s) of (50) is always defined.

• pos ⦃a b : T⦄ : a < b → 0 < μ (Set.Ioc a b)
• surjOn (s : T) : Set.SurjOn (fun (l : T) => μ (Set.Ioc l s)) (Set.Iio s) (Set.Ioi 0)

theorem Rouillard2026.IsTimeMeasure.pos_iff {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] {μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}} [IsTimeMeasure μ] {a b : T} : 0 < μ (Set.Ioc a b) ↔ a < b

A span has positive measure exactly when it is nondegenerate.

theorem Rouillard2026.IsTimeMeasure.strictAntiOn {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [IsOrderedCancelAddMonoid α] (s : T) : StrictAntiOn (fun (l : T) => μ (Set.Ioc l s)) (Set.Iic s)

Moving the start of a span later shortens it, which is (7) for abutting spans.

theorem Rouillard2026.IsTimeMeasure.exists_Ioc_eq {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [CanonicallyOrderedAdd α] (s : T) (n : α) : ∃ l ≤ s, μ (Set.Ioc l s) = n

Every number measures a span ending at any given time.

theorem Rouillard2026.IsTimeMeasure.exists_Ioc_eq_of_le {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] {μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}} [IsTimeMeasure μ] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] {a s : T} {n : α} (h : μ (Set.Ioc a s) ≤ n) : ∃ l ≤ a, μ (Set.Ioc l s) = n

Every larger number measures a leftward extension of a span, the surjectivity of a measure onto the positive numbers (§2.2.3).

theorem Rouillard2026.IsTimeMeasure.exists_Ioc_eq_of_ge {T : Type u_1} {α : Type u_2} [LinearOrder T] [AddCommMonoid α] [PartialOrder α] {μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}} [IsTimeMeasure μ] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] {a s : T} {n : α} (has : a ≤ s) (h : n ≤ μ (Set.Ioc a s)) : ∃ l ∈ Set.Icc a s, μ (Set.Ioc l s) = n

Every smaller number measures a final part of a span, (13).

The Maximal Informativity Principle (§4.1.3)

def Rouillard2026.IsMIPLicensed {W : Type u_1} {N : Type u_5} (φ : N → Set W) : Prop

A property of numbers is licensed when at some world the numeral is its unique maximally informative value, (92) with (75).

Equations

• Rouillard2026.IsMIPLicensed φ = ∃ (w : W), ∃! n : N, Question.IsStrongestTrueAnswer (Set.range φ) w (φ n)

theorem Rouillard2026.not_isMIPLicensed_of_forall_eq {W : Type u_1} {N : Type u_5} [Nontrivial N] {φ : N → Set W} (h : ∀ (n m : N), φ n = φ m) : ¬IsMIPLicensed φ

A property that does not depend on the numeral is not licensed, the information collapse.

theorem Rouillard2026.not_isMIPLicensed_of_not_isLeast {W : Type u_1} {N : Type u_5} [LinearOrder N] {φ : N → Set W} (hφ : Monotone φ) (h : ∀ (w : W) (n : N), ¬IsLeast {m : N | w ∈ φ m} n) : ¬IsMIPLicensed φ

An upward scalar property with no least true value is not licensed.

theorem Rouillard2026.isMIPLicensed_of_isGreatest {W : Type u_1} {N : Type u_5} [LinearOrder N] {φ : N → Set W} (hφ : StrictAnti φ) {w : W} (h : ∃ (n : N), IsGreatest {m : N | w ∈ φ m} n) : IsMIPLicensed φ

A strictly downward scalar property with a greatest true value at some world is licensed.

theorem Rouillard2026.isMIPLicensed_of_isLeast {W : Type u_1} {N : Type u_5} [LinearOrder N] {φ : N → Set W} (hφ : StrictMono φ) {w : W} (h : ∃ (n : N), IsLeast {m : N | w ∈ φ m} n) : IsMIPLicensed φ

A strictly upward scalar property with a least true value at some world is licensed.

E-TIAs (§4.1)

def Rouillard2026.eTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (Q : W → E → Prop) (n : α) : Set W

The E-TIA property (76) holds of n when n measures a time including a Q-event, Q being the event predicate the rest of the LF supplies ((78) for the simple past).

Equations

• Rouillard2026.eTIA μ Q n = {w : W | ∃ (t : NonemptyInterval T), Rouillard2026.duration μ t = n ∧ ∃ (e : E), Q w e ∧ Event.τ e ≤ t}

theorem Rouillard2026.eTIA_monotone {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] (Q : W → E → Prop) : Monotone (eTIA μ Q)

The E-TIA property is upward scalar, since a longer time still includes the event.

theorem Rouillard2026.eTIA_eq_of_hasSubintervalProperty {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] {Q : W → E → Prop} (hQ : Aspect.HasSubintervalProperty Q) (n m : α) : eTIA μ Q n = eTIA μ Q m

Under the subinterval property the E-TIA property does not depend on the numeral, the information collapse of (83).

theorem Rouillard2026.not_isMIPLicensed_eTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [Nontrivial α] {Q : W → E → Prop} (hQ : Aspect.HasSubintervalProperty Q) : ¬IsMIPLicensed (eTIA μ Q)

With an atelic VP, as in Mary was sick in three days, the E-TIA is not licensed.

theorem Rouillard2026.isLeast_eTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) {Q : W → E → Prop} {w : W} {e₀ : E} (h₀ : Q w e₀) (hmin : ∀ (e : E), Q w e → duration μ (Event.τ e₀) ≤ duration μ (Event.τ e)) : IsLeast {n : α | w ∈ eTIA μ Q n} (duration μ (Event.τ e₀))

In the telic case, at a world whose shortest Q-event is e₀, the least true numeral is its duration.

theorem Rouillard2026.isMIPLicensed_eTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) {Q : W → E → Prop} (hφ : StrictMono (eTIA μ Q)) {w : W} {e₀ : E} (h₀ : Q w e₀) (hmin : ∀ (e : E), Q w e → duration μ (Event.τ e₀) ≤ duration μ (Event.τ e)) : IsMIPLicensed (eTIA μ Q)

In Mary wrote up a paper in three days, when worlds differ in the event's duration, a telic VP is licensed at the world whose shortest event lasts the numeral's measure.

G-TIAs (§4.2)

def Rouillard2026.gTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (P : W → E → Prop) (s : T) (n : α) : Set W

The G-TIA property (101) holds of n when the open counterpart of the span of measure n ending at s, pts(n, d, s) of (50), includes the closed run time of a P-event.

Equations

• Rouillard2026.gTIA μ P s n = {w : W | ∃ (l : T), μ (Set.Ioc l s) = n ∧ ∃ (e : E), P w e ∧ ↑(Event.τ e) ⊆ Set.Ioo l s}

def Rouillard2026.gTIANeg {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (P : W → E → Prop) (s : T) (n : α) : Set W

gTIANeg is the negated G-TIA property (104).

Equations

• Rouillard2026.gTIANeg μ P s n = (Rouillard2026.gTIA μ P s n)ᶜ

theorem Rouillard2026.gTIA_monotone {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] (P : W → E → Prop) (s : T) : Monotone (gTIA μ P s)

theorem Rouillard2026.gTIANeg_antitone {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] (P : W → E → Prop) (s : T) : Antitone (gTIANeg μ P s)

theorem Rouillard2026.exists_lt_of_mem_gTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [DenselyOrdered T] {P : W → E → Prop} {s : T} {w : W} {n : α} (h : w ∈ gTIA μ P s n) : ∃ (m : α), 0 < m ∧ m < n ∧ w ∈ gTIA μ P s m

Under density every witnessing open span shrinks to a strictly smaller one, still positive in measure, that includes the same run time (§4.2.2).

theorem Rouillard2026.not_isLeast_gTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [DenselyOrdered T] (P : W → E → Prop) (s : T) (w : W) (n : α) : ¬IsLeast {m : α | w ∈ gTIA μ P s m} n

There is no smallest open span including a closed run time.

theorem Rouillard2026.not_isMIPLicensed_gTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [DenselyOrdered T] (P : W → E → Prop) (s : T) : ¬IsMIPLicensed (gTIA μ P s)

A positive G-TIA, as in Mary has been sick in three days, is not licensed over dense time.

theorem Rouillard2026.isGreatest_gTIANeg {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] {P : W → E → Prop} {s : T} {w : W} {l₀ : T} (hall : ∀ (e : E), P w e → (Event.τ e).toProd.1 ≤ l₀) (hwit : ∃ (e : E), P w e ∧ (Event.τ e).toProd.1 = l₀ ∧ (Event.τ e).toProd.2 < s) : IsGreatest {n : α | w ∈ gTIANeg μ P s n} (μ (Set.Ioc l₀ s))

When every P-event starts by l₀, and one starts exactly at l₀ and ends before s, the open span from l₀ to s is the largest excluding every P-event (§4.2.2): the greatest true numeral of the negated property is its measure.

theorem Rouillard2026.isMIPLicensed_gTIANeg {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] {P : W → E → Prop} {s : T} (hφ : StrictAnti (gTIANeg μ P s)) {w : W} {l₀ : T} (hall : ∀ (e : E), P w e → (Event.τ e).toProd.1 ≤ l₀) (hwit : ∃ (e : E), P w e ∧ (Event.τ e).toProd.1 = l₀ ∧ (Event.τ e).toProd.2 < s) : IsMIPLicensed (gTIANeg μ P s)

In Mary hasn't been sick in three days, when worlds separate the gap's length, a negated G-TIA is licensed at the world where the last event abuts the span.

The rational model

noncomputable def Rouillard2026.ratLength : MeasureTheory.AddContent ℚ≥0 {s : Set ℚ | ∃ (u : ℚ) (v : ℚ), u ≤ v ∧ s = Set.Ioc u v}

ratLength measures a span of rational time by its length.

Equations

• Rouillard2026.ratLength = { toFun := fun (s : Set ℚ) => ((MeasureTheory.AddContent.onIoc id) s).toNNRat, empty' := Rouillard2026.ratLength._proof_1, sUnion' := ⋯ }

theorem Rouillard2026.ratLength_Ioc {a b : ℚ} (h : a ≤ b) : ratLength (Set.Ioc a b) = (b - a).toNNRat

instance Rouillard2026.instIsTimeMeasureRatNNRatRatLength : IsTimeMeasure ratLength

Table 1 (§5.1.1)

The four readings of Mary has been sick in three days — E- or G-TIA under an E- or U-perfect (perfective or imperfective aspect) — and their negations, over the positive numerals.

def Rouillard2026.ePerfFrame {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (s : T) (w : W) (e : E) : Prop

The E-perfect hands an E-TIA the event predicate (114) of a P-event inside an open span ending at s.

Equations

• Rouillard2026.ePerfFrame P s w e = (P w e ∧ ∃ (l : T), ↑(Event.τ e) ⊆ Set.Ioo l s)

def Rouillard2026.uPerfFrame {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (s : T) (w : W) (e : E) : Prop

The U-perfect hands an E-TIA the event predicate (117) of a P-event including a nondegenerate open span ending at s.

Equations

• Rouillard2026.uPerfFrame P s w e = (P w e ∧ ∃ l < s, Set.Ioo l s ⊆ ↑(Event.τ e))

def Rouillard2026.uPerfGTIA {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (P : W → E → Prop) (s : T) (n : α) : Set W

The G-TIA property under a U-perfect, (122), holds when some nondegenerate open span ending at s lies inside a P-event and inside a time of measure n.

Equations

• Rouillard2026.uPerfGTIA μ P s n = {w : W | ∃ (t : NonemptyInterval T), Rouillard2026.duration μ t = n ∧ ∃ l < s, Set.Ioo l s ⊆ ↑t ∧ ∃ (e : E), P w e ∧ Set.Ioo l s ⊆ ↑(Event.τ e)}

theorem Rouillard2026.hasSubintervalProperty_ePerfFrame {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {s : T} (hP : Aspect.HasSubintervalProperty P) : Aspect.HasSubintervalProperty (ePerfFrame P s)

The E-perfect frame inherits the subinterval property.

theorem Rouillard2026.eTIA_uPerfFrame_eq {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [DenselyOrdered T] {P : W → E → Prop} {s : T} (hP : Aspect.HasSubintervalProperty P) {n m : α} (hn : 0 < n) (hm : 0 < m) : eTIA μ (uPerfFrame P s) n = eTIA μ (uPerfFrame P s) m

For positive numerals the U-perfect E-TIA property (117) collapses to (118) and does not depend on the numeral.

theorem Rouillard2026.uPerfGTIA_eq {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] {P : W → E → Prop} {s : T} {n m : α} (hn : 0 < n) (hm : 0 < m) : uPerfGTIA μ P s n = uPerfGTIA μ P s m

For positive numerals the U-perfect G-TIA property (122) collapses to (123) and does not depend on the numeral.

inductive Rouillard2026.Adverbial : Type

An Adverbial is event-level or gap-level.

• event : Adverbial
• gap : Adverbial

@[instance_reducible]

instance Rouillard2026.instDecidableEqAdverbial : DecidableEq Adverbial

Equations

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

inductive Rouillard2026.Viewpoint : Type

A Viewpoint is perfective (E-perfect) or imperfective (U-perfect) aspect under the perfect.

• pfv : Viewpoint
• impv : Viewpoint

@[instance_reducible]

instance Rouillard2026.instDecidableEqViewpoint : DecidableEq Viewpoint

Equations

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

def Rouillard2026.positiveReading {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (P : W → E → Prop) (s : T) : Adverbial → Viewpoint → α → Set W

positiveReading gives the four positive readings of Mary has been sick in three days.

Equations

• Rouillard2026.positiveReading μ P s Rouillard2026.Adverbial.event Rouillard2026.Viewpoint.pfv = Rouillard2026.eTIA μ (Rouillard2026.ePerfFrame P s)
• Rouillard2026.positiveReading μ P s Rouillard2026.Adverbial.event Rouillard2026.Viewpoint.impv = Rouillard2026.eTIA μ (Rouillard2026.uPerfFrame P s)
• Rouillard2026.positiveReading μ P s Rouillard2026.Adverbial.gap Rouillard2026.Viewpoint.pfv = Rouillard2026.gTIA μ P s
• Rouillard2026.positiveReading μ P s Rouillard2026.Adverbial.gap Rouillard2026.Viewpoint.impv = Rouillard2026.uPerfGTIA μ P s

def Rouillard2026.reading {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) (P : W → E → Prop) (s : T) (pol : Polarity) (a : Adverbial) (v : Viewpoint) (n : { n : α // 0 < n }) : Set W

reading gives a cell of Table 1 over the positive numerals, the positive reading under the row's polarity.

Equations

• Rouillard2026.reading μ P s pol a v n = pol • Rouillard2026.positiveReading μ P s a v ↑n

theorem Rouillard2026.table1_blocked {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] [DenselyOrdered T] [NoMaxOrder α] {P : W → E → Prop} {s : T} (hP : Aspect.HasSubintervalProperty P) (pol : Polarity) (a : Adverbial) (v : Viewpoint) (h : (pol, a, v) ≠ (Polarity.negative, Adverbial.gap, Viewpoint.pfv)) : ¬IsMIPLicensed (reading μ P s pol a v)

In Table 1 every cell but negated G-TIA under perfective aspect is blocked, the E-TIA cells and the imperfective G-TIA cell by information collapse, the positive perfective G-TIA by density, and negation preserves collapse.

theorem Rouillard2026.table1_survivor {W : Type u_1} {T : Type u_2} {E : Type u_3} {α : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] [AddCommMonoid α] [LinearOrder α] [IsOrderedCancelAddMonoid α] [CanonicallyOrderedAdd α] (μ : MeasureTheory.AddContent α {s : Set T | ∃ (u : T) (v : T), u ≤ v ∧ s = Set.Ioc u v}) [IsTimeMeasure μ] {P : W → E → Prop} {s : T} (hφ : StrictAnti (gTIANeg μ P s)) {w : W} {l₀ : T} (hall : ∀ (e : E), P w e → (Event.τ e).toProd.1 ≤ l₀) (hwit : ∃ (e : E), P w e ∧ (Event.τ e).toProd.1 = l₀ ∧ (Event.τ e).toProd.2 < s) : IsMIPLicensed (reading μ P s Polarity.negative Adverbial.gap Viewpoint.pfv)

The survivor of Table 1 is negated G-TIA under perfective aspect, licensed where worlds separate gap lengths and some world's last event abuts the span.