Bantu Language Family: Shared Parameters

@cite{carstens-1991} @cite{kramer-2015} @cite{carstens-2026} @cite{halpert-hammerly-2026} @cite{hammerly-2023}

Shared types for Bantu language fragments, capturing cross-Bantu structural regularities in the noun class system. Individual Bantu languages (Swahili, Xhosa, Shona) import these types and specialize them with language-specific class inventories and morphological forms.

Key shared structure

• Noun classes come in singular/plural pairs that define genders (@cite{carstens-1991}, @cite{kramer-2015})
• A small number of genders have semantic cores — salient associations with entity classes like [human], [animal], [inanimate] (@cite{carstens-2026} §4.2)
• The semantic core determines whether a gender is interpretable (bears an i[entity] flavor) or uninterpretable (purely formal)
• All Bantu nouns are underlyingly specified for core noun class via bivalent features [±Animate] and [±Human], from @cite{hammerly-2023}'s containment hierarchy (@cite{halpert-hammerly-2026} (19))

Design

This file stores pure data — types, inventories, and status classifications. Resolution logic (percolation, intersection) lives in the Theory layer (GenderResolution.lean); study files connect the two.

structure Fragments.Bantu.AnimacyFeatures : Type

Bivalent animacy features from @cite{hammerly-2023}'s containment hierarchy, applied to Bantu core noun class by @cite{halpert-hammerly-2026}.

Two features determine core noun class:

• [±Animate]: distinguishes animate from inanimate entities
• [±Human]: distinguishes humans from non-human animates

These stand in a containment relation: [+Human] entails [+Animate] (being human entails being animate). The fourth combination [−Animate, +Human] is semantically incoherent and ruled out by wellFormed.

• isAnimate : Bool
• isHuman : Bool

def Fragments.Bantu.instDecidableEqAnimacyFeatures.decEq (x✝ x✝¹ : AnimacyFeatures) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqAnimacyFeatures : DecidableEq AnimacyFeatures

Equations

• Fragments.Bantu.instDecidableEqAnimacyFeatures = Fragments.Bantu.instDecidableEqAnimacyFeatures.decEq

@[implicit_reducible]

instance Fragments.Bantu.instReprAnimacyFeatures : Repr AnimacyFeatures

Equations

• Fragments.Bantu.instReprAnimacyFeatures = { reprPrec := Fragments.Bantu.instReprAnimacyFeatures.repr }

def Fragments.Bantu.instReprAnimacyFeatures.repr : AnimacyFeatures → ℕ → Std.Format

Equations

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

def Fragments.Bantu.AnimacyFeatures.wellFormed (af : AnimacyFeatures) : Bool

Well-formedness: [+Human] → [+Animate]. Being human entails being animate (@cite{halpert-hammerly-2026} fn. 10).

Equations

• af.wellFormed = (!af.isHuman || af.isAnimate)

def Fragments.Bantu.AnimacyFeatures.human : AnimacyFeatures

HUMAN = [+Animate, +Human] ≈ class 1/2

Equations

• Fragments.Bantu.AnimacyFeatures.human = { isAnimate := true, isHuman := true }

def Fragments.Bantu.AnimacyFeatures.animal : AnimacyFeatures

NON-HUMAN ANIMATE = [+Animate, −Human] ≈ class 9/10

Equations

• Fragments.Bantu.AnimacyFeatures.animal = { isAnimate := true, isHuman := false }

def Fragments.Bantu.AnimacyFeatures.inanimate : AnimacyFeatures

INANIMATE = [−Animate, −Human] ≈ class 7/8

Equations

• Fragments.Bantu.AnimacyFeatures.inanimate = { isAnimate := false, isHuman := false }

theorem Fragments.Bantu.AnimacyFeatures.illFormed_only : { isAnimate := false, isHuman := true }.wellFormed = false

The fourth combination [−Animate, +Human] violates well-formedness.

theorem Fragments.Bantu.AnimacyFeatures.exactly_three : (List.filter wellFormed [{ isAnimate := true, isHuman := true }, { isAnimate := true, isHuman := false }, { isAnimate := false, isHuman := true }, { isAnimate := false, isHuman := false }]).length = 3

Exactly three well-formed core noun classes. This is an instance of the general PrivativePair.no_four_way: any PhiFeatures type supports at most 3 well-formed cells.

@[implicit_reducible]

instance Fragments.Bantu.AnimacyFeatures.instPhiFeatures : Features.PhiFeatures AnimacyFeatures

Animacy features instantiate the PhiFeatures privative pair: outer = [±Animate], inner = [±Human]. This is the same mathematical structure as person features (outer = [±participant], inner = [±author]), confirming @cite{hammerly-2023}'s claim that person and animacy features share a common containment architecture.

Equations

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

def Fragments.Bantu.AnimacyFeatures.toAnimacyLevel : AnimacyFeatures → Features.Prominence.AnimacyLevel

Bridge to Features.Prominence.AnimacyLevel: the three well-formed feature bundles map to the three animacy levels used throughout the codebase for differential argument marking, agreement hierarchies, etc.

Equations

• { isAnimate := isAnimate, isHuman := true }.toAnimacyLevel = Features.Prominence.AnimacyLevel.human
• { isAnimate := true, isHuman := false }.toAnimacyLevel = Features.Prominence.AnimacyLevel.animate
• { isAnimate := false, isHuman := false }.toAnimacyLevel = Features.Prominence.AnimacyLevel.inanimate

theorem Fragments.Bantu.AnimacyFeatures.human_level : human.toAnimacyLevel = Features.Prominence.AnimacyLevel.human

theorem Fragments.Bantu.AnimacyFeatures.animal_level : animal.toAnimacyLevel = Features.Prominence.AnimacyLevel.animate

theorem Fragments.Bantu.AnimacyFeatures.inanimate_level : inanimate.toAnimacyLevel = Features.Prominence.AnimacyLevel.inanimate

inductive Fragments.Bantu.FinalVowel : Type

Bantu nominalizing final vowels encode core noun class on the categorizing head n (@cite{halpert-hammerly-2026} (22)).

• -i: n[+Animate, +Human] (human nominalizer)
• -o: n[±Animate, −Human] (non-human nominalizer)
• -a: verbalizing final vowel (not a core noun class marker)

• i : FinalVowel
• o : FinalVowel
• a : FinalVowel

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqFinalVowel : DecidableEq FinalVowel

Equations

• Fragments.Bantu.instDecidableEqFinalVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Bantu.instReprFinalVowel.repr : FinalVowel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Bantu.instReprFinalVowel : Repr FinalVowel

Equations

• Fragments.Bantu.instReprFinalVowel = { reprPrec := Fragments.Bantu.instReprFinalVowel.repr }

def Fragments.Bantu.AnimacyFeatures.toFinalVowel (af : AnimacyFeatures) : FinalVowel

Core noun class features determine the nominalizing final vowel (@cite{halpert-hammerly-2026} (22)).

Equations

• af.toFinalVowel = if af.isHuman = true then Fragments.Bantu.FinalVowel.i else Fragments.Bantu.FinalVowel.o

theorem Fragments.Bantu.AnimacyFeatures.human_fv : human.toFinalVowel = FinalVowel.i

theorem Fragments.Bantu.AnimacyFeatures.animal_fv : animal.toFinalVowel = FinalVowel.o

theorem Fragments.Bantu.AnimacyFeatures.inanimate_fv : inanimate.toFinalVowel = FinalVowel.o

inductive Fragments.Bantu.SemanticCore : Type

Semantic cores of Bantu gender: salient associations between genders and entity classes (@cite{carstens-2026} §4.2, (71)).

Not all Bantu genders have a semantic core. Those that do have an interpretable i[entity] flavor at their innermost nP layer. Those that don't are purely formal (uninterpretable).

Xhosa has three cores — [human], [animal], [inanimate] — reflecting a three-way entity split. Shona collapses [animal] and [inanimate] into a single [non-human] default, adding a fourth constructor. The Xhosa distinction is the parametric maximum.

• human : SemanticCore
• animal : SemanticCore
• inanimate : SemanticCore
• nonhuman : SemanticCore

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqSemanticCore : DecidableEq SemanticCore

Equations

• Fragments.Bantu.instDecidableEqSemanticCore x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Bantu.instReprSemanticCore : Repr SemanticCore

Equations

• Fragments.Bantu.instReprSemanticCore = { reprPrec := Fragments.Bantu.instReprSemanticCore.repr }

def Fragments.Bantu.instReprSemanticCore.repr : SemanticCore → ℕ → Std.Format

Equations

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

def Fragments.Bantu.AnimacyFeatures.toCoreClass : AnimacyFeatures → SemanticCore

Derive SemanticCore from bivalent features (@cite{halpert-hammerly-2026} (19)).

Equations

• { isAnimate := true, isHuman := true }.toCoreClass = Fragments.Bantu.SemanticCore.human
• { isAnimate := true, isHuman := false }.toCoreClass = Fragments.Bantu.SemanticCore.animal
• { isAnimate := false, isHuman := isHuman }.toCoreClass = Fragments.Bantu.SemanticCore.inanimate

def Fragments.Bantu.SemanticCore.toFeatures : SemanticCore → AnimacyFeatures

Inverse: recover features from SemanticCore (for the three Bantu cores).

Equations

• Fragments.Bantu.SemanticCore.human.toFeatures = Fragments.Bantu.AnimacyFeatures.human
• Fragments.Bantu.SemanticCore.animal.toFeatures = Fragments.Bantu.AnimacyFeatures.animal
• Fragments.Bantu.SemanticCore.inanimate.toFeatures = Fragments.Bantu.AnimacyFeatures.inanimate
• Fragments.Bantu.SemanticCore.nonhuman.toFeatures = Fragments.Bantu.AnimacyFeatures.inanimate

theorem Fragments.Bantu.AnimacyFeatures.roundtrip (af : AnimacyFeatures) (h : af.wellFormed = true) : af.toCoreClass.toFeatures = af

Round-trip: features → core → features is identity for well-formed features.

structure Fragments.Bantu.ConflationPattern : Type

A language's conflation pattern: which containment features it is sensitive to. Dropping a feature merges the categories it distinguishes (@cite{halpert-hammerly-2026} (5), following @cite{mcginnis-2005}).

• usesAnimate : Bool
• usesHuman : Bool

def Fragments.Bantu.instDecidableEqConflationPattern.decEq (x✝ x✝¹ : ConflationPattern) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqConflationPattern : DecidableEq ConflationPattern

Equations

• Fragments.Bantu.instDecidableEqConflationPattern = Fragments.Bantu.instDecidableEqConflationPattern.decEq

@[implicit_reducible]

instance Fragments.Bantu.instReprConflationPattern : Repr ConflationPattern

Equations

• Fragments.Bantu.instReprConflationPattern = { reprPrec := Fragments.Bantu.instReprConflationPattern.repr }

def Fragments.Bantu.instReprConflationPattern.repr : ConflationPattern → ℕ → Std.Format

Equations

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

def Fragments.Bantu.ConflationPattern.classCount : ConflationPattern → ℕ

The number of core noun classes distinguished under a conflation pattern.

Equations

• { usesAnimate := true, usesHuman := true }.classCount = 3
• { usesAnimate := true, usesHuman := false }.classCount = 2
• { usesAnimate := false, usesHuman := true }.classCount = 2
• { usesAnimate := false, usesHuman := false }.classCount = 1

def Fragments.Bantu.ConflationPattern.xhosa : ConflationPattern

Xhosa uses both features: three-way distinction.

Equations

• Fragments.Bantu.ConflationPattern.xhosa = { usesAnimate := true, usesHuman := true }

def Fragments.Bantu.ConflationPattern.swahili : ConflationPattern

Swahili lacks [±Human]: GENERIC ANIMATE (human + animal) vs INANIMATE.

Equations

• Fragments.Bantu.ConflationPattern.swahili = { usesAnimate := true, usesHuman := false }

theorem Fragments.Bantu.xhosa_three_classes : ConflationPattern.xhosa.classCount = 3

theorem Fragments.Bantu.swahili_two_classes : ConflationPattern.swahili.classCount = 2

structure Fragments.Bantu.FeatureConjunction : Type

A feature-definable category: a conjunction of constraints on [±Animate] and/or [±Human]. none means the feature is unconstrained (conflated). This captures exactly the categories that arise from the containment hierarchy (@cite{halpert-hammerly-2026} (4)–(5)).

• animateReq : Option Bool
• humanReq : Option Bool

def Fragments.Bantu.instDecidableEqFeatureConjunction.decEq (x✝ x✝¹ : FeatureConjunction) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqFeatureConjunction : DecidableEq FeatureConjunction

Equations

• Fragments.Bantu.instDecidableEqFeatureConjunction = Fragments.Bantu.instDecidableEqFeatureConjunction.decEq

@[implicit_reducible]

instance Fragments.Bantu.instReprFeatureConjunction : Repr FeatureConjunction

Equations

• Fragments.Bantu.instReprFeatureConjunction = { reprPrec := Fragments.Bantu.instReprFeatureConjunction.repr }

def Fragments.Bantu.instReprFeatureConjunction.repr : FeatureConjunction → ℕ → Std.Format

Equations

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

def Fragments.Bantu.FeatureConjunction.matches (fc : FeatureConjunction) (af : AnimacyFeatures) : Bool

Whether a feature bundle satisfies a conjunction.

Equations

• fc.matches af = ((fc.animateReq.isNone || fc.animateReq == some af.isAnimate) && (fc.humanReq.isNone || fc.humanReq == some af.isHuman))

theorem Fragments.Bantu.impossible_human_inanimate_without_animal : ¬∃ (fc : FeatureConjunction), fc.matches AnimacyFeatures.human = true ∧ fc.matches AnimacyFeatures.inanimate = true ∧ fc.matches AnimacyFeatures.animal = false

Impossible conflation: no feature-definable category (conjunction of [±Animate, ±Human] constraints) can select HUMAN and INANIMATE while excluding ANIMAL. This follows from containment: HUMAN shares [+Animate] with ANIMAL, and INANIMATE shares [−Human] with ANIMAL, so any conjunction selecting both endpoints must also select the middle (@cite{halpert-hammerly-2026} §2, p. 5).

inductive Fragments.Bantu.GenderStatus : Type

Gender interpretability status (@cite{carstens-2026} §4.2).

An interpretable gender has an i[entity] flavor associated with a salient class of countable entities. An uninterpretable gender has no such association — its members are semantically arbitrary.

This distinction directly controls agreement with conjoined singulars: gender-matching plural agreement succeeds with uniform conjuncts only for interpretable genders (@cite{carstens-2026} (52), (54)).

• interpretable : SemanticCore → GenderStatus
• uninterpretable : GenderStatus

def Fragments.Bantu.instDecidableEqGenderStatus.decEq (x✝ x✝¹ : GenderStatus) : Decidable (x✝ = x✝¹)

Equations

• Fragments.Bantu.instDecidableEqGenderStatus.decEq (Fragments.Bantu.GenderStatus.interpretable a) (Fragments.Bantu.GenderStatus.interpretable b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Fragments.Bantu.instDecidableEqGenderStatus.decEq (Fragments.Bantu.GenderStatus.interpretable a) Fragments.Bantu.GenderStatus.uninterpretable = isFalse ⋯
• Fragments.Bantu.instDecidableEqGenderStatus.decEq Fragments.Bantu.GenderStatus.uninterpretable (Fragments.Bantu.GenderStatus.interpretable a) = isFalse ⋯
• Fragments.Bantu.instDecidableEqGenderStatus.decEq Fragments.Bantu.GenderStatus.uninterpretable Fragments.Bantu.GenderStatus.uninterpretable = isTrue ⋯

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqGenderStatus : DecidableEq GenderStatus

Equations

• Fragments.Bantu.instDecidableEqGenderStatus = Fragments.Bantu.instDecidableEqGenderStatus.decEq

@[implicit_reducible]

instance Fragments.Bantu.instReprGenderStatus : Repr GenderStatus

Equations

• Fragments.Bantu.instReprGenderStatus = { reprPrec := Fragments.Bantu.instReprGenderStatus.repr }

def Fragments.Bantu.instReprGenderStatus.repr : GenderStatus → ℕ → Std.Format

Equations

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

def Fragments.Bantu.GenderStatus.isInterpretable : GenderStatus → Bool

Equations

• (Fragments.Bantu.GenderStatus.interpretable a).isInterpretable = true
• Fragments.Bantu.GenderStatus.uninterpretable.isInterpretable = false

def Fragments.Bantu.GenderStatus.core : GenderStatus → Option SemanticCore

Equations

• (Fragments.Bantu.GenderStatus.interpretable a).core = some a
• Fragments.Bantu.GenderStatus.uninterpretable.core = none

structure Fragments.Bantu.NPStack : Type

Stacked nP structure for Bantu nominals (@cite{carstens-2026} §4, (72)–(73)).

Bantu nouns have an inner semantic nP (bearing the i-core gender) wrapped by zero or more outer nPs (determining the visible noun class). For nouns in their canonical class, visible = core; for nouns appearing in non-canonical classes (e.g. [human] nouns in classes 3/4 or 5/6), the outer nP differs from the inner core.

visibleClass is the outer noun class number (determines morphological agreement with non-conjoined DPs). coreClass is the inner class determined by the semantic core (or equal to visibleClass if no stacking).

• visibleClass : ℕ
• coreClass : ℕ
• status : GenderStatus

def Fragments.Bantu.instDecidableEqNPStack.decEq (x✝ x✝¹ : NPStack) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Bantu.instDecidableEqNPStack : DecidableEq NPStack

Equations

• Fragments.Bantu.instDecidableEqNPStack = Fragments.Bantu.instDecidableEqNPStack.decEq

def Fragments.Bantu.instReprNPStack.repr : NPStack → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Bantu.instReprNPStack : Repr NPStack

Equations

• Fragments.Bantu.instReprNPStack = { reprPrec := Fragments.Bantu.instReprNPStack.repr }

def Fragments.Bantu.NPStack.isCanonical (s : NPStack) : Bool

Equations

• s.isCanonical = (s.visibleClass == s.coreClass)

def Fragments.Bantu.NPStack.hasAnimateCore (s : NPStack) : Bool

Whether the core noun class is [+Animate] (HUMAN or ANIMAL). This is the predicate that [+Animate]-relativized probes and object-doubling conditions both target (@cite{halpert-hammerly-2026} (29)).

Equations

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

def Fragments.Bantu.SemanticCore.defaultPluralClass : SemanticCore → ℕ

Default agreement class for a semantic core (@cite{carstens-2026} (52c)). Class 2 ba- for [human], class 8 zi- for [inanimate] and [animal].

Equations

• Fragments.Bantu.SemanticCore.human.defaultPluralClass = 2
• Fragments.Bantu.SemanticCore.animal.defaultPluralClass = 8
• Fragments.Bantu.SemanticCore.inanimate.defaultPluralClass = 8
• Fragments.Bantu.SemanticCore.nonhuman.defaultPluralClass = 8