feat(Core): instantiate holds & LindstromQuantifier as mathlib homs

Linglib.lean

@@ -251,6 +251,7 @@ import Linglib.Semantics.Intensional.WorldTimeIndex
 import Linglib.Core.Order.Interval
 import Linglib.Semantics.Aspect.Boundedness
 import Linglib.Core.Order.Relation
+import Linglib.Core.Order.Opposition
 import Linglib.Semantics.Aspect.AtomDist
 import Linglib.Core.Order.AllenRelation
 import Linglib.Semantics.Tense.Orientation

Linglib/Core/Logic/FirstOrder/Lindstrom.lean

@@ -1,4 +1,5 @@
 import Mathlib.ModelTheory.Bundled
+import Mathlib.Order.Hom.Lattice
 
 /-!
 # Lindström generalized quantifiers
@@ -19,8 +20,10 @@ and the linguistic generalized-quantifier API live downstream in `Semantics.Quan
 ## Main definitions
 
 * `FirstOrder.Language.LindstromQuantifier` — an iso-invariant class of `L`-structures.
-* `compl`/`inf`/`sup` — the Boolean algebra of generalized quantifiers (closed under
-  complement, intersection, union, since iso-invariance is preserved).
+* `BooleanAlgebra (LindstromQuantifier L)` — the Boolean algebra of generalized quantifiers
+  (`Qᶜ` outer negation, `Q ⊓ R`/`Q ⊔ R` conjunction/disjunction, `⊤`/`⊥` the trivial quantifiers),
+  obtained by pulling the powerset algebra back along the injective `holds`; `holdsHom` bundles that
+  embedding as a `BoundedLatticeHom`.
 -/
 
 universe u v w
@@ -43,29 +46,58 @@ namespace LindstromQuantifier
 
 variable {L : Language.{u, v}}
 
-/-- Outer negation `¬Q`: the structures *not* in `Q`. (`every ↦ not-every`.) -/
-def compl (Q : LindstromQuantifier.{u, v, w} L) : LindstromQuantifier.{u, v, w} L where
-  holds := Q.holdsᶜ
-  iso_inv h := not_congr (Q.iso_inv h)
-
-/-- Meet `Q ⊓ R`: structures in both classes (conjunction of quantifiers). -/
-def inf (Q R : LindstromQuantifier.{u, v, w} L) : LindstromQuantifier.{u, v, w} L where
-  holds := Q.holds ∩ R.holds
-  iso_inv h := and_congr (Q.iso_inv h) (R.iso_inv h)
-
-/-- Join `Q ⊔ R`: structures in either class (disjunction of quantifiers). -/
-def sup (Q R : LindstromQuantifier.{u, v, w} L) : LindstromQuantifier.{u, v, w} L where
-  holds := Q.holds ∪ R.holds
-  iso_inv h := or_congr (Q.iso_inv h) (R.iso_inv h)
-
-@[simp] theorem compl_holds (Q : LindstromQuantifier.{u, v, w} L) : Q.compl.holds = Q.holdsᶜ := rfl
-@[simp] theorem inf_holds (Q R : LindstromQuantifier.{u, v, w} L) :
-    (Q.inf R).holds = Q.holds ∩ R.holds := rfl
-@[simp] theorem sup_holds (Q R : LindstromQuantifier.{u, v, w} L) :
-    (Q.sup R).holds = Q.holds ∪ R.holds := rfl
-
-@[simp] theorem compl_compl (Q : LindstromQuantifier.{u, v, w} L) : Q.compl.compl = Q := by
-  ext : 1; simp
+/-! ### Boolean-algebra structure
+
+The iso-invariant classes are a sub-Boolean-algebra of `Set (Bundled L.Structure)` — closed under
+complement, finite meet/join, `⊤` (all structures) and `⊥` (none), because `L`-isomorphism is an
+equivalence. `holds` is the injective embedding, so the algebra is pulled back along it: `Qᶜ` is
+outer negation (`every ↦ not-every`), `Q ⊓ R`/`Q ⊔ R` are conjunction/disjunction. -/
+
+instance : LE (LindstromQuantifier.{u, v, w} L) := ⟨fun Q R => Q.holds ≤ R.holds⟩
+instance : LT (LindstromQuantifier.{u, v, w} L) := ⟨fun Q R => Q.holds < R.holds⟩
+instance : Max (LindstromQuantifier.{u, v, w} L) :=
+  ⟨fun Q R => ⟨Q.holds ∪ R.holds, fun h => or_congr (Q.iso_inv h) (R.iso_inv h)⟩⟩
+instance : Min (LindstromQuantifier.{u, v, w} L) :=
+  ⟨fun Q R => ⟨Q.holds ∩ R.holds, fun h => and_congr (Q.iso_inv h) (R.iso_inv h)⟩⟩
+instance : Top (LindstromQuantifier.{u, v, w} L) := ⟨⟨Set.univ, fun _ => Iff.rfl⟩⟩
+instance : Bot (LindstromQuantifier.{u, v, w} L) := ⟨⟨∅, fun _ => Iff.rfl⟩⟩
+instance : Compl (LindstromQuantifier.{u, v, w} L) :=
+  ⟨fun Q => ⟨Q.holdsᶜ, fun h => not_congr (Q.iso_inv h)⟩⟩
+instance : SDiff (LindstromQuantifier.{u, v, w} L) :=
+  ⟨fun Q R => ⟨Q.holds \ R.holds,
+    fun h => by simp only [Set.mem_sdiff]; exact and_congr (Q.iso_inv h) (not_congr (R.iso_inv h))⟩⟩
+instance : HImp (LindstromQuantifier.{u, v, w} L) :=
+  ⟨fun Q R => ⟨Q.holds ⇨ R.holds,
+    fun h => by simp only [himp_eq]; exact or_congr (R.iso_inv h) (not_congr (Q.iso_inv h))⟩⟩
+
+theorem holds_injective : Function.Injective (holds : LindstromQuantifier.{u, v, w} L → _) :=
+  fun _ _ h => LindstromQuantifier.ext h
+
+/-- The Boolean algebra of generalized quantifiers over `L`, pulled back along the injective `holds`
+embedding into the powerset algebra `Set (Bundled L.Structure)`. -/
+instance : BooleanAlgebra (LindstromQuantifier.{u, v, w} L) :=
+  Function.Injective.booleanAlgebra holds holds_injective
+    (fun {_ _} => Iff.rfl) (fun {_ _} => Iff.rfl)
+    (fun _ _ => rfl) (fun _ _ => rfl) rfl rfl (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
+
+@[simp] theorem holds_sup (Q R : LindstromQuantifier.{u, v, w} L) :
+    (Q ⊔ R).holds = Q.holds ∪ R.holds := rfl
+@[simp] theorem holds_inf (Q R : LindstromQuantifier.{u, v, w} L) :
+    (Q ⊓ R).holds = Q.holds ∩ R.holds := rfl
+@[simp] theorem holds_compl (Q : LindstromQuantifier.{u, v, w} L) : Qᶜ.holds = Q.holdsᶜ := rfl
+@[simp] theorem holds_top : (⊤ : LindstromQuantifier.{u, v, w} L).holds = Set.univ := rfl
+@[simp] theorem holds_bot : (⊥ : LindstromQuantifier.{u, v, w} L).holds = ∅ := rfl
+
+/-- `holds` bundled: the embedding of the generalized-quantifier Boolean algebra into the powerset
+algebra `Set (Bundled L.Structure)` is a `BoundedLatticeHom` (it also preserves `ᶜ`, see
+`holds_compl`) — the Lindström analogue of `Core.Order.holdsHom`. -/
+def holdsHom :
+    BoundedLatticeHom (LindstromQuantifier.{u, v, w} L) (Set (Bundled.{w} L.Structure)) where
+  toFun := holds
+  map_sup' _ _ := rfl
+  map_inf' _ _ := rfl
+  map_top' := rfl
+  map_bot' := rfl
 
 end LindstromQuantifier
 

Linglib/Core/Order/Opposition.lean

@@ -0,0 +1,53 @@
+import Linglib.Core.Order.Relation
+import Linglib.Core.Logic.Aristotelian.Basic
+
+/-!
+# Comparison categories as an Aristotelian diagram
+
+The eight comparison categories (`Core.Order.Relation`) are the elements of the Boolean algebra
+`𝒫 {lt, eq, gt}`; their logical oppositions are exactly the four Aristotelian relations
+[demey-smessaert-2018] (`Core.Logic.Aristotelian`). This file is where the two finite-Boolean-algebra
+developments meet: the comparison/point algebra (with `holds` its relation-algebra homomorphism) and
+the theory of opposition (over any `[BooleanAlgebra α]`).
+
+Because `Finset Ordering` *is* a `BooleanAlgebra`, the Aristotelian relations apply to the named
+categories with no bridge construction — the classic square of opposition for `<`/`=`/`>` is a
+`decide`-check over the eight-element carrier. Via `Tense.past = before` etc.
+(`Semantics/Tense/Defs.lean`) these specialise to grammatical tense: past and nonpast are
+contradictories, past and future contraries, `≤` and `≥` subcontraries.
+-/
+
+namespace Core.Order
+
+open Aristotelian
+
+/-! ### The square of opposition for `<`/`=`/`>` -/
+
+/-- `<` and `≥` are **contradictories**: `before` and `notBefore` are complementary cells of
+    `𝒫 {lt, eq, gt}` — exactly one holds of any pair. -/
+theorem isContradictory_before_notBefore : IsContradictory before notBefore := by decide
+
+/-- `>` and `≤` are **contradictories**. -/
+theorem isContradictory_after_notAfter : IsContradictory after notAfter := by decide
+
+/-- `<` and `>` are **contraries**: disjoint (never both) but not jointly exhaustive — both fail
+    at `=`. -/
+theorem isContrary_before_after : IsContrary before after := by decide
+
+/-- `≤` and `≥` are **subcontraries**: jointly exhaustive (one always holds) but not disjoint —
+    both hold at `=`. -/
+theorem isSubcontrary_notAfter_notBefore : IsSubcontrary notAfter notBefore := by decide
+
+/-- `<` is **subaltern** to `≤`: strict precedence implies weak precedence. -/
+theorem isSubaltern_before_notAfter : IsSubaltern before notAfter := by decide
+
+/-- `>` is **subaltern** to `≥`. -/
+theorem isSubaltern_after_notBefore : IsSubaltern after notBefore := by decide
+
+/-- The two-axis classifier agrees: `<` opposes `≥` as a contradictory. -/
+theorem opposition_before_notBefore : opposition before notBefore = .contradictory := by decide
+
+/-- `=` and `≠` are **contradictories**: `overlapping` and `distinct` partition the carrier. -/
+theorem isContradictory_overlapping_distinct : IsContradictory overlapping distinct := by decide
+
+end Core.Order

Linglib/Core/Order/Relation.lean

@@ -1,4 +1,5 @@
 import Mathlib.Order.Compare
+import Mathlib.Order.Hom.Lattice
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Finset.Union
@@ -15,6 +16,14 @@ This is framework-agnostic order theory (the point analogue of `AllenRelation` f
 generic over any `[LinearOrder α]` and bakes in **no** notion of time. Tense, evidential, and
 modal-base-time semantics each supply the order (`Time`) and name the categories they use
 (`Tense.past = before`, etc.).
+
+`Finset Ordering` is the eight-element Boolean algebra `𝒫 {lt, eq, gt}` — the Aristotelian diagram of
+the trichotomy, with the three singletons as atoms and `≤`/`≥`/`≠` as their joins. For each pair
+`a, b`, the map `s ↦ holds s a b` is its **Stone-dual point-evaluation** at `compare a b`: a
+`BoundedLatticeHom` into `Prop` (`holdsHom`, `holds_sup`/`holds_inf`/`holds_compl`/`holds_top`/
+`holds_bot`). Together with `converse` (↦ `SetRel.inv`) and `comp` (↦ `SetRel.comp`) below, this
+exhibits `holds` as a homomorphism from the finite point algebra into the relation algebra
+`SetRel α α`, and makes the named categories' `holds_*` reductions corollaries of one morphism.
 -/
 
 namespace Core.Order
@@ -27,22 +36,72 @@ def holds (s : Finset Ordering) (a b : α) : Prop := compare a b ∈ s
 instance (s : Finset Ordering) (a b : α) : Decidable (holds s a b) :=
   inferInstanceAs (Decidable (_ ∈ s))
 
-/-! ### Named comparison categories -/
+/-! ### `holds` as a Boolean-algebra homomorphism
+
+For each pair `a, b`, `s ↦ holds s a b` preserves the Boolean structure of `Finset Ordering`: it is
+point-evaluation of the membership relation at `compare a b`. These are the `∪`/`∩`/`ᶜ`/`⊤`/`⊥` half
+of the relation-algebra homomorphism (the `converse`/`comp` half is below). -/
+
+@[simp] theorem holds_sup (s t : Finset Ordering) (a b : α) :
+    holds (s ⊔ t) a b ↔ holds s a b ∨ holds t a b := by
+  simp only [holds, Finset.sup_eq_union, Finset.mem_union]
+
+@[simp] theorem holds_inf (s t : Finset Ordering) (a b : α) :
+    holds (s ⊓ t) a b ↔ holds s a b ∧ holds t a b := by
+  simp only [holds, Finset.inf_eq_inter, Finset.mem_inter]
+
+@[simp] theorem holds_compl (s : Finset Ordering) (a b : α) :
+    holds sᶜ a b ↔ ¬ holds s a b := by
+  simp only [holds, Finset.mem_compl]
+
+@[simp] theorem holds_top (a b : α) : holds (⊤ : Finset Ordering) a b ↔ True := by
+  simp only [holds, Finset.top_eq_univ, Finset.mem_univ]
+
+@[simp] theorem holds_bot (a b : α) : holds (⊥ : Finset Ordering) a b ↔ False := by
+  simp only [holds, Finset.bot_eq_empty, Finset.notMem_empty]
 
-/-- `a < b`. -/
+/-- `holds`, bundled. For every `[LinearOrder α]`, the map `s ↦ fun a b => holds s a b` is a
+    `BoundedLatticeHom` from the eight-element Boolean algebra `Finset Ordering` (= `𝒫 {lt, eq, gt}`)
+    into the relation algebra `α → α → Prop` — the Stone-dual evaluation of the comparison-category
+    algebra. With `converse` (`holds_converse`) and `comp` (`holds_comp`) it is the point algebra's
+    image in the concrete relation algebra. -/
+def holdsHom : BoundedLatticeHom (Finset Ordering) (α → α → Prop) where
+  toFun s := fun a b => holds s a b
+  map_sup' s t := by ext a b; simp only [Pi.sup_apply, sup_Prop_eq]; exact holds_sup s t a b
+  map_inf' s t := by ext a b; simp only [Pi.inf_apply, inf_Prop_eq]; exact holds_inf s t a b
+  map_top' := by ext a b; simp only [Pi.top_apply]; exact holds_top a b
+  map_bot' := by ext a b; simp only [Pi.bot_apply]; exact holds_bot a b
+
+@[simp] theorem holdsHom_apply (s : Finset Ordering) (a b : α) :
+    holdsHom s a b = holds s a b := rfl
+
+/-! ### Named comparison categories
+
+The three atoms are the singletons `before`/`overlapping`/`after`; every other category is a Boolean
+combination of them, so the composite `holds_*` reductions below are corollaries of `holds_sup`, not
+separate `compare`-inspections. -/
+
+/-- `a < b` (atom `lt`). -/
 def before : Finset Ordering := {.lt}
-/-- `a > b`. -/
+/-- `a > b` (atom `gt`). -/
 def after : Finset Ordering := {.gt}
-/-- `a = b` (points overlap). -/
+/-- `a = b`, points overlap (atom `eq`). -/
 def overlapping : Finset Ordering := {.eq}
-/-- `a ≤ b`. -/
-def notAfter : Finset Ordering := {.lt, .eq}
-/-- `a ≥ b`. -/
-def notBefore : Finset Ordering := {.gt, .eq}
-/-- no constraint. -/
+/-- `a ≤ b` — the join `before ⊔ overlapping`. -/
+def notAfter : Finset Ordering := before ⊔ overlapping
+/-- `a ≥ b` — the join `after ⊔ overlapping`. -/
+def notBefore : Finset Ordering := after ⊔ overlapping
+/-- `a ≠ b` — the join `before ⊔ after` (the one non-convex category). -/
+def distinct : Finset Ordering := before ⊔ after
+/-- no constraint (`= ⊤`, see `unrestricted_eq_top`); kept as the explicit literal so the
+    `decide`-checked relation-algebra laws below reduce without unfolding `Finset.univ`. -/
 def unrestricted : Finset Ordering := {.lt, .eq, .gt}
 
-/-! ### Reductions to the underlying order (so consumers' `<`-shaped proofs go through) -/
+/-! ### Reductions to the underlying order (so consumers' `<`-shaped proofs go through)
+
+`holds_before`/`holds_after`/`holds_overlapping` discharge the three atoms; each composite category
+then reduces through the homomorphism (`holds_sup`) plus those atoms, rather than by re-inspecting
+`compare`. -/
 
 @[simp] theorem holds_before (a b : α) : holds before a b ↔ a < b := by
   simp [holds, before, compare_lt_iff_lt]
@@ -51,17 +110,15 @@ def unrestricted : Finset Ordering := {.lt, .eq, .gt}
 @[simp] theorem holds_overlapping (a b : α) : holds overlapping a b ↔ a = b := by
   simp [holds, overlapping]
 @[simp] theorem holds_notAfter (a b : α) : holds notAfter a b ↔ a ≤ b := by
-  simp [holds, notAfter, compare_lt_iff_lt, le_iff_lt_or_eq]
+  rw [notAfter, holds_sup, holds_before, holds_overlapping, le_iff_lt_or_eq]
 @[simp] theorem holds_notBefore (a b : α) : holds notBefore a b ↔ b ≤ a := by
-  rw [← not_lt, ← compare_lt_iff_lt]
-  simp only [holds, notBefore, Finset.mem_insert, Finset.mem_singleton]
-  cases compare a b <;> simp
+  rw [notBefore, holds_sup, holds_after, holds_overlapping, le_iff_lt_or_eq, eq_comm]
+@[simp] theorem holds_distinct (a b : α) : holds distinct a b ↔ a ≠ b := by
+  rw [distinct, holds_sup, holds_before, holds_after, lt_or_lt_iff_ne]
+/-- `unrestricted` is the top of the comparison-category Boolean algebra. -/
+theorem unrestricted_eq_top : unrestricted = (⊤ : Finset Ordering) := by decide
 @[simp] theorem holds_unrestricted (a b : α) : holds unrestricted a b ↔ True := by
-  simp only [holds, unrestricted, iff_true]
-  rcases lt_trichotomy a b with h | h | h
-  · simp [compare_lt_iff_lt.mpr h]
-  · simp [compare_eq_iff_eq.mpr h]
-  · simp [compare_gt_iff_gt.mpr h]
+  rw [unrestricted_eq_top, holds_top]
 
 /-! ### Relation-algebra structure: converse and composition
 

Linglib/Semantics/Quantification/Lindstrom.lean

@@ -260,9 +260,9 @@ theorem someDet_holds_eq_compl : (someDet.{u}).holds = (noDet.{u}).holdsᶜ := b
 iso-invariant class to GQ outer negation: `(¬Q).toGQ = outerNeg Q.toGQ`
 ([deklerck-vignero-demey-2024]). With `everyDet`, this realizes the `A`/`O` contradictory
 diagonal as `Quantification.every_contradicts_notEvery`. -/
-theorem toGQ_compl (Q : Det.{u}) (α : Type u) : Det.toGQ Q.compl α = outerNeg (Q.toGQ α) := by
+theorem toGQ_compl (Q : Det.{u}) (α : Type u) : Det.toGQ Qᶜ α = outerNeg (Q.toGQ α) := by
   funext A B
-  simp only [Det.toGQ, LindstromQuantifier.compl_holds, Set.mem_compl_iff, outerNeg_apply]
+  simp only [Det.toGQ, LindstromQuantifier.holds_compl, Set.mem_compl_iff, outerNeg_apply]
 
 /-- The `E` corner: `no` realizes the inner negation of `every` (`every…not = no`). -/
 theorem noDet_toGQ_eq_innerNeg (α : Type u) :