Extent Functions

@cite{kennedy-1999}

Given a measure function μ : Entity → D on a linearly ordered set, the extent functions partition the scale into degrees the entity "has" and degrees it "lacks":

• posExt(μ, x) = {d | d ≤ μ(x)} — the principal downset (positive extent)
• negExt(μ, x) = {d | μ(x) < d} — the strict upper set (negative extent)

These two sets are disjoint and exhaustive (they partition D).

Note on boundary convention: @cite{kennedy-1999} defines POSδ(a) = {p ∈ Sδ | p ≤ d(a)} and NEGδ(a) = {p ∈ Sδ | d(a) ≤ p}, with the boundary point d(a) in BOTH sets (a cover, not a partition). We use the strict inequality for negExt, placing d(a) in posExt only. This gives a true partition without affecting any linguistic claims — the key theorems (monotonicity, cross-polar anomaly, antonymy biconditional) hold under either convention.

Three degree-semantic frameworks independently arrived at the positive extent under different names:

Framework	Name	Motivation
Kennedy	degree set / pos-ext	antonymy, cross-polar
Heim	than-clause denotation	comparative composition
Schwarzschild	positive interval	differential measures

This module defines the common algebraic core that all three use.

def Core.Scale.posExt {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (x : Entity) : Set D

Positive extent: the set of degrees entity x "has" on scale μ. posExt(μ, x) = {d | d ≤ μ(x)}. This is the principal downset (initial segment) of μ(x).

Equations

• Core.Scale.posExt μ x = {d : D | d ≤ μ x}

def Core.Scale.negExt {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (x : Entity) : Set D

Negative extent: the set of degrees entity x "lacks" on scale μ. negExt(μ, x) = {d | μ(x) < d}. This is the strict upper set above μ(x). Negative adjectives (short, light) access the negative extent of the same underlying measure function as their positive counterpart.

Equations

• Core.Scale.negExt μ x = {d : D | μ x < d}

theorem Core.Scale.extent_disjoint {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (x : Entity) : posExt μ x ∩ negExt μ x = ∅

Extents are disjoint: no degree is both "had" and "lacked".

theorem Core.Scale.extent_exhaustive {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (x : Entity) : posExt μ x ∪ negExt μ x = Set.univ

Extents exhaust the scale: every degree is either had or lacked.

theorem Core.Scale.posExt_downward_closed {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (x : Entity) {d₁ d₂ : D} (h₁ : d₁ ≤ d₂) (h₂ : d₂ ∈ posExt μ x) : d₁ ∈ posExt μ x

Positive extent is downward closed.

theorem Core.Scale.negExt_upward_closed {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (x : Entity) {d₁ d₂ : D} (h₁ : d₁ < d₂) (h₂ : d₁ ∈ negExt μ x) : d₂ ∈ negExt μ x

Negative extent is upward closed (strict).

theorem Core.Scale.posExt_subset_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : posExt μ a ⊆ posExt μ b ↔ μ a ≤ μ b

Higher degree ↔ larger positive extent.

theorem Core.Scale.posExt_ssubset_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : posExt μ a ⊂ posExt μ b ↔ μ a < μ b

Strict extent inclusion ↔ strict degree ordering.

theorem Core.Scale.negExt_subset_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negExt μ a ⊆ negExt μ b ↔ μ b ≤ μ a

Higher degree ↔ SMALLER negative extent (reverse monotonicity).

theorem Core.Scale.negExt_ssubset_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negExt μ a ⊂ negExt μ b ↔ μ b < μ a

Strict negative extent inclusion ↔ strict degree ordering (reversed).

theorem Core.Scale.antonymy_biconditional {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : posExt μ b ⊂ posExt μ a ↔ negExt μ a ⊂ negExt μ b

Antonymy biconditional (@cite{kennedy-1999}): "A is taller than B" iff "B is shorter than A".

posExt(a) ⊃ posExt(b) ↔ negExt(b) ⊃ negExt(a)

This is the central theorem of @cite{kennedy-1999} Ch. 3: the equivalence of positive and negative comparative sentences is DERIVED from the complementarity of positive and negative extents, rather than stipulated as a lexical property of antonym pairs.

theorem Core.Scale.antonymy_biconditional_weak {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : posExt μ b ⊆ posExt μ a ↔ negExt μ a ⊆ negExt μ b

Weak antonymy biconditional (subset version): posExt(b) ⊆ posExt(a) ↔ negExt(a) ⊆ negExt(b).

def Core.Scale.crossExtentInclusion {Entity : Type u_1} {D : Type u_2} [Preorder D] (μ : Entity → D) (a b : Entity) : Prop

Cross-extent inclusion: posExt of one entity ⊆ negExt of another. This is the semantic content of a cross-polar equative like "Kim is as tall as Lee is short".

Equations

• Core.Scale.crossExtentInclusion μ a b = (Core.Scale.posExt μ a ⊆ Core.Scale.negExt μ b)

theorem Core.Scale.crossExtent_always_false {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : ¬crossExtentInclusion μ a b

Cross-extent inclusion is always false on any linear order. This is the algebraic core of the cross-polar anomaly: you cannot coherently compare a positive extent with a negative extent because they occupy complementary parts of the scale.