diff --git a/Linglib/Data/UD/Basic.lean b/Linglib/Data/UD/Basic.lean
index d97e72c48..6b9123941 100644
--- a/Linglib/Data/UD/Basic.lean
+++ b/Linglib/Data/UD/Basic.lean
@@ -378,7 +378,7 @@ def MorphFeatures.compatible (f1 f2 : MorphFeatures) : Bool :=
     f.compatible f = true := by
   simp only [MorphFeatures.compatible, beq_self_eq_true, Bool.or_true, Bool.and_true]
 
-private theorem MorphFeatures.compat_clause_comm {α : Type _} [BEq α] [LawfulBEq α]
+private theorem MorphFeatures.compatible_clause_comm {α : Type _} [BEq α] [LawfulBEq α]
     (a b : Option α) :
     (a.isNone || b.isNone || a == b) = (b.isNone || a.isNone || b == a) := by
   cases a <;> cases b <;> simp [beq_iff_eq, eq_comm]
@@ -387,13 +387,13 @@ private theorem MorphFeatures.compat_clause_comm {α : Type _} [BEq α] [LawfulB
 theorem MorphFeatures.compatible_comm (f1 f2 : MorphFeatures) :
     f1.compatible f2 = f2.compatible f1 := by
   unfold MorphFeatures.compatible
-  rw [compat_clause_comm f1.number, compat_clause_comm f1.gender,
-      compat_clause_comm f1.case_, compat_clause_comm f1.definite,
-      compat_clause_comm f1.degree, compat_clause_comm f1.pronType,
-      compat_clause_comm f1.person, compat_clause_comm f1.verbForm,
-      compat_clause_comm f1.tense, compat_clause_comm f1.aspect,
-      compat_clause_comm f1.mood, compat_clause_comm f1.voice,
-      compat_clause_comm f1.polarity]
+  rw [compatible_clause_comm f1.number, compatible_clause_comm f1.gender,
+      compatible_clause_comm f1.case_, compatible_clause_comm f1.definite,
+      compatible_clause_comm f1.degree, compatible_clause_comm f1.pronType,
+      compatible_clause_comm f1.person, compatible_clause_comm f1.verbForm,
+      compatible_clause_comm f1.tense, compatible_clause_comm f1.aspect,
+      compatible_clause_comm f1.mood, compatible_clause_comm f1.voice,
+      compatible_clause_comm f1.polarity]
 
 /-- The information-join of two bundles, field-by-field: keep every committed value
     (left-biased per field, which on `compatible` inputs is symmetric since doubly
diff --git a/Linglib/Morphology/Unification.lean b/Linglib/Morphology/Unification.lean
index 5923fc0f2..d65cb4213 100644
--- a/Linglib/Morphology/Unification.lean
+++ b/Linglib/Morphology/Unification.lean
@@ -28,9 +28,29 @@ Unification (§3.2.3) is "the most general feature structure `D` such that `D′
 * `instance : PartialOrder UD.MorphFeatures` — subsumption ("only a partial order",
   §3.2.3), with decidable `≤`.
 * `instance : OrderBot UD.MorphFeatures` — the empty bundle is bottom.
-* `UD.MorphFeatures.Compatible` — `Prop`-native compatibility;
-  `compatible_iff_bddAbove` characterizes the `Bool` check as boundedness above.
-* `unify_isLUB`, `unify_comm`, `unify_self`, `bot_unify` — the §3.2.3 laws.
+* `instance : SemilatticeInf UD.MorphFeatures` — the meet is Shieber's
+  *generalization* (anti-unification): total, unlike the join.
+* `UD.MorphFeatures.Compatible` — boundedness above (`BddAbove {f, g}`), decidable
+  via the `Bool` check (`compatible_iff_bddAbove`).
+* `unify_isLUB`, `unify_eq_some_iff_isLUB`, `unify_comm`, `unify_assoc`,
+  `unify_self`, `bot_unify`/`unify_bot`, `unify_mono` — the §3.2.3 laws plus
+  associativity and guarded monotonicity.
+
+## Theory-neutrality boundary
+
+Three strata with different statuses: the *record* is annotation consensus
+(`Data/UD/Basic.lean`); the *order* `≤` is shared substrate every framework consumes
+its own way (DM's matching clause, underspecification, syncretism down-sets); the
+*operations* `⊔`/`⊓` are commitments of the unification tradition — [shieber-1986]
+§3.1 states unification-as-sole-combinator as a design constraint, and rival
+frameworks combine differently (DM matches and competes; Minimalist Agree values
+asymmetrically). This file is *not* that tradition's headquarters: unification-based
+grammar (PATR, HPSG, LFG — reentrant feature structures, phrasal combination) is a
+syntax family whose substrate belongs in `Syntax/` when consuming studies demand it.
+What lives here is only the tradition's morphological-bundle fragment — the algebra
+of one token's Feats column — which it shares with rivals: at the level of claims
+about morphological feature combination this file is a sibling of `DM/` and
+`Nanosyntax/`, not a foundation beneath them.
 
 ## Implementation notes
 
@@ -146,10 +166,11 @@ instance : OrderBot MorphFeatures where
 
 /-! ### Compatibility is boundedness above; unification is the least upper bound -/
 
-/-- `Prop`-native compatibility: the two bundles have an upper bound in the
-subsumption order. Characterized by the executable `compatible` check via
-`compatible_iff_bddAbove`. -/
-def Compatible (f g : MorphFeatures) : Prop := ∃ u, f ≤ u ∧ g ≤ u
+/-- `Prop`-native compatibility: the pair is bounded above in the subsumption
+order — mathlib's `BddAbove`, so the bounds API applies directly. Characterized by
+the executable `compatible` check via `compatible_iff_bddAbove`, which also makes
+it decidable. -/
+def Compatible (f g : MorphFeatures) : Prop := BddAbove ({f, g} : Set MorphFeatures)
 
 private theorem clause_of_some_some {α : Type _} [BEq α] [LawfulBEq α] {x y : α}
     (h : ((some x : Option α).isNone || (some y : Option α).isNone
@@ -245,9 +266,17 @@ order-theoretic identity of "compatible". -/
 theorem compatible_iff_bddAbove (f g : MorphFeatures) :
     f.compatible g = true ↔ Compatible f g := by
   constructor
-  · exact fun h => ⟨f.merge g, le_merge_left f g, le_merge_right h⟩
-  · rintro ⟨u, hf, hg⟩
-    exact compatible_of_le hf hg
+  · intro h
+    refine ⟨f.merge g, fun x hx => ?_⟩
+    rcases hx with rfl | hx
+    · exact le_merge_left _ g
+    · rw [Set.mem_singleton_iff.mp hx]
+      exact le_merge_right h
+  · rintro ⟨u, hu⟩
+    exact compatible_of_le (hu (Set.mem_insert _ _)) (hu (Set.mem_insert_of_mem _ rfl))
+
+instance (f g : MorphFeatures) : Decidable (Compatible f g) :=
+  decidable_of_iff _ (compatible_iff_bddAbove f g)
 
 /-- Unification succeeds exactly on compatible inputs (§3.2.3: otherwise it "fails"). -/
 theorem unify_eq_some_iff (f g : MorphFeatures) :
@@ -329,4 +358,197 @@ the empty bundle returns the other input. -/
   cases f
   rfl
 
+/-! ### Generalization: the meet
+
+Shieber's *generalization* (anti-unification): the most specific bundle subsumed by
+both inputs. Unlike unification it is total — the meet always exists — so
+`MorphFeatures` is a genuine `SemilatticeInf` with `⊥`. -/
+
+private def slotInf {α : Type _} [DecidableEq α] (a b : Option α) : Option α :=
+  if a = b then a else none
+
+private theorem slotInf_flatLE_left {α : Type _} [DecidableEq α] (a b : Option α) :
+    (slotInf a b).FlatLE a := by
+  unfold slotInf; split
+  · exact .refl _
+  · exact .none_le _
+
+private theorem slotInf_flatLE_right {α : Type _} [DecidableEq α] (a b : Option α) :
+    (slotInf a b).FlatLE b := by
+  unfold slotInf; split
+  · next h => subst h; exact .refl _
+  · exact .none_le _
+
+private theorem flatLE_slotInf {α : Type _} [DecidableEq α] {a b c : Option α}
+    (h1 : c.FlatLE a) (h2 : c.FlatLE b) : c.FlatLE (slotInf a b) := by
+  intro x hx
+  have ha := h1 x hx
+  have hb := h2 x hx
+  unfold slotInf
+  rw [ha, hb]
+  simp
+
+instance : Min MorphFeatures where
+  min f g :=
+    { number   := slotInf f.number g.number
+      gender   := slotInf f.gender g.gender
+      case_    := slotInf f.case_ g.case_
+      definite := slotInf f.definite g.definite
+      degree   := slotInf f.degree g.degree
+      pronType := slotInf f.pronType g.pronType
+      reflex   := f.reflex && g.reflex
+      person   := slotInf f.person g.person
+      verbForm := slotInf f.verbForm g.verbForm
+      tense    := slotInf f.tense g.tense
+      aspect   := slotInf f.aspect g.aspect
+      mood     := slotInf f.mood g.mood
+      voice    := slotInf f.voice g.voice
+      polarity := slotInf f.polarity g.polarity }
+
+private theorem band_true_left {x y : Bool} (h : (x && y) = true) : x = true := by
+  cases x <;> simp_all
+
+private theorem band_true_right {x y : Bool} (h : (x && y) = true) : y = true := by
+  cases y <;> simp_all
+
+private theorem band_true_intro {x y : Bool} (hx : x = true) (hy : y = true) :
+    (x && y) = true := by simp [hx, hy]
+
+instance : SemilatticeInf MorphFeatures :=
+  { (inferInstance : PartialOrder MorphFeatures),
+    (inferInstance : Min MorphFeatures) with
+    inf := min
+    inf_le_left := fun f g => show Subsumes (min f g) f from
+      ⟨slotInf_flatLE_left _ _, slotInf_flatLE_left _ _, slotInf_flatLE_left _ _,
+       slotInf_flatLE_left _ _, slotInf_flatLE_left _ _, slotInf_flatLE_left _ _,
+       fun hr => band_true_left hr,
+       slotInf_flatLE_left _ _, slotInf_flatLE_left _ _, slotInf_flatLE_left _ _,
+       slotInf_flatLE_left _ _, slotInf_flatLE_left _ _, slotInf_flatLE_left _ _,
+       slotInf_flatLE_left _ _⟩
+    inf_le_right := fun f g => show Subsumes (min f g) g from
+      ⟨slotInf_flatLE_right _ _, slotInf_flatLE_right _ _, slotInf_flatLE_right _ _,
+       slotInf_flatLE_right _ _, slotInf_flatLE_right _ _, slotInf_flatLE_right _ _,
+       fun hr => band_true_right hr,
+       slotInf_flatLE_right _ _, slotInf_flatLE_right _ _, slotInf_flatLE_right _ _,
+       slotInf_flatLE_right _ _, slotInf_flatLE_right _ _, slotInf_flatLE_right _ _,
+       slotInf_flatLE_right _ _⟩
+    le_inf := fun c f g hcf hcg => by
+      obtain ⟨a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14⟩ := hcf
+      obtain ⟨b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14⟩ := hcg
+      exact ⟨flatLE_slotInf a1 b1, flatLE_slotInf a2 b2, flatLE_slotInf a3 b3,
+             flatLE_slotInf a4 b4, flatLE_slotInf a5 b5, flatLE_slotInf a6 b6,
+             fun hr => band_true_intro (a7 hr) (b7 hr),
+             flatLE_slotInf a8 b8, flatLE_slotInf a9 b9, flatLE_slotInf a10 b10,
+             flatLE_slotInf a11 b11, flatLE_slotInf a12 b12, flatLE_slotInf a13 b13,
+             flatLE_slotInf a14 b14⟩ }
+
+/-! ### Unification computes least upper bounds — further laws -/
+
+/-- Unification succeeds with value `u` exactly when `u` is the least upper bound. -/
+theorem unify_eq_some_iff_isLUB {f g u : MorphFeatures} :
+    f.unify g = some u ↔ IsLUB {f, g} u := by
+  refine ⟨unify_isLUB, fun hu => ?_⟩
+  have hc : f.compatible g = true :=
+    compatible_of_le (hu.1 (Set.mem_insert _ _)) (hu.1 (Set.mem_insert_of_mem _ rfl))
+  have hm : f.unify g = some (f.merge g) := by simp [unify, hc]
+  rw [hm, Option.some_inj]
+  exact (unify_isLUB hm).unique hu
+
+private theorem isLUB_pair_step {f g h v u : MorphFeatures} (hv : IsLUB {f, g} v) :
+    IsLUB {v, h} u ↔ IsLUB ({f, g, h} : Set MorphFeatures) u := by
+  have hub : upperBounds ({v, h} : Set MorphFeatures) = upperBounds {f, g, h} := by
+    ext w
+    constructor
+    · intro hw x hx
+      rcases hx with rfl | rfl | rfl
+      · exact (hv.1 (Set.mem_insert _ _)).trans (hw (Set.mem_insert _ _))
+      · exact (hv.1 (Set.mem_insert_of_mem _ rfl)).trans (hw (Set.mem_insert _ _))
+      · exact hw (Set.mem_insert_of_mem _ rfl)
+    · intro hw x hx
+      rcases hx with rfl | rfl
+      · exact hv.2 fun y hy => by
+          rcases hy with rfl | rfl
+          · exact hw (Set.mem_insert _ _)
+          · exact hw (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
+      · exact hw (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ rfl))
+  unfold IsLUB
+  rw [hub]
+
+/-- Unification is associative, with failure propagating ([shieber-1986] §3.2.3's
+order-independence): both associations compute the lub of all three bundles. -/
+theorem unify_assoc (f g h : MorphFeatures) :
+    (f.unify g).bind (·.unify h) = (g.unify h).bind (f.unify ·) := by
+  apply Option.ext
+  intro u
+  simp only [Option.bind_eq_some_iff]
+  constructor
+  · rintro ⟨v, hv, hu⟩
+    have h3 : IsLUB ({f, g, h} : Set MorphFeatures) u :=
+      (isLUB_pair_step (unify_isLUB hv)).mp (unify_isLUB hu)
+    have hgh : g.compatible h = true := by
+      refine compatible_of_le (u := u) ?_ ?_
+      · exact h3.1 (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
+      · exact h3.1 (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ rfl))
+    refine ⟨g.merge h, by simp [unify, hgh], ?_⟩
+    have hw : IsLUB ({g, h} : Set MorphFeatures) (g.merge h) :=
+      unify_isLUB (by simp [unify, hgh])
+    rw [unify_eq_some_iff_isLUB]
+    have : IsLUB ({g, h, f} : Set MorphFeatures) u := by
+      have : ({g, h, f} : Set MorphFeatures) = {f, g, h} := by
+        ext x; simp [Set.mem_insert_iff]; tauto
+      rw [this]; exact h3
+    have step := (isLUB_pair_step hw).mpr this
+    have : ({g.merge h, f} : Set MorphFeatures) = {f, g.merge h} := Set.pair_comm _ _
+    rwa [← this]
+  · rintro ⟨w, hw, hu⟩
+    have hu' : IsLUB ({g.merge h, f} : Set MorphFeatures) u := by
+      rw [Set.pair_comm]
+      rw [unify_eq_some_iff_isLUB] at hu
+      have hwm : g.merge h = w := by
+        have : g.unify h = some w := hw
+        have hgh : g.compatible h = true :=
+          compatible_of_le ((unify_isLUB hw).1 (Set.mem_insert _ _))
+            ((unify_isLUB hw).1 (Set.mem_insert_of_mem _ rfl))
+        simpa [unify, hgh] using this
+      rwa [← hwm] at hu
+    have h3 : IsLUB ({g, h, f} : Set MorphFeatures) u := by
+      have hgh : g.compatible h = true :=
+        compatible_of_le ((unify_isLUB hw).1 (Set.mem_insert _ _))
+          ((unify_isLUB hw).1 (Set.mem_insert_of_mem _ rfl))
+      exact (isLUB_pair_step (unify_isLUB (by simp [unify, hgh] :
+        g.unify h = some (g.merge h)))).mp hu'
+    have h3' : IsLUB ({f, g, h} : Set MorphFeatures) u := by
+      have : ({g, h, f} : Set MorphFeatures) = {f, g, h} := by
+        ext x; simp [Set.mem_insert_iff]; tauto
+      rwa [this] at h3
+    have hfg : f.compatible g = true := by
+      refine compatible_of_le (u := u) ?_ ?_
+      · exact h3'.1 (Set.mem_insert _ _)
+      · exact h3'.1 (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
+    refine ⟨f.merge g, by simp [unify, hfg], ?_⟩
+    rw [unify_eq_some_iff_isLUB]
+    exact (isLUB_pair_step (unify_isLUB (by simp [unify, hfg] :
+      f.unify g = some (f.merge g)))).mpr h3'
+
+/-- The empty bundle is a right identity for unification. -/
+@[simp] theorem unify_bot (f : MorphFeatures) : f.unify (⊥ : MorphFeatures) = some f := by
+  rw [unify_comm]; exact bot_unify f
+
+/-- Unification fails exactly on incompatible inputs. -/
+theorem unify_eq_none_iff (f g : MorphFeatures) :
+    f.unify g = none ↔ ¬ Compatible f g := by
+  rw [← compatible_iff_bddAbove]
+  unfold unify
+  by_cases hc : f.compatible g = true <;> simp [hc]
+
+/-- Unification is monotone where defined: shrinking both inputs preserves success and
+shrinks the output. (Unguarded `merge`-monotonicity is false — the guard is needed.) -/
+theorem unify_mono {f₁ f₂ g₁ g₂ u₂ : MorphFeatures} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂)
+    (h2 : f₂.unify g₂ = some u₂) : ∃ u₁, f₁.unify g₁ = some u₁ ∧ u₁ ≤ u₂ := by
+  have hlub := unify_isLUB h2
+  have hf1 : f₁ ≤ u₂ := hf.trans (hlub.1 (Set.mem_insert _ _))
+  have hg1 : g₁ ≤ u₂ := hg.trans (hlub.1 (Set.mem_insert_of_mem _ rfl))
+  have hc : f₁.compatible g₁ = true := compatible_of_le hf1 hg1
+  exact ⟨f₁.merge g₁, by simp [unify, hc], merge_le hf1 hg1⟩
+
 end UD.MorphFeatures
diff --git a/Linglib/Morphology/Word.lean b/Linglib/Morphology/Word.lean
index 101d0e5c3..a1cdf0068 100644
--- a/Linglib/Morphology/Word.lean
+++ b/Linglib/Morphology/Word.lean
@@ -68,12 +68,27 @@ instance (w1 w2 : Word) : Decidable (Word.Agree w1 w2) := by
   UD.MorphFeatures.compatible_self w.phi
 
 /-- φ-agreement is symmetric — the docstring's "symmetric tolerance relation", as a
-    theorem. (It is *not* transitive: an unspecified feature is a wildcard, so
-    `she ~ they ~ he` while `she ≁ he`.) -/
+    theorem. -/
 @[symm] theorem Word.Agree.symm {w1 w2 : Word} (h : Word.Agree w1 w2) : Word.Agree w2 w1 := by
   unfold Word.Agree at h ⊢
   rwa [UD.MorphFeatures.compatible_comm]
 
+/-- φ-agreement is *not* transitive: an unspecified feature is a wildcard, so
+    underspecified *they* agrees with both *she* and *he* while *she ≁ he*. -/
+theorem Word.Agree.not_transitive :
+    ¬ ∀ w1 w2 w3 : Word, Word.Agree w1 w2 → Word.Agree w2 w3 → Word.Agree w1 w3 := by
+  intro h
+  exact absurd
+    (h ⟨"she", .PRON, { person := some .third, number := some .Sing, gender := some .Fem }⟩
+       ⟨"they", .PRON, { person := some .third }⟩
+       ⟨"he", .PRON, { person := some .third, number := some .Sing, gender := some .Masc }⟩
+       (by decide) (by decide))
+    (by decide)
+
+-- `reflex` is deliberately not an agreement feature: a reflexive-marked token still
+-- agrees with an unmarked one (the φ-projection drops it).
+example : Word.Agree ⟨"sich", .PRON, { reflex := true }⟩ ⟨"Kind", .NOUN, {}⟩ := by decide
+
 /-- Derive a passive variant: sets voice to passive. The valence change
     (detransitivization) is a frame-level fact carried by the passive analysis on
     `DepTree.frames`, not token data. Composes with `VerbEntry.toWordPastPart`. -/
diff --git a/Linglib/Studies/Bubnov2026.lean b/Linglib/Studies/Bubnov2026.lean
index bcece549d..e337b603f 100644
--- a/Linglib/Studies/Bubnov2026.lean
+++ b/Linglib/Studies/Bubnov2026.lean
@@ -60,6 +60,7 @@ set_option autoImplicit false
 namespace Bubnov2026
 
 open DeganoAloni2025
+open scoped Syntax.Case.Caha
 open DeganoAloni2025.DependenceLogic
 open Morphology.Nanosyntax
 open Dekier2021
diff --git a/Linglib/Studies/Caha2009.lean b/Linglib/Studies/Caha2009.lean
index aa8a92a95..91e523e24 100644
--- a/Linglib/Studies/Caha2009.lean
+++ b/Linglib/Studies/Caha2009.lean
@@ -57,11 +57,12 @@ Ch. 6), and Hungarian (GEN-less, dative-as-possessor syncretism per
 namespace Caha2009
 
 open Features (Case)
+open scoped Syntax.Case.Caha
 
 /-! ## Caha containment-respect predicate
 
 Does an inventory respect Caha's containment hierarchy? True iff `inv`
-is downward-closed under the canonical `PartialOrder Case` (Caha
+is downward-closed under the scoped Caha order (`Syntax.Case.Caha`;
 containment) defined in `Core/Case/Order.lean`: whenever `c ∈ inv` and
 `d ≤ c`, then `d ∈ inv`. Off-hierarchy cases (ERG, ABS, INST, COM, …)
 impose no constraint — in the Caha order they only have `c ≤ c`, so
diff --git a/Linglib/Syntax/Case/Order.lean b/Linglib/Syntax/Case/Order.lean
index 697d5f962..523f453f4 100644
--- a/Linglib/Syntax/Case/Order.lean
+++ b/Linglib/Syntax/Case/Order.lean
@@ -4,9 +4,10 @@ import Linglib.Features.Case
 # Caha Containment Order on Case
 [caha-2009] [mcfadden-2018]
 
-The canonical order on `Features.Case`: state-of-the-art syntax
-(configurational case + nanosyntactic spellout) assumes Caha's
-containment as the default. Each case on the hierarchy literally
+Caha's containment order on `Features.Case`, as a **scoped** instance
+(`open scoped Syntax.Case.Caha` to use `≤`): theoretical orders are borne
+by features as opt-in commitments, not as global instances on the UD
+annotation enums — the annotation substrate default is order-free. Each case on the hierarchy literally
 *contains* the representations of all cases below it:
 
     [[[[[ NOM ] ACC ] GEN ] DAT ] LOC ]
@@ -17,8 +18,8 @@ That silence is the theoretical content: Caha's hierarchy is silent on
 those cases, and the `PartialOrder` structure preserves the silence.
 
 Other orders (Blake's typological frequency in `Features/Case.lean`,
-per-language syncretism graphs) live as named `def`s used locally via
-`letI` rather than as competing instances on `Case`.
+per-language syncretism graphs) likewise live as named `def`s or scoped
+instances rather than competing global instances on `Case`.
 -/
 
 open Features (Case)
@@ -109,12 +110,7 @@ def cahaLE (c₁ c₂ : Case) : Prop := c₁ = c₂ ∨ cahaLT c₁ c₂
 instance : DecidableRel cahaLE := fun _ _ =>
   inferInstanceAs (Decidable (_ ∨ _))
 
-instance : LE Case := ⟨cahaLE⟩
-
-instance (c₁ c₂ : Case) : Decidable (c₁ ≤ c₂) :=
-  inferInstanceAs (Decidable (cahaLE c₁ c₂))
-
-theorem cahaLE_refl (c : Case) : c ≤ c := Or.inl rfl
+theorem cahaLE_refl (c : Case) : cahaLE c c := Or.inl rfl
 
 theorem cahaLT_trans {a b c : Case} : cahaLT a b → cahaLT b c → cahaLT a c := by
   unfold cahaLT
@@ -122,7 +118,7 @@ theorem cahaLT_trans {a b c : Case} : cahaLT a b → cahaLT b c → cahaLT a c :
     cases hc : containmentRank c <;> simp_all
   exact lt_trans
 
-theorem cahaLE_trans (a b c : Case) : a ≤ b → b ≤ c → a ≤ c := by
+theorem cahaLE_trans (a b c : Case) : cahaLE a b → cahaLE b c → cahaLE a c := by
   intro hab hbc
   rcases hab with rfl | hab
   · exact hbc
@@ -130,7 +126,7 @@ theorem cahaLE_trans (a b c : Case) : a ≤ b → b ≤ c → a ≤ c := by
   · exact Or.inr hab
   exact Or.inr (cahaLT_trans hab hbc)
 
-theorem cahaLE_antisymm (a b : Case) : a ≤ b → b ≤ a → a = b := by
+theorem cahaLE_antisymm (a b : Case) : cahaLE a b → cahaLE b a → a = b := by
   intro hab hba
   rcases hab with rfl | hab
   · rfl
@@ -141,13 +137,32 @@ theorem cahaLE_antisymm (a b : Case) : a ≤ b → b ≤ a → a = b := by
     unfold cahaLT
     cases ha : containmentRank a <;> simp_all)
 
-instance : Preorder Case where
+/-! ### The Caha order as scoped instances
+
+A feature bears its theoretical order as an opt-in commitment
+(`open scoped Syntax.Case.Caha`), never as a global instance on the
+annotation enum. -/
+
+namespace Caha
+
+scoped instance instLECaha : LE Case := ⟨cahaLE⟩
+
+scoped instance (c₁ c₂ : Case) : Decidable (c₁ ≤ c₂) :=
+  inferInstanceAs (Decidable (cahaLE c₁ c₂))
+
+scoped instance instPreorderCaha : Preorder Case where
+  toLE := instLECaha
   le_refl := cahaLE_refl
   le_trans _ _ _ := cahaLE_trans _ _ _
 
-instance : PartialOrder Case where
+scoped instance : PartialOrder Case where
+  toPreorder := instPreorderCaha
   le_antisymm _ _ := cahaLE_antisymm _ _
 
+end Caha
+
+open scoped Caha
+
 /-- A case is **nonnominative** iff its representation contains ACC's, i.e.
     `(.acc : Case) ≤ c` in the Caha order. [mcfadden-2018] argues this is
     the key natural class for stem allomorphy: a VI rule conditioned on