Roots

The formal definition of roothood over Morph, relative to a fragment's word and free-form inventories ([Blo33], the base definition of [Qin25]): a morph is a root iff it occurs in a primary word — one with no free form as a proper part. The definition is deliberately inclusive (meaning-free cores like -fer qualify; so do free function words); Studies/Qin2025.lean grades instances by canonicity, and [Has25b]'s contentfulness-gated alternative is Studies/Haspelmath2025Root.lean. Consonantal skeletons are ConsonantalRoot; DM's acategorial root is Morphology/DM/Root.lean.

Main declarations

• IsPrimaryWord — no proper contiguous part is a free form.
• Morph.IsCoreIn — the root property: occurrence in a primary word.
• Morph.IsTypicalAffixIn — occurrence in secondary words only.

def Morphology.IsPrimaryWord (freeForms : List (List Morph)) (w : List Morph) : Prop

A word is primary ([Blo33]): no proper contiguous part of it is a free form. cat and refer are primary; cats and blackbirds are secondary.

Equations

• Morphology.IsPrimaryWord freeForms w = ∀ f ∈ freeForms, f.length < w.length → ¬f <:+: w

@[implicit_reducible]

instance Morphology.instDecidableIsPrimaryWord (freeForms : List (List Morph)) (w : List Morph) : Decidable (IsPrimaryWord freeForms w)

Equations

• Morphology.instDecidableIsPrimaryWord freeForms w = Morphology.instDecidableIsPrimaryWord._aux_1 freeForms w

def Morphology.Morph.IsCoreIn (m : Morph) (words freeForms : List (List Morph)) : Prop

A morphological core — [Qin25]'s base definition of a root: a morph occurring in some primary word.

Equations

• m.IsCoreIn words freeForms = ∃ w ∈ words, Morphology.IsPrimaryWord freeForms w ∧ m ∈ w

@[implicit_reducible]

instance Morphology.instDecidableIsCoreIn (m : Morph) (words freeForms : List (List Morph)) : Decidable (m.IsCoreIn words freeForms)

Equations

• Morphology.instDecidableIsCoreIn m words freeForms = Morphology.instDecidableIsCoreIn._aux_1 m words freeForms

def Morphology.Morph.IsTypicalAffixIn (m : Morph) (words freeForms : List (List Morph)) : Prop

A typical affix occurs only in secondary words ([Blo33]): -s and -ness attach to free forms.

Equations

• m.IsTypicalAffixIn words freeForms = ∀ w ∈ words, m ∈ w → ¬Morphology.IsPrimaryWord freeForms w

theorem Morphology.isPrimaryWord_singleton {freeForms : List (List Morph)} (h : [] ∉ freeForms) (m : Morph) : IsPrimaryWord freeForms [m]

A singleton word is primary when the free-form inventory has no empty form.

theorem Morphology.Morph.isCoreIn_of_free_word {words freeForms : List (List Morph)} {m : Morph} (hw : [m] ∈ words) (h : [] ∉ freeForms) : m.IsCoreIn words freeForms

A free morpheme standing as a word is a morphological core.