Consonantal roots

A consonantal root is an ordered melody of segments stored independently of vocalization or template — the nonconcatenative counterpart of a linear Morph. The segment type α is parametric: sonority-class roots instantiate α := Phonology.Sonority.Class ([AZ25b]), IPA-symbol roots α := String. Debates over the cognitive reality of roots are orthogonal to the data type — what status a theory gives the sequence is parameterized at the study level. In autosegmental terms a root is an unlinked melody on the consonantal tier; the canonical injection into Phonology/Autosegmental/Melody.lean awaits its first root-and-pattern consumer, as does a vocalism sibling (the same melody shape on the vowel tier).

Namespace separation

Owner-relative roots coexist: the top-level root is a contentful morph (Morphology/Root/Basic.lean, under whose definition consonantal skeletons are explicitly not roots); Morphology.ConsonantalRoot (this file) is the consonantal melody; Morphology.DM.Root is the abstract acategorial terminal; Panagiotidis2015.RootFamily records a category-neutral lexical root with its category-stamped derivatives; Verb.Root (Semantics/Verb/Root/) is the lexical-semantic root. No identification between them is substrate — homs live in the studies that assert them.

structure Morphology.ConsonantalRoot (α : Type u_1) : Type u_1

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 α

  The root segments, in order.

def Morphology.instReprConsonantalRoot.repr {α✝ : Type u_1} [Repr α✝] : ConsonantalRoot α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.instReprConsonantalRoot {α✝ : Type u_1} [Repr α✝] : Repr (ConsonantalRoot α✝)

Equations

• Morphology.instReprConsonantalRoot = { reprPrec := Morphology.instReprConsonantalRoot.repr }

@[implicit_reducible]

instance Morphology.instDecidableEqConsonantalRoot {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ConsonantalRoot α✝)

Equations

• Morphology.instDecidableEqConsonantalRoot = Morphology.instDecidableEqConsonantalRoot.decEq

def Morphology.instDecidableEqConsonantalRoot.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : ConsonantalRoot α✝) : Decidable (x✝ = x✝¹)

Equations

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

def Morphology.ConsonantalRoot.arity {α : Type u_1} (r : ConsonantalRoot α) : ℕ

The number of root segments.

Equations

• r.arity = r.segments.length

def Morphology.ConsonantalRoot.IsFinal {α : Type u_1} (r : ConsonantalRoot α) (i : ℕ) : Prop

Position i is the final root position.

Equations

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

@[implicit_reducible]

instance Morphology.ConsonantalRoot.instDecidableIsFinal {α : Type u_1} (r : ConsonantalRoot α) (i : ℕ) : Decidable (r.IsFinal i)

Equations

• r.instDecidableIsFinal i = Morphology.ConsonantalRoot.instDecidableIsFinal._aux_1 r i

def Morphology.ConsonantalRoot.IsNonfinal {α : Type u_1} (r : ConsonantalRoot α) (i : ℕ) : Prop

Position i is nonfinal (some position strictly past it exists). Used by *Misalignment ([Fau26] (2)).

Equations

• r.IsNonfinal i = (i + 1 < r.arity)

@[implicit_reducible]

instance Morphology.ConsonantalRoot.instDecidableIsNonfinal {α : Type u_1} (r : ConsonantalRoot α) (i : ℕ) : Decidable (r.IsNonfinal i)

Equations

• r.instDecidableIsNonfinal i = Morphology.ConsonantalRoot.instDecidableIsNonfinal._aux_1 r i

def Morphology.ConsonantalRoot.Biradical {α : Type u_1} (r : ConsonantalRoot α) : Prop

A root with exactly two segments (e.g. √qt → QaTaT-template biradicals in Hebrew, [McC81]).

Equations

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

def Morphology.ConsonantalRoot.Triradical {α : Type u_1} (r : ConsonantalRoot α) : Prop

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

Equations

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

def Morphology.ConsonantalRoot.Quadriradical {α : Type u_1} (r : ConsonantalRoot α) : Prop

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

Equations

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

@[implicit_reducible]

instance Morphology.ConsonantalRoot.instDecidableBiradical {α : Type u_1} (r : ConsonantalRoot α) : Decidable r.Biradical

Equations

• r.instDecidableBiradical = Morphology.ConsonantalRoot.instDecidableBiradical._aux_1 r

@[implicit_reducible]

instance Morphology.ConsonantalRoot.instDecidableTriradical {α : Type u_1} (r : ConsonantalRoot α) : Decidable r.Triradical

Equations

• r.instDecidableTriradical = Morphology.ConsonantalRoot.instDecidableTriradical._aux_1 r

@[implicit_reducible]

instance Morphology.ConsonantalRoot.instDecidableQuadriradical {α : Type u_1} (r : ConsonantalRoot α) : Decidable r.Quadriradical

Equations

• r.instDecidableQuadriradical = Morphology.ConsonantalRoot.instDecidableQuadriradical._aux_1 r

def Morphology.ConsonantalRoot.finalSegment {α : Type u_1} (r : ConsonantalRoot α) : Option α

The last segment of the root, if any.

Equations

• r.finalSegment = r.segments.getLast?

def Morphology.ConsonantalRoot.segmentAt {α : Type u_1} (r : ConsonantalRoot α) (i : ℕ) : Option α

The segment at position i, if in range.

Equations

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

def Morphology.ConsonantalRoot.IsOCPClean {α : Type u_1} [DecidableEq α] (r : ConsonantalRoot α) : Prop

Root-level OCP ([McC81], [Fau26]): a consonantal root has no two adjacent identical segments. Segment-level and theory-neutral — it commits to no tier projection or feature decomposition (stronger tier-relative variants go through OCP.IsCleanOn). Definitionally the segment tier being OCP.IsClean.

Equations

• r.IsOCPClean = OCP.IsClean r.segments

@[implicit_reducible]

instance Morphology.ConsonantalRoot.instDecidablePredIsOCPClean {α : Type u_1} [DecidableEq α] : DecidablePred IsOCPClean

Equations

• r.instDecidablePredIsOCPClean = Morphology.ConsonantalRoot.instDecidablePredIsOCPClean._aux_1 r