Degree comparison: the point-standard core

[Ken99] [Ret26] [Sch08g] [vS84] [Hoe83]

Comparative semantics shared across all degree frameworks: the binary comparativeSem / equativeSem, antonymy as scale reversal, and downward-entailingness of than-clauses. Both binary comparators are measure-pullback predications of the reified Core.Order.Comparison (over at a point standard, overSet at a set standard); comparativeSem_positive_eq_over makes that an identity. The set-of-degrees S-comparative ([Hoe83]) is Comparison.gt.overSet μ directly — there is no separate clausal-comparison definition; its properties are stated about overSet here (anti-additivity) and reuse the Comparison.overSet/over API for the rest. Framework-specific content for [Ret26] (MAX, ambidirectionality, manner implicature) lives in Studies/Rett2026.lean; [Hoe83]'s polarity-asymmetry consumers in Studies/Hoeksema1983.lean.

Main declarations

• comparativeSem / equativeSem — "A is Adj-er / as-Adj-as B" via a directed measure on a scale.
• gtOverSet_isAntiAdditive — the S-comparative Comparison.gt.overSet μ ([Hoe83]) is anti-additive in its standard: the algebraic source of than-clause NPI licensing.
• mem_gtOverSet_iff_subset_Iio — the set-of-degrees comparative as Set.Iio interval inclusion (strict mirror of mathlib's mem_upperBounds_iff_subset_Iic), collapsing to the binary comparator at a singleton via Comparison.overSet_singleton.
• gtOverSet_eq_singleton_of_isGreatest — a than-clause with a greatest degree reduces to that degree ([BP04], order-theoretic form).
• maxComparative — the max-quantified clausal comparative ([vS84], [Rul95]): independent matrix/than witness predicates over thanDegrees, with the unique-witness collapse maxComparative_unique.
• taller_shorter_antonymy — antonymy is argument swap plus direction reversal.
• comparative_iff_Iic_ssubset — comparison as extent inclusion ([Ken99]).
• antonymy_biconditional / not_crossExtentInclusion — the antonymy biconditional derived from extent complementarity, and cross-polar anomaly as unsatisfiable extent inclusion ([Ken99]).

Comparative and equative semantics

def Degree.comparativeSem {Entity : Type u_1} {α : Type u_2} [Preorder α] (μ : Entity → α) (a b : Entity) (dir : Core.Order.ScalePolarity) : Prop

Comparative semantics over a measure function ([Ken99]; [Ret26], [Sch08g]): "A is Adj-er than B" iff μ a exceeds μ b on the directed scale. Only [Preorder α] — connectedness-agnostic background orderings (CSW confidence states) are in scope.

Equations

• Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive = (μ a > μ b)
• Degree.comparativeSem μ a b Core.Order.ScalePolarity.negative = (μ a < μ b)

def Degree.equativeSem {Entity : Type u_1} {α : Type u_2} [Preorder α] (μ : Entity → α) (a b : Entity) (dir : Core.Order.ScalePolarity) : Prop

Equative semantics: "A is as Adj as B" iff μ a ≥ μ b on the directed scale.

Equations

• Degree.equativeSem μ a b Core.Order.ScalePolarity.positive = (μ a ≥ μ b)
• Degree.equativeSem μ a b Core.Order.ScalePolarity.negative = (μ a ≤ μ b)

theorem Degree.comparativeSem_positive_eq_over {Entity : Type u_1} {α : Type u_2} [Preorder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ a ∈ Core.Order.Comparison.gt.over μ (μ b)

Grounding: the positive binary comparative is the strict-> point predication of Core.Order.Comparison at the standard μ b — not a reinvention.

theorem Degree.equativeSem_positive_eq_over {Entity : Type u_1} {α : Type u_2} [Preorder α] (μ : Entity → α) (a b : Entity) : equativeSem μ a b Core.Order.ScalePolarity.positive ↔ a ∈ Core.Order.Comparison.ge.over μ (μ b)

Grounding: the positive equative is the ≥ point predication of Core.Order.Comparison at the standard μ b.

theorem Degree.comparativeSem_eq_MAX {Entity : Type u_1} {β : Type u_3} [LinearOrder β] (μ : Entity → β) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ ∃ m ∈ Core.Order.maxOnScale Core.Order.Comparison.gt {μ b}, μ a > m

MAX–direct bridge: the direct comparison μ a > μ b is equivalent to the MAX-based formulation.

Antonymy as scale reversal

theorem Degree.taller_shorter_antonymy {Entity : Type u_1} {α : Type u_2} [Preorder α] (μ : Entity → α) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ comparativeSem μ b a Core.Order.ScalePolarity.negative

"A taller than B" ↔ "B shorter than A" — antonymy is argument swap plus direction reversal.

theorem Degree.equative_antonymy {Entity : Type u_1} {α : Type u_2} [Preorder α] (μ : Entity → α) (a b : Entity) : equativeSem μ a b Core.Order.ScalePolarity.positive ↔ equativeSem μ b a Core.Order.ScalePolarity.negative

Equative antonymy: "A as tall as B" ↔ "B as short as A".

Boundary dependence

theorem Degree.comparative_boundary {α : Type u_1} [LinearOrder α] (μ_a μ_b : α) : (∃ m ∈ Core.Order.maxOnScale Core.Order.Comparison.ge {d : α | d ≤ μ_b}, μ_a > m) ↔ μ_a > μ_b

The comparative depends only on the boundary μ_b.

theorem Degree.equative_boundary {α : Type u_1} [LinearOrder α] (μ_a μ_b : α) : (∃ m ∈ Core.Order.maxOnScale Core.Order.Comparison.ge {d : α | d ≤ μ_b}, μ_a ≥ m) ↔ μ_a ≥ μ_b

The equative depends only on the boundary μ_b.

Comparison as extent inclusion

Kennedy's positive/negative extents are Set.Iic (μ x) / Set.Ioi (μ x) directly ([Ken99]); the binary comparator equals strict extent inclusion, and antonymy follows from extent complementarity rather than being stipulated. Boundary convention: the paper's eqs (30)–(31) define both extents with ≤ (a cover); the strict Ioi here is a strict partition, and the antonymy biconditional (eq (54)) is convention-independent.

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

Cross-polar inclusion: one entity's positive extent inside another's negative extent — the LF a cross-polar equative ("as tall as Lee is short") would assign ([Ken99]).

Equations

• Degree.crossExtentInclusion μ a b = (Set.Iic (μ a) ⊆ Set.Ioi (μ b))

theorem Degree.gtOverSet_atomic_eq_comparativeSem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : a ∈ Core.Order.Comparison.gt.overSet μ {μ b} ↔ comparativeSem μ a b Core.Order.ScalePolarity.positive

Bridge: the atomic S-comparative Comparison.gt.overSet μ {μ b} coincides with the binary comparativeSem on a LinearOrder. The set-of-degrees schema strictly generalizes the binary comparator, collapsing at a singleton via Comparison.overSet_singleton.

theorem Degree.comparative_iff_Iic_ssubset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ Set.Iic (μ b) ⊂ Set.Iic (μ a)

"A is taller than B" iff A's positive extent (Set.Iic (μ a), [Ken99]) strictly contains B's.

theorem Degree.comparative_iff_Ioi_ssubset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ Set.Ioi (μ a) ⊂ Set.Ioi (μ b)

"A taller than B" iff "B shorter than A" on the negative extents (Set.Ioi), derived rather than stipulated ([Ken99]).

theorem Degree.antonymy_biconditional {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Set.Iic (μ b) ⊂ Set.Iic (μ a) ↔ Set.Ioi (μ a) ⊂ Set.Ioi (μ b)

Antonymy biconditional ([Ken99] eq (54)): "A is taller than B" iff "B is shorter than A", derived from extent complementarity.

theorem Degree.extent_galois_antitone {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Set.Iic (μ a) ⊆ Set.Iic (μ b) ↔ Set.Ioi (μ b) ⊆ Set.Ioi (μ a)

Weak-inclusion antonymy: the Galois-antitone face of the biconditional.

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

Cross-polar inclusion never holds on a linear order — the lattice-algebraic shadow of [Ken99]'s sortal cross-polar anomaly argument (§3.1.7).

Strengthened, negated, and extent-theoretic equatives

[Ken07] [rett-2020-equatives] [Sch08g] [TD20]

The literal equative is "at least as" (equativeSem .positive); the "exactly as" reading is derived by scalar implicature (choosing as tall as over the stronger taller than). A granularity-based alternative is in Degree.Granularity.

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

Equative strengthened semantics: "A is as tall as B" iff μ a = μ b — the "exactly as" reading, derived by implicature.

Equations

• Degree.equativeStrengthened μ a b = (μ a = μ b)

theorem Degree.equativeStrengthened_entails_sem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (h : equativeStrengthened μ a b) : equativeSem μ a b Core.Order.ScalePolarity.positive

The strengthened reading entails the literal ≥ reading.

def Degree.negatedEquative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Prop

Negated equative: "A is not as tall as B" iff μ a < μ b.

Equations

• Degree.negatedEquative μ a b = (μ a < μ b)

theorem Degree.negatedEquative_iff_not_sem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negatedEquative μ a b ↔ ¬equativeSem μ a b Core.Order.ScalePolarity.positive

Negated equative is the negation of the literal equative.

theorem Degree.equativeSem_iff_Iic_subset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : equativeSem μ a b Core.Order.ScalePolarity.positive ↔ Set.Iic (μ b) ⊆ Set.Iic (μ a)

Equative as positive extent inclusion ([Ken99]): "A is as tall as B" iff every degree B has (Set.Iic (μ b)), A also has.

theorem Degree.equativeSem_iff_Ioi_subset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : equativeSem μ a b Core.Order.ScalePolarity.positive ↔ Set.Ioi (μ a) ⊆ Set.Ioi (μ b)

Equative antonymy on negative extents: "A is as tall as B" iff "B is as short as A" (Set.Ioi inclusion in the reversed direction).

theorem Degree.negatedEquative_iff_Iic_ssubset {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : negatedEquative μ a b ↔ Set.Iic (μ a) ⊂ Set.Iic (μ b)

Negated equative as strict extent inclusion: B has strictly more degrees than A.

Subcomparatives

[SW02a]

def Degree.subcomparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ₁ μ₂ : Entity → D) (a b : Entity) : Prop

Subcomparative ("longer than it is wide"): two commensurable measure functions compared in shared units.

Equations

• Degree.subcomparative μ₁ μ₂ a b = (μ₁ a > μ₂ b)