refactor(Semantics/Degree): retire clausalComparison for overSet

Linglib/Semantics/Degree/Comparative.lean

@@ -9,11 +9,14 @@ import Linglib.Core.Order.Comparison
 [rett-2026] [schwarzschild-2008] [von-stechow-1984] [hoeksema-1983]
 
 Comparative semantics shared across all degree frameworks: the binary
-`comparativeSem` / `equativeSem`, the set-of-degrees generalization
-`clausalComparison`, antonymy as scale reversal, and downward-entailingness of
-*than*-clauses. All three are the measure-pullback predications of the reified
-`Core.Order.Comparison` (`over` at a point standard, `overSet` at a set standard);
-`clausalComparison_eq_overSet` / `comparativeSem_positive_eq_over` make that an identity.
+`comparativeSem` / `equativeSem`, antonymy as scale reversal, and
+downward-entailingness of *than*-clauses. Both binary comparators are
+measure-pullback predications of the reified `Core.Order.Comparison`
+(`over` at a point standard, `overSet` at a set standard);
+`comparativeSem_positive_eq_over` makes that an identity. The set-of-degrees
+S-comparative ([hoeksema-1983]) *is* `Comparison.gt.overSet μ` directly — there is
+no separate clausal-comparison definition; its properties are stated about `overSet`
+here (anti-additivity) and reuse the `Comparison.overSet`/`over` API for the rest.
 Framework-specific content for [rett-2026] (MAX, ambidirectionality, manner
 implicature) lives in `Studies/Rett2026.lean`; [hoeksema-1983]'s polarity-asymmetry
 consumers in `Studies/Hoeksema1983.lean`.
@@ -22,13 +25,13 @@ consumers in `Studies/Hoeksema1983.lean`.
 
 * `comparativeSem` / `equativeSem` — "A is Adj-er / as-Adj-as B" via a directed
   measure on a scale.
-* `clausalComparison` — set-of-degrees comparative ([hoeksema-1983]), anti-additive in
-  its standard (`clausalComparison_isAntiAdditive`): the algebraic source of
+* `gtOverSet_isAntiAdditive` — the S-comparative `Comparison.gt.overSet μ`
+  ([hoeksema-1983]) is anti-additive in its standard: the algebraic source of
   *than*-clause NPI licensing.
-* `mem_clausalComparison_iff_subset_Iio` / `clausalComparison_singleton` — the set-of-degrees
-  comparative as `Set.Iio` interval inclusion (strict mirror of mathlib's
-  `mem_upperBounds_iff_subset_Iic`), collapsing to the binary comparator at a singleton.
-* `clausalComparison_eq_singleton_of_isGreatest` — a than-clause with a greatest degree
+* `mem_gtOverSet_iff_subset_Iio` — the set-of-degrees comparative as `Set.Iio`
+  interval inclusion (strict mirror of mathlib's `mem_upperBounds_iff_subset_Iic`),
+  collapsing to the binary comparator at a singleton via `Comparison.overSet_singleton`.
+* `gtOverSet_eq_singleton_of_isGreatest` — a than-clause with a greatest degree
   reduces to that degree ([bhatt-pancheva-2004], order-theoretic form).
 * `taller_shorter_antonymy` — antonymy is argument swap plus direction reversal.
 * `comparative_iff_posExt_ssubset` — comparison as extent inclusion ([kennedy-1999]).
@@ -118,72 +121,43 @@ end Boundary
 
 /-! ### Set-of-degrees comparative
 
-The S-comparative `clausalComparison` ([hoeksema-1983] §3.8 Def 7) generalizes
-`comparativeSem` from a single standard to an arbitrary degree-set standard.
-It needs only `[Preorder D]`. -/
+The S-comparative ([hoeksema-1983] §3.8 Def 7) generalizes `comparativeSem` from a
+single standard to an arbitrary degree-set standard. It *is* `Comparison.gt.overSet μ`
+(`μ ⁻¹' strictUpperBounds Δ`) — the strict-`>` set-standard predication of
+`Core.Order.Comparison` — not a separate definition; the binary comparator is its
+singleton case (`Comparison.overSet_singleton`). The properties below are stated
+about `Comparison.gt.overSet μ` directly. Needs only `[Preorder D]`. -/
 
 section SetOfDegrees
 variable {Entity D : Type*} [Preorder D]
 
-/-- S-comparative on a set of degrees ([hoeksema-1983] §3.8 Def 7):
-`y ∈ clausalComparison μ Δ` iff `μ y` strictly exceeds every degree in `Δ`. The
-than-clause supplies the degree set `Δ` (typically existentially closed). -/
-def clausalComparison (μ : Entity → D) (Δ : Set D) : Set Entity :=
-  fun y => ∀ d ∈ Δ, d < μ y
-
-/-- **Grounding**: the set-of-degrees comparative is the strict-`>` *set-standard*
-predication of `Core.Order.Comparison` (`μ ⁻¹' strictUpperBounds Δ`) — the
-fundamental object, with the binary comparator its singleton case
-(`Comparison.overSet_singleton`). True by `rfl`: this is not a reinvention. -/
-theorem clausalComparison_eq_overSet (μ : Entity → D) (Δ : Set D) :
-    clausalComparison μ Δ = Comparison.gt.overSet μ Δ :=
-  rfl
-
-/-- The set-of-degrees comparative as a strict-interval inclusion: `y` clears the
-than-clause iff every standard degree lies strictly below `μ y`. Strict mirror of
-mathlib's `mem_upperBounds_iff_subset_Iic`; both faces are `Iff.rfl` siblings. -/
-theorem mem_clausalComparison_iff_subset_Iio (μ : Entity → D) (Δ : Set D) (y : Entity) :
-    y ∈ clausalComparison μ Δ ↔ Δ ⊆ Set.Iio (μ y) :=
+/-- The set-of-degrees comparative `Comparison.gt.overSet μ` ([hoeksema-1983]) as a
+strict-interval inclusion: `y` clears the than-clause iff every standard degree lies
+strictly below `μ y`. Strict mirror of mathlib's `mem_upperBounds_iff_subset_Iic`;
+both faces are `Iff.rfl` siblings. -/
+theorem mem_gtOverSet_iff_subset_Iio (μ : Entity → D) (Δ : Set D) (y : Entity) :
+    y ∈ Comparison.gt.overSet μ Δ ↔ Δ ⊆ Set.Iio (μ y) :=
   Iff.rfl
 
-/-- A than-clause whose denotation is the single degree `d` reduces to the binary
-comparator `d < μ y`. Strict mirror of mathlib's
-`upperBounds_singleton : upperBounds {a} = Ici a`. -/
-theorem clausalComparison_singleton (μ : Entity → D) (d : D) :
-    clausalComparison μ {d} = {y | d < μ y} := by
-  ext y
-  refine ⟨fun h => h d rfl, ?_⟩
-  intro h x hx
-  rw [Set.mem_singleton_iff] at hx
-  rw [hx]
-  exact h
-
-/-- [hoeksema-1983] Fact 4: the S-comparative is anti-additive in its
-set-of-degrees argument — the algebraic source of NPI licensing in clausal
-*than*-comparatives. -/
-theorem clausalComparison_isAntiAdditive (μ : Entity → D) :
-    Entailment.IsAntiAdditive (clausalComparison μ) :=
+/-- [hoeksema-1983] Fact 4: the S-comparative `Comparison.gt.overSet μ` is
+anti-additive in its set-of-degrees argument — the algebraic source of NPI licensing
+in clausal *than*-comparatives. -/
+theorem gtOverSet_isAntiAdditive (μ : Entity → D) :
+    Entailment.IsAntiAdditive (Comparison.gt.overSet μ) :=
   Entailment.isAntiAdditive_forall_mem (fun d y => d < μ y)
 
-/-- Atomic specialization: at the singleton `{μ b}`, S-comparative membership
-reduces to the binary "taller than `b`" relation. Corollary of
-`clausalComparison_singleton`. -/
-theorem clausalComparison_atomic (μ : Entity → D) (a b : Entity) :
-    a ∈ clausalComparison μ {μ b} ↔ μ b < μ a := by
-  simp only [clausalComparison_singleton, Set.mem_setOf_eq]
-
 /-- **Reduction lemma** ([bhatt-pancheva-2004] §3, order-theoretic form): the
-S-comparative is determined by the *greatest* element of its degree-set
-argument. Needs neither linearity nor density — only `[Preorder D]` and the
+S-comparative `Comparison.gt.overSet μ` is determined by the *greatest* element of its
+degree-set argument. Needs neither linearity nor density — only `[Preorder D]` and the
 `IsGreatest` witness. -/
-theorem clausalComparison_eq_singleton_of_isGreatest (μ : Entity → D) {Δ : Set D}
+theorem gtOverSet_eq_singleton_of_isGreatest (μ : Entity → D) {Δ : Set D}
     {m : D} (hm : IsGreatest Δ m) :
-    clausalComparison μ Δ = clausalComparison μ ({m} : Set D) := by
+    Comparison.gt.overSet μ Δ = Comparison.gt.overSet μ ({m} : Set D) := by
   ext y
   refine ⟨fun h d hd => ?_, fun h d hd => ?_⟩
   · rw [Set.mem_singleton_iff] at hd
-    exact hd ▸ h m hm.1
-  · exact lt_of_le_of_lt (hm.2 hd) (h m rfl)
+    exact hd ▸ h hm.1
+  · exact lt_of_le_of_lt (hm.2 hd) (h rfl)
 
 end SetOfDegrees
 
@@ -207,12 +181,13 @@ extent complementarity rather than being stipulated. -/
 section Extent
 variable {Entity D : Type*} [LinearOrder D]
 
-/-- Bridge: the atomic S-comparative coincides with the binary `comparativeSem`
-on a `LinearOrder`. The set-of-degrees schema strictly generalizes the binary
-comparator. -/
-theorem clausalComparison_atomic_eq_comparativeSem (μ : Entity → D) (a b : Entity) :
-    a ∈ clausalComparison μ {μ b} ↔ comparativeSem μ a b .positive :=
-  clausalComparison_atomic μ a b
+/-- Bridge: the atomic S-comparative `Comparison.gt.overSet μ {μ b}` coincides with
+the binary `comparativeSem` on a `LinearOrder`. The set-of-degrees schema strictly
+generalizes the binary comparator, collapsing at a singleton via
+`Comparison.overSet_singleton`. -/
+theorem gtOverSet_atomic_eq_comparativeSem (μ : Entity → D) (a b : Entity) :
+    a ∈ Comparison.gt.overSet μ {μ b} ↔ comparativeSem μ a b .positive := by
+  rw [Comparison.overSet_singleton, ← comparativeSem_positive_eq_over]
 
 /-- "A is taller than B" iff A's positive extent strictly contains B's
 ([kennedy-1999]). Bridges the point comparison to `posExt_ssubset_iff`. -/

Linglib/Semantics/Entailment/AntiAdditivity.lean

@@ -232,7 +232,7 @@ end Bridges
 section ToyWitnesses
 
 /-- Any function of the form `fun X y => ∀ x ∈ X, P x y` is anti-additive in
-`X`. `npComparative` and `clausalComparison` ([hoeksema-1983]) instantiate this
+`X`. `npComparative` and `Comparison.gt.overSet` ([hoeksema-1983]) instantiate this
 with `P x y := μ x < μ y` and `P d y := d < μ y` respectively. -/
 theorem isAntiAdditive_forall_mem {α β : Type*} (P : α → β → Prop) :
     IsAntiAdditive (fun (X : Set α) (y : β) => ∀ x ∈ X, P x y) := by

Linglib/Studies/BhattPancheva2004.lean

@@ -74,7 +74,8 @@ open Minimalist.DegreeMovement
    ScopeBinding IsHeimKennedy not_isHeimKennedy_QP_above_bound_DegP
    isHeimKennedy_no_dependency isHeimKennedy_dependency_requires_high_DegP
    williams_scope_correlation williams_exempt_when_no_binding)
-open Semantics.Degree (clausalComparison clausalComparison_eq_singleton_of_isGreatest)
+open Core.Order (Comparison)
+open Semantics.Degree (gtOverSet_eq_singleton_of_isGreatest)
 open Semantics.Degree.ThanClause (thanClauseDenotation thanClauseMax thanClauseMax_isGreatest)
 open Typology.PolarityItem (LicensingContext)
 open Semantics.Polarity.Licensing (contextProperties)
@@ -154,14 +155,14 @@ theorem bp_hkc_matches_heim_intensional_data :
 
 /-- B&P's clausal-source than-clause denotation `{d | d ≤ μ b}`
     collapses to the singleton `{μ b}` when fed to the S-comparative.
-    Direct corollary of `clausalComparison_eq_singleton_of_isGreatest`
+    Direct corollary of `gtOverSet_eq_singleton_of_isGreatest`
     instantiated at the than-clause's greatest element (the standard's
     measure). -/
 theorem thanClause_reduces_to_max
     {D : Type*} [Preorder D] (μ : Entity → D) (b : Entity) :
-    clausalComparison μ (thanClauseDenotation μ b) =
-      clausalComparison μ ({μ b} : Set D) :=
-  clausalComparison_eq_singleton_of_isGreatest μ (thanClauseMax_isGreatest μ b)
+    Comparison.gt.overSet μ (thanClauseDenotation μ b) =
+      Comparison.gt.overSet μ ({μ b} : Set D) :=
+  gtOverSet_eq_singleton_of_isGreatest μ (thanClauseMax_isGreatest μ b)
 
 /-- Combining [hoeksema-1983] §3.9 (the principal-ultrafilter /
     singleton-degree-set equivalence) with the B&P reduction:
@@ -172,8 +173,8 @@ theorem thanClause_reduces_to_max
 theorem npGQ_principal_eq_sComp_thanClause
     {D : Type*} [Preorder D] (μ : Entity → D) (b : Entity) :
     npComparativeGQ μ (principalUltrafilter b) =
-      clausalComparison μ (thanClauseDenotation μ b) := by
-  rw [npComparativeGQ_principal_eq_clausalComparison_singleton,
+      Comparison.gt.overSet μ (thanClauseDenotation μ b) := by
+  rw [npComparativeGQ_principal_eq_gtOverSet_singleton,
       ← thanClause_reduces_to_max]
 
 -- ════════════════════════════════════════════════════

Linglib/Studies/Gajewski2011.lean

@@ -53,7 +53,7 @@ with "DE + scalar endpoint" (Conjecture 48).
   Gajewski's headline empirical claim made `decide`-checkable over the
   Fragment registry.
 - Hoeksema S-comparative SAA bridge
-  (`bridge_hoeksema_clausalComparison_strawsonAA`) — the positive test case
+  (`bridge_hoeksema_gtOverSet_strawsonAA`) — the positive test case
   for Gajewski's framework: classically AA → strong NPIs predicted ✓.
 
 ## §4 framework — both halves now in skeleton
@@ -472,7 +472,7 @@ context-dependent truncation à la Chierchia 2004 axiom (i)). Deferred.
 - [crnic-2014] challenges Strawson-based analyses with a
   non-monotonicity reanalysis; engages directly with this paper.
 - [hoeksema-1983] S-comparative is anti-additive (per
-  `bridge_hoeksema_clausalComparison_strawsonDE` in VonFintel1999) — hence,
+  `bridge_hoeksema_gtOverSet_strawsonDE` in VonFintel1999) — hence,
   per the Zwarts-classical theory, predicted to license strong NPIs.
   Empirically borne out (Hoeksema's data).
 -/
@@ -604,19 +604,19 @@ theorem only_satisfies_condition2_no_alts (x : World → Prop) :
 /-! ## Hoeksema S-comparative — the positive test case
 
 [hoeksema-1983]'s S-comparative is *classically* anti-additive
-(`Semantics/Degree/Comparative.lean::clausalComparison_isAntiAdditive`),
+(`Semantics/Degree/Comparative.lean::gtOverSet_isAntiAdditive`),
 hence by `antiAdditive_implies_strawsonAA` it is also Strawson-AA.
 This is the **positive test** for Gajewski's framework: an AA operator
 licenses strong NPIs (Hoeksema's data confirms — "Mary is taller than
 anyone is", "in years"-style strong NPIs grammatical in than-S
 comparatives). Contrast vF's recalcitrants which are SAA-but-not-AA
 and hence don't license strong NPIs. -/
-theorem bridge_hoeksema_clausalComparison_strawsonAA
+theorem bridge_hoeksema_gtOverSet_strawsonAA
     {Entity D : Type*} [Preorder D] (μ : Entity → D)
     (defined : Set D → Entity → Prop) :
-    IsStrawsonAntiAdditive (Semantics.Degree.clausalComparison μ) defined :=
+    IsStrawsonAntiAdditive (Core.Order.Comparison.gt.overSet μ) defined :=
   antiAdditive_implies_strawsonAA _
-    (Semantics.Degree.clausalComparison_isAntiAdditive μ) _
+    (Semantics.Degree.gtOverSet_isAntiAdditive μ) _
 
 /-! ## Strong-NPI registry consistency
 

Linglib/Studies/Hoeksema1983.lean

@@ -42,19 +42,19 @@ and arbitrary `sSup`/`sInf` (strengthening Hoeksema's finitary claim)
 gives complement preservation for free on `BooleanAlgebra → BooleanAlgebra`
 homs.
 
-The S-comparative `clausalComparison` (originally [hoeksema-1983] §3.8
-Def 7) and its anti-additivity (Fact 4) live in
-`Semantics/Degree/Comparative.lean` as the natural
-generalization of `comparativeSem` from a binary comparator to a
-degree-set comparator. This file imports them from there.
+The S-comparative is `Core.Order.Comparison.gt.overSet μ` (originally
+[hoeksema-1983] §3.8 Def 7); its anti-additivity (Fact 4,
+`gtOverSet_isAntiAdditive`) lives in `Semantics/Degree/Comparative.lean`
+as the natural generalization of `comparativeSem` from a binary comparator
+to a degree-set comparator. This file imports them from there.
 
 ## Hoeksema's algebraic spine: Definitions 4–8 and Facts 1–4
 
 The §3 algebraic content is formalized in five layers:
 - **Definition 4** (`IsOrderingPreserving`): the abstract property
   `μ b < μ a ↔ a ∈ f Q_b`, where `Q_b = {X | b ∈ X}` is the principal
   ultrafilter at `b` (`principalUltrafilter`).
-- **Definition 7/8** (`clausalComparison` in
+- **Definition 7/8** (`Comparison.gt.overSet μ`, from
   `Semantics/Degree/Comparative.lean`): the S-comparative as
   a set-of-degrees operator.
 - **Fact 1** (`fact1_agree_on_atoms`): two `>`-preserving functions
@@ -68,12 +68,12 @@ The §3 algebraic content is formalized in five layers:
 - **Fact 3** (`npComparativeGQ_monotone`): every Boolean hom is
   monotone increasing — disqualifies the NP-comparative as a Ladusaw
   NPI environment.
-- **Fact 4** (`clausalComparison_isAntiAdditive` in
+- **Fact 4** (`gtOverSet_isAntiAdditive` in
   `Semantics/Degree/Comparative.lean`, cited from
   `IsAntiAdditive.antitone` in `AntiAdditivity.lean`): every
   anti-additive function is antitone — hence the S-comparative
   qualifies as an NPI environment.
-- **§3.9 NP↔S equivalence** (`npComparativeGQ_principal_eq_clausalComparison_singleton`):
+- **§3.9 NP↔S equivalence** (`npComparativeGQ_principal_eq_gtOverSet_singleton`):
   on principal ultrafilters / singleton degree sets, the two
   constructions deliver the same predicate.
 
@@ -95,8 +95,8 @@ namespace Hoeksema1983
 open Semantics.Polarity.Licensing
 
 open Entailment
-open Semantics.Degree (clausalComparison clausalComparison_isAntiAdditive
-  clausalComparison_atomic)
+open Core.Order (Comparison)
+open Semantics.Degree (gtOverSet_isAntiAdditive gtOverSet_atomic_eq_comparativeSem)
 open Typology.PolarityItem (LicensingContext)
 open Semantics.Polarity.Licensing (contextProperties)
 
@@ -317,14 +317,13 @@ theorem npComparativeGQ_uniqueness {μ : Entity → D}
     set `{μ b}`. Both reduce to "is taller than `b`" — explaining the
     empirical equivalence of "I am bigger than you" (NP-form) and
     "I am bigger than you are" (S-form), Hoeksema's Eq. 44a–b. -/
-theorem npComparativeGQ_principal_eq_clausalComparison_singleton
+theorem npComparativeGQ_principal_eq_gtOverSet_singleton
     (μ : Entity → D) (b : Entity) :
-    npComparativeGQ μ (principalUltrafilter b) = clausalComparison μ {μ b} := by
+    npComparativeGQ μ (principalUltrafilter b) = Comparison.gt.overSet μ {μ b} := by
   ext a
-  unfold npComparativeGQ principalUltrafilter clausalComparison npThreshold
-  simp only [CompleteLatticeHom.coe_setPreimage, Set.mem_preimage,
-             Set.mem_setOf_eq, Set.mem_singleton_iff]
-  refine ⟨fun h d hd => hd ▸ h, fun h => h (μ b) rfl⟩
+  unfold npComparativeGQ principalUltrafilter npThreshold
+  simp only [CompleteLatticeHom.coe_setPreimage, Set.mem_preimage, Set.mem_setOf_eq,
+             Comparison.overSet_singleton, Comparison.mem_over, Comparison.rel, gt_iff_lt]
 
 /-! ## Connection to the licensing-context registry -/
 
@@ -336,7 +335,7 @@ theorem comparativeNP_signature_monotone :
     (contextProperties .comparativeNP).strawsonSignature = .mono := rfl
 
 /-- The `.comparativeS` registry slot is anti-additive, matching
-    `clausalComparison_isAntiAdditive`. -/
+    `gtOverSet_isAntiAdditive`. -/
 theorem comparativeS_signature_anti_additive :
     (contextProperties .comparativeS).strawsonSignature = .antiAdd := rfl
 

Linglib/Studies/VonFintel1999.lean

@@ -491,18 +491,18 @@ theorem bridge_lahiri_glad_settle_overgeneration :
 
 /-- **Hoeksema's S-comparative is anti-additive, hence trivially Strawson-DE.**
     [hoeksema-1983] proves the S-comparative anti-additive
-    (`Semantics.Degree.clausalComparison_isAntiAdditive`); the
+    (`Semantics.Degree.gtOverSet_isAntiAdditive`); the
     inheritance chain AA → DE → Strawson-DE makes the bridge automatic.
 
     This places the S-comparative in the same Strawson-DE class as
     [von-fintel-1999]'s recalcitrants, but with the additional
     classical AA backing — meaning S-comparatives license *strong* NPIs
     too (whereas vF's `only` only licenses weak NPIs). -/
-theorem bridge_hoeksema_clausalComparison_strawsonDE
+theorem bridge_hoeksema_gtOverSet_strawsonDE
     {Entity D : Type*} [Preorder D] (μ : Entity → D)
     (defined : Set D → Entity → Prop) :
-    IsStrawsonDE (Semantics.Degree.clausalComparison μ) defined :=
+    IsStrawsonDE (Core.Order.Comparison.gt.overSet μ) defined :=
   antitone_implies_strawsonDE _
-    (Semantics.Degree.clausalComparison_isAntiAdditive μ).antitone defined
+    (Semantics.Degree.gtOverSet_isAntiAdditive μ).antitone defined
 
 end VonFintel1999