refactor(Semantics/Degree): retire degree-property family + relationalGQ

Linglib/Core/Order/Comparison.lean

@@ -88,6 +88,14 @@ def Comparison.over {E α : Type*} [Preorder α]
     x ∈ c.over μ n ↔ c.rel (μ x) n := by
   simp [Comparison.over]
 
+instance Comparison.relDecidable {α : Type*} [Preorder α] [DecidableEq α] [DecidableLE α]
+    [DecidableLT α] (c : Comparison) (a n : α) : Decidable (c.rel a n) := by
+  cases c <;> simp only [Comparison.rel, ge_iff_le, gt_iff_lt] <;> infer_instance
+
+instance Comparison.overDecidable {E α : Type*} [Preorder α] [DecidableEq α] [DecidableLE α]
+    [DecidableLT α] (c : Comparison) (μ : E → α) (n : α) (x : E) : Decidable (x ∈ c.over μ n) :=
+  decidable_of_iff _ (Comparison.mem_over c μ n x).symm
+
 /-- **Class A/B is interval-endpoint membership.** A non-strict comparison
     (bare `=`, Class B `≥`/`≤`) keeps the boundary `n`; a strict one (Class A
     `>`/`<`) drops it — the whole Class A/B distinction

Linglib/Semantics/Degree/DirectedMeasure.lean

@@ -16,8 +16,8 @@ degree-domain constructors and epistemic threshold semantics.
 - `DirectedMeasure`: the bundled measure structure.
 - `DirectedMeasure.IsLicensed`: endpoint-based licensing via `Boundedness.IsLicensed`.
 - `DirectedMeasure.degreeProperty`: the degree property derived from
-  `direction` (`atLeastDeg` positive, `atMostDeg` negative); its maximal
-  informativity is characterized in `Semantics/Entailment/Extremum.lean`.
+  `direction` (`Comparison.ge.over` positive, `Comparison.le.over` negative); its
+  maximal informativity is characterized in `Semantics/Entailment/Extremum.lean`.
 - `DirectedMeasure.numeral`, `DirectedMeasure.adjective`: Kennedy-style
   numeral and gradable-adjective domains.
 
@@ -49,10 +49,10 @@ open Core.Order
 
     Common algebraic core of the `numeral`/`adjective` domain constructors and
     epistemic thresholds (`epistemicAsDirectedMeasure`, on
-    `DirectedMeasure ℚ (E × (W → Bool))`). The degree property (`atLeastDeg`
-    for positive, `atMostDeg` for negative) is derived from `direction`, not
-    stored — per [lassiter-goodman-2017], the binary direction choice is the
-    fundamental parameter. -/
+    `DirectedMeasure ℚ (E × (W → Bool))`). The degree property
+    (`Comparison.ge.over` for positive, `Comparison.le.over` for negative) is
+    derived from `direction`, not stored — per [lassiter-goodman-2017], the
+    binary direction choice is the fundamental parameter. -/
 structure DirectedMeasure (D : Type*) [LinearOrder D] (E : Type*) extends ComparativeScale D where
   /-- Measure function: maps entities to degrees on the scale -/
   μ : E → D
@@ -75,14 +75,14 @@ def IsLicensed (dm : DirectedMeasure D E) : Prop := dm.boundedness.IsLicensed
 instance (dm : DirectedMeasure D E) : Decidable dm.IsLicensed :=
   inferInstanceAs (Decidable dm.boundedness.IsLicensed)
 
-/-- The degree property derived from the measure's direction: `atLeastDeg`
-    for positive scales (tall, likely), `atMostDeg` for negative ones
+/-- The degree property derived from the measure's direction: `Comparison.ge.over`
+    for positive scales (tall, likely), `Comparison.le.over` for negative ones
     (short, unlikely). The derivation the structure docstring promises:
     `direction` is the stored parameter, the property follows. -/
-def degreeProperty (dm : DirectedMeasure D E) : D → E → Prop :=
+def degreeProperty (dm : DirectedMeasure D E) : D → Set E :=
   match dm.direction with
-  | .positive => atLeastDeg dm.μ
-  | .negative => atMostDeg dm.μ
+  | .positive => Comparison.ge.over dm.μ
+  | .negative => Comparison.le.over dm.μ
 
 end DirectedMeasure
 
@@ -102,7 +102,7 @@ variable {α : Type*} [LinearOrder α] {W : Type*}
 
 /-- [kennedy-2015] numeral domain: "at least n" over cardinality.
     Closed scale (ℕ well-ordered) → always licensed.
-    Type-shift to exact = MIP applied to atLeastDeg. -/
+    Type-shift to exact = MIP applied to `Comparison.ge.over`. -/
 def numeral (μ : W → α) : DirectedMeasure α W :=
   { boundedness := .closed, μ := μ }
 

Linglib/Semantics/Entailment/Extremum.lean

@@ -60,6 +60,7 @@ not their primary formulation.
 namespace Entailment
 
 open Semantics.Degree
+open Core.Order (Comparison)
 variable {α : Type*} [LinearOrder α]
 
 -- ════════════════════════════════════════════════════
@@ -133,11 +134,10 @@ def MIP_LicensedDown {W : Type*} (P : α → W → Prop) : Prop :=
 -- § 4. Degree-predicate IsMaxInf characterizations
 -- ════════════════════════════════════════════════════
 
-/-! Migrated from `Core/Scales/Scale.lean`: applications of `IsMaxInf` to
-    the canonical degree predicates `atLeastDeg`, `moreThanDeg`, `atMostDeg`
-    (defined in Scale.lean, monotonicity proven there). The pure scale
-    theory stays in Scale.lean; the IsMaxInf-flavored consequences live
-    here as a downstream entailment-theoretic application. -/
+/-! Applications of `IsMaxInf` to the canonical degree predicates
+    `Comparison.{ge,gt,le}.over` (defined in `Core/Order/Comparison.lean`,
+    monotonicity in `Semantics/Degree/Predicate.lean`). The IsMaxInf-flavored
+    consequences live here as a downstream entailment-theoretic application. -/
 
 /-- "At least d" always has a maximally informative element: d₀ = μ(w).
 
@@ -149,7 +149,7 @@ def MIP_LicensedDown {W : Type*} (P : α → W → Prop) : Prop :=
     of scale density: the `≥` relation creates a closed set with a
     natural maximum at the true value. -/
 theorem atLeast_hasMaxInf {W : Type*} (μ : W → α) (w : W) :
-    HasMaxInf (atLeastDeg μ) w :=
+    HasMaxInf (Comparison.ge.over μ) w :=
   ⟨μ w, le_refl _, fun _ hd _ hw' => le_trans hd hw'⟩
 
 /-- **Implicature asymmetry** ([fox-2007], [fox-hackl-2006]):
@@ -163,7 +163,7 @@ theorem atLeast_hasMaxInf {W : Type*} (μ : W → α) (w : W) :
     possible world. -/
 theorem moreThan_noMaxInf {W : Type*} [DenselyOrdered α] (μ : W → α)
     (hSurj : Function.Surjective μ) (w : W) :
-    ¬ HasMaxInf (moreThanDeg μ) w := by
+    ¬ HasMaxInf (Comparison.gt.over μ) w := by
   intro ⟨d₀, hd₀, hent⟩
   obtain ⟨d', hd₀d', hd'w⟩ := DenselyOrdered.dense d₀ (μ w) hd₀
   obtain ⟨m, hd₀m, hmd'⟩ := DenselyOrdered.dense d₀ d' hd₀d'
@@ -177,7 +177,7 @@ theorem moreThan_noMaxInf {W : Type*} [DenselyOrdered α] (μ : W → α)
     actually used in the proof. -/
 theorem isMaxInf_atLeast_of_hit {W : Type*} (μ : W → α) (m : α) (w : W)
     (hHit : ∃ w', μ w' = m) :
-    IsMaxInf (atLeastDeg μ) m w ↔ μ w = m := by
+    IsMaxInf (Comparison.ge.over μ) m w ↔ μ w = m := by
   constructor
   · intro ⟨hge, hent⟩
     obtain ⟨w_m, hw_m⟩ := hHit
@@ -192,21 +192,21 @@ theorem isMaxInf_atLeast_of_hit {W : Type*} (μ : W → α) (m : α) (w : W)
     equals m, under full surjectivity. Corollary of `isMaxInf_atLeast_of_hit`. -/
 theorem isMaxInf_atLeast_iff_eq {W : Type*} (μ : W → α) (m : α) (w : W)
     (hSurj : Function.Surjective μ) :
-    IsMaxInf (atLeastDeg μ) m w ↔ μ w = m :=
+    IsMaxInf (Comparison.ge.over μ) m w ↔ μ w = m :=
   isMaxInf_atLeast_of_hit μ m w (hSurj m)
 
 /-- On ℕ, "more than m" has `HasMaxInf`: the discrete collapse rescues maximality.
     Contrast with `moreThan_noMaxInf`: on dense scales, `HasMaxInf` fails. -/
 theorem moreThan_nat_hasMaxInf {W : Type*} (μ : W → ℕ) (w : W)
-    (hw : moreThanDeg μ 0 w) : HasMaxInf (moreThanDeg μ) w := by
+    (hw : w ∈ Comparison.gt.over μ 0) : HasMaxInf (Comparison.gt.over μ) w := by
   refine ⟨μ w - 1, ?_, fun d hd w' hw' => ?_⟩
   · have : μ w > 0 := hw; show μ w > μ w - 1; omega
   · have : μ w' > μ w - 1 := hw'; have : μ w > d := hd; show μ w' > d; omega
 
 /-- "At most d" always has a maximally informative element: d₀ = μ(w).
     Symmetric to `atLeast_hasMaxInf`. -/
 theorem atMost_hasMaxInf {W : Type*} (μ : W → α) (w : W) :
-    HasMaxInf (atMostDeg μ) w :=
+    HasMaxInf (Comparison.le.over μ) w :=
   ⟨μ w, le_refl _, fun _ hd _ hw' => le_trans hw' hd⟩
 
 /-- **Kennedy / [rouillard-2026] bridge**: `IsMaxInf` of "at most d" at
@@ -215,7 +215,7 @@ theorem atMost_hasMaxInf {W : Type*} (μ : W → α) (w : W) :
     just as it does from "at least". -/
 theorem isMaxInf_atMost_iff_eq {W : Type*} (μ : W → α) (m : α) (w : W)
     (hSurj : Function.Surjective μ) :
-    IsMaxInf (atMostDeg μ) m w ↔ μ w = m := by
+    IsMaxInf (Comparison.le.over μ) m w ↔ μ w = m := by
   constructor
   · intro ⟨hle, hent⟩
     obtain ⟨w_m, hw_m⟩ := hSurj m
@@ -238,21 +238,21 @@ theorem isMaxInf_atMost_iff_eq {W : Type*} (μ : W → α) (m : α) (w : W)
 /-- MIP derives exact meaning from "at least" (Kennedy's direction). -/
 theorem mip_atLeast_is_exact {W : Type*} (μ : W → α) (m : α) (w : W)
     (hSurj : Function.Surjective μ) :
-    IsMaxInf (atLeastDeg μ) m w ↔ eqDeg μ m w :=
-  isMaxInf_atLeast_iff_eq μ m w hSurj
+    IsMaxInf (Comparison.ge.over μ) m w ↔ w ∈ Comparison.eq.over μ m := by
+  rw [isMaxInf_atLeast_iff_eq μ m w hSurj, Comparison.mem_over, Comparison.rel]
 
 /-- MIP derives exact meaning from "at most" (Rouillard's direction). -/
 theorem mip_atMost_is_exact {W : Type*} (μ : W → α) (m : α) (w : W)
     (hSurj : Function.Surjective μ) :
-    IsMaxInf (atMostDeg μ) m w ↔ eqDeg μ m w :=
-  isMaxInf_atMost_iff_eq μ m w hSurj
+    IsMaxInf (Comparison.le.over μ) m w ↔ w ∈ Comparison.eq.over μ m := by
+  rw [isMaxInf_atMost_iff_eq μ m w hSurj, Comparison.mem_over, Comparison.rel]
 
 /-- The MIP is direction-invariant: "at least" and "at most" yield the
     same exact meaning under maximal informativity. Kennedy's type-shift
     and Rouillard's MIP are literally the same operation. -/
 theorem mip_direction_invariant {W : Type*} (μ : W → α) (m : α) (w : W)
     (hSurj : Function.Surjective μ) :
-    IsMaxInf (atLeastDeg μ) m w ↔ IsMaxInf (atMostDeg μ) m w := by
+    IsMaxInf (Comparison.ge.over μ) m w ↔ IsMaxInf (Comparison.le.over μ) m w := by
   rw [mip_atLeast_is_exact μ m w hSurj, mip_atMost_is_exact μ m w hSurj]
 
 /-! ### The bundled form: `DirectedMeasure.degreeProperty`

Linglib/Semantics/Measurement/Basic.lean

@@ -317,7 +317,7 @@ realization (`∃ e, μ(e) = n`) rather than full surjectivity. Mass nouns
 realize every n ∈ ℚ≥0 (rice is uniformly divisible by hypothesis); count
 nouns realize only n ∈ ℕ. -/
 
-open Semantics.Degree (atLeastDeg)
+open Core.Order (Comparison)
 open Entailment (IsMaxInf HasMaxInf)
 
 /-- For a measure function μ on ℚ: when n is realized by some entity, the
@@ -328,14 +328,14 @@ Bridges Scontras's exact measure-term meaning with the `max{n | ...} = n`
 form of Kennedy's de-Fregean analysis. -/
 theorem scontras_kennedy_dense {E : Type*} (μ : MeasureFn E) (n : ℚ) (x : E)
     (hHit : ∃ e, μ.apply e = n) :
-    IsMaxInf (atLeastDeg μ.apply) n x ↔ μ.apply x = n :=
+    IsMaxInf (Comparison.ge.over μ.apply) n x ↔ μ.apply x = n :=
   Entailment.isMaxInf_atLeast_of_hit μ.apply n x hHit
 
 /-- For a cardinality function on ℕ: same point-realization equivalence.
 *Formalization-internal observation* — see the prose above. -/
 theorem scontras_kennedy_card {E : Type*} (cardFn : E → ℕ) (n : ℕ) (x : E)
     (hHit : ∃ e, cardFn e = n) :
-    IsMaxInf (atLeastDeg cardFn) n x ↔ cardFn x = n :=
+    IsMaxInf (Comparison.ge.over cardFn) n x ↔ cardFn x = n :=
   Entailment.isMaxInf_atLeast_of_hit cardFn n x hHit
 
 -- ============================================================================