Maximal Informativity Principle (MIP)

@cite{rouillard-2026} @cite{kennedy-2015} @cite{fox-2007}

The Maximal Informativity Principle is the licensing condition originally proposed for temporal in-adverbials (E-TIAs and G-TIAs) by Rouillard 2026, later recognized as the same mechanism that drives Kennedy 2015's de-Fregean type-shift for numerals. The unifying claim: given a measure function μ and a monotone degree property P, the maximally informative satisfying value is always μ(w) — the true value.

Frameworks unified

Construction	μ	Degree prop	Direction	MIP result
Numerals (Kennedy)	cardinality	atLeastDeg	down mono	max⊨ = μ(w)
Adjectives (Kennedy)	degree	atLeastDeg	down mono	max⊨ = μ(w)
E-TIAs (Rouillard)	runtime	atMostDeg	up mono	max⊨ = μ(w)

Operators

• etia — event-runtime time-of-interval adverbial domain (Rouillard 2026)
• gtia — general time-of-interval adverbial domain (always open → blocked)
• etia_telic_licensed / etia_atelic_blocked — predicted licensing
• gtia_blocked — G-TIAs always blocked (information collapse)

Renamed from rouillardETIA/rouillardGTIA per master plan v4 idea-naming discipline (file names + operators describe the IDEA, not the proposer). The proposer is cited in @cite{} blocks throughout.

Cross-framework agreement

The Kennedy numeral/adjective MIP-domain operators (DirectedMeasure.numeral, DirectedMeasure.adjective) live in Core/Scales/DirectedMeasure.lean since they're domain-general DirectedMeasure constructors. The Rouillard E-TIA/G-TIA operators live here because they have direction-negative as the lexically-fixed commitment (the MIP's central insight: atMostDeg + monotone runtime).

def Semantics.Gradability.MaximalInformativity.etia {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (b : Core.Scale.Boundedness) : Core.Scale.DirectedMeasure α W

@cite{rouillard-2026} E-TIA domain: event runtime ≤ interval size. Boundedness determined by Vendler class (telic → closed, atelic → open). Direction is negative (atMostDeg) per Rouillard's MIP analysis.

Equations

• Semantics.Gradability.MaximalInformativity.etia μ b = { boundedness := b, μ := μ, direction := Core.Scale.ScalePolarity.negative }

def Semantics.Gradability.MaximalInformativity.gtia {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : Core.Scale.DirectedMeasure α W

@cite{rouillard-2026} G-TIA domain: PTS extent on open intervals. Always open → always blocked (information collapse).

Equations

• Semantics.Gradability.MaximalInformativity.gtia μ = { boundedness := Core.Scale.Boundedness.open_, μ := μ, direction := Core.Scale.ScalePolarity.negative }

theorem Semantics.Gradability.MaximalInformativity.etia_telic_licensed {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : (etia μ Core.Scale.Boundedness.closed).licensed = true

Telic E-TIAs are licensed (closed runtime scale).

theorem Semantics.Gradability.MaximalInformativity.etia_atelic_blocked {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : (etia μ Core.Scale.Boundedness.open_).licensed = false

Atelic E-TIAs are blocked (open runtime scale).

theorem Semantics.Gradability.MaximalInformativity.gtia_blocked {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : (gtia μ).licensed = false

G-TIAs are always blocked (open PTS).

theorem Semantics.Gradability.MaximalInformativity.numeral_etia_same_licensing {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ₁ μ₂ : W → α) : (Core.Scale.DirectedMeasure.numeral μ₁).licensed = (etia μ₂ Core.Scale.Boundedness.closed).licensed

The deep isomorphism: a Kennedy numeral domain (positive direction) and a Rouillard E-TIA domain on a closed scale (negative direction) have identical licensing — boundedness alone determines the prediction.

theorem Semantics.Gradability.MaximalInformativity.four_frameworks_agree {α : Type u_1} [LinearOrder α] {W : Type u_2} (b : Core.Scale.Boundedness) (μ₁ μ₂ : W → α) : (Core.Scale.DirectedMeasure.adjective μ₁ b).licensed = (etia μ₂ b).licensed

All four frameworks (Kennedy adjectives, Rouillard E-TIAs, Krifka quantization, Zwarts paths) agree: licensing depends solely on boundedness. @cite{kennedy-2007} @cite{rouillard-2026} @cite{krifka-1989} @cite{zwarts-2005}.