diff --git a/Linglib.lean b/Linglib.lean
index 5b3fa15d0..78b3a6dfc 100644
--- a/Linglib.lean
+++ b/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
diff --git a/Linglib/Core/Logic/FirstOrder/Lindstrom.lean b/Linglib/Core/Logic/FirstOrder/Lindstrom.lean
index 0a817d0bd..2ffd71db0 100644
--- a/Linglib/Core/Logic/FirstOrder/Lindstrom.lean
+++ b/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
 
diff --git a/Linglib/Core/Order/Opposition.lean b/Linglib/Core/Order/Opposition.lean
new file mode 100644
index 000000000..8e07d0bb5
--- /dev/null
+++ b/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
diff --git a/Linglib/Core/Order/Relation.lean b/Linglib/Core/Order/Relation.lean
index 4cf895e56..99861bd84 100644
--- a/Linglib/Core/Order/Relation.lean
+++ b/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
 
diff --git a/Linglib/Semantics/Quantification/Lindstrom.lean b/Linglib/Semantics/Quantification/Lindstrom.lean
index 1c06d0ab5..89b286b9a 100644
--- a/Linglib/Semantics/Quantification/Lindstrom.lean
+++ b/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) :
diff --git a/Linglib/Semantics/Tense/DeRe.lean b/Linglib/Semantics/Tense/DeRe.lean
index 2cd1d188f..d3ffabcec 100644
--- a/Linglib/Semantics/Tense/DeRe.lean
+++ b/Linglib/Semantics/Tense/DeRe.lean
@@ -37,7 +37,7 @@ live in `Studies/Abusch1997.lean`.
   property that distinguishes de re from de dicto temporal anaphora.
   `IsRigidOn` (set-relativized) is the workhorse for modal-alternative
   rigidity.
-- `Semantics.Context.KContext W E P T` (`Core/Context/Basic.lean`) — the
+- `Semantics.Context.KContext W E P T` (`Semantics/Context/Basic.lean`) — the
   centered Kaplanian context `⟨agent, addressee, world, time, position⟩`.
   Abusch's `⟨x_self, t_now, w⟩` is a 3-field projection; `KContext` is
   the richer object the rest of linglib already commits to.
@@ -56,11 +56,11 @@ live in `Studies/Abusch1997.lean`.
 
 ## Two felicity predicates (value-level vs Abusch-faithful)
 
-- `isFelicitousWith` — local constraint check at the holder's now
+- `IsFelicitousWith` — local constraint check at the holder's now
   (= `holderContext.time`). The value-level shadow of Abusch's
   reading. Equivalent to `TensePronoun.fullPresupposition` (see
   shadow lemma).
-- `isAbuschFelicitous` — adds Abusch §3 modal rigidity: the
+- `IsAbuschFelicitous` — adds Abusch §3 modal rigidity: the
   time-concept identifies the same time across an alternative-set
   parameter. The substrate is **agnostic** about whether the
   alternatives are doxastic (Hintikka belief alternatives, the
@@ -92,9 +92,14 @@ live in `Studies/Abusch1997.lean`.
   exposes the *output* of res-movement (a coherent ⟨concept, holder⟩
   bundle), not the syntactic operation that produces it.
 - **PLA-side individual unification.** The `EntityConcept` analog at
-  `Idx := Assignment E × WitnessSeq E` is what PLA's `Concept E` is
-  (definitionally); the formal unification theorem is in
-  `Studies/Abusch1997.lean`.
+  `Idx := Assignment E × WitnessSeq E` (PLA's `Poss E`) *is* PLA's
+  `Concept E` definitionally — both unfold to `Intension (Poss E) E`.
+  What `Studies/Abusch1997.lean` proves is the *acquaintance-predicate*
+  unification (`pla_isAcquaintedWith_unifies_with_polymorphic`, by
+  `Iff.rfl`): PLA's individual de re and this file's temporal de re are
+  the same polymorphic `Reference.Acquaintance.isAcquaintedWith` at
+  their respective indices. A concept-type unification theorem is not
+  separately stated.
 -/
 
 namespace Tense.DeRe
@@ -172,7 +177,7 @@ theorem baseCoherent (dr : TemporalDeReReading W E P T) :
     for embedded tenses — a past-marked tense res-moved from under
     `believe` is constrained to denote a time before the believer's
     now, NOT before the outer speaker's speech time. -/
-def isFelicitousWith [LinearOrder T] (dr : TemporalDeReReading W E P T)
+def IsFelicitousWith [LinearOrder T] (dr : TemporalDeReReading W E P T)
     (constraint : Finset Ordering) : Prop :=
   Core.Order.holds constraint dr.actualRes dr.holderContext.time
 
@@ -190,8 +195,8 @@ theorem isFelicitousWith_iff_tensePronoun_fullPresupposition
     (g : TemporalAssignment T)
     (hRes : tp.resolve g = dr.actualRes)
     (hEval : tp.evalTime g = dr.holderContext.time) :
-    dr.isFelicitousWith tp.constraint ↔ tp.fullPresupposition g := by
-  simp only [isFelicitousWith, TensePronoun.fullPresupposition, hRes, hEval]
+    dr.IsFelicitousWith tp.constraint ↔ tp.fullPresupposition g := by
+  simp only [IsFelicitousWith, TensePronoun.fullPresupposition, hRes, hEval]
 
 
 /-! ### Modal-alternative quantification (Abusch §3) -/
@@ -227,12 +232,12 @@ def IsRigidAcrossAlternatives (dr : TemporalDeReReading W E P T)
 /-- **Full Abusch felicity** ([abusch-1997] §3): value-level
     constraint check (actual res-time stands in the constraint's
     relation to the holder's now) AND modal rigidity across a
-    supplied alternative-set. The value-level shadow `isFelicitousWith`
+    supplied alternative-set. The value-level shadow `IsFelicitousWith`
     captures only the first conjunct; this predicate is what an
     Abusch-faithful study should use. -/
-def isAbuschFelicitous [LinearOrder T] (dr : TemporalDeReReading W E P T)
+def IsAbuschFelicitous [LinearOrder T] (dr : TemporalDeReReading W E P T)
     (alternatives : Set (WorldTimeIndex W T)) (constraint : Finset Ordering) : Prop :=
-  dr.isFelicitousWith constraint ∧ dr.IsRigidAcrossAlternatives alternatives
+  dr.IsFelicitousWith constraint ∧ dr.IsRigidAcrossAlternatives alternatives
 
 /-- A rigid time-concept (constant intension, `Intensional.Intension.IsRigid`)
     is automatically rigid across any alternative-set. The rigid-concept
@@ -247,7 +252,7 @@ def isAbuschFelicitous [LinearOrder T] (dr : TemporalDeReReading W E P T)
     visible: temporal de re ≡ rigidity preserved under the centered
     coordinate-shift, restricted to whichever alternative set the
     consumer supplies. -/
-theorem IsRigidAcrossAlternatives_of_concept_isRigid
+theorem isRigidAcrossAlternatives_of_isRigid
     (dr : TemporalDeReReading W E P T)
     (h : Intension.IsRigid dr.concept)
     (alternatives : Set (WorldTimeIndex W T)) :
@@ -256,14 +261,14 @@ theorem IsRigidAcrossAlternatives_of_concept_isRigid
 
 /-- **Abusch felicity ⇒ value-level felicity**: the modal-quantified
     predicate strictly refines the value-level shadow. Old code that
-    only checks `isFelicitousWith` is conservative — anything proved
-    via `isAbuschFelicitous` projects through. -/
+    only checks `IsFelicitousWith` is conservative — anything proved
+    via `IsAbuschFelicitous` projects through. -/
 theorem isFelicitousWith_of_isAbuschFelicitous [LinearOrder T]
     (dr : TemporalDeReReading W E P T)
     (alternatives : Set (WorldTimeIndex W T))
     (constraint : Finset Ordering)
-    (h : dr.isAbuschFelicitous alternatives constraint) :
-    dr.isFelicitousWith constraint := h.1
+    (h : dr.IsAbuschFelicitous alternatives constraint) :
+    dr.IsFelicitousWith constraint := h.1
 
 
 /-! ### Alternative-set constructors (modal-base instantiations) -/
@@ -303,7 +308,7 @@ abbrev TimeCover (W E P T : Type*) :=
     out `t` at `c`. The temporal analog of [lewis-1979-attitudes]'s
     acquaintance — instantiating polymorphic `isAcquaintedWith` at
     `Idx := KContext`, `Res := T`. -/
-abbrev isTemporallyAcquaintedWith {W E P T : Type*}
+abbrev isTemporallyAcquaintedWith
     (t : T) (C : TimeCover W E P T) (c : KContext W E P T) : Prop :=
   Semantics.Reference.Acquaintance.isAcquaintedWith t C c
 
diff --git a/Linglib/Semantics/Tense/Defs.lean b/Linglib/Semantics/Tense/Defs.lean
index 4b47954f3..0b16c9440 100644
--- a/Linglib/Semantics/Tense/Defs.lean
+++ b/Linglib/Semantics/Tense/Defs.lean
@@ -39,4 +39,8 @@ abbrev future : Finset Ordering := after
     circumstantial modals have future-oriented readings (⟦NPST⟧ requires ref ≥ perspective). -/
 abbrev nonpast : Finset Ordering := notBefore
 
+/-- [klecha-2016]'s point made literal: nonpast **is** the Boolean join of present and future in the
+    comparison-category algebra (`Core.Order`), not a fourth atomic tense. -/
+theorem nonpast_eq_present_sup_future : nonpast = present ⊔ future := by decide
+
 end Tense
diff --git a/Linglib/Studies/Abusch1997.lean b/Linglib/Studies/Abusch1997.lean
index dd35dfe4b..f6aeb8119 100644
--- a/Linglib/Studies/Abusch1997.lean
+++ b/Linglib/Studies/Abusch1997.lean
@@ -184,7 +184,7 @@ theorem abusch_derives_temporal_de_re_via_acquaintance
     {W E P Time : Type*} [LinearOrder Time]
     (dr : Tense.DeRe.TemporalDeReReading W E P Time)
     (hBefore : dr.actualRes < dr.holderContext.time) :
-    dr.isFelicitousWith Tense.past :=
+    dr.IsFelicitousWith Tense.past :=
   (Core.Order.holds_before dr.actualRes dr.holderContext.time).mpr hBefore
 
 /-- [abusch-1997]'s temporal de re with **modal-alternative
@@ -193,7 +193,7 @@ theorem abusch_derives_temporal_de_re_via_acquaintance
     `alternatives : Set (WorldTimeIndex W Time)`. The substrate is
     modal-base-agnostic; this theorem holds for any alternative-set
     the consumer supplies (doxastic, metaphysical, or other). The
-    full `isAbuschFelicitous` predicate combines the value-level past
+    full `IsAbuschFelicitous` predicate combines the value-level past
     constraint with this modal rigidity.
 
     A rigid time-concept (constant intension) discharges the modal
@@ -205,9 +205,9 @@ theorem abusch_derives_temporal_de_re_full
     (hRigid : Intensional.Intension.IsRigid dr.concept)
     (alternatives : Set (Intensional.WorldTimeIndex W Time))
     (hBefore : dr.actualRes < dr.holderContext.time) :
-    dr.isAbuschFelicitous alternatives Tense.past := by
+    dr.IsAbuschFelicitous alternatives Tense.past := by
   refine ⟨(Core.Order.holds_before dr.actualRes dr.holderContext.time).mpr hBefore, ?_⟩
-  exact Tense.DeRe.TemporalDeReReading.IsRigidAcrossAlternatives_of_concept_isRigid
+  exact Tense.DeRe.TemporalDeReReading.isRigidAcrossAlternatives_of_isRigid
     dr hRigid alternatives
 
 /-- **Metaphysical-instantiation specialization** of
@@ -221,7 +221,7 @@ theorem abusch_derives_temporal_de_re_full_metaphysical
     (hRigid : Intensional.Intension.IsRigid dr.concept)
     (history : HistoricalAlternatives W Time)
     (hBefore : dr.actualRes < dr.holderContext.time) :
-    dr.isAbuschFelicitous (dr.metaphysicalAlternatives history) Tense.past :=
+    dr.IsAbuschFelicitous (dr.metaphysicalAlternatives history) Tense.past :=
   abusch_derives_temporal_de_re_full dr hRigid _ hBefore
 
 /-- **PLA ↔ Abusch substrate unification**: PLA's `isAcquaintedWith`
diff --git a/Linglib/Studies/HeimComments1994.lean b/Linglib/Studies/HeimComments1994.lean
index b8d316d74..f04d5ff42 100644
--- a/Linglib/Studies/HeimComments1994.lean
+++ b/Linglib/Studies/HeimComments1994.lean
@@ -185,7 +185,7 @@ theorem toSubstrate_factors_iff_agent_blind {W E P T : Type*}
     `Tense.upperLimitConstraint` (typed `[LE Time]`,
     anchored to [heim-1994-comments] in its docstring). This
     bridge theorem projects the substrate's `TemporalDeReReading`
-    `isFelicitousWith .past` (strict `<`) onto the substrate's ULC
+    `IsFelicitousWith .past` (strict `<`) onto the substrate's ULC
     primitive (weak `≤`), via `le_of_lt`.
 
     The implication is one-way: substrate `.past` is strict precedence,
@@ -196,7 +196,7 @@ theorem toSubstrate_factors_iff_agent_blind {W E P T : Type*}
 theorem isFelicitousWith_past_imp_upperLimitConstraint
     {W E P T : Type*} [LinearOrder T]
     (dr : TemporalDeReReading W E P T)
-    (h : dr.isFelicitousWith Tense.past) :
+    (h : dr.IsFelicitousWith Tense.past) :
     Tense.upperLimitConstraint
       dr.actualRes dr.holderContext.time :=
   le_of_lt ((Core.Order.holds_before dr.actualRes dr.holderContext.time).mp h)