refactor(Core,Features): one UD file; feature types to Features/

Linglib.lean

@@ -8,7 +8,7 @@ and their interfaces. See README.md for documentation links.
 import Linglib.Features.Dimension
 import Linglib.Features.Gender
 import Linglib.Core.Valence
-import Linglib.Core.UD.Word
+import Linglib.Core.UniversalDependencies
 import Linglib.Typology.NegativeConcord
 import Linglib.Typology.PolarityItem
 import Linglib.Typology.Negation
@@ -38,7 +38,6 @@ import Linglib.Core.Logic.Team.Closure
 import Linglib.Core.Logic.Team.Definability
 import Linglib.Features.Acceptability
 import Linglib.Semantics.Dynamic.ParameterizedUpdate
-import Linglib.Core.UD.Basic
 import Linglib.Core.Tree
 import Linglib.Features.Coordination
 import Linglib.Core.Logic.Duality
@@ -221,6 +220,7 @@ import Linglib.Features.Evidentiality
 import Linglib.Features.Mirativity
 import Linglib.Semantics.Epistemicity
 import Linglib.Features.Logophoricity
+import Linglib.Features.MassCount
 import Linglib.Core.WorldTimeIndex
 import Linglib.Core.Time.Interval.Basic
 import Linglib.Core.Time.Interval.Generalized

Linglib/Core/Tree.lean

@@ -1,6 +1,6 @@
 import Mathlib.Data.List.Infix
 import Mathlib.Algebra.Free
-import Linglib.Core.UD.Basic
+import Linglib.Core.UniversalDependencies
 import Linglib.Core.Order.Tree
 
 /-!

Linglib/Core/UD/Basic.lean → Linglib/Core/UniversalDependencies.lean

@@ -547,3 +547,52 @@ structure DepArc where
   deriving DecidableEq, Repr
 
 end UD
+
+-- ============================================================================
+-- Word: the CoNLL-U surface token
+-- ============================================================================
+
+structure Word where
+  form : String
+  cat : UD.UPOS
+  features : UD.MorphFeatures := {}
+  deriving Repr
+
+/-- Convenience constructor for a featureless word (form + category only). -/
+def Word.mk' (form : String) (cat : UD.UPOS) : Word := { form := form, cat := cat }
+
+/-- The φ-feature subset (person, number, gender) of a word, as a
+    `UD.MorphFeatures` bundle. -/
+def Word.phi (w : Word) : UD.MorphFeatures :=
+  { person := w.features.person, number := w.features.number,
+    gender := w.features.gender }
+
+/-- φ-agreement between two words: their person/number/gender features are
+    compatible (an unspecified feature is a wildcard). A reflexive, symmetric
+    *tolerance* relation on `Word` (not transitive), decided by the shared
+    `UD.MorphFeatures.compatible`. This is the feature-based agreement primitive
+    binding and concord consumers share — no surface-form gender lookup. -/
+def Word.Agree (w1 w2 : Word) : Prop := w1.phi.compatible w2.phi
+
+instance (w1 w2 : Word) : Decidable (Word.Agree w1 w2) := by
+  unfold Word.Agree; infer_instance
+
+@[refl] theorem Word.Agree.refl (w : Word) : Word.Agree w w :=
+  UD.MorphFeatures.compatible_self w.phi
+
+
+/-- 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`. -/
+def Word.asPassive (w : Word) : Word :=
+  { w with features := { w.features with voice := some .Pass } }
+
+instance : BEq Word where
+  beq w1 w2 := w1.form == w2.form && w1.cat == w2.cat
+
+instance : ToString Word where
+  toString w := w.form
+
+/-- Convert a word list to a readable string. -/
+def wordsToString (ws : List Word) : String :=
+  " ".intercalate (ws.map (·.form))

Linglib/Features/Case.lean

@@ -1,7 +1,7 @@
 import Mathlib.Data.Finset.Card
 import Mathlib.Order.Lattice
 import Mathlib.Tactic.DeriveFintype
-import Linglib.Core.UD.Basic
+import Linglib.Core.UniversalDependencies
 
 /-!
 # Case — Feature Taxonomy

Linglib/Features/Gender.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD.Basic
+import Linglib.Core.UniversalDependencies
 import Linglib.Features.PrivativePair
 
 /-!

Linglib/Features/MassCount.lean

@@ -0,0 +1,15 @@
+/-!
+# Mass/count
+
+The morphosyntactic mass/count feature ([krifka-2026]). No UD equivalent, so it is a
+linglib feature taxonomy rather than a `UD.*` alias.
+-/
+
+/-- Morphosyntactic mass/count feature. A formal feature parallel to grammatical
+    gender — not an ontological distinction. Determines kind-anaphor morphology:
+    [MASS] → *it*, [COUNT] → *they*. Evidence: *pollen*[MASS] → *it* vs
+    *pollen grains*[COUNT] → *they* for the same referent ([krifka-2026] §2). -/
+inductive MassCount where
+  | mass   -- mass nouns: *mold*, *pollen*, *milk*, *gold*
+  | count  -- count nouns: *spider*, *pollen grain*, *dog*, *cup*
+  deriving Repr, DecidableEq, Hashable

Linglib/Features/Number.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD.Basic
+import Linglib.Core.UniversalDependencies
 import Linglib.Features.PrivativePair
 
 /-!
@@ -42,6 +42,10 @@ hierarchy, language data) remains in
 
 -/
 
+/-- Grammatical number — UD's descriptive vocabulary (`UD.Number`: `.Sing`, `.Plur`,
+`.Dual`, …) as the canonical type; the analytical apparatus below is its API. -/
+abbrev Features.Number := UD.Number
+
 namespace Features.Number
 
 -- ============================================================================

Linglib/Features/OntologicalCategory.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD.Basic
+import Linglib.Core.UniversalDependencies
 import Linglib.Features.Prominence
 
 /-!

Linglib/Features/Person.lean

@@ -1,4 +1,4 @@
-import Linglib.Core.UD.Basic
+import Linglib.Core.UniversalDependencies
 import Linglib.Features.Prominence
 import Linglib.Features.PrivativePair
 
@@ -42,6 +42,10 @@ language data) remains in `Phenomena/Agreement/PersonMarkingTypology.lean`.
 
 -/
 
+/-- Grammatical person — UD's descriptive vocabulary (`UD.Person`: `.first`, `.second`,
+`.third`, `.zero`) as the canonical type; the feature theory below is its API. -/
+abbrev Features.Person := UD.Person
+
 namespace Features.Person
 
 -- ============================================================================
@@ -74,13 +78,13 @@ def Features.wellFormed (pf : Features) : Bool :=
 -- ============================================================================
 
 /-- 1st person features: [+participant, +author]. -/
-def first : Features := ⟨true, true⟩
+def firstF : Features := ⟨true, true⟩
 
 /-- 2nd person features: [+participant, −author]. -/
-def second : Features := ⟨true, false⟩
+def secondF : Features := ⟨true, false⟩
 
 /-- 3rd person features: [−participant, −author]. -/
-def third : Features := ⟨false, false⟩
+def thirdF : Features := ⟨false, false⟩
 
 -- ============================================================================
 -- § 3: PersonLevel Bridge
@@ -92,9 +96,9 @@ namespace Features.Prominence
 
 /-- Decompose `PersonLevel` into binary person features. -/
 def PersonLevel.toFeatures : PersonLevel → Features.Person.Features
-  | .first  => Features.Person.first
-  | .second => Features.Person.second
-  | .third  => Features.Person.third
+  | .first  => Features.Person.firstF
+  | .second => Features.Person.secondF
+  | .third  => Features.Person.thirdF
 
 /-- Convert `UD.Person` to `PersonLevel`. The UD `.zero` (impersonal)
     case has no `PersonLevel` analogue; everything else is direct. -/
@@ -114,9 +118,9 @@ open Features.Prominence
 -- § 4: Features Verification
 -- ============================================================================
 
-@[simp] theorem first_wellFormed : first.wellFormed = true := rfl
-@[simp] theorem second_wellFormed : second.wellFormed = true := rfl
-@[simp] theorem third_wellFormed : third.wellFormed = true := rfl
+@[simp] theorem firstF_wellFormed : firstF.wellFormed = true := rfl
+@[simp] theorem secondF_wellFormed : secondF.wellFormed = true := rfl
+@[simp] theorem thirdF_wellFormed : thirdF.wellFormed = true := rfl
 
 /-- The ill-formed combination [−participant, +author] is the only
     combination that violates well-formedness. -/
@@ -150,9 +154,9 @@ instance : Features.PhiFeatures Features where
   roundtrip := fun ⟨_, _⟩ => rfl
 
 /-- The three canonical person values map to the three PrivativePair cells. -/
-@[simp] theorem first_is_maximal : PhiFeatures.toPair first = .maximal := rfl
-@[simp] theorem second_is_intermediate : PhiFeatures.toPair second = .intermediate := rfl
-@[simp] theorem third_is_minimal : PhiFeatures.toPair third = .minimal := rfl
+@[simp] theorem firstF_is_maximal : PhiFeatures.toPair firstF = .maximal := rfl
+@[simp] theorem secondF_is_intermediate : PhiFeatures.toPair secondF = .intermediate := rfl
+@[simp] theorem thirdF_is_minimal : PhiFeatures.toPair thirdF = .minimal := rfl
 
 /-- The `[±participant, ±author]` decomposition **is** the privative pair: an equivalence
 `Features ≃ PrivativePair` ([harbour-2016]'s phi-kernel skeleton as an isomorphism, not a