Morphisms between gradability representations

[Kam75] [Kle80] [Ken99] [Ken07] [Sco14] [BS22]

The maps between the three framework objects for gradable predicates, with their faithfulness theorems — the degree-semantic analogue of the representation maps in Phonology/Autosegmental (AR ↔ tone strings):

Klein (Delineation)          — most general
  ↑ measureDelineation
Kennedy (measure functions)  — specialization: single linear scale
  ↑ DimensionedMeasure.apply
Scontras / Bale & Schwarz (typed measurement)

Each map is an embedding (ordering_faithful, measurement_refines_degree); the composite is measure_to_delineation. Strictness: delineation expresses nonlinear adjectives ("clever") that no degree function induces (delineation_strictly_more_general, nonlinear_delineation_exists).

What each framework adds

Framework	Ontology	Comparative	Unique capacity
Klein	No degrees	∃C. A(x,C) ∧ ¬A(y,C)	Nonlinear adjectives
Kennedy	Degrees (D,≤)	μ(x) > μ(y)	Measure phrases, DegP
Measurement	Degrees + dim	μ_d(x) > μ_d(y)	Typed dimensions, CARD

Theorems in this file

1. measure_to_degree: every DimensionedMeasure forgets to a plain degree function
2. degree_to_delineation: every degree function induces a Klein delineation
3. ordering_faithful: the induced delineation's ordering = degree comparison
4. degree_delineations_are_linear: all degree-induced delineations are linear
5. nonlinear_delineation_exists: a concrete nonlinear delineation witness
6. monotone_excludes_nonlinear: monotone delineations are never nonlinear
7. delineation_strictly_more_general: delineation ⊋ degree (strict containment)
8. nlDel_not_degree_representable: no degree function can induce the nonlinear witness
9. nondistinct_iff_equal_measure: Klein's emergent degrees = actual degree equality
10. degree_delineation_strict_weak_order: degree orderings are strict weak orders
11. very_degree_chain: Klein's very = two-step degree chain

Measurement → Degree → Delineation

The maps themselves carry no new definitions: measurement forgets to a bare degree function by the DimensionedMeasure.apply projection ([Sco14]'s insight that measure terms and CARD are one degree-assigning operation), and any degree function μ over a linear order induces a Klein delineation via Degree.Delineation.measureDelineation — the embedding of measure-function degree semantics ([Ken99], developed in [Ken07]) into [Kle80]'s framework. The embedding is faithful (ordering_iff_degree: Klein's ordering under the induced delineation is exactly degree comparison) and lands in the monotone, linear fragment (measureDelineation_monotone, measureDelineation_is_linear).

Strict Separation: Delineation > Degree

Klein's delineation framework is STRICTLY more general than degree semantics. The key witness: nonlinear adjectives like "clever" produce cyclic orderings (both a > b and b > a for different comparison classes). This is impossible for any degree-induced delineation, since degree orderings are asymmetric.

See `Studies/Klein1980.lean` for the empirical
motivation and the concrete "clever" witness. Here we prove the
theoretical separation at the framework level. 

theorem Degree.monotone_excludes_nonlinear {Entity : Type u_1} (delineation : Delineation.ComparisonClass Entity → Entity → Prop) (hmono : Delineation.IsMonotoneDelineation delineation Set.univ) (hnn : Delineation.IsNonlinearDelineation delineation) : False

Monotone delineations cannot be nonlinear: monotonicity forces asymmetry, which excludes cycles. This is the core constraint that degree semantics imposes — and that Klein's framework relaxes.

theorem Degree.nonlinear_delineation_exists : Delineation.IsNonlinearDelineation Degree.nlDel✝

theorem Degree.delineation_strictly_more_general : (∀ (E : Type u_1) (D : Type u_2) [inst : LinearOrder D] (μ : E → D), Delineation.IsMonotoneDelineation (Delineation.measureDelineation μ) Set.univ) ∧ ∃ (E : Type) (del : Delineation.ComparisonClass E → E → Prop), Delineation.IsNonlinearDelineation del

The strict separation theorem: Klein's delineation framework is strictly more general than degree-based frameworks.

Forward: every degree function induces a monotone delineation (measureDelineation_monotone).

Backward FAILS: there exist delineations (nonlinear ones) that no degree function can induce, because degree-induced delineations are always monotone, and monotonicity excludes nonlinearity.

This is the formal content of Klein's critique of degree semantics: multi-criteria adjectives like "clever" require the richer delineation framework.

Degree = Monotone Delineation (Characterization)

The degree-based frameworks correspond EXACTLY to the monotone fragment of Klein's delineation theory. This is not a coincidence: monotonicity is what ensures a delineation induces a well-behaved ordering (strict weak order), which is exactly what a degree scale provides.

- Forward: degree → monotone delineation (`measureDelineation_monotone`)
- Backward: monotone delineation → degree-recoverable ([klein-1980] §4.2,
  proved in `Klein1980.lean` as `kleinDegree_measureDelineation`)

Together: `degree semantics = monotone delineation semantics`.
Klein's full framework adds the non-monotone fragment for
multi-criteria adjectives. 

theorem Degree.degree_characterization {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) : Delineation.IsMonotoneDelineation (Delineation.measureDelineation μ) Set.univ ∧ Delineation.IsLinearDelineation (Delineation.measureDelineation μ) ∧ ∀ (cc : Delineation.ComparisonClass E) (a b : E), a ∈ cc → b ∈ cc → (Delineation.ordering (Delineation.measureDelineation μ) cc a b ↔ μ b < μ a)

Degree functions always yield monotone delineations AND the ordering is faithful. This characterizes exactly what degree semantics buys you within the delineation framework.

Measurement = Degree + Dimension Typing

The relationship between measurement semantics ([Sco14], [BS22]) and degree semantics ([Ken07]) is simple: measurement adds typed dimensions to degree functions.

A `DimensionedMeasure E` is a degree function `apply : E → ℚ` PLUS a
`dimension : Dimension` label. The degree function is recoverable
via `DimensionedMeasure.toHasDegree`, but the dimension label is lost.

What dimension typing buys you:
- Multiple measure functions per entity (weight AND volume AND count)
- The No Division Hypothesis: compositional operations respect dimension types
- Measure term semantics: ⟦kilo⟧ = λn.λx. μ_kg(x) = n, typed to mass

What it does NOT buy you: any new ordering structure. Measurement
adjectives are still degree adjectives under the hood. 

The degree construction ([Cre76] §4, [Bal08])

Degrees built from comparisons rather than assumed: [Cre76] (4.1) quotients an arbitrary comparison relation φ by two-sided φ-indistinguishability, and (4.2) shows the induced comparison on classes is well-defined. On a preorder the construction coincides with mathlib's Antisymmetrization (cresswellSetoid_le_iff). [Bal08] then maps any finite scale into the universal scale Ω ≅ ℚ ∩ (0, 1] by relative position (relativeRank), the homomorphism that licenses indirect cross-scale comparison.

def Degree.cresswellSetoid {E : Type u_1} (φ : E → E → Prop) : Setoid E

Two-sided indistinguishability under a comparison φ ([Cre76] (4.1)): same φ-profile on the left and right.

Equations

• Degree.cresswellSetoid φ = { r := fun (a b : E) => (∀ (c : E), φ a c ↔ φ b c) ∧ ∀ (c : E), φ c a ↔ φ c b, iseqv := ⋯ }

@[reducible, inline]

abbrev Degree.CresswellDegree {E : Type u_1} (φ : E → E → Prop) : Type u_1

Degrees of comparison as φ-equivalence classes ([Cre76] (4.1)).

Equations

• Degree.CresswellDegree φ = Quotient (Degree.cresswellSetoid φ)

def Degree.CresswellDegree.rel {E : Type u_1} {φ : E → E → Prop} : CresswellDegree φ → CresswellDegree φ → Prop

The induced comparison on degrees; well-definedness is [Cre76]'s own consistency proof for (4.2).

Equations

• Degree.CresswellDegree.rel = Quotient.lift₂ φ ⋯

@[simp]

theorem Degree.CresswellDegree.rel_mk {E : Type u_1} {φ : E → E → Prop} (a b : E) : rel ⟦a⟧ ⟦b⟧ ↔ φ a b

[Cre76] (4.2): ā >_φ b̄ iff φ(a, b).

theorem Degree.cresswellSetoid_le_iff {E : Type u_1} [Preorder E] (a b : E) : (cresswellSetoid fun (x1 x2 : E) => x1 ≤ x2) a b ↔ AntisymmRel (fun (x1 x2 : E) => x1 ≤ x2) a b

On a preorder, φ-indistinguishability under ≤ is mathlib's AntisymmRel: the Cresswell quotient IS Antisymmetrization.

def Degree.relativeRank {D : Type u_1} [Fintype D] [LinearOrder D] (d : D) : ℚ

[Bal08]'s universal-degree homomorphism on a finite scale: the relative position of d, valued in an order-isomorphic model of Ω (the paper takes Ω to be isomorphic to ℚ ∩ [0, 1]; only the order on the values is ever consumed — universal degrees are ordinal, not arithmetic). Defined on whatever carrier plays the primary scale — in Bale's regime the quotient, so equivalent individuals share a universal degree by construction and the value counts equivalence classes, not individuals.

Equations

• Degree.relativeRank d = ↑{x : D | x ≤ d}.card / ↑(Fintype.card D)

theorem Degree.relativeRank_strictMono {D : Type u_1} [Fintype D] [LinearOrder D] : StrictMono relativeRank

The universal-degree map preserves the primary scale's order ([Bal08]: ℌ preserves ≥_δ).

theorem Degree.relativeRank_mem_Ioc {D : Type u_1} [Fintype D] [LinearOrder D] (d : D) : relativeRank d ∈ Set.Ioc 0 1

Universal degrees land in (0, 1].

Transport: which operators are natural in the scale

The functoriality table for degree operators under change of scale representation (a StrictMono map between scales — precisely the admissibleMeasure condition, so an admissible measure IS a scale-morphism): comparatives, equatives, and the max-quantified comparative are invariant; the positive form transports only if the threshold rides along. This derives the classic observation that comparatives are context-independent while the positive form needs a contextually fixed standard: pos is the one non-natural operator.

theorem Degree.comparativeSem_comp {Entity : Type u_1} {D : Type u_2} {D' : Type u_3} [LinearOrder D] [Preorder D'] {f : D → D'} {μ : Entity → D} (hf : StrictMono f) (a b : Entity) (dir : Core.Order.ScalePolarity) : comparativeSem (f ∘ μ) a b dir ↔ comparativeSem μ a b dir

Comparatives are invariant under change of scale representation.

theorem Degree.equativeSem_comp {Entity : Type u_1} {D : Type u_2} {D' : Type u_3} [LinearOrder D] [Preorder D'] {f : D → D'} {μ : Entity → D} (hf : StrictMono f) (a b : Entity) (dir : Core.Order.ScalePolarity) : equativeSem (f ∘ μ) a b dir ↔ equativeSem μ a b dir

Equatives are invariant under change of scale representation.

theorem Degree.maxComparative_comp {Entity : Type u_1} {D : Type u_2} {D' : Type u_3} [LinearOrder D] [LinearOrder D'] {f : D → D'} {μ : Entity → D} (hf : StrictMono f) (Pmatrix Pthan : Entity → Prop) : maxComparative Pmatrix Pthan (f ∘ μ) ↔ maxComparative Pmatrix Pthan μ

The max-quantified comparative is invariant under change of scale representation. Not immediate: thanDegrees is a downset and images of downsets need not be downsets, but the greatest element rides along (f δ is greatest in the transported set, and conversely any greatest transported degree is f of a witness measure).

theorem Degree.mem_ge_over_comp {Entity : Type u_1} {D : Type u_2} {D' : Type u_3} [LinearOrder D] [LinearOrder D'] {f : D → D'} {μ : Entity → D} (hf : StrictMono f) (θ : D) (x : Entity) : x ∈ Core.Order.Comparison.ge.over (f ∘ μ) (f θ) ↔ x ∈ Core.Order.Comparison.ge.over μ θ

The positive form transports only as a pair: rescaling the measure commutes with membership when the threshold is rescaled too.

theorem Degree.positive_not_natural : ∃ (f : ℚ → ℚ), StrictMono f ∧ ∃ (μ : ℚ → ℚ) (θ : ℚ), ∃ x ∈ Core.Order.Comparison.ge.over μ θ, x ∉ Core.Order.Comparison.ge.over (f ∘ μ) θ

With a fixed threshold the positive form is not natural: some strictly monotone rescaling changes the verdict. The one non-natural operator in the table — the formal face of the positive form's context-dependence.

theorem Degree.factors_through_cresswellDegree {E : Type u_1} {X : Type u_2} {φ : E → E → Prop} (g : E → X) (hg : ∀ (a b : E), (cresswellSetoid φ) a b → g a = g b) : ∃ (ĝ : CresswellDegree φ → X), ĝ ∘ Quotient.mk (cresswellSetoid φ) = g

Universal property of the degree construction: any φ-invariant map factors through CresswellDegree φ — the quotient is the initial scale a comparison relation determines.