Haspelmath 2025: the contentfulness-gated root

[Has25b]

Definition (1): a root is a contentful morph — a morph denoting an action, an object or a property — that can occur as part of a free form without another contentful morph. Against the formal base definition of Morphology/Root/Basic.lean, contentfulness is a gate: the qualifying clause excludes contentful affixes (the Japanese causative -ase) and neoclassical combining forms (geo-, socio-), which are contentful but never the sole contentful morph of a free form (geo_not_root). Formally identical roots with related meanings (hammer the instrument, hammer the action) are heterosemous sister roots, not one precategorial root — the classification cls assigns each its own class; the paper's §6 divergence from precategorial root families is deferred content.

Main declarations

• RootClass — action, object, and property roots; RootClass.upos — word classes as comparative concepts.
• Morph.IsRootIn — definition (1), relative to a fragment's free forms and contentfulness classification.
• geo_not_root — a combining form is contentful yet fails the definition.

inductive Haspelmath2025Root.RootClass : Type

The three semantic root classes: roots denoting actions, objects, and properties. Their prototypical combinations with discourse functions — predication, reference, modification — need no function indicators, which is what makes these the crucial classes for word-class typology.

• action : RootClass

  A root denoting an action (sing, open).

• object : RootClass

  A root denoting an object (tree, bird).

• property : RootClass

  A root denoting a property (good, small).

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqRootClass : DecidableEq RootClass

Equations

• Haspelmath2025Root.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instReprRootClass : Repr RootClass

Equations

• Haspelmath2025Root.instReprRootClass = { reprPrec := Haspelmath2025Root.instReprRootClass.repr }

def Haspelmath2025Root.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

def Haspelmath2025Root.RootClass.upos : RootClass → UD.UPOS

Word classes as comparative concepts: a verb is an action-denoting root, a noun an object-denoting root, an adjective a property-denoting root.

Equations

• Haspelmath2025Root.RootClass.action.upos = UD.UPOS.VERB
• Haspelmath2025Root.RootClass.object.upos = UD.UPOS.NOUN
• Haspelmath2025Root.RootClass.property.upos = UD.UPOS.ADJ

def Morphology.Morph.IsRootIn (m : Morph) (freeForms : List (List Morph)) (cls : Morph → Option Haspelmath2025Root.RootClass) : Prop

m.IsRootIn freeForms cls is definition (1) relative to a fragment: the classification cls assigns m a root class (it is contentful), and m occurs in some free form in which every other morph is non-contentful.

Equations

• m.IsRootIn freeForms cls = ((cls m).isSome = true ∧ ∃ w ∈ freeForms, m ∈ w ∧ ∀ m' ∈ w, m' ≠ m → cls m' = none)

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableIsRootIn (m : Morphology.Morph) (freeForms : List (List Morphology.Morph)) (cls : Morphology.Morph → Option RootClass) : Decidable (m.IsRootIn freeForms cls)

Equations

• Haspelmath2025Root.instDecidableIsRootIn m freeForms cls = Haspelmath2025Root.instDecidableIsRootIn._aux_1 m freeForms cls

The combining-form exclusion

def Haspelmath2025Root.geo : Morphology.Morph

The neoclassical combining form geo-.

Equations

• Haspelmath2025Root.geo = Morphology.Morph.root "geo"

def Haspelmath2025Root.logy : Morphology.Morph

The neoclassical combining form -logy.

Equations

• Haspelmath2025Root.logy = Morphology.Morph.root "logy"

def Haspelmath2025Root.geoCls : Morphology.Morph → Option RootClass

The classification: both pieces of geology are contentful.

Equations

• Haspelmath2025Root.geoCls x✝ = if x✝ = Haspelmath2025Root.geo ∨ x✝ = Haspelmath2025Root.logy then some Haspelmath2025Root.RootClass.object else none

theorem Haspelmath2025Root.geo_not_root : ¬geo.IsRootIn [[geo, logy]] geoCls ∧ geo.IsCoreIn [[geo, logy]] [[geo, logy]]

geo- is contentful yet not a root: in geology it never occurs as the sole contentful morph of a free form — the definition's qualifying clause in action. Under the formal base definition it is a morphological core.

Sister roots vs one root, as hom-existence

The paper's heterosemy claim — hammer the instrument and hammer the action are two sister roots, not one precategorial root — rendered on Morphology.Realization: the sister carving (two frame-restricted indices) and the single-√ carving (one index, allosemous across frames) are hom-incomparable on the strict tier, so neither analysis reduces to the other; and accidental homophones (bank₁/bank₂) spellout-merge but never interp-merge into any target — the strict tier separates identity from homophony.

inductive Haspelmath2025Root.Frame : Type

The two categorial frames.

• nominal : Frame
• verbal : Frame

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqFrame : DecidableEq Frame

Equations

• Haspelmath2025Root.instDecidableEqFrame x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instFintypeFrame : Fintype Frame

Equations

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

@[implicit_reducible]

instance Haspelmath2025Root.instReprFrame : Repr Frame

Equations

• Haspelmath2025Root.instReprFrame = { reprPrec := Haspelmath2025Root.instReprFrame.repr }

def Haspelmath2025Root.instReprFrame.repr : Frame → ℕ → Std.Format

Equations

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

inductive Haspelmath2025Root.BankLex : Type

The two bank homophones.

• river : BankLex
• money : BankLex

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqBankLex : DecidableEq BankLex

Equations

• Haspelmath2025Root.instDecidableEqBankLex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instFintypeBankLex : Fintype BankLex

Equations

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

@[implicit_reducible]

instance Haspelmath2025Root.instReprBankLex : Repr BankLex

Equations

• Haspelmath2025Root.instReprBankLex = { reprPrec := Haspelmath2025Root.instReprBankLex.repr }

def Haspelmath2025Root.instReprBankLex.repr : BankLex → ℕ → Std.Format

Equations

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

inductive Haspelmath2025Root.BankSense : Type

Their senses.

• riverside : BankSense
• institution : BankSense

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqBankSense : DecidableEq BankSense

Equations

• Haspelmath2025Root.instDecidableEqBankSense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instFintypeBankSense : Fintype BankSense

Equations

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

@[implicit_reducible]

instance Haspelmath2025Root.instReprBankSense : Repr BankSense

Equations

• Haspelmath2025Root.instReprBankSense = { reprPrec := Haspelmath2025Root.instReprBankSense.repr }

def Haspelmath2025Root.instReprBankSense.repr : BankSense → ℕ → Std.Format

Equations

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

def Haspelmath2025Root.bankSisters : Morphology.Realization.Interpreted BankLex Frame String BankSense

The homophone system: identical spellout everywhere, distinct senses.

Equations

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

def Haspelmath2025Root.bankMerged : Morphology.Realization Unit Frame String

The merged one-index target for the spellout level.

Equations

• Haspelmath2025Root.bankMerged = { realize := fun (x : Unit) (x_1 : Haspelmath2025Root.Frame) => {"bank"} }

theorem Haspelmath2025Root.bank_spellout_merger : Nonempty (bankSisters.Hom bankMerged)

At the spellout level the homophones merge: a transport hom exists.

theorem Haspelmath2025Root.bank_no_identity {R₂ : Type u_1} {C₂ : Type u_2} {T : Morphology.Realization.Interpreted R₂ C₂ String BankSense} (φ : bankSisters.Hom T) : φ.onRoot BankLex.river ≠ φ.onRoot BankLex.money

No strict hom into any target merges the homophones: identification would force their senses to coincide contextwise (Realization.Interpreted.Hom.interp_eq_of_onRoot_eq). Homophony is not identity.

inductive Haspelmath2025Root.HammerSense : Type

The heterosemous senses of hammer.

• instrument : HammerSense
• action : HammerSense

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqHammerSense : DecidableEq HammerSense

Equations

• Haspelmath2025Root.instDecidableEqHammerSense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instFintypeHammerSense : Fintype HammerSense

Equations

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

@[implicit_reducible]

instance Haspelmath2025Root.instReprHammerSense : Repr HammerSense

Equations

• Haspelmath2025Root.instReprHammerSense = { reprPrec := Haspelmath2025Root.instReprHammerSense.repr }

def Haspelmath2025Root.instReprHammerSense.repr : HammerSense → ℕ → Std.Format

Equations

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

inductive Haspelmath2025Root.Sisters : Type

The paper's carving: two sister roots.

• hammerN : Sisters
• hammerV : Sisters

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqSisters : DecidableEq Sisters

Equations

• Haspelmath2025Root.instDecidableEqSisters x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instFintypeSisters : Fintype Sisters

Equations

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

@[implicit_reducible]

instance Haspelmath2025Root.instReprSisters : Repr Sisters

Equations

• Haspelmath2025Root.instReprSisters = { reprPrec := Haspelmath2025Root.instReprSisters.repr }

def Haspelmath2025Root.instReprSisters.repr : Sisters → ℕ → Std.Format

Equations

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

inductive Haspelmath2025Root.Sqrt : Type

The rival carving: one acategorial root.

• hammer : Sqrt

@[implicit_reducible]

instance Haspelmath2025Root.instDecidableEqSqrt : DecidableEq Sqrt

Equations

• Haspelmath2025Root.instDecidableEqSqrt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Haspelmath2025Root.instFintypeSqrt : Fintype Sqrt

Equations

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

@[implicit_reducible]

instance Haspelmath2025Root.instReprSqrt : Repr Sqrt

Equations

• Haspelmath2025Root.instReprSqrt = { reprPrec := Haspelmath2025Root.instReprSqrt.repr }

def Haspelmath2025Root.instReprSqrt.repr : Sqrt → ℕ → Std.Format

Equations

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

def Haspelmath2025Root.sisterCarving : Morphology.Realization.Interpreted Sisters Frame String HammerSense

The sister carving: each root licensed only in its own frame, with its own sense.

Equations

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

def Haspelmath2025Root.sqrtCarving : Morphology.Realization.Interpreted Sqrt Frame String HammerSense

The single-√ carving: one root licensed in both frames, allosemous.

Equations

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

theorem Haspelmath2025Root.sisters_to_sqrt_none (φ : sisterCarving.Hom sqrtCarving) : False

No strict hom from the sister carving to the single-√ carving: the sisters' licensing gaps (hammer-the-noun has no verbal cell) cannot be reproduced by the total √.

theorem Haspelmath2025Root.sqrt_to_sisters_none (φ : sqrtCarving.Hom sisterCarving) : False

No strict hom from the single-√ carving to the sister carving either: the total √ must land on one frame-restricted sister, whose single licensed cell cannot carry both allosemes. The two carvings are hom-incomparable — the rivalry is between genuinely distinct systems.

theorem Haspelmath2025Root.sisters_lax_merge : Nonempty (sisterCarving.LaxHom sqrtCarving)

The sisters do lax-merge into the single √ (Realization.Interpreted.LaxHom): each sister's forms and senses are among the √'s. The lax-not-strict gradient characterizes the relation between the two analyses — the precategorial carving subsumes the sister carving's data without being identical to it. The heterosemy view's own positive machinery is different: per (17b), the sisters are related by sister schemas ([JA20]; Morphology/Construction/Sister.lean), not by a shared realization target.