refactor(Semantics/Modality): dedup ModalFlavor, de-echo Orthologic namespace

Linglib/Fragments/Farsi/Determiners.lean

@@ -1,5 +1,6 @@
 import Linglib.Core.Word
 import Linglib.Semantics.Quantification.ChoiceFunction
+import Linglib.Semantics.Modality.ModalTypes
 import Mathlib.Data.Rat.Defs
 
 /-! # Farsi Determiner and Indefinite Lexicon
@@ -136,16 +137,13 @@ def indef_i : IndefiniteEntry :=
   }
 
 
-/--
-Modal flavor type for context specification.
--/
-inductive ModalFlavor where
-  | deontic   -- Permission, obligation
-  | epistemic -- Knowledge, belief
-  deriving DecidableEq, Repr
+open Semantics.Modality (ModalFlavor)
 
 /--
-Context for determining EFCI reading.
+Context for determining EFCI reading. Uses the project-canonical
+`Semantics.Modality.ModalFlavor`; @cite{alonso-ovalle-moghiseh-2025} only
+distinguishes deontic (free choice) from epistemic (modal variation), so the
+other canonical flavors are not licensing-relevant here (see `getReading`).
 -/
 structure EFCIContext where
   /-- Is the context downward-entailing? -/
@@ -191,6 +189,9 @@ def getReading (entry : IndefiniteEntry) (ctx : EFCIContext) : Option EFCIReadin
   else match ctx.modalFlavor with
     | some .deontic => some .freeChoice
     | some .epistemic => some .modalVariation
+    -- @cite{alonso-ovalle-moghiseh-2025} specifies only deontic/epistemic;
+    -- other flavors do not license an EFCI reading.
+    | some .bouletic | some .circumstantial => some .plainExistential
     | none =>
       -- Root context: depends on rescue mechanism
       match entry.efciRescue with

Linglib/Phenomena/FreeChoice/Divergences.lean

@@ -31,7 +31,7 @@ proper Lean theorem.
 namespace Phenomena.FreeChoice.Divergences
 
 open Core.Logic.Modal.BSML
-open Semantics.Modality.Orthologic
+open Orthologic
 open Aloni2022
 open HollidayMandelkern2024
 

Linglib/Semantics/Modality/Orthologic/Frames.lean

@@ -50,7 +50,7 @@ two-world lifting) live in
   definitions stay Fintype-free.
 -/
 
-namespace Semantics.Modality.Orthologic
+namespace Orthologic
 
 -- ════════════════════════════════════════════════════
 -- § 1. Compatibility Frames
@@ -279,4 +279,4 @@ def regularClosure {S : Type*} (F : CompatFrame S) : ClosureOperator (Set S) whe
 theorem regularClosure_isClosed_iff_isRegular {S : Type*} (F : CompatFrame S) (A : Set S) :
     (regularClosure F).IsClosed A ↔ isRegular F A := Iff.rfl
 
-end Semantics.Modality.Orthologic
+end Orthologic

Linglib/Semantics/Modality/Orthologic/Modal.lean

@@ -38,7 +38,7 @@ Decidability of `access` is *not* bundled — provide a `DecidableRel`
 instance separately (mirrors the `CompatFrame` convention).
 -/
 
-namespace Semantics.Modality.Orthologic
+namespace Orthologic
 
 -- ════════════════════════════════════════════════════
 -- § 1. Epistemic Compatibility Frames
@@ -189,9 +189,9 @@ namespace EpistemicCompatFrame
     `wittgensteinLaw`. -/
 theorem wittgensteinLaw {S : Type*} (F : EpistemicCompatFrame S) (A : Set S) :
     orthoNeg F.toCompatFrame A ∩ diamond F.toModalCompatFrame A = ∅ :=
-  _root_.Semantics.Modality.Orthologic.wittgensteinLaw
+  _root_.Orthologic.wittgensteinLaw
     F.toModalCompatFrame F.knowable A
 
 end EpistemicCompatFrame
 
-end Semantics.Modality.Orthologic
+end Orthologic

Linglib/Semantics/Modality/Orthologic/RegularProp.lean

@@ -44,7 +44,7 @@ future ortholattice consumer (BSML, inquisitive semantics, truthmaker
 semantics — all of which traffic in non-Boolean propositional algebras).
 -/
 
-namespace Semantics.Modality.Orthologic
+namespace Orthologic
 
 variable {S : Type*} {F : CompatFrame S}
 
@@ -250,4 +250,4 @@ instance instOrthocomplementedLattice : OrthocomplementedLattice (RegularProp F)
 
 end RegularProp
 
-end Semantics.Modality.Orthologic
+end Orthologic

Linglib/Studies/AlonsoOvalleMoghiseh2025.lean

@@ -2,6 +2,7 @@ import Linglib.Semantics.Exhaustification.InnocentExclusion
 import Linglib.Semantics.Exhaustification.Tolerant
 import Linglib.Semantics.Exhaustification.Structural
 import Linglib.Fragments.Farsi.Determiners
+import Linglib.Semantics.Modality.ModalTypes
 import Linglib.Data.Examples.Schema
 import Linglib.Core.Logic.Quantification.Exclusive
 import Mathlib.Tactic.DeriveFintype
@@ -101,7 +102,8 @@ open Exhaustification (innocent tolerant predToFinset altsFromPreds
   innocent_exh_singleton_proper
   innocent_exh_pairwise_disjoint_partial)
 open Data.Examples (LinguisticExample)
-export Fragments.Farsi.Determiners (EFCIRescue EFCIReading ModalFlavor)
+export Fragments.Farsi.Determiners (EFCIRescue EFCIReading)
+export Semantics.Modality (ModalFlavor)
 
 
 /-!

Linglib/Studies/HollidayMandelkern2024.lean

@@ -65,7 +65,7 @@ predictions that depend on them.
 
 namespace HollidayMandelkern2024
 
-open Semantics.Modality.Orthologic
+open Orthologic
 
 -- ════════════════════════════════════════════════════
 -- § 1. The Five-Possibility Path Frame (Example 4.11, Figure 7)