Carstens 2026: The Grammar of Gender

@cite{carstens-2026}

Carstens, Vicki. 2026. "The grammar of gender: Insights from Bantu asymmetries of AGR with conjoined subjects." Natural Language & Linguistic Theory 44:20.

Core claims

1. nP stacking: Bantu nominals have stacked nP structure where visible gender (class prefix) wraps around a semantic i-gender core. The internal structure is [nP₁ n1 [nP₂ n2+root]]; n2 is always the bearer of the semantic gender.

2. Three semantic cores in Xhosa: genders A (1/2), D (7/8), E (9/10) have interpretable i[entity] flavors — [human], [inanimate], [animal] respectively. Genders B (3/4) and C (5/6) are uninterpretable.

3. Resolution via percolation + intersection: Following @cite{adamson-anagnostopoulou-2025}, agreement with conjoined singulars works by percolating conjuncts' i-features to &P and intersecting them. u-features are excluded. Non-empty intersection → gender-matching plural agreement; empty intersection → default agreement.

4. Diagnostic: Gender-matching plural agreement with uniform conjoined singulars succeeds iff the gender is interpretable (has i[entity] flavor).

5. Shona confirmation: In Shona (8 genders), only 2 are interpretable ([human] 1/2 and [non-human] 7/8). The 6:2 ratio of uninterpretable to interpretable confirms that matching agreement is the exception, not the rule.

Formalization

Resolution uses GenderResolution.resolve — the single compositional endpoint — via statusToBundle which bridges Bantu GenderStatus to FeatureBundle SemanticCore. Study-level theorems verify the mechanism's predictions against @cite{carstens-2026}'s empirical data.

def Carstens2026.nP (c : Fragments.Bantu.SemanticCore) : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

A single interpretable nP layer bearing SemanticCore c.

Equations

• Carstens2026.nP c = [{ value := c, interp := Minimalist.Interpretability.interpretable }]

def Carstens2026.nP_u : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

An uninterpretable nP layer (no features to percolate).

Equations

• Carstens2026.nP_u = []

def Carstens2026.nPStack (outer inner : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore) : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Stack an outer gender layer on an inner core (outer ++ inner).

Equations

• Carstens2026.nPStack outer inner = outer ++ inner

def Carstens2026.statusToBundle (s : Fragments.Bantu.GenderStatus) : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Convert GenderStatus to a feature bundle for resolve. Interpretable genders produce a singleton i-feature bundle; uninterpretable genders produce an empty bundle.

Equations

• Carstens2026.statusToBundle (Fragments.Bantu.GenderStatus.interpretable c) = Carstens2026.nP c
• Carstens2026.statusToBundle Fragments.Bantu.GenderStatus.uninterpretable = Carstens2026.nP_u

theorem Carstens2026.interpretable_self_nonempty (c : Fragments.Bantu.SemanticCore) : Minimalist.Agreement.GenderResolution.resolve (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c)) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c)) = some [c]

Interpretable genders yield non-empty intersection with themselves.

theorem Carstens2026.uninterpretable_self_empty : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Bantu.GenderStatus.uninterpretable) (statusToBundle Fragments.Bantu.GenderStatus.uninterpretable) = none

Uninterpretable genders yield empty intersection with themselves.

theorem Carstens2026.uninterpretable_interpretable_empty (c : Fragments.Bantu.SemanticCore) : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Bantu.GenderStatus.uninterpretable) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c)) = none

Uninterpretable + interpretable yields empty intersection.

theorem Carstens2026.mismatched_cores_empty (c1 c2 : Fragments.Bantu.SemanticCore) (h : c1 ≠ c2) : Minimalist.Agreement.GenderResolution.resolve (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c1)) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c2)) = none

Mismatched interpretable cores yield empty intersection.

theorem Carstens2026.bantu_matching_iff_interpretable (s : Fragments.Bantu.GenderStatus) : (Minimalist.Agreement.GenderResolution.resolve (statusToBundle s) (statusToBundle s)).isSome = s.isInterpretable

The central claim (@cite{carstens-2026}): for ANY Bantu gender, matching agreement with uniform conjoined singulars succeeds iff the gender is interpretable. This holds at the parameter type level, not just for specific Xhosa/Shona inventories.

The language-specific xhosa_matching_iff_interpretable and shona_matching_iff_interpretable are corollaries of this theorem.

Matching agreement available (interpretable genders)

theorem Carstens2026.xhosa_1and1_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Xhosa.Gender.genderA.status) (statusToBundle Fragments.Xhosa.Gender.genderA.status) = some [Fragments.Bantu.SemanticCore.human]

[1&1] human conjuncts: intersection = [human] → matching cl 2 available. @cite{carstens-2026} Table 13: 100% ba- (matching = default for [human]).

theorem Carstens2026.xhosa_7and7_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Xhosa.Gender.genderD.status) (statusToBundle Fragments.Xhosa.Gender.genderD.status) = some [Fragments.Bantu.SemanticCore.inanimate]

[7&7] inanimate conjuncts: intersection = [inanimate] → matching cl 8. @cite{carstens-2026} Table 13: 100% zi- for non-human [7&7].

theorem Carstens2026.xhosa_9and9_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Xhosa.Gender.genderE.status) (statusToBundle Fragments.Xhosa.Gender.genderE.status) = some [Fragments.Bantu.SemanticCore.animal]

[9&9] animal conjuncts: intersection = [animal] → matching cl 10. @cite{carstens-2026} Table 13: 50% zi- matching + 40% ba- default for human [9&9]; 100% zi- for non-human [9&9].

Matching agreement unavailable (uninterpretable genders)

theorem Carstens2026.xhosa_3and3_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Xhosa.Gender.genderB.status) (statusToBundle Fragments.Xhosa.Gender.genderB.status) = none

[3&3] conjuncts: intersection = ∅ → default agreement only. @cite{carstens-2026} Table 13: 0% matching for human (100% ba-); 2.2% matching for non-human (73.3% zi- default).

theorem Carstens2026.xhosa_5and5_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Xhosa.Gender.genderC.status) (statusToBundle Fragments.Xhosa.Gender.genderC.status) = none

[5&5] conjuncts: intersection = ∅ → default agreement only. @cite{carstens-2026} Table 13: 0% matching; 63.33% ba- for human, 73.33% zi- for non-human.

The core prediction: matching ↔ interpretability

theorem Carstens2026.xhosa_matching_iff_interpretable (g : Fragments.Xhosa.Gender) : (Minimalist.Agreement.GenderResolution.resolve (statusToBundle g.status) (statusToBundle g.status)).isSome = g.status.isInterpretable

Every Xhosa gender: matching agreement is available iff interpretable.

theorem Carstens2026.xhosa_mismatched_human : Minimalist.Agreement.GenderResolution.resolve (statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)) = some [Fragments.Bantu.SemanticCore.human]

Mismatched [human] conjuncts (e.g. [3&5] gangster + policeman): both have [human] core from stacking → intersection = [human]. @cite{carstens-2026} (85)a, (86)a: class 2 ba- agreement.

theorem Carstens2026.xhosa_mismatched_inanimate : Minimalist.Agreement.GenderResolution.resolve (statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate)) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate)) = some [Fragments.Bantu.SemanticCore.inanimate]

Mismatched [inanimate] conjuncts (e.g. [3&5] carrot + egg): both have [inanimate] core from stacking → intersection = [inanimate]. @cite{carstens-2026} (85)b, (86)b: class 8 zi- agreement.

theorem Carstens2026.xhosa_human_inanimate_ineffable : Minimalist.Agreement.GenderResolution.resolve (statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate)) = none

Human + inanimate (e.g. [9&1a] girl + train): [human] ∩ [inanimate] = ∅ → ineffable. @cite{carstens-2026} (91)–(92): agreement with conjoined humans and inanimates is generally ineffable.

theorem Carstens2026.default_human_is_class2 : Fragments.Bantu.SemanticCore.human.defaultPluralClass = 2

Default for [human]: class 2 ba- (@cite{carstens-2026} (52c)).

theorem Carstens2026.default_inanimate_is_class8 : Fragments.Bantu.SemanticCore.inanimate.defaultPluralClass = 8

Default for [inanimate]: class 8 zi- (@cite{carstens-2026} (52c)).

theorem Carstens2026.default_animal_is_class8 : Fragments.Bantu.SemanticCore.animal.defaultPluralClass = 8

Default for [animal]: class 8 zi- (class 10 = syncretic with 8 for default purposes; @cite{carstens-2026} §3.4).

theorem Carstens2026.shona_1and1_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderA.status) (statusToBundle Fragments.Shona.Gender.genderA.status) = some [Fragments.Bantu.SemanticCore.human]

Shona [1&1]: class 2 va- (human matching/default). @cite{carstens-2026} (58): va- for conjoined [1&1] (consistent across speakers).

theorem Carstens2026.shona_7and7_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderD.status) (statusToBundle Fragments.Shona.Gender.genderD.status) = some [Fragments.Bantu.SemanticCore.nonhuman]

Shona [7&7]: class 8 zvi- (non-human matching/default). @cite{carstens-2026} (62): zvi- for non-human [7&7] (consistent across speakers).

theorem Carstens2026.shona_3and3_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderB.status) (statusToBundle Fragments.Shona.Gender.genderB.status) = none

Shona [3&3]: no matching → default only. @cite{carstens-2026} (59): zvi- (class 8 default) for non-human.

theorem Carstens2026.shona_5and5_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderC.status) (statusToBundle Fragments.Shona.Gender.genderC.status) = none

Shona [5&5]: no matching → default only. @cite{carstens-2026} (60)–(61).

theorem Carstens2026.shona_9and9_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderE.status) (statusToBundle Fragments.Shona.Gender.genderE.status) = none

Shona [9&9]: no matching → default only. Unlike Xhosa [9&9], Shona's [animal] core has bleached from 9/10. @cite{carstens-2026} §5.2, (64)b–d: va- for human, zvi- for non-human.

theorem Carstens2026.shona_11and11_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderF.status) (statusToBundle Fragments.Shona.Gender.genderF.status) = none

Shona [11&11]: no matching → default only. @cite{carstens-2026} (65): zvi- (class 8 default).

theorem Carstens2026.shona_14and14_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderG.status) (statusToBundle Fragments.Shona.Gender.genderG.status) = none

Shona [14&14]: no matching → default only (abstract nouns). @cite{carstens-2026}: genderG (14/6) is uninterpretable.

theorem Carstens2026.shona_12and12_no_matching : Minimalist.Agreement.GenderResolution.resolve (statusToBundle Fragments.Shona.Gender.genderH.status) (statusToBundle Fragments.Shona.Gender.genderH.status) = none

Shona [12&12]: no matching → default only (diminutives). @cite{carstens-2026}: conjoined diminutives take class 8 zvi-.

theorem Carstens2026.shona_matching_iff_interpretable (g : Fragments.Shona.Gender) : (Minimalist.Agreement.GenderResolution.resolve (statusToBundle g.status) (statusToBundle g.status)).isSome = g.status.isInterpretable

Every Shona gender: matching ↔ interpretable.

theorem Carstens2026.xhosa_interpretable_count : (List.filter (fun (g : Fragments.Xhosa.Gender) => g.status.isInterpretable) [Fragments.Xhosa.Gender.genderA, Fragments.Xhosa.Gender.genderB, Fragments.Xhosa.Gender.genderC, Fragments.Xhosa.Gender.genderD, Fragments.Xhosa.Gender.genderE]).length = 3

Xhosa has 3 interpretable genders out of 5 (60%).

theorem Carstens2026.shona_interpretable_count : (List.filter (fun (g : Fragments.Shona.Gender) => g.status.isInterpretable) [Fragments.Shona.Gender.genderA, Fragments.Shona.Gender.genderB, Fragments.Shona.Gender.genderC, Fragments.Shona.Gender.genderD, Fragments.Shona.Gender.genderE, Fragments.Shona.Gender.genderF, Fragments.Shona.Gender.genderG, Fragments.Shona.Gender.genderH]).length = 2

Shona has 2 interpretable genders out of 8 (25%).

theorem Carstens2026.shona_matching_is_minority : (List.filter (fun (g : Fragments.Shona.Gender) => !(Minimalist.Agreement.GenderResolution.resolve (statusToBundle g.status) (statusToBundle g.status)).isSome) [Fragments.Shona.Gender.genderA, Fragments.Shona.Gender.genderB, Fragments.Shona.Gender.genderC, Fragments.Shona.Gender.genderD, Fragments.Shona.Gender.genderE, Fragments.Shona.Gender.genderF, Fragments.Shona.Gender.genderG, Fragments.Shona.Gender.genderH]).length = 6

Core insight (@cite{carstens-2026} §3.5, §5.2): in Shona, genders in which matching agreement succeeds are outnumbered by those where it fails by 6:2, confirming that matching is the exception.

theorem Carstens2026.human_canonical_no_stacking : Fragments.Xhosa.humanCanonical.isCanonical = true

Canonical [human] nouns: visible = core (no stacking).

theorem Carstens2026.human_class3_stacked : Fragments.Xhosa.humanInClass3.isCanonical = false

[Human] nouns in class 3: stacked (visible ≠ core).

theorem Carstens2026.human_class5_stacked : Fragments.Xhosa.humanInClass5.isCanonical = false

[Human] nouns in class 5: stacked (visible ≠ core).

theorem Carstens2026.stacking_preserves_core : Fragments.Xhosa.humanInClass3.status = Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human ∧ Fragments.Xhosa.humanInClass5.status = Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human ∧ Fragments.Xhosa.animalInClass1.status = Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.animal

Stacked nouns retain the core gender despite different visible class.

def Carstens2026.toDMInterpretability : Fragments.Bantu.GenderStatus → Morphology.DM.Interpretability

Bantu SemanticCore → DM Interpretability bridge. Interpretable genders bear Interpretability.i (natural gender); uninterpretable genders bear Interpretability.u (arbitrary gender). @cite{carstens-2026} directly extends @cite{kramer-2015}'s i/u distinction.

Equations

• Carstens2026.toDMInterpretability (Fragments.Bantu.GenderStatus.interpretable c) = Morphology.DM.Interpretability.i
• Carstens2026.toDMInterpretability Fragments.Bantu.GenderStatus.uninterpretable = Morphology.DM.Interpretability.u

theorem Carstens2026.dm_bridge_faithful (s : Fragments.Bantu.GenderStatus) : (toDMInterpretability s == Morphology.DM.Interpretability.i) = s.isInterpretable

The bridge preserves the interpretability predicate.

def Carstens2026.toSemanticBasis : Fragments.Bantu.SemanticCore → Typology.Gender.SemanticBasis

Bantu SemanticCore → typological SemanticBasis bridge. @cite{carstens-2026}'s cores map to @cite{kramer-2020}'s core semantic bases. All are isCore = true.

The [non-human] core (Shona 7/8) maps to .humanness because Shona's system is organized around the human/non-human distinction. Xhosa's finer [animal] and [inanimate] cores map to .animacy.

Equations

• Carstens2026.toSemanticBasis Fragments.Bantu.SemanticCore.human = Typology.Gender.SemanticBasis.humanness
• Carstens2026.toSemanticBasis Fragments.Bantu.SemanticCore.animal = Typology.Gender.SemanticBasis.animacy
• Carstens2026.toSemanticBasis Fragments.Bantu.SemanticCore.inanimate = Typology.Gender.SemanticBasis.animacy
• Carstens2026.toSemanticBasis Fragments.Bantu.SemanticCore.nonhuman = Typology.Gender.SemanticBasis.humanness

theorem Carstens2026.bantu_cores_are_kramer_cores (c : Fragments.Bantu.SemanticCore) : (toSemanticBasis c).isCore = true

All Bantu semantic cores map to Kramer's semantic core bases.

@[reducible, inline]

abbrev Carstens2026.xhosaGenderProfile : Typology.Gender.GenderProfile

Xhosa gender profile drawn from Fragments/Xhosa/Gender.lean. @cite{carstens-2026} §2.2: semantic cores for some genders, formal (class prefix) assignment for others.

Equations

• Carstens2026.xhosaGenderProfile = Fragments.Xhosa.Gender.genderTypology

@[reducible, inline]

abbrev Carstens2026.shonaGenderProfile : Typology.Gender.GenderProfile

Shona gender profile drawn from Fragments/Shona/Gender.lean.

Equations

• Carstens2026.shonaGenderProfile = Fragments.Shona.Gender.genderTypology

theorem Carstens2026.xhosa_satisfies_semantic_core : xhosaGenderProfile.satisfiesSemanticCore = true

Both profiles satisfy the Semantic Core Generalization (@cite{kramer-2020} ex. 2/28).

theorem Carstens2026.shona_satisfies_semantic_core : shonaGenderProfile.satisfiesSemanticCore = true

def Carstens2026.resolveStacks (s1 s2 : Fragments.Bantu.NPStack) : Option (List Fragments.Bantu.SemanticCore)

Resolution with nP stacking: agreement is determined by the stack's semantic core, not the visible class. Two nouns in different visible classes but the same core gender resolve to that core. @cite{carstens-2026} (85)–(88): mismatched [3&5] humans → ba-, mismatched [3&5] inanimates → zi-.

Equations

• Carstens2026.resolveStacks s1 s2 = Minimalist.Agreement.GenderResolution.resolve (Carstens2026.statusToBundle s1.status) (Carstens2026.statusToBundle s2.status)

theorem Carstens2026.mismatched_3and5_human : resolveStacks { visibleClass := 3, coreClass := 1, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human } { visibleClass := 5, coreClass := 1, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human } = some [Fragments.Bantu.SemanticCore.human]

Criminal (cl3) + policeman (cl5): both [human] core → class 2 ba-. @cite{carstens-2026} (85)a, (86)a.

theorem Carstens2026.mismatched_3and5_inanimate : resolveStacks { visibleClass := 3, coreClass := 7, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate } { visibleClass := 5, coreClass := 7, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate } = some [Fragments.Bantu.SemanticCore.inanimate]

Carrot (cl3) + egg (cl5): both [inanimate] core → class 8 zi-. @cite{carstens-2026} (85)b, (86)b.

theorem Carstens2026.mismatched_7and9_both_human : resolveStacks { visibleClass := 7, coreClass := 1, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human } { visibleClass := 9, coreClass := 1, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human } = some [Fragments.Bantu.SemanticCore.human]

Medium (cl7, human) + girl (cl9, human): both have [human] core from nP stacking → [human] ∩ [human] = {[human]} → class 2 ba-. Visible genders differ (7 vs 9) but cores agree. @cite{carstens-2026} (87)a, (88)a.

theorem Carstens2026.mismatched_1aand9_both_inanimate : resolveStacks { visibleClass := 1, coreClass := 7, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate } { visibleClass := 9, coreClass := 7, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate } = some [Fragments.Bantu.SemanticCore.inanimate]

Backpack (cl1a, inanimate) + book (cl9, inanimate): both have [inanimate] core → [inanimate] ∩ [inanimate] = {[inanimate]} → class 8 zi-. @cite{carstens-2026} (87)b, (88)b.

theorem Carstens2026.swahili_genderA_interpretable : Fragments.Swahili.Gender.genderA.status.isInterpretable = true

Swahili's 5 genders also instantiate the Bantu semantic core system. @cite{carstens-2026} §8 discusses Swahili's GAC (General Animate Concords) as evidence for a [+animate] feature.

theorem Carstens2026.swahili_genderE_interpretable : Fragments.Swahili.Gender.genderE.status.isInterpretable = true

theorem Carstens2026.three_languages_agree_on_human : Fragments.Xhosa.Gender.genderA.status = Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human ∧ Fragments.Shona.Gender.genderA.status = Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human ∧ Fragments.Swahili.Gender.genderA.status = Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human

Three Bantu languages, shared diagnostic: A (1/2) = [human] in all.

The "deepest derivation" from the paper connects nP stacking to agreement outcome through the full chain:

1. **nP stacking**: assign feature bundles from layered nP structure
2. **Percolation**: exclude u-features
3. **Intersection**: find shared i-features
4. **Agreement**: matching (non-empty) or default (empty)

Each theorem below traces this chain for a concrete example from
@cite{carstens-2026} §5. 

def Carstens2026.citizenBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: citizen (class 1, canonical human — no stacking). Structure: [n₁/₂ √CITIZEN]. @cite{carstens-2026} (6)a, (72)a.

Equations

• Carstens2026.citizenBundle = Carstens2026.nP Fragments.Bantu.SemanticCore.human

def Carstens2026.gangsterBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: gangster (class 3, human core via stacking). Structure: [n₃/₄ [n₁/₂ √GULUKUDU]]. Outer n₃/₄ is u → excluded. Inner n₁/₂ is i[human] → percolates. @cite{carstens-2026} (28)d, (85)a, (86)a; structure type per (72)b.

Equations

• Carstens2026.gangsterBundle = Carstens2026.nPStack Carstens2026.nP_u (Carstens2026.nP Fragments.Bantu.SemanticCore.human)

def Carstens2026.policemanBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: policeman (class 5, human core via stacking). Structure: [n₅/₆ [n₁/₂ √POLISA]]. @cite{carstens-2026} (85)a; structure type per (72)c.

Equations

• Carstens2026.policemanBundle = Carstens2026.nPStack Carstens2026.nP_u (Carstens2026.nP Fragments.Bantu.SemanticCore.human)

def Carstens2026.hatBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: hat (class 3, no stacking — arbitrary inanimate in u-gender). Structure: [n₃/₄ √HAT]. No inner layer. @cite{carstens-2026} (38)a, (77)a.

Equations

• Carstens2026.hatBundle = Carstens2026.nP_u

def Carstens2026.carrotBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: carrot (class 3, inanimate core via stacking). Structure: [n₃/₄ [n₇/₈ √CARROT]]. @cite{carstens-2026} (86)b.

Equations

• Carstens2026.carrotBundle = Carstens2026.nPStack Carstens2026.nP_u (Carstens2026.nP Fragments.Bantu.SemanticCore.inanimate)

def Carstens2026.eggBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: egg (class 5, inanimate core via stacking). Structure: [n₅/₆ [n₇/₈ √EGG]]. @cite{carstens-2026} (86)b.

Equations

• Carstens2026.eggBundle = Carstens2026.nPStack Carstens2026.nP_u (Carstens2026.nP Fragments.Bantu.SemanticCore.inanimate)

def Carstens2026.elephantBundle : Minimalist.Agreement.GenderResolution.FeatureBundle Fragments.Bantu.SemanticCore

Feature bundle: elephant (class 9, canonical animal — no stacking). Structure: [n₉/₁₀ √ELEPHANT]. @cite{carstens-2026} (49)b, (73)a.

Equations

• Carstens2026.elephantBundle = Carstens2026.nP Fragments.Bantu.SemanticCore.animal

theorem Carstens2026.derivation_1and1_human : Minimalist.Agreement.GenderResolution.resolve citizenBundle citizenBundle = some [Fragments.Bantu.SemanticCore.human]

End-to-end derivation: citizen.1 & president.1 → matching [human]. @cite{carstens-2026} (6)a: class 2 ba- agreement.

Chain: canonical class 1 → i[human] percolates → {human} ∩ {human} = {human} → matching → class 2 ba-.

theorem Carstens2026.derivation_3and5_human : Minimalist.Agreement.GenderResolution.resolve gangsterBundle policemanBundle = some [Fragments.Bantu.SemanticCore.human]

End-to-end derivation: gangster.3 & policeman.5 → matching [human]. @cite{carstens-2026} (86)a: class 2 ba- agreement.

Chain: nP stacking gives u-outer + i[human]-inner → u excluded, {human} percolates from each → {human} ∩ {human} = {human} → matching → class 2 ba-.

theorem Carstens2026.derivation_3and5_inanimate : Minimalist.Agreement.GenderResolution.resolve carrotBundle eggBundle = some [Fragments.Bantu.SemanticCore.inanimate]

End-to-end derivation: carrot.3 & egg.5 → matching [inanimate]. @cite{carstens-2026} (86)b: class 8 zi- agreement.

Chain: u-outer + i[inanimate]-inner → {inanimate} ∩ {inanimate} = {inanimate} → matching → class 8 zi-.

theorem Carstens2026.derivation_3and3_default : Minimalist.Agreement.GenderResolution.resolve hatBundle hatBundle = none

End-to-end derivation: hat.3 & gun.3 → default. @cite{carstens-2026} (77)a, (38)a: class 8 zi- (default for non-human).

Chain: u-gender, no stacking → no i-features to percolate → {} ∩ {} = {} → default → class 8 zi-.

theorem Carstens2026.derivation_9and9_animal : Minimalist.Agreement.GenderResolution.resolve elephantBundle elephantBundle = some [Fragments.Bantu.SemanticCore.animal]

End-to-end derivation: elephant.9 & leopard.9 → matching [animal]. @cite{carstens-2026} (49)b, (82)a: class 10 zi- agreement.

Chain: canonical class 9 → i[animal] percolates → {animal} ∩ {animal} = {animal} → matching → class 10 zi-.

theorem Carstens2026.derivation_human_inanimate_default : Minimalist.Agreement.GenderResolution.resolve citizenBundle (nP Fragments.Bantu.SemanticCore.inanimate) = none

End-to-end derivation: human + inanimate → default (generally ineffable). @cite{carstens-2026} (91)–(92): *girl.9 & train.1a → no agreement.

Chain: i[human] vs i[inanimate] → {human} ∩ {inanimate} = {} → default. But no default class satisfies both cores → ineffable.

@cite{carstens-2026} §5.1, (78)–(81): when arbitrary members of interpretable genders stack in non-canonical classes, both the outer (arbitrary) and inner (core) i-features percolate to &P. The intersection then contains multiple features, and two grammars determine which one selects the agreement class.

We use a structured feature type that carries both the class number
(determining agreement morphology) and a core/arbitrary flag
(determining BSM specificity). 

structure Carstens2026.TwoGrammarFeature : Type

Feature with core/arbitrary distinction for the two-grammars analysis. @cite{carstens-2026} (71): n₁ = i[entity] i[core]; n₂ = i[entity] (for arbitrary members). Core features are more specific.

• classNum : ℕ
• isCore : Bool

@[implicit_reducible]

instance Carstens2026.instDecidableEqTwoGrammarFeature : DecidableEq TwoGrammarFeature

Equations

• Carstens2026.instDecidableEqTwoGrammarFeature = Carstens2026.instDecidableEqTwoGrammarFeature.decEq

def Carstens2026.instDecidableEqTwoGrammarFeature.decEq (x✝ x✝¹ : TwoGrammarFeature) : Decidable (x✝ = x✝¹)

Equations

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

def Carstens2026.instReprTwoGrammarFeature.repr : TwoGrammarFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Carstens2026.instReprTwoGrammarFeature : Repr TwoGrammarFeature

Equations

• Carstens2026.instReprTwoGrammarFeature = { reprPrec := Carstens2026.instReprTwoGrammarFeature.repr }

def Carstens2026.TwoGrammarFeature.specificity (f : TwoGrammarFeature) : ℕ

BSM specificity: core flavors outrank arbitrary i[entity].

Equations

• f.specificity = if f.isCore = true then 2 else 1

def Carstens2026.trainFeatures : Minimalist.Agreement.GenderResolution.FeatureBundle TwoGrammarFeature

Feature bundle for train.1a: [n₁ₐ(arbitrary) [n₇(core inanimate) √TRAIN]]. Outer: class 1, arbitrary i[entity] from gender A. Inner: class 7, core i[inanimate] from gender D. @cite{carstens-2026} (78)a, (79)a, (80)a.

Equations

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

def Carstens2026.divinerFeatures : Minimalist.Agreement.GenderResolution.FeatureBundle TwoGrammarFeature

Feature bundle for diviner.7: [n₇(arbitrary) [n₁(core human) √DIVINER]]. Outer: class 7, arbitrary i[entity] from gender D. Inner: class 1, core i[human] from gender A. @cite{carstens-2026} (78)b, (79)b, (80)b.

Equations

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

theorem Carstens2026.train_intersection : Minimalist.Agreement.GenderResolution.resolve trainFeatures trainFeatures = some [{ classNum := 1, isCore := false }, { classNum := 7, isCore := true }]

Intersection for train.1a & machine.1a: both layers survive. @cite{carstens-2026} (79)a: &P {1, {7}} ∩ {1, {7}} = {1, {7}}.

theorem Carstens2026.diviner_intersection : Minimalist.Agreement.GenderResolution.resolve divinerFeatures divinerFeatures = some [{ classNum := 7, isCore := false }, { classNum := 1, isCore := true }]

Intersection for diviner.7 & scholar.7: both layers survive. @cite{carstens-2026} (79)b: &P {7, {1}} ∩ {7, {1}} = {7, {1}}.

theorem Carstens2026.train_highest_wins : Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.highestWins TwoGrammarFeature.specificity [{ classNum := 1, isCore := false }, { classNum := 7, isCore := true }] = some { classNum := 1, isCore := false }

Highest Wins for train.1a & machine.1a: outermost = class 1 → cl 2 ba-. @cite{carstens-2026} (79)a.

theorem Carstens2026.train_best_semantic_match : Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.bestSemanticMatch TwoGrammarFeature.specificity [{ classNum := 1, isCore := false }, { classNum := 7, isCore := true }] = some { classNum := 7, isCore := true }

BSM for train.1a & machine.1a: core class 7 (inanimate) → cl 8 zi-. @cite{carstens-2026} (80)a.

theorem Carstens2026.diviner_highest_wins : Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.highestWins TwoGrammarFeature.specificity [{ classNum := 7, isCore := false }, { classNum := 1, isCore := true }] = some { classNum := 7, isCore := false }

Highest Wins for diviner.7 & scholar.7: outermost = class 7 → cl 8 zi-. @cite{carstens-2026} (79)b.

theorem Carstens2026.diviner_best_semantic_match : Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.bestSemanticMatch TwoGrammarFeature.specificity [{ classNum := 7, isCore := false }, { classNum := 1, isCore := true }] = some { classNum := 1, isCore := true }

BSM for diviner.7 & scholar.7: core class 1 (human) → cl 2 ba-. @cite{carstens-2026} (80)b: 'The fool and the scholar are studying' with ba- agreement.

theorem Carstens2026.two_grammars_differ_train : Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.highestWins TwoGrammarFeature.specificity [{ classNum := 1, isCore := false }, { classNum := 7, isCore := true }] ≠ Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.bestSemanticMatch TwoGrammarFeature.specificity [{ classNum := 1, isCore := false }, { classNum := 7, isCore := true }]

The two grammars give DIFFERENT predictions for stacked nPs: for train.1a & machine.1a, HW picks class 1 (ba-) while BSM picks class 7 (zi-). Both are attested by Xhosa speakers. @cite{carstens-2026} (81)a: zi- for [L & M] = BSM; (45)a: ba- for [L & M] = HW.

theorem Carstens2026.two_grammars_differ_diviner : Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.highestWins TwoGrammarFeature.specificity [{ classNum := 7, isCore := false }, { classNum := 1, isCore := true }] ≠ Minimalist.Agreement.GenderResolution.selectFeature Minimalist.Agreement.GenderResolution.SelectionGrammar.bestSemanticMatch TwoGrammarFeature.specificity [{ classNum := 7, isCore := false }, { classNum := 1, isCore := true }]

And they also differ for diviner.7 & scholar.7: HW → class 7 (zi-), BSM → class 1 (ba-).

Bantu–CoordinateResolution bridge

The unified `CoordinateResolution` framework resolves all three
phi-dimensions (person, number, gender) independently. Here we
show that the gender dimension, instantiated with `SemanticCore`
via `statusToBundle`, gives the expected outcomes for conjoined
Bantu singular DPs. 

def Carstens2026.bantuDP (s : Fragments.Bantu.GenderStatus) : Minimalist.Agreement.CoordinateResolution.PhiBundle Fragments.Bantu.SemanticCore

A Bantu singular DP's phi-bundle: 3rd person (all full DPs are 3rd), singular number, gender from the noun's gender status.

Equations

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

theorem Carstens2026.bantu_coordinate_number (s₁ s₂ : Fragments.Bantu.GenderStatus) : (Minimalist.Agreement.CoordinateResolution.resolveCoordinate [Features.Number.Category.singular, Features.Number.Category.plural] (bantuDP s₁) (bantuDP s₂)).number = some Features.Number.Category.plural

Conjoined Bantu singulars → plural number (summation). Bantu languages have a {sg, pl} number system.

theorem Carstens2026.bantu_coordinate_person (s₁ s₂ : Fragments.Bantu.GenderStatus) : (Minimalist.Agreement.CoordinateResolution.resolveCoordinate [Features.Number.Category.singular, Features.Number.Category.plural] (bantuDP s₁) (bantuDP s₂)).person = some Features.Prominence.PersonLevel.third

Conjoined Bantu singulars → 3rd person (full DPs are always 3rd).

theorem Carstens2026.bantu_coordinate_gender (s₁ s₂ : Fragments.Bantu.GenderStatus) : (Minimalist.Agreement.CoordinateResolution.resolveCoordinate [Features.Number.Category.singular, Features.Number.Category.plural] (bantuDP s₁) (bantuDP s₂)).gender = Minimalist.Agreement.GenderResolution.resolve (statusToBundle s₁) (statusToBundle s₂)

Gender dimension of composed resolution matches direct resolve.

theorem Carstens2026.xhosa_human_coordinate : Minimalist.Agreement.CoordinateResolution.resolveCoordinate [Features.Number.Category.singular, Features.Number.Category.plural] (bantuDP (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)) (bantuDP (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)) = { person := some Features.Prominence.PersonLevel.third, number := some Features.Number.Category.plural, gender := some [Fragments.Bantu.SemanticCore.human] }

End-to-end: conjoined [human] Xhosa singulars via unified resolution. Person: 3rd + 3rd → 3rd. Number: sg + sg → pl. Gender: [human] ∩ [human] = some [human]. All three succeed.

theorem Carstens2026.xhosa_uninterpretable_coordinate : Minimalist.Agreement.CoordinateResolution.resolveCoordinate [Features.Number.Category.singular, Features.Number.Category.plural] (bantuDP Fragments.Bantu.GenderStatus.uninterpretable) (bantuDP Fragments.Bantu.GenderStatus.uninterpretable) = { person := some Features.Prominence.PersonLevel.third, number := some Features.Number.Category.plural, gender := none }

End-to-end: conjoined uninterpretable Xhosa singulars. Person and number resolve; gender fails → default.

Shared mechanism

@cite{carstens-2026} explicitly adopts @cite{adamson-anagnostopoulou-2025}'s
percolation-and-intersection mechanism. Both studies use the same
`GenderResolution.resolve` function, instantiated with different
feature types:
- A&A: `GenderNode` (privative geometry nodes — CLASS, MASC, FEM, etc.)
- Carstens: `SemanticCore` (entity flavors — human, animal, inanimate)

The bridge below proves this is not just a narrative claim but a
structural fact: both resolution functions are projections of the same
parameterized mechanism. 

theorem Carstens2026.bantu_aa_self_matching_consistent : (∀ (c : Fragments.Bantu.SemanticCore), (Minimalist.Agreement.GenderResolution.resolve (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c)) (statusToBundle (Fragments.Bantu.GenderStatus.interpretable c))).isSome = true) ∧ ∀ (f : AdamsonAnagnostopoulou2025.GenderNode), (Minimalist.Agreement.GenderResolution.resolve [{ value := f, interp := Minimalist.Interpretability.interpretable }] [{ value := f, interp := Minimalist.Interpretability.interpretable }]).isSome = true

Both studies agree on the self-matching property for interpretable features: Bantu interpretable cores self-match via statusToBundle, and A&A singleton i-features self-match — both through resolve.

MRH failure in Bantu

Unlike Greek/Icelandic (@cite{adamson-anagnostopoulou-2025}), Bantu
does NOT satisfy MRH: uninterpretable genders produce empty
intersections, requiring default agreement. This is the structural
reason why default agreement is needed in Bantu but not in Greek. 

theorem Carstens2026.bantu_fails_mrh : Minimalist.Agreement.GenderResolution.satisfiesMRH [statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.animal), statusToBundle Fragments.Bantu.GenderStatus.uninterpretable] = false

Bantu does not satisfy MRH: the full inventory includes uninterpretable genders that yield empty intersections.

theorem Carstens2026.bantu_interpretable_fails_mrh : Minimalist.Agreement.GenderResolution.satisfiesMRH [statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.animal)] = false

Restricted to interpretable-only, MRH still fails: mismatched cores (human ≠ inanimate) yield empty intersection.

theorem Carstens2026.bantu_uniform_satisfies_mrh (c : Fragments.Bantu.SemanticCore) : Minimalist.Agreement.GenderResolution.satisfiesMRH [statusToBundle (Fragments.Bantu.GenderStatus.interpretable c), statusToBundle (Fragments.Bantu.GenderStatus.interpretable c)] = true

But uniform cores satisfy MRH trivially (self-matching).

Three or more conjuncts

`resolveN` extends the mechanism to n-ary coordination.
Bantu predictions generalize cleanly: matching agreement requires
ALL conjuncts to share the same interpretable core. 

theorem Carstens2026.nary_three_humans : Minimalist.Agreement.GenderResolution.resolveN [statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)] = some [Fragments.Bantu.SemanticCore.human]

Three [human] conjuncts → matching [human].

theorem Carstens2026.nary_three_inanimates : Minimalist.Agreement.GenderResolution.resolveN [statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate)] = some [Fragments.Bantu.SemanticCore.inanimate]

Three [inanimate] conjuncts → matching [inanimate].

theorem Carstens2026.nary_three_uninterpretable : Minimalist.Agreement.GenderResolution.resolveN [statusToBundle Fragments.Bantu.GenderStatus.uninterpretable, statusToBundle Fragments.Bantu.GenderStatus.uninterpretable, statusToBundle Fragments.Bantu.GenderStatus.uninterpretable] = none

Three uninterpretable conjuncts → default (none).

theorem Carstens2026.nary_mixed_fails : Minimalist.Agreement.GenderResolution.resolveN [statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate)] = none

Mixed: two [human] + one [inanimate] → default (none). A single mismatched conjunct blocks matching agreement.

theorem Carstens2026.nary_human_plus_unintrp_fails : Minimalist.Agreement.GenderResolution.resolveN [statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human), statusToBundle Fragments.Bantu.GenderStatus.uninterpretable] = none

Mixed: two [human] + one uninterpretable → default (none). Uninterpretable conjuncts block matching even with uniform cores.

theorem Carstens2026.nary_subsumes_binary_bantu (s₁ s₂ : Fragments.Bantu.GenderStatus) : Minimalist.Agreement.GenderResolution.resolveN [statusToBundle s₁, statusToBundle s₂] = Minimalist.Agreement.GenderResolution.resolve (statusToBundle s₁) (statusToBundle s₂)

N-ary subsumes binary for Bantu.