From 6cb0563602ec9886a67c50543cc79d06ac6be7a4 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Fri, 19 Jun 2026 16:12:59 -0700 Subject: [PATCH] refactor(Semantics/Degree): reify maxOnScale via Comparison --- Linglib/Semantics/Degree/Bounds.lean | 52 ++++++++++++----------- Linglib/Semantics/Degree/Comparative.lean | 6 +-- Linglib/Studies/BeaverCondoravdi2003.lean | 6 +-- Linglib/Studies/Rett2020.lean | 20 +++++---- 4 files changed, 46 insertions(+), 38 deletions(-) diff --git a/Linglib/Semantics/Degree/Bounds.lean b/Linglib/Semantics/Degree/Bounds.lean index b89c737b7..d963f291b 100644 --- a/Linglib/Semantics/Degree/Bounds.lean +++ b/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 diff --git a/Linglib/Semantics/Degree/Comparative.lean b/Linglib/Semantics/Degree/Comparative.lean index bbd81f265..0ec7ccf40 100644 --- a/Linglib/Semantics/Degree/Comparative.lean +++ b/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] diff --git a/Linglib/Studies/BeaverCondoravdi2003.lean b/Linglib/Studies/BeaverCondoravdi2003.lean index f42db37cb..64c46cb67 100644 --- a/Linglib/Studies/BeaverCondoravdi2003.lean +++ b/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 diff --git a/Linglib/Studies/Rett2020.lean b/Linglib/Studies/Rett2020.lean index 89540bd80..a61e628f5 100644 --- a/Linglib/Studies/Rett2020.lean +++ b/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 -- ============================================================================