Morphisms between gradability representations

[Kam75] [klein-1980] [Ken99] [kennedy-2007] [scontras-2014] [bale-schwarz-2022]

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 ([scontras-2014]'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 [kennedy-2007]) into [klein-1980]'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 ([scontras-2014], [bale-schwarz-2022]) and degree semantics ([kennedy-2007]) 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, [bale-2008])

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). [bale-2008] 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 φ)

@[instance_reducible]

instance Degree.instLTCresswellDegree {E : Type u_1} {φ : E → E → Prop} : LT (CresswellDegree φ)

The comparison a relation induces on its degrees, ⟦a⟧ < ⟦b⟧ iff φ b a, strict exactly when φ is; well-definedness is [Cre76]'s own consistency proof for (4.2).

Equations

• Degree.instLTCresswellDegree = { lt := Quotient.lift₂ (fun (a b : E) => φ b a) ⋯ }

@[simp]

theorem Degree.CresswellDegree.mk_lt_mk {E : Type u_1} {φ : E → E → Prop} {a b : E} : ⟦a⟧ < ⟦b⟧ ↔ φ b a

[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) : ℚ

[bale-2008]'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 ([bale-2008]: ℌ 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].

Universal degrees of a ranking

def Degree.relativeRankIn {D : Type u_1} [LinearOrder D] (S : Finset D) (d : D) : ℚ

The relative position of d among the values of a finite scale S: the fraction of S at or below it. relativeRank is the case S = univ.

Equations

• Degree.relativeRankIn S d = ↑{x ∈ S | x ≤ d}.card / ↑S.card

theorem Degree.relativeRank_eq_relativeRankIn_univ {D : Type u_1} [LinearOrder D] [Fintype D] (d : D) : relativeRank d = relativeRankIn Finset.univ d

theorem Degree.relativeRankIn_lt_iff {D : Type u_1} [LinearOrder D] {S : Finset D} {d₁ d₂ : D} (h₁ : d₁ ∈ S) (h₂ : d₂ ∈ S) : relativeRankIn S d₁ < relativeRankIn S d₂ ↔ d₁ < d₂

theorem Degree.relativeRankIn_le_iff {D : Type u_1} [LinearOrder D] {S : Finset D} {d₁ d₂ : D} (h₁ : d₁ ∈ S) (h₂ : d₂ ∈ S) : relativeRankIn S d₁ ≤ relativeRankIn S d₂ ↔ d₁ ≤ d₂

theorem Degree.relativeRankIn_of_forall_le {D : Type u_1} [LinearOrder D] {S : Finset D} {d : D} (hd : d ∈ S) (hmax : ∀ x ∈ S, x ≤ d) : relativeRankIn S d = 1

The greatest value of a scale has degree one.

theorem Degree.relativeRankIn_of_forall_ge {D : Type u_1} [LinearOrder D] {S : Finset D} {d : D} (hd : d ∈ S) (hmin : ∀ x ∈ S, d ≤ x) : relativeRankIn S d = 1 / ↑S.card

The least value of a scale has degree one over the number of values.

def Degree.universalDegree {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] (rank : α → D) (x : α) : ℚ

[bale-2008]'s universal degree of x under the quasi-order a ranking induces: the relative position of rank x among the values the ranking takes. Equivalent elements share a degree, and the denominator counts equivalence classes, not elements.

Equations

• Degree.universalDegree rank x = Degree.relativeRankIn (Finset.image rank Finset.univ) (rank x)

theorem Degree.universalDegree_lt_iff {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] (rank : α → D) (x y : α) : universalDegree rank x < universalDegree rank y ↔ rank x < rank y

theorem Degree.universalDegree_le_iff {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] (rank : α → D) (x y : α) : universalDegree rank x ≤ universalDegree rank y ↔ rank x ≤ rank y

theorem Degree.universalDegree_lt_iff_of_image_eq {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] {β : Type u_3} [Fintype β] {rank₁ : α → D} {rank₂ : β → D} (h : Finset.image rank₁ Finset.univ = Finset.image rank₂ Finset.univ) (x : α) (y : β) : universalDegree rank₁ x < universalDegree rank₂ y ↔ rank₁ x < rank₂ y

Two rankings taking the same values are compared across scales as their values are: a direct comparison.

theorem Degree.universalDegree_comp_of_surjective {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] {α' : Type u_3} [Fintype α'] [DecidableEq α] (rank : α → D) {rep : α' → α} (hrep : Function.Surjective rep) (x : α') : universalDegree (rank ∘ rep) x = universalDegree rank (rep x)

Adding elements equivalent to existing ones changes no degree: the classes, not the elements, are counted.

theorem Degree.universalDegree_of_surjective {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] [Fintype D] {rank : α → D} (h : Function.Surjective rank) (x : α) : universalDegree rank x = relativeRank (rank x)

A ranking onto a finite linear order gives each element the relative rank of its value.

theorem Degree.universalDegree_of_forall_le {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] (rank : α → D) {x : α} (h : ∀ (y : α), rank y ≤ rank x) : universalDegree rank x = 1

An element ranked at least as high as every other has degree one.

theorem Degree.universalDegree_of_forall_ge {D : Type u_1} [LinearOrder D] {α : Type u_2} [Fintype α] (rank : α → D) {x : α} (h : ∀ (y : α), rank x ≤ rank y) : universalDegree rank x = 1 / ↑(Finset.image rank Finset.univ).card

An element ranked at most as high as every other has degree one over the number of classes.

theorem Degree.relativeRank_fin {n : ℕ} (k : Fin n) : relativeRank k = (↑↑k + 1) / ↑n

On Fin n, position k has relative rank (k + 1) / n.

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 : 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 : 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 ∈ Comparison.ge.over (f ∘ μ) (f θ) ↔ x ∈ 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 ∈ Comparison.ge.over μ θ, x ∉ 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.