diff --git a/Linglib/Semantics/Attitudes/EpistemicThreshold.lean b/Linglib/Semantics/Attitudes/EpistemicThreshold.lean
index d597f22db..2e919c8e3 100644
--- a/Linglib/Semantics/Attitudes/EpistemicThreshold.lean
+++ b/Linglib/Semantics/Attitudes/EpistemicThreshold.lean
@@ -49,7 +49,7 @@ function maps an entity to a degree on a scale, and the predicate holds
 iff the degree meets a contextual/lexical threshold. Epistemic expressions
 are gradable predicates on a probability scale bounded by [0, 1].
 
-This connection is formalized in §8 via `epistemicAsGradable`.
+This connection is formalized in §8 via `epistemicAsDirectedMeasure`.
 
 ## Unification of Three Formalizations
 
@@ -478,7 +478,7 @@ expressions.
 def epistemicBoundedness : Core.Order.Boundedness := .closed
 
 /-- An epistemic gradable predicate: an `EpistemicEntry` viewed as a
-    `GradablePredicate` on the probability scale.
+    `DirectedMeasure` on the probability scale.
 
     The entity type is `E × (W → Bool)` (agent–proposition pairs), and the
     measure function is agent credence `cr`. This makes the structural
@@ -487,9 +487,8 @@ def epistemicBoundedness : Core.Order.Boundedness := .closed
     Polarity: threshold entries (`believes`, `must`, `likely`) are positive
     (upward monotone: higher credence → more likely to satisfy). Reversed
     entries (`uncertain`, `unlikely`) are negative (downward monotone). -/
-def epistemicAsGradable (cr : AgentCredence E W) (_entry : EpistemicEntry)
-    : Semantics.Degree.GradablePredicate (E × (W → Bool)) ℚ where
-  form := ""
+def epistemicAsDirectedMeasure (cr : AgentCredence E W) (_entry : EpistemicEntry)
+    : Semantics.Degree.DirectedMeasure ℚ (E × (W → Bool)) where
   μ := fun ⟨a, φ⟩ => cr a φ
   boundedness := epistemicBoundedness
 
diff --git a/Linglib/Semantics/Degree/Abstraction.lean b/Linglib/Semantics/Degree/Abstraction.lean
index e3684a8d8..342d41e0a 100644
--- a/Linglib/Semantics/Degree/Abstraction.lean
+++ b/Linglib/Semantics/Degree/Abstraction.lean
@@ -143,22 +143,6 @@ theorem matrixPredicate_monotone {Entity D : Type*} [Preorder D]
 -- § 3. Degree Operators
 -- ════════════════════════════════════════════════════
 
-/-- Heim's `-er` operating on degree predicates (paper def. (6)):
-    ⟦-er⟧(D₂)(D₁) = max(D₁) > max(D₂)
-
-    Takes two degree predicates and compares their maxima. -/
-def erOnPredicates {D : Type*} [LE D] [LT D]
-    (_P₁ _P₂ : DegreePredicate D) (d₁ d₂ : D)
-    (_h₁ : IsMaxDeg _P₁ d₁) (_h₂ : IsMaxDeg _P₂ d₂) : Prop :=
-  d₁ > d₂
-
-/-- Heim's `less` operator (paper (23)):
-    ⟦less than P⟧ = λQ. max(Q) < max(P) -/
-def lessOnPredicates {D : Type*} [LE D] [LT D]
-    (_P₁ _P₂ : DegreePredicate D) (d₁ d₂ : D)
-    (_h₁ : IsMaxDeg _P₁ d₁) (_h₂ : IsMaxDeg _P₂ d₂) : Prop :=
-  d₁ < d₂
-
 /-- Heim comparative with measure function: the result of composing
     `-er` with degree predicates derived from a monotone adjective.
 
diff --git a/Linglib/Semantics/Degree/Bounds.lean b/Linglib/Semantics/Degree/Bounds.lean
index 9882b1e46..b89c737b7 100644
--- a/Linglib/Semantics/Degree/Bounds.lean
+++ b/Linglib/Semantics/Degree/Bounds.lean
@@ -17,8 +17,8 @@ Two clusters of theorems:
    `NoMinOrder`) interact with monotonicity to admit/block optima.
 
 2. **Order-sensitive maximality** (§6b of legacy Scale.lean):
-   `maxOnScale R X`, `IsMaxDetermined`, `isAmbidirectional` — Rett 2026's
-   relation-parameterized MAX operator + ambidirectionality scaffolding.
+   `maxOnScale R X`, `isAmbidirectional` — Rett 2026's relation-parameterized
+   MAX operator + ambidirectionality predicate.
 
 This file is part of the Phase A decomposition of the legacy
 `Core/Scales/Scale.lean` dumping ground (master plan v4).
@@ -192,45 +192,6 @@ theorem maxOnScale_gt_closedInterval {α : Type*} [LinearOrder α]
 def isAmbidirectional {α : Type*} (f : Set α → Prop) (B : Set α) : Prop :=
   f B ↔ f Bᶜ
 
-/-- A predicate `f` is **MAX_R-determined** iff its value depends only on
-    `maxOnScale R` of its argument: any two sets with the same `MAX_R`
-    yield the same `f`-verdict. The before/until/comparative theorems all
-    establish exactly this: *before* relates A to `MAX₍<₎` of B, the
-    comparative *than*-clause to `MAX₍≥₎` of the degree set, etc. -/
-def IsMaxDetermined {α : Type*} (R : α → α → Prop) (f : Set α → Prop) : Prop :=
-  ∀ B₁ B₂ : Set α, maxOnScale R B₁ = maxOnScale R B₂ → (f B₁ ↔ f B₂)
-
-/-- **Shared informative bound** ⇒ ambidirectionality. The general
-    template behind Rett's typology: if a construction is `MAX_R`-determined
-    and `B` and `Bᶜ` share their `MAX_R`-bound, then the construction is
-    truth-conditionally insensitive to negation of B.
-
-    Each per-construction ambidirectionality theorem in the library is an
-    instance of this template — they prove the shared-bound side condition
-    for a specific `f` and a class of `B`'s, then this lemma packages the
-    result. See `Tense.TemporalConnectives.before_preEvent_ambidirectional`
-    for the canonical instance. -/
-theorem ambidirectional_of_shared_max {α : Type*} {R : α → α → Prop}
-    (f : Set α → Prop) (hf : IsMaxDetermined R f) (B : Set α)
-    (hshared : maxOnScale R B = maxOnScale R Bᶜ) :
-    isAmbidirectional f B :=
-  hf B Bᶜ hshared
-
-/-- **Converse**: an ambidirectional construction must share its `MAX_R`
-    bound between B and Bᶜ — but only when MAX_R alone *witnesses* the
-    distinction. Stated as a contrapositive to make the empirical content
-    explicit: if MAX_R differs between B and Bᶜ but the construction
-    cannot tell them apart by any *other* means (i.e. MAX_R-determined),
-    then the construction is non-ambidirectional. The full converse
-    requires assuming `f` separates sets with distinct MAX_R values, so
-    we instead expose this as a derived fact only under that assumption. -/
-theorem not_ambidirectional_of_distinct_max_separated {α : Type*}
-    {R : α → α → Prop} (f : Set α → Prop) (B : Set α)
-    (hsep : ∀ B₁ B₂ : Set α,
-      maxOnScale R B₁ ≠ maxOnScale R B₂ → ¬ (f B₁ ↔ f B₂))
-    (hdiff : maxOnScale R B ≠ maxOnScale R Bᶜ) :
-    ¬ isAmbidirectional f B :=
-  hsep B Bᶜ hdiff
 
 /-- **Bridge**: `maxOnScale (· ≥ ·)` applied to the "at least" degree set
     `{d | d ≤ μ(w)}` yields `{μ(w)}` — the singleton containing the true
diff --git a/Linglib/Semantics/Degree/Defs.lean b/Linglib/Semantics/Degree/Defs.lean
index c313a45a9..d1cafe5e2 100644
--- a/Linglib/Semantics/Degree/Defs.lean
+++ b/Linglib/Semantics/Degree/Defs.lean
@@ -14,7 +14,6 @@ economy classification is in `Kennedy.lean`. Klein-style delineation
 
 ## Main definitions
 
-* `GradablePredicate` — measure-function interface extending `DirectedMeasure`
 * `DegPType`, `StandardType` — DegP compositional taxonomy
 * `ModifierDirection` — amplifier / downtoner axis
 * `AdjectivalConstruction` — surface-construction type for evaluativity
@@ -24,17 +23,6 @@ economy classification is in `Kennedy.lean`. Klein-style delineation
 namespace Semantics.Degree
 
 open Core.Order (Boundedness)
-/-- Minimal interface for a gradable predicate: a measure function mapping
-entities to degrees on a scale with known boundedness.
-
-Extends `DirectedMeasure D Entity` with a lexical `form` field. Every
-degree framework (Kennedy, Heim, Schwarzschild) provides an instance;
-Klein's delineation approach does not use degrees and so does not instantiate
-this interface (see `Gradability/Delineation.lean`). -/
-structure GradablePredicate (Entity D : Type*) [LinearOrder D]
-    extends Semantics.Degree.DirectedMeasure D Entity where
-  /-- The adjective's lexical form (for identification). -/
-  form : String
 
 /-- The compositional structure of a Degree Phrase (DegP).
 
@@ -153,7 +141,7 @@ inductive AdjectiveClass where
   /-- Necessity-relative threshold — *decent*, *acceptable* ([beltrama-2025]). -/
   | mildlyPositive
   /-- Non-gradable: no degree argument, no scale — *atomic*, *prime*,
-  *deceased*, *pregnant*. Outside the `GradablePredicate` fragment;
+  *deceased*, *pregnant*. Outside the gradable (`DirectedMeasure`) system;
   consumers that classify a general adjective should map non-gradables
   here rather than coercing them into a gradable class. -/
   | nonGradable
diff --git a/Linglib/Semantics/Degree/DirectedMeasure.lean b/Linglib/Semantics/Degree/DirectedMeasure.lean
index 3a6ddc142..dbb116647 100644
--- a/Linglib/Semantics/Degree/DirectedMeasure.lean
+++ b/Linglib/Semantics/Degree/DirectedMeasure.lean
@@ -8,9 +8,8 @@ import Linglib.Semantics.Degree.Predicate
 [kennedy-2007] [kennedy-2015] [lassiter-goodman-2017] [krantz-1971]
 
 A `DirectedMeasure D E` packages a degree type, entity type, measure function,
-boundedness classification, and direction. The common algebraic core of
-`GradablePredicate`, degree-domain constructors, and epistemic threshold
-semantics.
+boundedness classification, and direction. The common algebraic core of the
+degree-domain constructors and epistemic threshold semantics.
 
 ## Main declarations
 
@@ -48,9 +47,9 @@ open Core.Order
     an entity type `E`, a measure function `μ : E → D`, boundedness
     (from `ComparativeScale`), and a direction.
 
-    Common algebraic core of `GradablePredicate` (which extends it with `form`),
-    the `numeral`/`adjective` domain constructors, and epistemic thresholds
-    (`DirectedMeasure ℚ (E × (W → Prop))`). The degree property (`atLeastDeg`
+    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. -/
diff --git a/Linglib/Semantics/Degree/Superlative.lean b/Linglib/Semantics/Degree/Superlative.lean
index dbef9352f..7dbd6c660 100644
--- a/Linglib/Semantics/Degree/Superlative.lean
+++ b/Linglib/Semantics/Degree/Superlative.lean
@@ -36,7 +36,7 @@ namespace Semantics.Degree.Superlative
     y ≠ x in C, height(x) > height(y). -/
 def absoluteSuperlative {Entity D : Type*} [LinearOrder D]
     (μ : Entity → D) (C : Set Entity) (x : Entity) : Prop :=
-  x ∈ C ∧ ∀ y ∈ C, y ≠ x → μ x > μ y
+  x ∈ C ∧ ∀ y ∈ C, y ≠ x → comparativeSem μ x y .positive
 
 -- ════════════════════════════════════════════════════
 -- § 2. Relative Superlative
@@ -52,7 +52,7 @@ def absoluteSuperlative {Entity D : Type*} [LinearOrder D]
 def relativeSuperlative {Alt Entity D : Type*} [LinearOrder D]
     (μ : Entity → D) (f : Alt → Entity) (focusedAlt : Alt)
     (alternatives : Set Alt) : Prop :=
-  ∀ a ∈ alternatives, a ≠ focusedAlt → μ (f focusedAlt) > μ (f a)
+  ∀ a ∈ alternatives, a ≠ focusedAlt → comparativeSem μ (f focusedAlt) (f a) .positive
 
 -- ════════════════════════════════════════════════════
 -- § 3. Uniqueness and Definiteness
@@ -104,7 +104,7 @@ theorem superlative_iff_universal_comparative {Entity D : Type*} [LinearOrder D]
     (μ : Entity → D) (C : Set Entity) (x : Entity) :
     absoluteSuperlative μ C x ↔
       x ∈ C ∧ ∀ y ∈ C, y ≠ x →
-        Semantics.Degree.comparativeSem μ x y .positive := by
-  simp [absoluteSuperlative, Semantics.Degree.comparativeSem]
+        Semantics.Degree.comparativeSem μ x y .positive :=
+  Iff.rfl
 
 end Semantics.Degree.Superlative