refactor(Semantics/Degree): reify maxOnScale via Comparison

Linglib/Semantics/Degree/Bounds.lean

@@ -3,6 +3,7 @@ import Mathlib.Order.BoundedOrder.Basic
 import Mathlib.Order.Max
 import Mathlib.Data.Set.Basic
 import Linglib.Core.Order.Boundedness
+import Linglib.Core.Order.Comparison
 import Linglib.Semantics.Degree.Predicate
 
 /-!
@@ -17,8 +18,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`, `isAmbidirectional` — Rett 2026's relation-parameterized
-   MAX operator + ambidirectionality predicate.
+   `maxOnScale c X`, `isAmbidirectional` — Rett 2026's MAX operator (the
+   dominance direction is the reified `Comparison`) + ambidirectionality predicate.
 
 This file is part of the Phase A decomposition of the legacy
 `Core/Scales/Scale.lean` dumping ground (master plan v4).
@@ -124,24 +125,27 @@ theorem not_noMaxOrder_of_orderTop {β : Type*} [Preorder β] [OrderTop β] :
 
 /-! ### Scale-sensitive maximality operator
 
-[rett-2026]: MAX_R(X) picks the element(s)
-of X that R-dominate all other members. For the `<` scale this is the GLB
-(earliest / smallest), for `>` the LUB (latest / largest). The same operator
+[rett-2026]: MAX_c(X) picks the element(s)
+of X that c-dominate all other members. For the `<` scale (`.lt`) this is the GLB
+(earliest / smallest), for `>` (`.gt`) the LUB (latest / largest). The same operator
 underlies both temporal connectives (*before*/*after*) and degree comparatives.
 
 - Rett, J. (2026). Semantic ambivalence and expletive negation. Ms.
 -/
 
 /-- Order-sensitive maximality ([rett-2026], def. 1):
-    MAX_R(X) = { x ∈ X | ∀ x' ∈ X, x' ≠ x → R x x' }.
-    Domain-general over any relation R and set X. -/
-def maxOnScale {α : Type*} (R : α → α → Prop) (X : Set α) : Set α :=
-  { x | x ∈ X ∧ ∀ x' ∈ X, x' ≠ x → R x x' }
-
-/-- MAX on a singleton is that singleton: MAX_R({x}) = {x}.
-    The universal quantifier is vacuously satisfied. -/
-theorem maxOnScale_singleton {α : Type*} (R : α → α → Prop) (x : α) :
-    maxOnScale R {x} = {x} := by
+    MAX_c(X) = { x ∈ X | ∀ x' ∈ X, x' ≠ x → c.rel x x' }.
+    The dominance relation is the reified `Core.Order.Comparison` rather than a
+    lawless `R : α → α → Prop` — removing the "fake generality" of an unconstrained
+    relation parameter. Each concrete `c` (`.lt`, `.gt`, `.ge`, …) names an
+    order relation via `Comparison.rel`. -/
+def maxOnScale {α : Type*} [Preorder α] (c : Comparison) (X : Set α) : Set α :=
+  { x | x ∈ X ∧ ∀ x' ∈ X, x' ≠ x → c.rel x x' }
+
+/-- MAX on a singleton is that singleton: MAX_c({x}) = {x}.
+    The universal quantifier is vacuously satisfied, so this holds for any `c`. -/
+theorem maxOnScale_singleton {α : Type*} [Preorder α] (c : Comparison) (x : α) :
+    maxOnScale c {x} = {x} := by
   ext y
   simp only [maxOnScale, Set.mem_setOf_eq, Set.mem_singleton_iff]
   constructor
@@ -154,9 +158,9 @@ theorem maxOnScale_singleton {α : Type*} (R : α → α → Prop) (x : α) :
     Dual: MAX₍>₎ on the same interval is `{f}`. -/
 theorem maxOnScale_lt_closedInterval {α : Type*} [LinearOrder α]
     (s f : α) (hsf : s ≤ f) :
-    maxOnScale (· < ·) { x : α | s ≤ x ∧ x ≤ f } = {s} := by
+    maxOnScale .lt { x : α | s ≤ x ∧ x ≤ f } = {s} := by
   ext x
-  simp only [maxOnScale, Set.mem_setOf_eq, Set.mem_singleton_iff]
+  simp only [maxOnScale, Comparison.rel, Set.mem_setOf_eq, Set.mem_singleton_iff]
   constructor
   · rintro ⟨⟨hxs, _⟩, hdom⟩
     by_contra hne
@@ -171,9 +175,9 @@ theorem maxOnScale_lt_closedInterval {α : Type*} [LinearOrder α]
     The maximum element R-dominates all others on the `>` scale. -/
 theorem maxOnScale_gt_closedInterval {α : Type*} [LinearOrder α]
     (s f : α) (hsf : s ≤ f) :
-    maxOnScale (· > ·) { x : α | s ≤ x ∧ x ≤ f } = {f} := by
+    maxOnScale .gt { x : α | s ≤ x ∧ x ≤ f } = {f} := by
   ext x
-  simp only [maxOnScale, Set.mem_setOf_eq, Set.mem_singleton_iff]
+  simp only [maxOnScale, Comparison.rel, Set.mem_setOf_eq, Set.mem_singleton_iff]
   constructor
   · rintro ⟨⟨_, hxf⟩, hdom⟩
     by_contra hne
@@ -193,17 +197,17 @@ def isAmbidirectional {α : Type*} (f : Set α → Prop) (B : Set α) : Prop :=
   f B ↔ f Bᶜ
 
 
-/-- **Bridge**: `maxOnScale (· ≥ ·)` applied to the "at least" degree set
+/-- **Bridge**: `maxOnScale .ge` applied to the "at least" degree set
     `{d | d ≤ μ(w)}` yields `{μ(w)}` — the singleton containing the true
     value. This connects the relational MAX to `IsMaxInf`.
 
-    The convention: `maxOnScale R X` picks elements x ∈ X with `R x x'` for
-    all other x'. With `R = (· ≥ ·)`, this picks elements ≥ all others,
+    The convention: `maxOnScale c X` picks elements x ∈ X with `c.rel x x'` for
+    all other x'. With `c = .ge`, this picks elements ≥ all others,
     i.e., the maximum. -/
 theorem maxOnScale_atLeast_singleton {W : Type*} (μ : W → α) (w : W) :
-    maxOnScale (· ≥ ·) { d : α | d ≤ μ w } = { μ w } := by
+    maxOnScale .ge { d : α | d ≤ μ w } = { μ w } := by
   ext x
-  simp only [maxOnScale, Set.mem_setOf_eq, Set.mem_singleton_iff, ge_iff_le]
+  simp only [maxOnScale, Comparison.rel, Set.mem_setOf_eq, Set.mem_singleton_iff, ge_iff_le]
   constructor
   · rintro ⟨hx, hdom⟩
     by_contra hne
@@ -216,7 +220,7 @@ theorem maxOnScale_atLeast_singleton {W : Type*} (μ : W → α) (w : W) :
 /-- MAX₍≥₎ on {d | d ≤ b} is {b}. Corollary of `maxOnScale_atLeast_singleton`
     with `μ = id`. Used by the comparative boundary theorems. -/
 theorem maxOnScale_ge_atMost (b : α) :
-    maxOnScale (· ≥ ·) {d | d ≤ b} = {b} :=
+    maxOnScale .ge {d | d ≤ b} = {b} :=
   maxOnScale_atLeast_singleton id b
 
 end Semantics.Degree

Linglib/Semantics/Degree/Comparative.lean

@@ -79,7 +79,7 @@ theorem equativeSem_positive_eq_over (μ : Entity → α) (a b : Entity) :
 the MAX-based formulation. -/
 theorem comparativeSem_eq_MAX (μ : Entity → α) (a b : Entity) :
     comparativeSem μ a b .positive ↔
-      ∃ m ∈ maxOnScale (· > ·) ({μ b} : Set α), μ a > m := by
+      ∃ m ∈ maxOnScale .gt ({μ b} : Set α), μ a > m := by
   simp only [comparativeSem, maxOnScale_singleton, Set.mem_singleton_iff, exists_eq_left]
 
 /-! ### Antonymy as scale reversal -/
@@ -104,13 +104,13 @@ variable {α : Type*} [LinearOrder α]
 
 /-- The comparative depends only on the boundary `μ_b`. -/
 theorem comparative_boundary (μ_a μ_b : α) :
-    (∃ m ∈ maxOnScale (· ≥ ·) {d | d ≤ μ_b}, μ_a > m) ↔ μ_a > μ_b := by
+    (∃ m ∈ maxOnScale .ge {d | d ≤ μ_b}, μ_a > m) ↔ μ_a > μ_b := by
   rw [maxOnScale_ge_atMost]
   simp only [Set.mem_singleton_iff, exists_eq_left]
 
 /-- The equative depends only on the boundary `μ_b`. -/
 theorem equative_boundary (μ_a μ_b : α) :
-    (∃ m ∈ maxOnScale (· ≥ ·) {d | d ≤ μ_b}, μ_a ≥ m) ↔ μ_a ≥ μ_b := by
+    (∃ m ∈ maxOnScale .ge {d | d ≤ μ_b}, μ_a ≥ m) ↔ μ_a ≥ μ_b := by
   rw [maxOnScale_ge_atMost]
   simp only [Set.mem_singleton_iff, exists_eq_left]
 

Linglib/Studies/BeaverCondoravdi2003.lean

@@ -165,15 +165,15 @@ def instTimes (worlds : Set W) (B : Set (W × T)) : Set T :=
 /-- `earliest` across alternatives: the earliest time at which B is
     instantiated in any world of `alt(w,t)`.
 
-    Uses `maxOnScale (· < ·)` which selects elements dominated by all others
+    Uses `maxOnScale .lt` which selects elements dominated by all others
     on the < ordering — i.e., the minimum / GLB. This is the same operator
     [rett-2020] uses for her MAX₍<₎. -/
 def earliestAlt (alt : HistAlt W T) (B : Set (W × T)) (w : W) (t : T) : Set T :=
-  maxOnScale (· < ·) (instTimes (alt w t) B)
+  maxOnScale .lt (instTimes (alt w t) B)
 
 /-- Membership in `earliestAlt` is exactly mathlib's `IsLeast` on the
     instantiation-times set: B&C's `earliest` operator is the least element
-    of `instTimes`, computed via `maxOnScale (· < ·)`. -/
+    of `instTimes`, computed via `maxOnScale .lt`. -/
 theorem mem_earliestAlt_iff_isLeast (alt : HistAlt W T) (B : Set (W × T))
     (w : W) (t te : T) :
     te ∈ earliestAlt alt B w t ↔ IsLeast (instTimes (alt w t) B) te := by

Linglib/Studies/Rett2020.lean

@@ -57,12 +57,12 @@ variable {Time : Type*} [LinearOrder Time]
 /-- Rett's *before* (eq. 22a): ∃t ∈ times(A) [t ≺ MAX(times(B)_≺)].
     Some time in A precedes the maximal (on the ≺ scale) time of B. -/
 def Rett.before (A B : SentDenotation Time) : Prop :=
-  ∃ t ∈ timeTrace A, ∃ m ∈ maxOnScale (· < ·) (timeTrace B), t < m
+  ∃ t ∈ timeTrace A, ∃ m ∈ maxOnScale .lt (timeTrace B), t < m
 
 /-- Rett's *after* (eq. 22b): ∃t ∈ times(A) [t ≻ MAX(times(B)_≻)].
     Some time in A succeeds the maximal (on the ≻ scale) time of B. -/
 def Rett.after (A B : SentDenotation Time) : Prop :=
-  ∃ t ∈ timeTrace A, ∃ m ∈ maxOnScale (· > ·) (timeTrace B), t > m
+  ∃ t ∈ timeTrace A, ∃ m ∈ maxOnScale .gt (timeTrace B), t > m
 
 -- ============================================================================
 -- § 2: Aspectual Coercion Operators
@@ -215,7 +215,7 @@ to this bound, so negating B is truth-conditionally vacuous.
 
 /-- *Before* truth conditions depend only on MAX₍<₎ of B's time trace. -/
 theorem before_determined_by_max (A B₁ B₂ : SentDenotation Time)
-    (h : maxOnScale (· < ·) (timeTrace B₁) = maxOnScale (· < ·) (timeTrace B₂)) :
+    (h : maxOnScale .lt (timeTrace B₁) = maxOnScale .lt (timeTrace B₂)) :
     Rett.before A B₁ ↔ Rett.before A B₂ := by
   constructor <;> rintro ⟨t, ht, m, hm, htm⟩ <;> exact ⟨t, ht, m, h ▸ hm, htm⟩
 
@@ -255,7 +255,7 @@ theorem timeTrace_stative_closedInterval (i : NonemptyInterval Time) :
 
 /-- MAX₍<₎ of a stative denotation's time trace is {start}. -/
 theorem maxOnScale_lt_stative (i : NonemptyInterval Time) :
-    maxOnScale (· < ·) (timeTrace (stativeDenotation i)) = {i.fst} := by
+    maxOnScale .lt (timeTrace (stativeDenotation i)) = {i.fst} := by
   rw [timeTrace_stative_closedInterval, maxOnScale_lt_closedInterval _ _ i.fst_le_snd]
 
 /-- The time trace of `COMPLET(preEventDenotation bot i)` is the degenerate
@@ -271,7 +271,7 @@ theorem timeTrace_complet_preEvent (bot : Time) (i : NonemptyInterval Time) (hbo
 
 /-- MAX₍<₎ of the COMPLET of a pre-event denotation is {start}. -/
 theorem maxOnScale_lt_complet_preEvent (bot : Time) (i : NonemptyInterval Time) (hbot : bot ≤ i.fst) :
-    maxOnScale (· < ·) (timeTrace (COMPLET (preEventDenotation bot i hbot))) =
+    maxOnScale .lt (timeTrace (COMPLET (preEventDenotation bot i hbot))) =
     {i.fst} := by
   rw [timeTrace_complet_preEvent, maxOnScale_lt_closedInterval _ _ (le_refl _)]
 
@@ -292,12 +292,12 @@ theorem before_preEvent_ambidirectional (A : SentDenotation Time) (i_B : Nonempt
     truth conditions because MAX₍>₎(B) ≠ MAX₍>₎(¬B). -/
 theorem after_not_ambidirectional (hab : ∃ (a b : Time), a < b) :
     ¬ ∀ (A : SentDenotation Time) (B : Set Time),
-      isAmbidirectional (λ X => ∃ t ∈ timeTrace A, ∃ m ∈ maxOnScale (· > ·) X, t > m) B := by
+      isAmbidirectional (λ X => ∃ t ∈ timeTrace A, ∃ m ∈ maxOnScale .gt X, t > m) B := by
   obtain ⟨a, b, hab⟩ := hab
   intro h
   have h_amb := h {NonemptyInterval.pure b} {a}
   have h_fB : ∃ t ∈ timeTrace ({NonemptyInterval.pure b} : SentDenotation Time),
-      ∃ m ∈ maxOnScale (· > ·) ({a} : Set Time), t > m :=
+      ∃ m ∈ maxOnScale .gt ({a} : Set Time), t > m :=
     ⟨b, ⟨NonemptyInterval.pure b, rfl, le_refl _, le_refl _⟩,
      a, ⟨rfl, fun _ hx' hne => absurd hx' hne⟩, hab⟩
   obtain ⟨t, ht_A, m, ⟨hm_mem, hm_dom⟩, htm⟩ := h_amb.mp h_fB
@@ -443,6 +443,7 @@ theorem scenario1_rett : Rett.before A_early B_stative := by
   refine ⟨1, mem_tt_early.mpr rfl, 5, ⟨mem_tt_stative.mpr ⟨le_refl _, by omega⟩, ?_⟩, by omega⟩
   intro x' hx' hne
   have ⟨h1, _⟩ := mem_tt_stative.mp hx'
+  show 5 < x'
   omega
 
 -- ============================================================================
@@ -460,6 +461,7 @@ theorem scenario2_rett : Rett.after A_late B_stative := by
   refine ⟨12, mem_tt_late.mpr rfl, 10, ⟨mem_tt_stative.mpr ⟨by omega, le_refl _⟩, ?_⟩, by omega⟩
   intro x' hx' hne
   have ⟨_, h2⟩ := mem_tt_stative.mp hx'
+  show 10 > x'
   omega
 
 -- ============================================================================
@@ -480,6 +482,7 @@ theorem scenario3_rett : Rett.before A_early B_telic := by
   refine ⟨1, mem_tt_early.mpr rfl, 3, ⟨mem_tt_telic.mpr ⟨le_refl _, by omega⟩, ?_⟩, by omega⟩
   intro x' hx' hne
   have ⟨h1, _⟩ := mem_tt_telic.mp hx'
+  show 3 < x'
   omega
 
 -- ============================================================================
@@ -497,6 +500,7 @@ theorem scenario4_rett : Rett.after A_late B_telic := by
   refine ⟨12, mem_tt_late.mpr rfl, 8, ⟨mem_tt_telic.mpr ⟨by omega, le_refl _⟩, ?_⟩, by omega⟩
   intro x' hx' hne
   have ⟨_, h2⟩ := mem_tt_telic.mp hx'
+  show 8 > x'
   omega
 
 -- ============================================================================
@@ -524,7 +528,7 @@ theorem scenario6_rett_false : ¬ Rett.after A_inside B_stative := by
   -- If m = 10, then 7 > 10 is false.
   by_cases hm10 : m = 10
   · omega
-  · have h10 := hm_max 10 (mem_tt_stative.mpr ⟨by omega, le_refl _⟩) (Ne.symm hm10)
+  · have h10 : m > 10 := hm_max 10 (mem_tt_stative.mpr ⟨by omega, le_refl _⟩) (Ne.symm hm10)
     omega
 
 -- ============================================================================