Compositional Comparative Derivation (@cite{wellwood-2015}, §2–3)

@cite{wellwood-2015} @cite{cariani-santorio-wellwood-2024} @cite{schwarzschild-2008}@cite{wellwood-2015} argues that comparatives across nominal, verbal, and adjectival domains share a uniform DegP pipeline yielding truth conditions of the form:

∃ea. role(a, ea) ∧ P(ea) ∧ ∀eb. role(b, eb) → P(eb) →
     μ(extract(eb)) < μ(extract(ea))

The three domains differ only in the thematic relation (role), the extraction function (extract), and what is measured:

Domain	role	extract	Measured	Example
Nominal	Agent	themeOf	Entity	"more coffee than"
Verbal	Agent	id	Event	"ran more than"
Adjectival	Holder	id	State	"hotter than"

Under unique-max assumptions (each individual has exactly one relevant eventuality), this reduces to direct comparison: μ(extract(ea)) > μ(extract(eb)), bridging to comparativeSem (Rett/Schwarzschild) and statesComparativeSem (CSW).

The DimensionallyRestricted predicate from Measurement.lean explains WHY dimension type tracks measured domain (§3.4):

• State domains (linear orders) → dimensionally restricted → unique dimension
• Entity/event domains (partial orders) → not restricted → multiple dimensions

inductive Semantics.Degree.Wellwood.ComparativeDomain : Type

The three comparative domains of @cite{wellwood-2015}. Each domain determines the thematic relation (role), extraction function, and measured ontological sort.

• nominal : ComparativeDomain
• verbal : ComparativeDomain
• adjectival : ComparativeDomain

instance Semantics.Degree.Wellwood.instDecidableEqComparativeDomain : DecidableEq ComparativeDomain

Equations

• Semantics.Degree.Wellwood.instDecidableEqComparativeDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Degree.Wellwood.instBEqComparativeDomain : BEq ComparativeDomain

Equations

• Semantics.Degree.Wellwood.instBEqComparativeDomain = { beq := Semantics.Degree.Wellwood.instBEqComparativeDomain.beq }

def Semantics.Degree.Wellwood.instBEqComparativeDomain.beq : ComparativeDomain → ComparativeDomain → Bool

Equations

• Semantics.Degree.Wellwood.instBEqComparativeDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Degree.Wellwood.instReprComparativeDomain : Repr ComparativeDomain

Equations

• Semantics.Degree.Wellwood.instReprComparativeDomain = { reprPrec := Semantics.Degree.Wellwood.instReprComparativeDomain.repr }

def Semantics.Degree.Wellwood.instReprComparativeDomain.repr : ComparativeDomain → ℕ → Std.Format

Equations

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

def Semantics.Degree.Wellwood.comparativeTruth {Entity : Type u_1} {Time : Type u_2} {Measured : Type u_3} [LE Time] (role : Entity → Events.Ev Time → Prop) (P : Events.EvPred Time) (extract : Events.Ev Time → Measured) (μ : Measured → ℚ) (a b : Entity) : Prop

Universal comparative truth condition (@cite{wellwood-2015}, eq. 35/43/59).

"a V-s more than b does" is true iff there exists an eventuality ea with role(a, ea) and P(ea) such that for ALL eventualities eb with role(b, eb) and P(eb), μ(extract(eb)) < μ(extract(ea)).

Parameters:

• role: thematic relation linking individual to eventuality (Agent for nominal/verbal, Holder for adjectival)
• P: event/state predicate (the VP or GA denotation)
• extract: what to measure from the eventuality (themeOf for nominal, id for verbal/adjectival)
• μ: measure function on the extracted domain

Equations

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

def Semantics.Degree.Wellwood.nominalComparative {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : Events.ThematicRoles.ThematicFrame Entity Time) (P : Events.EvPred Time) (themeOf : Events.Ev Time → Entity) (μ : Entity → ℚ) (a b : Entity) : Prop

Nominal comparative (Wellwood eq. 35): "Al bought more coffee than Bill did."

Equations

• Semantics.Degree.Wellwood.nominalComparative frame P themeOf μ a b = Semantics.Degree.Wellwood.comparativeTruth frame.agent P themeOf μ a b

def Semantics.Degree.Wellwood.verbalComparative {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : Events.ThematicRoles.ThematicFrame Entity Time) (P : Events.EvPred Time) (μ : Events.Ev Time → ℚ) (a b : Entity) : Prop

Verbal comparative (Wellwood eq. 43): "Al ran more than Bill did."

Equations

• Semantics.Degree.Wellwood.verbalComparative frame P μ a b = Semantics.Degree.Wellwood.comparativeTruth frame.agent P id μ a b

def Semantics.Degree.Wellwood.adjectivalComparative {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : Events.ThematicRoles.ThematicFrame Entity Time) (P : Events.EvPred Time) (μ : Events.Ev Time → ℚ) (a b : Entity) : Prop

Adjectival comparative (Wellwood eq. 59): "This coffee is hotter than that coffee."

Equations

• Semantics.Degree.Wellwood.adjectivalComparative frame P μ a b = Semantics.Degree.Wellwood.comparativeTruth frame.holder P id μ a b

theorem Semantics.Degree.Wellwood.comparativeTruth_max {Entity : Type u_1} {Time : Type u_2} {Measured : Type u_3} [LE Time] {role : Entity → Events.Ev Time → Prop} {P : Events.EvPred Time} {extract : Events.Ev Time → Measured} {μ : Measured → ℚ} {a b : Entity} {ea eb : Events.Ev Time} (ha : role a ea ∧ P ea) (ha_unique : ∀ (e : Events.Ev Time), role a e → P e → e = ea) (hb : role b eb ∧ P eb) (hb_unique : ∀ (e : Events.Ev Time), role b e → P e → e = eb) : comparativeTruth role P extract μ a b ↔ μ (extract eb) < μ (extract ea)

Maximality reduction (@cite{wellwood-2015}, passim).

Under unique-event assumptions — each individual has exactly one eventuality satisfying P with the appropriate role — the full truth condition reduces to direct comparison of measured values.

theorem Semantics.Degree.Wellwood.adjectival_max_reduces {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : Events.ThematicRoles.ThematicFrame Entity Time} {P : Events.EvPred Time} {μ : Events.Ev Time → ℚ} {a b : Entity} {sa sb : Events.Ev Time} (ha : frame.holder a sa ∧ P sa) (ha_unique : ∀ (s : Events.Ev Time), frame.holder a s → P s → s = sa) (hb : frame.holder b sb ∧ P sb) (hb_unique : ∀ (s : Events.Ev Time), frame.holder b s → P s → s = sb) : adjectivalComparative frame P μ a b ↔ μ sb < μ sa

Adjectival comparative under maximality reduces to direct state comparison: μ(sb) < μ(sa).

theorem Semantics.Degree.Wellwood.statesComparativeSem_is_lt {S : Type u_1} {D : Type u_2} [Preorder S] [Preorder D] (μ : S → D) (sa sb : S) : Lexical.Adjective.StatesBased.statesComparativeSem μ sa sb ↔ μ sb < μ sa

CSW's statesComparativeSem is definitionally the direct comparison μ sb < μ sa.

theorem Semantics.Degree.Wellwood.max_eq_comparativeSem {Entity : Type u_1} {Time : Type u_2} {Measured : Type u_3} [LE Time] {role : Entity → Events.Ev Time → Prop} {P : Events.EvPred Time} {extract : Events.Ev Time → Measured} {μ : Measured → ℚ} {a b : Entity} {ea eb : Events.Ev Time} (ha : role a ea ∧ P ea) (ha_unique : ∀ (e : Events.Ev Time), role a e → P e → e = ea) (hb : role b eb ∧ P eb) (hb_unique : ∀ (e : Events.Ev Time), role b e → P e → e = eb) : comparativeTruth role P extract μ a b ↔ Comparative.comparativeSem (μ ∘ extract) ea eb Core.Scale.ScalePolarity.positive

All comparative domains under maximality = comparativeSem (Rett/Schwarzschild).

The Wellwood pipeline under maximality reduces to the same direct comparison as comparativeSem from Degree.Comparative on measured values.

theorem Semantics.Degree.Wellwood.state_domain_restricted {S : Type u_1} [LinearOrder S] : Lexical.Measurement.DimensionallyRestricted S

State domains are dimensionally restricted when linearly ordered.

theorem Semantics.Degree.Wellwood.not_restricted_of_disagreement {α : Type u_1} [Preorder α] {μ₁ μ₂ : α → ℚ} (hμ₁ : StrictMono μ₁) (hμ₂ : StrictMono μ₂) {a b : α} (h₁ : μ₁ a < μ₁ b) (h₂ : ¬μ₂ a < μ₂ b) : ¬Lexical.Measurement.DimensionallyRestricted α

If two admissible measures disagree on some pair, the domain is NOT dimensionally restricted.