Klein's Delineation Approach

@cite{klein-1980} @cite{kennedy-2007} @cite{kamp-1975}

@cite{klein-1980} "A Semantics for Positive and Comparative Adjectives": a degree-free analysis where gradable adjectives are simple predicates (type ⟨e,t⟩) whose extension is determined relative to a comparison class — a contextually supplied set of entities.

Lineage from Kamp (1975)

Klein's comparative — ∃ C. tall(a,C) ∧ ¬tall(b,C) — is a direct formalization of @cite{kamp-1975}'s definition (12): u₁ is at least as A as u₂ iff in every completion where u₂ is in the extension, u₁ is too. Kamp's "completions" become Klein's "comparison classes"; both derive the comparative from existential quantification over ways of making a vague predicate precise.

Key Ideas

1. No degrees: "tall" does not denote a relation between entities and degrees. It is simply a predicate whose extension varies with context.

2. Comparison class: The positive form "Kim is tall" is true iff Kim is tall relative to the contextually relevant comparison class C (e.g., basketball players, children, people in general).

3. Comparative via supervaluation: "Kim is taller than Lee" is true iff there exists a comparison class C where Kim is tall and Lee is not. This uses a supervaluation over comparison classes rather than degree comparison.

Comparison with Kennedy

Feature	@cite{kennedy-2007}	@cite{klein-1980}
Ontology	Degrees exist	No degrees
⟦tall⟧	λd.λx. height(x) ≥ d	λx. tall(x) in C
Comparative	max > max	∃C. tall(x) ∧ ¬tall(y)
Vagueness	Threshold variability	Comparison class var.
Comparison class	Not a semantic argument	Semantic argument of pos
Measure phrases	Direct (3 inches of d)	Via ≈-classes (§4.2)

@cite{kennedy-2007} argues (§2.2–2.3) that the comparison class is NOT a semantic argument of pos (contra Klein). Instead, the standard is determined by a context-sensitive function s (eq 27) that may draw on domain information descriptively called a "comparison class" but which "does not correspond to a constituent of the logical form" (p. 16).

Klein handles degree modifiers via comparison-class narrowing (§4.1, eqs 42–43) and measure phrases via equivalence classes on a measurement scale (§4.2), though the degree-based treatment is arguably more direct.

For the formal subsumption hierarchy (Klein ← Kennedy ← Measurement), see Theories/Semantics/Comparison/Hierarchy.lean.

@[reducible, inline]

abbrev Semantics.Gradability.Delineation.ComparisonClass (Entity : Type u_1) : Type u_1

A comparison class: a set of entities relevant for evaluating a gradable predicate. In Klein's framework, this is the only contextual parameter — there are no degrees or thresholds.

Equations

• Semantics.Gradability.Delineation.ComparisonClass Entity = Set Entity

def Semantics.Gradability.Delineation.comparativeSem {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (a b : Entity) : Prop

Klein's comparative: "Kim is taller than Lee" is true iff there EXISTS a comparison class C such that Kim is tall-in-C but Lee is not tall-in-C.

This is a supervaluation over comparison classes: the comparative holds when the predicate can discriminate the two entities.

Equations

• Semantics.Gradability.Delineation.comparativeSem delineation a b = ∃ (C : Semantics.Gradability.Delineation.ComparisonClass Entity), delineation C a ∧ ¬delineation C b

def Semantics.Gradability.Delineation.IsMonotoneDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (allClasses : Set (ComparisonClass Entity)) : Prop

Klein's comparative is asymmetric: if a is taller than b, then b is not taller than a.

This requires the monotonicity constraint on delineations: if a is tall-in-C and b is not, then for any C' where b is tall, a is also tall. Without this constraint, the comparative can fail to be asymmetric.

Equations

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

@cite{klein-1980}'s comparative is the existential dual of @cite{fine-1975}'s supervaluation. Where supervaluation asks "true at ALL specifications?", Klein asks "true at SOME specification where the other is false?" Both quantify over the same space — comparison classes (Klein) = specification points (Fine). The positive form "a is tall" maps to superTrue (delineation · a), and Klein's comparative ∃ C. tall(a,C) ∧ ¬tall(b,C) captures the asymmetry between a's and b's supervaluation status.

Under monotone delineation, Klein's comparative entails Fine's
comparative entailment: if b is super-true (tall in every comparison
class), then a — who is at least as tall — must also be super-true. 

theorem Semantics.Gradability.Delineation.monotone_comparative_superTrue {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) [(C : ComparisonClass Entity) → (x : Entity) → Decidable (delineation C x)] (a b : Entity) (S : Supervaluation.SpecSpace (ComparisonClass Entity)) (hmono : ∀ C₁ ∈ S.admissible, ∀ C₂ ∈ S.admissible, ∀ (x y : Entity), delineation C₁ x → ¬delineation C₁ y → delineation C₂ y → delineation C₂ x) (hdisc : ∃ C ∈ S.admissible, delineation C a ∧ ¬delineation C b) (hb : Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C b) = true) S = Core.Duality.Truth3.true) : Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C a) = true) S = Core.Duality.Truth3.true

Under monotone delineation, Klein's comparative entails Fine's comparative entailment: if b is super-true, a is super-true.

The proof extracts the discriminating comparison class C₀ (where a is tall but b isn't), then uses monotonicity: in any class C₂ where b is tall, a must also be tall.

theorem Semantics.Gradability.Delineation.comparative_prevents_superTrue {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) [(C : ComparisonClass Entity) → (x : Entity) → Decidable (delineation C x)] (a b : Entity) (S : Supervaluation.SpecSpace (ComparisonClass Entity)) (hdisc : ∃ C ∈ S.admissible, delineation C a ∧ ¬delineation C b) : Supervaluation.superTrue (fun (C : ComparisonClass Entity) => decide (delineation C b) = true) S ≠ Core.Duality.Truth3.true

Klein's comparative witnesses supervaluation indefiniteness for b: if a is taller than b (∃ discriminating class IN the space), then b is not super-true — the discriminating class falsifies b.

def Semantics.Gradability.Delineation.PartialDelineation (Entity : Type u_1) : Type u_1

Klein's partial extension function (§2.3, eq 12). For a vague predicate ζ at context c, F_ζ(c) assigns each entity in the comparison class to the positive extension (some true), negative extension (some false), or the extension gap (none).

The total delineation in §§1–5 is the special case where every entity receives a definite value (no gap).

Equations

• Semantics.Gradability.Delineation.PartialDelineation Entity = (Semantics.Gradability.Delineation.ComparisonClass Entity → Entity → Option Bool)

def Semantics.Gradability.Delineation.PartialDelineation.posExt {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) : Set Entity

Positive extension: pos_ζ(c) = {u ∈ U : F_ζ(c)(u) = 1} (eq 13i).

Equations

• d.posExt C = {x : Entity | d C x = some true}

def Semantics.Gradability.Delineation.PartialDelineation.negExt {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) : Set Entity

Negative extension: neg_ζ(c) = {u ∈ U : F_ζ(c)(u) = 0} (eq 13ii).

Equations

• d.negExt C = {x : Entity | d C x = some false}

def Semantics.Gradability.Delineation.PartialDelineation.extGap {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) : Set Entity

Extension gap: entities in the comparison class whose truth value is undefined — the borderline cases.

Equations

• d.extGap C = {x : Entity | x ∈ C ∧ d C x = none}

theorem Semantics.Gradability.Delineation.PartialDelineation.trichotomy {Entity : Type u_1} (d : PartialDelineation Entity) (C : ComparisonClass Entity) (x : Entity) (_hx : x ∈ C) (hdom : d C x ≠ none) : x ∈ d.posExt C ∨ x ∈ d.negExt C

The three zones partition the comparison class: every member is in exactly one of posExt, negExt, or extGap.

def Semantics.Gradability.Delineation.ordering {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (cc : ComparisonClass Entity) (u u' : Entity) : Prop

Klein's ordering at context c (eq 29): u >_{c,ζ} u' iff there exists a comparison class X ⊆ 𝒰(c) that puts u in the positive extension and u' in the negative extension. The existing comparativeSem is the unrestricted case (𝒰(c) = U).

Equations

• Semantics.Gradability.Delineation.ordering delineation cc u u' = ∃ X ⊆ cc, delineation X u ∧ ¬delineation X u'

theorem Semantics.Gradability.Delineation.comparativeSem_eq_ordering_univ {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (a b : Entity) : comparativeSem delineation a b ↔ ordering delineation Set.univ a b

The unrestricted comparative is the ordering over all of U.

theorem Semantics.Gradability.Delineation.ordering_asymm {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (hmono : IsMonotoneDelineation delineation Set.univ) (cc : ComparisonClass Entity) (u v : Entity) : ordering delineation cc u v → ¬ordering delineation cc v u

Klein's ordering is asymmetric under monotone delineation (§3.3, p. 23): if u >{c,ζ} u', then u' ≯{c,ζ} u.

theorem Semantics.Gradability.Delineation.ordering_trans {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (hmono : IsMonotoneDelineation delineation Set.univ) (cc : ComparisonClass Entity) (u v w : Entity) : ordering delineation cc u v → ordering delineation cc v w → ordering delineation cc u w

Klein's ordering is transitive under monotone delineation (§3.3, p. 23): if u >{c,ζ} v and v >{c,ζ} w, then u >_{c,ζ} w.

Proof: take X₂ (the class separating v from w). By monotonicity with X₁ separating u from v, u must also be positive in X₂. Since w is negative in X₂, X₂ separates u from w.

theorem Semantics.Gradability.Delineation.ordering_neg_trans {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (cc : ComparisonClass Entity) (u v w : Entity) : ordering delineation cc u w → ordering delineation cc u v ∨ ordering delineation cc v w

Negative transitivity of the ordering: if u >{c,ζ} w then for any v, either u >{c,ζ} v or v >_{c,ζ} w. No conditions required — follows from excluded middle on delineation X v.

This is the key structural property that, combined with asymmetry (from monotonicity), makes the ordering a strict weak order.

def Semantics.Gradability.Delineation.nondistinct {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (cc : ComparisonClass Entity) (u u' : Entity) : Prop

Two entities are NONDISTINCT w.r.t. ζ at c (eq 30) iff no comparison class containing both can distinguish them.

Nondistinctness is reflexive and symmetric but NOT transitive in general. For linear adjectives, nondistinctness collapses to equivalence (eq 40); for nonlinear adjectives it does not — this is what makes clever-type adjectives special.

Equations

• Semantics.Gradability.Delineation.nondistinct delineation cc u u' = ∀ X ⊆ cc, u ∈ X → u' ∈ X → (delineation X u ↔ delineation X u')

theorem Semantics.Gradability.Delineation.nondistinct_refl {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {cc : ComparisonClass Entity} {u : Entity} : nondistinct delineation cc u u

theorem Semantics.Gradability.Delineation.nondistinct_symm {Entity : Type u_1} {delineation : ComparisonClass Entity → Entity → Prop} {cc : ComparisonClass Entity} {u u' : Entity} (h : nondistinct delineation cc u u') : nondistinct delineation cc u' u

theorem Semantics.Gradability.Delineation.nondistinct_of_incomparable {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (cc : ComparisonClass Entity) (u u' : Entity) (hno1 : ¬ordering delineation cc u u') (hno2 : ¬ordering delineation cc u' u) : nondistinct delineation cc u u'

Incomparability implies nondistinctness: if neither u > u' nor u' > u in the ordering, then u and u' are nondistinct. No conditions required — follows from excluded middle on delineation.

The converse (nondistinct → incomparable) holds under Klein's domain restriction where the ordering additionally requires both entities to be members of the witness class X.

def Semantics.Gradability.Delineation.IsLinearDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) : Prop

A delineation is LINEAR (eq 9) iff the ordering it induces is connected: for any two distinct members of a comparison class, either one is ranked above the other or they are nondistinct.

Examples: tall, heavy, expensive — single-criterion adjectives that induce total orderings.

This is orthogonal to Kennedy's open/closed (RGA/AGA) axis: tall is both linear AND relative-gradable.

Equations

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

def Semantics.Gradability.Delineation.IsNonlinearDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) : Prop

A delineation is NONLINEAR iff its ordering can go both ways: there exist u, u' and a comparison class cc such that both u >_{cc} u' and u' >_{cc} u. This happens when different subsets of cc apply different criteria (e.g., math vs. social skills for "clever"), so the delineation is not monotone.

For linear adjectives (tall, heavy), monotonicity ensures the ordering is asymmetric; for nonlinear ones (clever, nice), the ordering can cycle. This is orthogonal to Kennedy's open/closed (RGA/AGA) distinction.

Equations

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

A measure function μ : E → D naturally induces a Klein delineation: entity x is "tall in C" iff x is strictly taller than some member of C. This bridges the degree world (Kennedy) and the degreeless world (Klein): the delineation is determined by the measure, but the semantics never mentions degrees directly.

def Semantics.Gradability.Delineation.measureDelineation {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) : ComparisonClass E → E → Prop

Delineation induced by a measure function: x is "A-in-C" iff there exists a member of C that x strictly exceeds on μ.

Equations

• Semantics.Gradability.Delineation.measureDelineation μ C x = ∃ y ∈ C, μ y < μ x

theorem Semantics.Gradability.Delineation.measureDelineation_monotone {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) : IsMonotoneDelineation (measureDelineation μ) Set.univ

A measure-induced delineation is monotone: if a is tall-in-C₁ and b is not, and b is tall-in-C₂, then a is tall-in-C₂.

theorem Semantics.Gradability.Delineation.measureDelineation_mono_in_class {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (x : E) : Monotone fun (C : ComparisonClass E) => measureDelineation μ C x

For a fixed entity x, measureDelineation μ · x is Monotone in the comparison class under ⊆: enlarging C adds potential witnesses y ∈ C with μ y < μ x, so if x is "tall in C" then x is "tall in C'" for any C' ⊇ C.

This connects Klein's parameter space to Mathlib's Monotone infrastructure. Note that general (non-measure-induced) delineations are NOT uniformly monotone — that's the whole point of nonlinear adjectives like "clever".

theorem Semantics.Gradability.Delineation.ordering_implies_degree {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (cc : ComparisonClass E) (a b : E) : ordering (measureDelineation μ) cc a b → μ b < μ a

Forward: Klein's ordering entails degree ordering.

theorem Semantics.Gradability.Delineation.degree_implies_ordering {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (cc : ComparisonClass E) (a b : E) (ha : a ∈ cc) (hb : b ∈ cc) : μ b < μ a → ordering (measureDelineation μ) cc a b

Backward: degree ordering entails Klein's ordering (provided both entities are in the comparison class).

theorem Semantics.Gradability.Delineation.ordering_iff_degree {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (cc : ComparisonClass E) (a b : E) (ha : a ∈ cc) (hb : b ∈ cc) : ordering (measureDelineation μ) cc a b ↔ μ b < μ a

Equivalence: Klein's ordering ↔ degree comparison. Justifies Klein's claim that degrees are dispensable (§4.2).

theorem Semantics.Gradability.Delineation.measureDelineation_is_linear {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) : IsLinearDelineation (measureDelineation μ)

A measure-induced delineation is linear: for any two entities in a comparison class, either one ranks above the other or they are nondistinct (equal measure). This connects Klein's typology (§2.2): single-criterion adjectives like "tall" are always linear.

Klein handles degree modifiers WITHOUT degrees: very and fairly are comparison-class narrowers. Under the correspondence with degree semantics, narrowing the CC is equivalent to shifting the threshold.

def Semantics.Gradability.Delineation.veryDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (C : ComparisonClass Entity) (x : Entity) : Prop

Klein's very (§4.1, eq 42): narrows the comparison class to the positive extension. "Very tall" = tall relative to the tall people.

Under the degree correspondence, this is equivalent to raising the threshold from θ to a higher θ' — the threshold for being tall among tall people.

Equations

• Semantics.Gradability.Delineation.veryDelineation delineation C x = delineation {u : Entity | delineation C u} x

def Semantics.Gradability.Delineation.fairlyDelineation {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (C : ComparisonClass Entity) (x : Entity) : Prop

Klein's fairly (§4.1, eq 43): narrows the comparison class to exclude the very-A entities. "Fairly tall" = tall among those who aren't very tall.

Equations

• Semantics.Gradability.Delineation.fairlyDelineation delineation C x = delineation {u : Entity | u ∈ C ∧ u ∉ {u : Entity | delineation {v : Entity | delineation C v} u}} x

theorem Semantics.Gradability.Delineation.very_entails_base {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (hcc : ∀ (C : ComparisonClass Entity) (x : Entity), delineation C x → x ∈ C) (C : ComparisonClass Entity) (x : Entity) (hv : veryDelineation delineation C x) : delineation C x

very entails the base predicate: if x is very-tall-in-C then x is tall-in-C. (The positive extension of very A is a subset of the positive extension of A.)

This requires Klein's domain restriction: the delineation only classifies entities that are members of the comparison class. Klein §2.3 eq (12) specifies that F_ζ(c) is a partial function on 𝒰(c), so delineation C x implies x ∈ C. Given this, the proof is immediate: if x is tall among the tall people, then x must be one of the tall people, hence tall in C.

For measure-induced delineations (which don't satisfy this domain restriction), very → base holds by a different argument — see Klein1980.measureDelineation_very_entails_base.

theorem Semantics.Gradability.Delineation.fairly_excludes_very {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) (hcc : ∀ (C : ComparisonClass Entity) (x : Entity), delineation C x → x ∈ C) (C : ComparisonClass Entity) (x : Entity) (hf : fairlyDelineation delineation C x) : ¬veryDelineation delineation C x

fairly excludes very: if x is fairly-A-in-C then x is NOT very-A-in-C. Under domain restriction, being in the fairly-CC requires being outside the very-positive extension.

@[reducible]

def Semantics.Gradability.Delineation.kleinPreorder {Entity : Type u_1} (delineation : ComparisonClass Entity → Entity → Prop) : Preorder Entity

Klein's delineation induces a Preorder on entities: u ≤ v iff every comparison class where v qualifies also qualifies u. This is Klein's "as A as" (§5.3, eq 89b) and Kamp's at-least-as (definition 12).

The strict part u < v is u ≤ v ∧ ¬ v ≤ u. Under monotone delineation, this coincides with comparativeSem.

Equations

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

Two typeclasses recording how a delineation del relates to an abstract scalar relation R : Entity → Entity → Prop. Both are substrate notions used across paper-anchor files: - Soundness = @cite{bochnak-2015} eq. (28b) Consistency Constraint b (cf. @cite{klein-1980}, @cite{kennedy-2011}, @cite{van-rooij-2011a}; @cite{bochnak-2015} adopts CC-b as the formal engine converting per-context conjoined-comparison content into the height-comparison entailment). - Completeness = the converse direction (NOT in @cite{bochnak-2015}; closer to @cite{burnett-2017}'s Plenitude / Granularity axioms and @cite{klein-1980} coverage assumptions).

Promoted here so that Kamp/Klein/Fine/Kennedy/Hierarchy and any
DSP-negative-language study (Bochnak's Washo, Beck-Krasikova-et-al's
Motu, Wellwood's *much* analyses) can import and instantiate
uniformly without going through any paper-specific anchor file.

@cite{bochnak-2015} eq. (28a) **Consistency Constraint a** is exactly
`IsMonotoneDelineation _ Set.univ` (§4 above) — no separate
typeclass needed.

## Cross-framework engagement

- **`Hierarchy.lean`**: the measure-induced instance theorems below
  factor through `ordering_implies_degree` and
  `degree_implies_ordering` from `Hierarchy.lean`'s established
  bridge content. `comparativeSem_iff_of_sound_and_complete`
  instantiated at `measureDelineation μ` is the `Set.univ`
  restriction of `ordering_iff_degree μ Set.univ`.
- **@cite{kamp-1975}**: `IsCompleteDelineation`'s "R-distinguished
  pairs admit a discriminating context" is the existential dual of
  Kamp's preorder universal `∀ C, del C v → del C u`. For monotone
  delineations, the equivalence fires via `comparativeSem ↔
  kleinPreorder.lt` (§12 above).
- **@cite{fine-1975}**: `monotone_comparative_superTrue` (§5 above)
  shows monotonicity carries `comparativeSem` into Fine's super-true
  entailment. CC-b is the delineation-side statement of the same
  supervaluationist content under the Klein↔Fine duality.
- **Tension with @cite{cobreros-etal-2012}**: CC-b
  is a strict-classical condition (`¬ del C y` absolutely). Under
  tolerant semantics for vague predicates, similar pairs would
  satisfy `tolerantAtom M P x ∧ tolerantAtom M P y` jointly, so
  strict separation `del C x ∧ ¬ del C y` would over-generate.
  CC-b implicitly rules out tolerant classifications. 

class Semantics.Gradability.Delineation.IsSoundDelineation {Entity : Type u_1} (del : ComparisonClass Entity → Entity → Prop) (R : Entity → Entity → Prop) : Prop

A delineation del is sound w.r.t. an abstract scalar relation R iff per-context separation entails R: whenever del C x ∧ ¬ del C y for some context C, R x y holds. The "scalar concept encoded by G" is left abstract — R : Entity → Entity → Prop is not constrained to be a strict order or scale-induced.

Generalises @cite{bochnak-2015} eq. (28b) from the measure-induced case to arbitrary relations. The Bochnak citation tag is preserved in ConsistencyConstraints.lean.

• sound (C : ComparisonClass Entity) (x y : Entity) : del C x → ¬del C y → R x y

  Per-context conjunction implies the scalar relation.

class Semantics.Gradability.Delineation.IsCompleteDelineation {Entity : Type u_1} (del : ComparisonClass Entity → Entity → Prop) (R : Entity → Entity → Prop) : Prop

A delineation del is complete w.r.t. an abstract scalar relation R iff every R-distinguished pair admits a discriminating context: whenever R x y, there is some context C with del C x ∧ ¬ del C y.

NOT in @cite{bochnak-2015} (whose footnote 11 explicitly notes the one-directional character of the comparison entailment); related to @cite{burnett-2017}'s Plenitude and Granularity axioms and to @cite{klein-1980} coverage assumptions. Required for the bidirectional comparativeSem ↔ R equivalence below; without it the right-to-left direction fails.

• complete (x y : Entity) : R x y → ∃ (C : ComparisonClass Entity), del C x ∧ ¬del C y

  R-distinguished pairs admit a discriminating context.

theorem Semantics.Gradability.Delineation.comparativeSem_iff_of_sound_and_complete {Entity : Type u_1} {del : ComparisonClass Entity → Entity → Prop} {R : Entity → Entity → Prop} [hSound : IsSoundDelineation del R] [hComplete : IsCompleteDelineation del R] {x y : Entity} : comparativeSem del x y ↔ R x y

The substrate-level bidirectional equivalence: comparativeSem coincides with the abstract scalar relation R whenever del is both sound and complete w.r.t. R.

Generalises the measure-based equivalence (ordering_iff_degree) to any abstract scalar concept — the comparison entailment is derivable WITHOUT a measure function in the lexical entry.

instance Semantics.Gradability.Delineation.instSoundMeasureDelineation {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) : IsSoundDelineation (measureDelineation μ) fun (a b : E) => μ b < μ a

Measure-induced delineations are sound w.r.t. their underlying measure-comparison relation. Derived from ordering_implies_degree

• comparativeSem_eq_ordering_univ rather than re-proven from scratch, so the substrate connects through Hierarchy.lean-style bridge content cleanly.

instance Semantics.Gradability.Delineation.instCompleteMeasureDelineation {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) : IsCompleteDelineation (measureDelineation μ) fun (a b : E) => μ b < μ a

Measure-induced delineations are complete w.r.t. their underlying measure-comparison relation. Derived from degree_implies_ordering (which uses the {a, b} two-element comparison class — the Klein/Kennedy/Fara minimum, not a degenerate singleton).