Root certificates: roothood as a role

Roothood is not a data type but a role an index plays in a Morphology.Realization, adjudicated by extensional certificates — the Prime-over-a-monoid pattern, where a predicate relative to a structure replaces a distinguished carrier. Three orthogonal axes probe the role, each decidable per fragment:

• Atomicity — does every licensed cell decompose to a nonempty set of cores? cellCores is the third instantiation of the IsConstantIn/IsVariantIn pair (after realize and interp): its constancy cut splits form-variance into affixal inflection (cat/cats, cores constant) and a suppletive core (go/went, cores vary), refining the landed IsOverabundant/IsProperlySuppletive cell-locus cut along a perpendicular axis.
• Listedness — does the profile factor through a grammatical type (an f-morpheme inventory), or does some index do lexical work its type cannot predict (an l-morpheme)? The Harley–Noyer l/f divide ([HN99], [Emb21]) as a provable dichotomy.
• Categorial freedom — is one index licensed under two distinct categorizers? DM acategoriality ([Mar97], [Ara05]) as a per-fragment decidable complement to the hom-tier merger theorems.

Core extraction is parametric in extract : F → Finset C, so the axis is not tied to concatenative form: the concatenative instance coreMorphsIn filters a word's morphs by Morph.IsCoreIn ([Blo33], [Qin25]); a consonantal-melody instance would take fun r => r.segments.toFinset for ConsonantalRoot (Root/Consonantal.lean), not built here.

These certificates adjudicate the descriptive taxonomy — the suppletion trichotomy, l-vs-f, per-fragment categorial freedom — and are deliberately extensional: they do not settle the derivational disputes (Arad-vs-Borer first-categorization locality), which live in the admissible lax mergers of Realization.lean (see its underdetermination paragraph). This is the root-question layer over Realization, co-equal with Paradigm/, Exponence/, and Construction/ — not a foundation beneath them.

Main declarations

• cellCores, HasNonemptyCores — parametric core extraction and the atomicity certificate.
• HasSuppletiveCore, IsAffixallyInflected, suppletive_core_dichotomy, suppletive_taxonomy — the constancy pair's third instantiation and the suppletion trichotomy.
• coreMorphsIn — the concatenative core-extraction instance.
• IsFunctionalInventory, DoesLexicalWork, isFunctionalInventory_iff_no_lexicalWork — the l/f-morpheme divide.
• IsCrossCategorial — categorial freedom.

The constancy pair as a negation dichotomy

theorem Morphology.Root.isConstantIn_iff_not_isVariantIn {R : Type u_1} {Ctx : Type u_2} {X : Type u_8} {g : R → Ctx → Finset X} {r : R} : IsConstantIn g r ↔ ¬IsVariantIn g r

Constancy and variance of a contextual map are exact complements: a strengthening of not_isConstantIn_of_isVariantIn to an Iff.

Atomicity: parametric core extraction

def Morphology.Root.cellCores {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] : R → Ctx → Finset C

The cores a realization exposes at a cell: the union, over the cell's forms, of each form's cores under extract. The third instantiation of the IsConstantIn/IsVariantIn contextual-map slot, after realize and interp.

Equations

• Morphology.Root.cellCores S extract r c = (S.realize r c).biUnion extract

@[simp]

theorem Morphology.Root.cellCores_singleton {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [DecidableEq F] (r : R) (c : Ctx) : cellCores S (fun (f : F) => {f}) r c = S.realize r c

def Morphology.Root.HasNonemptyCores {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] : Prop

Atomicity: every licensed cell decomposes to at least one core — the root always contributes segmental substance where it is realized.

Equations

• Morphology.Root.HasNonemptyCores S extract = ∀ (r : R) (c : Ctx), S.IsLicensed r c → (Morphology.Root.cellCores S extract r c).Nonempty

theorem Morphology.Root.hasNonemptyCores_of_extract_nonempty {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] (hne : ∀ (f : F), (extract f).Nonempty) : HasNonemptyCores S extract

An extraction that never returns an empty core certifies atomicity: the Option-shaped and total realizations are atomic under any pointwise-nonempty extract (e.g. a stem projection).

The suppletion trichotomy

def Morphology.Root.HasSuppletiveCore {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] (r : R) : Prop

Suppletive core: the cores themselves vary across contexts — go/went, where no shared core survives the alternation. The IsVariantIn instance at cellCores.

Equations

• Morphology.Root.HasSuppletiveCore S extract r = Morphology.IsVariantIn (Morphology.Root.cellCores S extract) r

def Morphology.Root.IsAffixallyInflected {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] (r : R) : Prop

Affixal inflection: forms vary but cores do not — cat/cats, one core across an added affix. Form-variance with a constant core.

Equations

• Morphology.Root.IsAffixallyInflected S extract r = (S.IsSuppletive r ∧ Morphology.IsConstantIn (Morphology.Root.cellCores S extract) r)

theorem Morphology.Root.isAffixallyInflected_iff {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] {r : R} : IsAffixallyInflected S extract r ↔ S.IsSuppletive r ∧ ¬HasSuppletiveCore S extract r

Affixal inflection is exactly form-variance without a suppletive core: the two core-axis outcomes are mutually exclusive.

theorem Morphology.Root.suppletive_core_dichotomy {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] {r : R} (h : S.IsSuppletive r) : IsAffixallyInflected S extract r ∨ HasSuppletiveCore S extract r

The core-axis dichotomy: a form-variant root is either affixally inflected (cat/cats) or has a suppletive core (go/went), exhaustively and exclusively.

theorem Morphology.Root.suppletive_taxonomy {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [DecidableEq C] {r : R} (h : S.IsSuppletive r) : (S.IsOverabundant r ∨ S.IsProperlySuppletive r) ∧ (IsAffixallyInflected S extract r ∨ HasSuppletiveCore S extract r)

The suppletion trichotomy: a form-variant root is classified by two orthogonal cuts — the landed cell-locus cut (IsOverabundant, cell-internal dived/dove, versus IsProperlySuppletive, cross-cell go/went) and the core-axis cut (IsAffixallyInflected versus HasSuppletiveCore). Their cross product is the descriptive taxonomy of root-form variation.

theorem Morphology.Root.hasSuppletiveCore_singleton {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [DecidableEq F] (r : R) : HasSuppletiveCore S (fun (f : F) => {f}) r ↔ S.IsSuppletive r

Under the identity core-extraction (a monomorphemic form is its own core), having a suppletive core coincides with form-suppletion: whole-root alternations like go/went are suppletive-cored. The bridge that lets a study certify a suppletive inventory without recomputing its fibers.

The concatenative core-extraction instance

def Morphology.Root.coreMorphsIn (words freeForms : List (List Morph)) (w : List Morph) : Finset Morph

The cores of a word ([Blo33], [Qin25]): its morphs that occur in some primary word, i.e. that satisfy Morph.IsCoreIn relative to the fragment's word and free-form inventories. The affix side (-s, -ness) is filtered out, so cat and cats share the single core cat.

Equations

• Morphology.Root.coreMorphsIn words freeForms w = {m ∈ w.toFinset | m.IsCoreIn words freeForms}

Listedness: the l/f-morpheme divide

def Morphology.Root.IsFunctionalInventory {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} {T : Type u_7} (S : Realization.Interpreted R Ctx F M) (τ : R → T) : Prop

An f-morpheme inventory ([HN99]): the interpretation-and-form profile factors through a grammatical type — same type, same profile — so the index carries no information its type does not.

Equations

• Morphology.Root.IsFunctionalInventory S τ = ∀ (r r' : R), τ r = τ r' → S.ProfileEq r r'

def Morphology.Root.DoesLexicalWork {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} {T : Type u_7} (S : Realization.Interpreted R Ctx F M) (τ : R → T) (r : R) : Prop

An index does lexical work ([Emb21]): another index shares its type yet differs in profile, so the type underdetermines it — the l-morpheme witness against IsFunctionalInventory.

Equations

• Morphology.Root.DoesLexicalWork S τ r = ∃ (r' : R), τ r = τ r' ∧ ¬S.ProfileEq r r'

theorem Morphology.Root.isFunctionalInventory_iff_no_lexicalWork {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} {T : Type u_7} (S : Realization.Interpreted R Ctx F M) (τ : R → T) : IsFunctionalInventory S τ ↔ ∀ (r : R), ¬DoesLexicalWork S τ r

The l/f dichotomy: an inventory is functional iff no index does lexical work. The Harley–Noyer split ([HN99], [Emb21]) as the negation duality between the two certificates.

Categorial freedom

def Morphology.Root.IsCrossCategorial {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {K : Type u_6} (S : Realization R Ctx F) (k : Ctx → K) (r : R) : Prop

Categorial freedom ([Mar97], [Ara05]): one index is licensed in two contexts of distinct category k — DM acategoriality, the per-fragment decidable complement to the hom-tier merger theorems of Realization.lean.

Equations

• Morphology.Root.IsCrossCategorial S k r = ∃ (c : Ctx) (c' : Ctx), k c ≠ k c' ∧ S.IsLicensed r c ∧ S.IsLicensed r c'

Decidability

@[implicit_reducible]

instance Morphology.Root.instDecidableHasNonemptyCoresOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [Fintype R] [Fintype Ctx] [DecidableEq F] [DecidableEq C] : Decidable (HasNonemptyCores S extract)

Equations

• Morphology.Root.instDecidableHasNonemptyCoresOfFintypeOfDecidableEq S extract = Morphology.Root.instDecidableHasNonemptyCoresOfFintypeOfDecidableEq._aux_1 S extract

@[implicit_reducible]

instance Morphology.Root.instDecidableHasSuppletiveCoreOfFintype {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [Fintype Ctx] [DecidableEq C] (r : R) : Decidable (HasSuppletiveCore S extract r)

Equations

• Morphology.Root.instDecidableHasSuppletiveCoreOfFintype S extract r = Morphology.Root.instDecidableHasSuppletiveCoreOfFintype._aux_1 S extract r

@[implicit_reducible]

instance Morphology.Root.instDecidableIsAffixallyInflectedOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {C : Type u_5} (S : Realization R Ctx F) (extract : F → Finset C) [Fintype Ctx] [DecidableEq F] [DecidableEq C] (r : R) : Decidable (IsAffixallyInflected S extract r)

Equations

• Morphology.Root.instDecidableIsAffixallyInflectedOfFintypeOfDecidableEq S extract r = Morphology.Root.instDecidableIsAffixallyInflectedOfFintypeOfDecidableEq._aux_1 S extract r

@[implicit_reducible]

instance Morphology.Root.instDecidableIsCrossCategorialOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {K : Type u_6} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] [DecidableEq K] (k : Ctx → K) (r : R) : Decidable (IsCrossCategorial S k r)

Equations

• Morphology.Root.instDecidableIsCrossCategorialOfFintypeOfDecidableEq S k r = Morphology.Root.instDecidableIsCrossCategorialOfFintypeOfDecidableEq._aux_1 S k r

@[implicit_reducible]

instance Morphology.Root.instDecidableProfileEqOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Realization.Interpreted R Ctx F M) [Fintype Ctx] [DecidableEq F] [DecidableEq M] (r r' : R) : Decidable (S.ProfileEq r r')

Equations

• Morphology.Root.instDecidableProfileEqOfFintypeOfDecidableEq S r r' = Morphology.Root.instDecidableProfileEqOfFintypeOfDecidableEq._aux_1 S r r'

@[implicit_reducible]

instance Morphology.Root.instDecidableIsFunctionalInventoryOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} {T : Type u_7} (S : Realization.Interpreted R Ctx F M) (τ : R → T) [Fintype R] [Fintype Ctx] [DecidableEq T] [DecidableEq F] [DecidableEq M] : Decidable (IsFunctionalInventory S τ)

Equations

• Morphology.Root.instDecidableIsFunctionalInventoryOfFintypeOfDecidableEq S τ = Morphology.Root.instDecidableIsFunctionalInventoryOfFintypeOfDecidableEq._aux_1 S τ

@[implicit_reducible]

instance Morphology.Root.instDecidableDoesLexicalWorkOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} {T : Type u_7} (S : Realization.Interpreted R Ctx F M) (τ : R → T) [Fintype R] [Fintype Ctx] [DecidableEq T] [DecidableEq F] [DecidableEq M] (r : R) : Decidable (DoesLexicalWork S τ r)

Equations

• Morphology.Root.instDecidableDoesLexicalWorkOfFintypeOfDecidableEq S τ r = Morphology.Root.instDecidableDoesLexicalWorkOfFintypeOfDecidableEq._aux_1 S τ r