Consonantal Roots

Single source of truth for the Semitic-style notion of a consonantal root: an ordered melody of segments stored independently of vocalization or template.

The segment type α is parametric. Studies of Tarifit Berber may instantiate α := Phonology.Syllable.NatClass (sonority-class roots, used by @cite{afkir-zellou-2025}); studies of Hebrew or Amharic typically instantiate α := String for IPA symbols.

Theory-laden questions about the cognitive reality of roots (e.g. Ussishkin 2000, Bat-El 2003) are orthogonal to the data type itself — Root is a sequence; what status linguistic theory gives that sequence is a separate matter, parameterized at the study level.

Namespace separation

Core.Morphology.Root (this file): a consonantal melody, a morphological primitive (the underlying form of a morpheme). Semantics.Lexical.Roots.Root (Theories/Semantics/Lexical/Roots/Basic.lean): a bundle of LexEntailment atoms in the @cite{beavers-koontz-garboden-2020} sense — same English word, different concept. Core.Lexical.RootFeatures (Core/Lexical/RootFeatures.lean): semantic quality dimensions on a verb root — orthogonal to both.

structure Core.Morphology.Root (α : Type) : Type

A consonantal root: an ordered list of segments. Polymorphic in the segment type so that fragments may pick the granularity they need (sonority class, IPA symbol, full feature matrix).

• segments : List α

@[implicit_reducible]

instance Core.Morphology.instReprRoot {α✝ : Type} [Repr α✝] : Repr (Root α✝)

Equations

• Core.Morphology.instReprRoot = { reprPrec := Core.Morphology.instReprRoot.repr }

def Core.Morphology.instReprRoot.repr {α✝ : Type} [Repr α✝] : Root α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.Morphology.instDecidableEqRoot.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : Root α✝) : Decidable (x✝ = x✝¹)

Equations

• Core.Morphology.instDecidableEqRoot.decEq { segments := a } { segments := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Morphology.instDecidableEqRoot {α✝ : Type} [DecidableEq α✝] : DecidableEq (Root α✝)

Equations

• Core.Morphology.instDecidableEqRoot = Core.Morphology.instDecidableEqRoot.decEq

def Core.Morphology.Root.arity {α : Type} (r : Root α) : Nat

The number of root segments.

Equations

• r.arity = r.segments.length

def Core.Morphology.Root.isFinal {α : Type} (r : Root α) (i : Nat) : Bool

Position i is the final root position.

Equations

• r.isFinal i = (i + 1 == r.arity)

def Core.Morphology.Root.isNonfinal {α : Type} (r : Root α) (i : Nat) : Bool

Position i is nonfinal (some position strictly past it exists). Used by *Misalignment (@cite{faust-2026} (2)).

Equations

• r.isNonfinal i = decide (i + 1 < r.arity)

def Core.Morphology.Root.biradical {α : Type} (r : Root α) : Bool

A root with exactly two segments (e.g. √qt → QaTaT-template biradicals in Hebrew, @cite{mccarthy-1981}).

Equations

• r.biradical = (r.arity == 2)

def Core.Morphology.Root.triradical {α : Type} (r : Root α) : Bool

A root with exactly three segments (the unmarked Semitic case).

Equations

• r.triradical = (r.arity == 3)

def Core.Morphology.Root.quadriradical {α : Type} (r : Root α) : Bool

A root with exactly four segments (e.g. quadriliteral verbs).

Equations

• r.quadriradical = (r.arity == 4)

def Core.Morphology.Root.finalSegment {α : Type} (r : Root α) : Option α

The last segment of the root, if any.

Equations

• r.finalSegment = r.segments.getLast?

def Core.Morphology.Root.segmentAt {α : Type} (r : Root α) (i : Nat) : Option α

The segment at position i, if in range.

Equations

• r.segmentAt i = r.segments[i]?

def Core.Morphology.Root.adjDupCount {α : Type} [BEq α] : List α → Nat

Auxiliary: count adjacent identical segments in a root. A root with no adjacent duplicates returns 0. Used by satisfiesOCP and by templatic-morphology studies that need to check root-level OCP independently of any specific tier projection (cf. Phonology.Constraints.adjacentIdentical, which is the tier-projection-level analogue used inside OT constraint constructors).

Equations

• Core.Morphology.Root.adjDupCount [] = 0
• Core.Morphology.Root.adjDupCount [head] = 0
• Core.Morphology.Root.adjDupCount (a :: b :: rest) = (if (a == b) = true then 1 else 0) + Core.Morphology.Root.adjDupCount (b :: rest)

def Core.Morphology.Root.satisfiesOCP {α : Type} [BEq α] (r : Root α) : Bool

Root-level OCP (@cite{mccarthy-1981}, @cite{faust-2026}): a root has no adjacent identical segments. The predicate is segment-level and theory-neutral — it does not commit to any particular tier projection or feature decomposition. Specific theories may impose stronger OCP variants on derived tiers (place, voicing, etc.) via Phonology.Constraints.mkOCP.

Equations

• r.satisfiesOCP = (Core.Morphology.Root.adjDupCount r.segments == 0)