Bantu Language Family: Shared Parameters

[Car91] [Kra15] [Car26] [HH26] [Ham23]

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 ([Car91], [Kra15])
• A small number of genders have semantic cores — salient associations with entity classes like [human], [animal], [inanimate] ([Car26] §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 [Ham23]'s containment hierarchy ([HH26] (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 Bantu.AnimacyFeatures : Type

Bivalent animacy features from [Ham23]'s containment hierarchy, applied to Bantu core noun class by [HH26].

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

@[implicit_reducible]

instance Bantu.instDecidableEqAnimacyFeatures : DecidableEq AnimacyFeatures

Equations

• Bantu.instDecidableEqAnimacyFeatures = Bantu.instDecidableEqAnimacyFeatures.decEq

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Bantu.instReprAnimacyFeatures : Repr AnimacyFeatures

Equations

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

@[implicit_reducible]

instance Bantu.instFintypeAnimacyFeatures : Fintype AnimacyFeatures

Equations

• Bantu.instFintypeAnimacyFeatures = Fintype.ofEquiv ((_ : Bool) × Bool) Bantu.AnimacyFeatures.proxyTypeEquiv

def Bantu.AnimacyFeatures.featuresEquiv : AnimacyFeatures ≃ Features.ContainmentPair

The [±Animate, ±Human] decomposition is carrier-equivalent to the containment pair: outer = [±Animate], inner = [±Human]. The same mathematical structure as person features (outer = [±participant], inner = [±author]), confirming [Ham23]'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.

@[implicit_reducible]

instance Bantu.AnimacyFeatures.instContainmentPairLike : Features.ContainmentPairLike AnimacyFeatures

Equations

• Bantu.AnimacyFeatures.instContainmentPairLike = Features.ContainmentPairLike.ofEquiv Bantu.AnimacyFeatures.featuresEquiv

@[reducible, inline]

abbrev Bantu.AnimacyFeatures.WellFormed (af : AnimacyFeatures) : Prop

Well-formedness: [+Human] → [+Animate]. Being human entails being animate ([HH26] fn. 10).

Equations

• af.WellFormed = Features.ContainmentPairLike.WellFormed af

def Bantu.AnimacyFeatures.human : AnimacyFeatures

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

Equations

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

def Bantu.AnimacyFeatures.animal : AnimacyFeatures

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

Equations

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

def Bantu.AnimacyFeatures.inanimate : AnimacyFeatures

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

Equations

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

theorem Bantu.AnimacyFeatures.illFormed_only : ¬{ isAnimate := false, isHuman := true }.WellFormed

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

theorem Bantu.AnimacyFeatures.exactly_three : Fintype.card { af : AnimacyFeatures // af.WellFormed } = 3

Exactly three well-formed core noun classes — the carrier count of the containment chain (ContainmentPair.card_wellFormed); any ContainmentPairLike type supports at most 3 well-formed cells.

def 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 Bantu.AnimacyFeatures.human_level : human.toAnimacyLevel = Features.Prominence.AnimacyLevel.human

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

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

inductive Bantu.FinalVowel : Type

Bantu nominalizing final vowels encode core noun class on the categorizing head n ([HH26] (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 Bantu.instDecidableEqFinalVowel : DecidableEq FinalVowel

Equations

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

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

Equations

• Bantu.instReprFinalVowel.repr Bantu.FinalVowel.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.FinalVowel.i")).group prec✝
• Bantu.instReprFinalVowel.repr Bantu.FinalVowel.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.FinalVowel.o")).group prec✝
• Bantu.instReprFinalVowel.repr Bantu.FinalVowel.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.FinalVowel.a")).group prec✝

@[implicit_reducible]

instance Bantu.instReprFinalVowel : Repr FinalVowel

Equations

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

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

Core noun class features determine the nominalizing final vowel ([HH26] (22)).

Equations

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

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

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

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

inductive Bantu.SemanticCore : Type

Semantic cores of Bantu gender: salient associations between genders and entity classes ([Car26] §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 Bantu.instDecidableEqSemanticCore : DecidableEq SemanticCore

Equations

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

@[implicit_reducible]

instance Bantu.instReprSemanticCore : Repr SemanticCore

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Bantu.instReprSemanticCore.repr Bantu.SemanticCore.human prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.SemanticCore.human")).group prec✝
• Bantu.instReprSemanticCore.repr Bantu.SemanticCore.animal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Bantu.SemanticCore.animal")).group prec✝

def Bantu.AnimacyFeatures.toCoreClass : AnimacyFeatures → SemanticCore

Derive SemanticCore from bivalent features ([HH26] (19)).

Equations

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

def Bantu.SemanticCore.toFeatures : SemanticCore → AnimacyFeatures

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

Equations

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

theorem Bantu.AnimacyFeatures.roundtrip (af : AnimacyFeatures) : af.WellFormed → af.toCoreClass.toFeatures = af

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

structure Bantu.ConflationPattern : Type

A language's conflation pattern: which containment features it is sensitive to. Dropping a feature merges the categories it distinguishes ([HH26] (5), following [McG05]).

• usesAnimate : Bool
• usesHuman : Bool

@[implicit_reducible]

instance Bantu.instDecidableEqConflationPattern : DecidableEq ConflationPattern

Equations

• Bantu.instDecidableEqConflationPattern = Bantu.instDecidableEqConflationPattern.decEq

def 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 Bantu.instReprConflationPattern : Repr ConflationPattern

Equations

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

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

Equations

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

def 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 Bantu.ConflationPattern.xhosa : ConflationPattern

Xhosa uses both features: three-way distinction.

Equations

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

def Bantu.ConflationPattern.swahili : ConflationPattern

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

Equations

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

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

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

structure 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 ([HH26] (4)–(5)).

• animateReq : Option Bool
• humanReq : Option Bool

@[implicit_reducible]

instance Bantu.instDecidableEqFeatureConjunction : DecidableEq FeatureConjunction

Equations

• Bantu.instDecidableEqFeatureConjunction = Bantu.instDecidableEqFeatureConjunction.decEq

def 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 Bantu.instReprFeatureConjunction : Repr FeatureConjunction

Equations

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

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

Equations

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

def 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 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 ([HH26] §2, p. 5).

inductive Bantu.GenderStatus : Type

Gender interpretability status ([Car26] §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 ([Car26] (52), (54)).

• interpretable : SemanticCore → GenderStatus
• uninterpretable : GenderStatus

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

Equations

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

@[implicit_reducible]

instance Bantu.instDecidableEqGenderStatus : DecidableEq GenderStatus

Equations

• Bantu.instDecidableEqGenderStatus = Bantu.instDecidableEqGenderStatus.decEq

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

Equations

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

@[implicit_reducible]

instance Bantu.instReprGenderStatus : Repr GenderStatus

Equations

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

def Bantu.GenderStatus.isInterpretable : GenderStatus → Bool

Equations

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

def Bantu.GenderStatus.core : GenderStatus → Option SemanticCore

Equations

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

structure Bantu.NPStack : Type

Stacked nP structure for Bantu nominals ([Car26] §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 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 Bantu.instDecidableEqNPStack : DecidableEq NPStack

Equations

• Bantu.instDecidableEqNPStack = Bantu.instDecidableEqNPStack.decEq

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

Equations

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

@[implicit_reducible]

instance Bantu.instReprNPStack : Repr NPStack

Equations

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

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

Equations

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

def 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 ([HH26] (29)).

Equations

• s.hasAnimateCore = match s.status with | Bantu.GenderStatus.interpretable Bantu.SemanticCore.human => true | Bantu.GenderStatus.interpretable Bantu.SemanticCore.animal => true | x => false

def Bantu.SemanticCore.defaultPluralClass : SemanticCore → ℕ

Default agreement class for a semantic core ([Car26] (52c)). Class 2 ba- for [human], class 8 zi- for [inanimate] and [animal].

Equations

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