refactor(Semantics/Degree): delete reducible duplicate names

Linglib/Semantics/Attitudes/EpistemicThreshold.lean

@@ -41,7 +41,7 @@ against a threshold (Table 1(a)):
 The threshold semantics is structurally identical to the positive form of
 gradable adjectives:
 
-    ⟦tall⟧(x) = height(x) ≥ θ_tall (Degree/Basic.positiveSem)
+    ⟦tall⟧(x) = height(x) ≥ θ_tall (the ≥-threshold condition)
     ⟦believes⟧(A, φ) = Pr(A, φ) ≥ θ_bel (meetsThreshold)
 
 Both are instances of the same degree-threshold architecture: a measure
@@ -190,7 +190,7 @@ variable {E W : Type*}
     This is the single mechanism underlying all epistemic vocabulary.
     `believes`, `knows`, `certain`, `must`, `might` are all instances.
 
-    Structurally identical to `Degree.positiveSem μ θ x`: both are
+    Structurally identical to the degree-semantic ≥-threshold condition
     `measure(entity) ≥ threshold`. -/
 def meetsThreshold (cr : AgentCredence E W) (θ : ℚ)
     (a : E) (φ : (W → Bool)) : Prop :=
@@ -449,7 +449,7 @@ The structural analogy between adjective degree semantics ([kennedy-2007],
 [lassiter-goodman-2017]) and epistemic threshold semantics: both are
 instances of `μ(entity) ≥ θ`. The threshold semantics makes this precise:
 
-    ⟦tall⟧(x) = height(x) ≥ θ_tall (Degree.positiveSem)
+    ⟦tall⟧(x) = height(x) ≥ θ_tall (the ≥-threshold condition)
     ⟦believes⟧(A, φ) = Pr(A, φ) ≥ θ_bel (meetsThreshold)
 
 Both are instances of `μ(entity) ≥ θ`. The epistemic scale is the
@@ -492,15 +492,15 @@ def epistemicAsDirectedMeasure (cr : AgentCredence E W) (_entry : EpistemicEntry
   μ := fun ⟨a, φ⟩ => cr a φ
   boundedness := epistemicBoundedness
 
-/-- The degree-threshold identity: `meetsThreshold` is `positiveSem`
-    instantiated on the epistemic scale.
+/-- The degree-threshold identity: `meetsThreshold` is the ≥-threshold
+    condition `θ ≤ μ(entity)` with credence as the measure function.
 
     This is the formal statement that epistemic threshold semantics IS
-    degree semantics with credence as the measure function. -/
-theorem meetsThreshold_eq_positiveSem (cr : AgentCredence E W) (θ : ℚ)
+    degree semantics (the positive-form `Comparison.ge.over μ θ`
+    condition) with credence as the measure function. -/
+theorem meetsThreshold_eq_threshold (cr : AgentCredence E W) (θ : ℚ)
     (a : E) (φ : (W → Bool)) :
-    meetsThreshold cr θ a φ ↔
-    Semantics.Degree.positiveSem (fun (p : E × (W → Bool)) => cr p.1 p.2) θ (a, φ) := by
+    meetsThreshold cr θ a φ ↔ θ ≤ cr a φ := by
   rfl
 
 /-- The epistemic scale is licensed: closed → admits absolute standards.

Linglib/Semantics/Degree/Abstraction.lean

@@ -34,9 +34,9 @@ and intensional verbs.
 ## Order-Theoretic Foundations
 
 Heim's maximality operator `IsMaxDeg` is Mathlib's `IsGreatest`.
-The matrix predicate `λd. μ(a) ≥ d` and [kennedy-1999]'s
-`posExt μ a` are both the principal downset `Set.Iic (μ a)` — the
-same mathematical object arrived at from different linguistic
+Heim's matrix degree predicate `λd. μ(a) ≥ d` is [kennedy-1999]'s
+`posExt μ a` — the principal downset `Set.Iic (μ a)`, the same
+mathematical object arrived at from different linguistic
 motivations. The scope collapse theorems factor through the degree
 image `μ '' {x | R x}`, connecting to `gc_sSup_Iic` under
 `ConditionallyCompleteLattice`.
@@ -74,45 +74,29 @@ theorem isMaxDeg_iff_isGreatest {D : Type*} [LE D] (P : DegreePredicate D) (d :
     IsMaxDeg P d ↔ IsGreatest {d' | P d'} d :=
   ⟨fun ⟨h1, h2⟩ => ⟨h1, h2⟩, fun ⟨h1, h2⟩ => ⟨h1, h2⟩⟩
 
-/-- The matrix degree predicate for "A is d-tall": λd. μ(A) ≥ d. -/
-def matrixPredicate {Entity D : Type*} [Preorder D]
-    (μ : Entity → D) (a : Entity) : DegreePredicate D :=
-  fun d => μ a ≥ d
-
 /-- The than-clause degree predicate for "B is d-tall": λd. μ(B) ≥ d. -/
 def thanClausePredicate {Entity D : Type*} [Preorder D]
     (μ : Entity → D) (b : Entity) : DegreePredicate D :=
   fun d => μ b ≥ d
 
--- ─── Matrix Predicate = posExt = Iic ──────────────
+-- ─── posExt = Iic: Heim's matrix predicate ──────────
 --
--- Heim's matrix predicate and Kennedy's positive extent
--- are the same mathematical object — the principal downset
--- (Mathlib's Set.Iic):
+-- Heim's matrix degree predicate λd. μ(a) ≥ d and Kennedy's
+-- positive extent are the same mathematical object — the
+-- principal downset (Mathlib's Set.Iic):
 --
---   Heim:    matrixPredicate μ a = λd. μ(a) ≥ d
---   Kennedy: posExt μ a         = {d | d ≤ μ a}
---   = Set.Iic (μ a)
-
-/-- Matrix predicate membership = `Set.Iic` membership. -/
-theorem matrixPredicate_mem_iff_Iic {Entity D : Type*} [Preorder D]
-    (μ : Entity → D) (a : Entity) (d : D) :
-    matrixPredicate μ a d ↔ d ∈ Set.Iic (μ a) := Iff.rfl
-
-/-- Matrix predicate membership = `posExt` membership
-    ([kennedy-1999]). -/
-theorem matrixPredicate_mem_iff_posExt {Entity D : Type*} [Preorder D]
-    (μ : Entity → D) (a : Entity) (d : D) :
-    matrixPredicate μ a d ↔ d ∈ posExt μ a := Iff.rfl
+--   [kennedy-1999]: posExt μ a = {d | d ≤ μ a} = Set.Iic (μ a)
+--
+-- so Heim's scope theory is stated directly on `posExt`.
 
-/-- The maximum of a monotone predicate λd. μ(a) ≥ d is μ(a) itself.
+/-- The maximum of the positive extent λd. μ(a) ≥ d is μ(a) itself.
     This grounds the Heim–Kennedy equivalence: max{d: tall(a,d)} = μ(a).
 
     This is Mathlib's `isGreatest_Iic` — the greatest element of
     `{d | d ≤ μ(a)}` is `μ(a)` — specialized to degree semantics. -/
-theorem isMaxDeg_matrixPredicate {Entity D : Type*} [LinearOrder D]
+theorem isMaxDeg_posExt {Entity D : Type*} [LinearOrder D]
     (μ : Entity → D) (a : Entity) :
-    IsMaxDeg (matrixPredicate μ a) (μ a) :=
+    IsMaxDeg (posExt μ a) (μ a) :=
   (isMaxDeg_iff_isGreatest _ _).mpr isGreatest_Iic
 
 -- ════════════════════════════════════════════════════
@@ -131,11 +115,11 @@ def IsMonotoneAdj {Entity D : Type*} [Preorder D]
     (adj : D → Entity → Prop) : Prop :=
   ∀ (x : Entity) (d d' : D), adj d x → d' ≤ d → adj d' x
 
-/-- `matrixPredicate μ a` is always monotone (by construction). -/
-theorem matrixPredicate_monotone {Entity D : Type*} [Preorder D]
+/-- `posExt μ a` is always downward-closed (by construction). -/
+theorem posExt_downwardClosed {Entity D : Type*} [Preorder D]
     (μ : Entity → D) (a : Entity) :
-    ∀ (d d' : D), matrixPredicate μ a d → d' ≤ d →
-      matrixPredicate μ a d' := by
+    ∀ (d d' : D), posExt μ a d → d' ≤ d →
+      posExt μ a d' := by
   intro d d' hd hle
   exact le_trans hle hd
 
@@ -304,9 +288,9 @@ theorem heim_extensional_equivalence {Entity D : Type*} [LinearOrder D]
 --
 -- The antonymy biconditional (Extent.lean § 7) is the
 -- statement that posExt and negExt form an antitone Galois
--- connection on (Set D, ⊆). Since matrixPredicate = posExt,
--- Heim's scope theory is built on the same Galois connection
--- that grounds Kennedy's antonymy:
+-- connection on (Set D, ⊆). Heim's matrix degree predicate is
+-- `posExt`, so his scope theory is built on the same Galois
+-- connection that grounds Kennedy's antonymy:
 --
 --   posExt μ a ⊆ posExt μ b  ↔  negExt μ b ⊆ negExt μ a
 --                             ↔  μ a ≤ μ b

Linglib/Semantics/Degree/Basic.lean

@@ -3,15 +3,15 @@ import Linglib.Semantics.Degree.Defs
 /-!
 # Degree Semantics: Positive-Form Semantics
 
-Positive-form semantic operations on the types declared in `Defs.lean`,
-plus threshold-comparison predicates on the concrete `Degree max` /
-`Threshold max` carriers [kennedy-2007] [heim-2001]
-[kennedy-mcnally-2005]. Kennedy 2007's interpretive economy lives
-in the sibling `Kennedy.lean`.
+Threshold-comparison predicates on the concrete `Degree max` /
+`Threshold max` carriers declared in `Defs.lean` [kennedy-2007]
+[heim-2001] [kennedy-mcnally-2005]. The abstract positive-form
+predicate `μ(x) ≥ θ` is just `Comparison.ge.over μ θ` — used directly
+where needed. Kennedy 2007's interpretive economy lives in the sibling
+`Kennedy.lean`.
 
 ## Main definitions
 
-* `positiveSem` — abstract positive-form predicate `μ(x) ≥ θ`
 * `positiveMeaning`, `negativeMeaning`, `antonymMeaning` — concrete
   threshold-comparison predicates on `Degree max` / `Threshold max`
 
@@ -21,34 +21,17 @@ in the sibling `Kennedy.lean`.
 
 ## Relationship to `Gradability.Basic`
 
-This module uses abstract types (`Entity D : Type*` with `LinearOrder D`)
-for framework-level theorems. `Gradability.Basic` uses concrete
-`Degree max := Fin (max + 1)` for computation in RSA models and Fragment
-entries. The two serve different clients: this module is imported by
-`Degree/Comparative.lean` and other framework siblings; `Gradability.Basic`
-is imported by `Fragments/English/` and gradability `Studies/` files.
+This module's concrete `Degree max := Fin (max + 1)` predicates serve
+computation in RSA models and Fragment entries. `Gradability.Basic`
+serves the same clients; this module is imported by
+`Degree/Comparative.lean` and other framework siblings, while
+`Gradability.Basic` is imported by `Fragments/English/` and gradability
+`Studies/` files.
 -/
 
 namespace Semantics.Degree
 
 open Semantics.Degree (Degree Threshold)
-section Abstract
-
-variable {Entity D : Type*} [LinearOrder D]
-
-/-- The positive (unmarked) form of a gradable adjective:
-"Kim is tall" is true iff `μ(Kim) ≥ θ` for a contextual standard `θ`.
-
-This is the common core across Kennedy and Heim:
-* Kennedy: `⟦tall⟧ = λd.λx. height(x) ≥ d`, with `θ = pos(tall)`
-* Heim: `⟦tall⟧ = λx. height(x) ≥ θ_c`
-
-Klein's approach is different: "tall" is true relative to a comparison
-class, with no degree parameter. -/
-def positiveSem (μ : Entity → D) (θ : D) (x : Entity) : Prop :=
-  μ x ≥ θ
-
-end Abstract
 
 /-! ### Concrete threshold-based meanings
 

Linglib/Semantics/Degree/Granularity.lean

@@ -99,21 +99,6 @@ end GranularityFunction
 
 variable {D : Type*} [LinearOrder D]
 
-/-- Equative at granularity interval: "as Adj as d_c".
-
-    Paper eq. (45): ⟦as...as d_c⟧^g = λGλx.∃d[d > inf(g(d_c)) ∧ G(d)(x)].
-
-    For upward-monotone G (e.g., tall, where G(d)(x) iff μ(x) ≥ d),
-    the existential reduces to μ_x > inf(g(d_c)). -/
-def eqAt (gi : GranInterval D) (μ_x : D) : Prop := μ_x > gi.lo
-
-/-- Comparative at granularity interval: "Adj-er than d_c".
-
-    Paper eq. (49): ⟦er/more than d_c⟧^g = λGλx.∃d[d > sup(g(d_c)) ∧ G(d)(x)].
-
-    For upward-monotone G, the existential reduces to μ_x > sup(g(d_c)). -/
-def compAt (gi : GranInterval D) (μ_x : D) : Prop := μ_x > gi.hi
-
 -- ════════════════════════════════════════════════════
 -- § 2. Entailment Reversal
 -- ════════════════════════════════════════════════════
@@ -133,20 +118,24 @@ The proofs are one-liners: transitivity of `<` and `≤`. -/
 
 /-- Equatives: finer grain (larger lo) entails coarser grain (smaller lo).
 
+    The equative "as Adj as d_c" (eq. 45) at grain cell `gi`, for
+    upward-monotone G, reduces to `μ_x > gi.lo` (the cell's infimum).
     If μ_x exceeds the fine-grain infimum, it a fortiori exceeds the
     coarse-grain infimum (which is smaller). -/
 theorem eq_fine_entails_coarse (gi₁ gi₂ : GranInterval D)
     (hlo : gi₂.lo ≤ gi₁.lo)
-    (μ_x : D) (h : eqAt gi₁ μ_x) : eqAt gi₂ μ_x :=
+    (μ_x : D) (h : μ_x > gi₁.lo) : μ_x > gi₂.lo :=
   lt_of_le_of_lt hlo h
 
 /-- Comparatives: coarser grain (larger hi) entails finer grain (smaller hi).
 
+    The comparative "Adj-er than d_c" (eq. 49) at grain cell `gi`, for
+    upward-monotone G, reduces to `μ_x > gi.hi` (the cell's supremum).
     If μ_x exceeds the coarse-grain supremum, it a fortiori exceeds the
     fine-grain supremum (which is smaller). -/
 theorem comp_coarse_entails_fine (gi₁ gi₂ : GranInterval D)
     (hhi : gi₁.hi ≤ gi₂.hi)
-    (μ_x : D) (h : compAt gi₂ μ_x) : compAt gi₁ μ_x :=
+    (μ_x : D) (h : μ_x > gi₂.hi) : μ_x > gi₁.hi :=
   lt_of_le_of_lt hhi h
 
 -- ════════════════════════════════════════════════════