Carstens 2026: The Grammar of Gender

[Car26]

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 [AA25], 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 resolve — the single compositional endpoint — via statusToBundle which bridges Bantu GenderStatus to AnnotatedFeatures SemanticCore. Study-level theorems verify the mechanism's predictions against [Car26]'s empirical data.

def Carstens2026.nP (c : Bantu.SemanticCore) : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

A single interpretable nP layer bearing SemanticCore c.

Equations

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

def Carstens2026.nP_u : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

An uninterpretable nP layer (no features to percolate).

Equations

• Carstens2026.nP_u = []

def Carstens2026.nPStack (outer inner : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore) : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

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

Equations

• Carstens2026.nPStack outer inner = outer ++ inner

def Carstens2026.statusToBundle (s : Bantu.GenderStatus) : AdamsonAnagnostopoulou2025.AnnotatedFeatures 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 (Bantu.GenderStatus.interpretable c) = Carstens2026.nP c
• Carstens2026.statusToBundle Bantu.GenderStatus.uninterpretable = Carstens2026.nP_u

theorem Carstens2026.interpretable_self_nonempty (c : Bantu.SemanticCore) : AdamsonAnagnostopoulou2025.resolve (statusToBundle (Bantu.GenderStatus.interpretable c)) (statusToBundle (Bantu.GenderStatus.interpretable c)) = some [c]

Interpretable genders yield non-empty intersection with themselves.

theorem Carstens2026.uninterpretable_self_empty : AdamsonAnagnostopoulou2025.resolve (statusToBundle Bantu.GenderStatus.uninterpretable) (statusToBundle Bantu.GenderStatus.uninterpretable) = none

Uninterpretable genders yield empty intersection with themselves.

theorem Carstens2026.uninterpretable_interpretable_empty (c : Bantu.SemanticCore) : AdamsonAnagnostopoulou2025.resolve (statusToBundle Bantu.GenderStatus.uninterpretable) (statusToBundle (Bantu.GenderStatus.interpretable c)) = none

Uninterpretable + interpretable yields empty intersection.

theorem Carstens2026.mismatched_cores_empty (c1 c2 : Bantu.SemanticCore) (h : c1 ≠ c2) : AdamsonAnagnostopoulou2025.resolve (statusToBundle (Bantu.GenderStatus.interpretable c1)) (statusToBundle (Bantu.GenderStatus.interpretable c2)) = none

Mismatched interpretable cores yield empty intersection.

theorem Carstens2026.bantu_matching_iff_interpretable (s : Bantu.GenderStatus) : (AdamsonAnagnostopoulou2025.resolve (statusToBundle s) (statusToBundle s)).isSome = s.isInterpretable

The central claim ([Car26]): 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 : AdamsonAnagnostopoulou2025.resolve (statusToBundle Xhosa.Gender.genderA.status) (statusToBundle Xhosa.Gender.genderA.status) = some [Bantu.SemanticCore.human]

[1&1] human conjuncts: intersection = [human] → matching cl 2 available. [Car26] Table 13: 100% ba- (matching = default for [human]).

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

[7&7] inanimate conjuncts: intersection = [inanimate] → matching cl 8. [Car26] Table 13: 100% zi- for non-human [7&7].

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

[9&9] animal conjuncts: intersection = [animal] → matching cl 10. [Car26] 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 : AdamsonAnagnostopoulou2025.resolve (statusToBundle Xhosa.Gender.genderB.status) (statusToBundle Xhosa.Gender.genderB.status) = none

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

theorem Carstens2026.xhosa_5and5_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Xhosa.Gender.genderC.status) (statusToBundle Xhosa.Gender.genderC.status) = none

[5&5] conjuncts: intersection = ∅ → default agreement only. [Car26] 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 : Xhosa.Gender) : (AdamsonAnagnostopoulou2025.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 : AdamsonAnagnostopoulou2025.resolve (statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human)) (statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human)) = some [Bantu.SemanticCore.human]

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

theorem Carstens2026.xhosa_mismatched_inanimate : AdamsonAnagnostopoulou2025.resolve (statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate)) (statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate)) = some [Bantu.SemanticCore.inanimate]

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

theorem Carstens2026.xhosa_human_inanimate_ineffable : AdamsonAnagnostopoulou2025.resolve (statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human)) (statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate)) = none

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

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

Default for [human]: class 2 ba- ([Car26] (52c)).

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

Default for [inanimate]: class 8 zi- ([Car26] (52c)).

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

Default for [animal]: class 8 zi- (class 10 = syncretic with 8 for default purposes; [Car26] §3.4).

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

Shona [1&1]: class 2 va- (human matching/default). [Car26] (58): va- for conjoined [1&1] (consistent across speakers).

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

Shona [7&7]: class 8 zvi- (non-human matching/default). [Car26] (62): zvi- for non-human [7&7] (consistent across speakers).

theorem Carstens2026.shona_3and3_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Shona.Gender.genderB.status) (statusToBundle Shona.Gender.genderB.status) = none

Shona [3&3]: no matching → default only. [Car26] (59): zvi- (class 8 default) for non-human.

theorem Carstens2026.shona_5and5_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Shona.Gender.genderC.status) (statusToBundle Shona.Gender.genderC.status) = none

Shona [5&5]: no matching → default only. [Car26] (60)–(61).

theorem Carstens2026.shona_9and9_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Shona.Gender.genderE.status) (statusToBundle 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. [Car26] §5.2, (64)b–d: va- for human, zvi- for non-human.

theorem Carstens2026.shona_11and11_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Shona.Gender.genderF.status) (statusToBundle Shona.Gender.genderF.status) = none

Shona [11&11]: no matching → default only. [Car26] (65): zvi- (class 8 default).

theorem Carstens2026.shona_14and14_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Shona.Gender.genderG.status) (statusToBundle Shona.Gender.genderG.status) = none

Shona [14&14]: no matching → default only (abstract nouns). [Car26]: genderG (14/6) is uninterpretable.

theorem Carstens2026.shona_12and12_no_matching : AdamsonAnagnostopoulou2025.resolve (statusToBundle Shona.Gender.genderH.status) (statusToBundle Shona.Gender.genderH.status) = none

Shona [12&12]: no matching → default only (diminutives). [Car26]: conjoined diminutives take class 8 zvi-.

theorem Carstens2026.shona_matching_iff_interpretable (g : Shona.Gender) : (AdamsonAnagnostopoulou2025.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 : Xhosa.Gender) => g.status.isInterpretable) [Xhosa.Gender.genderA, Xhosa.Gender.genderB, Xhosa.Gender.genderC, Xhosa.Gender.genderD, Xhosa.Gender.genderE]).length = 3

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

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

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

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

Core insight ([Car26] §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 : Xhosa.humanCanonical.isCanonical = true

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

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

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

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

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

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

Stacked nouns retain the core gender despite different visible class.

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

Bantu SemanticCore → DM Interpretability bridge. Interpretable genders bear Interpretability.i (natural gender); uninterpretable genders bear Interpretability.u (arbitrary gender). [Car26] directly extends [Kra15]'s i/u distinction.

Equations

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

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

The bridge preserves the interpretability predicate.

def Carstens2026.toSemanticBasis : Bantu.SemanticCore → Corbett1991.SemanticBasis

Bantu SemanticCore → typological SemanticBasis bridge. [Car26]'s cores map to [Kra20]'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 Bantu.SemanticCore.human = Corbett1991.SemanticBasis.humanness
• Carstens2026.toSemanticBasis Bantu.SemanticCore.animal = Corbett1991.SemanticBasis.animacy
• Carstens2026.toSemanticBasis Bantu.SemanticCore.inanimate = Corbett1991.SemanticBasis.animacy
• Carstens2026.toSemanticBasis Bantu.SemanticCore.nonhuman = Corbett1991.SemanticBasis.humanness

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

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

def Carstens2026.xhosaGenderProfile : Corbett1991.Profile

Xhosa gender profile ([Car26] §2.2: semantic cores for some genders, formal (class prefix) assignment for others). Stated in the [Cor91] study's Profile schema; Xhosa is WALS-silent for Chs 30/31/32, so the codings are this file's commitments.

Equations

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

def Carstens2026.shonaGenderProfile : Corbett1991.Profile

Shona gender profile (WALS-grounded; cf. Corbett1991.basis_wals_grounded for the sample-side analogues).

Equations

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

theorem Carstens2026.profiles_wals_grounded : xhosaGenderProfile.BasisGrounded ∧ xhosaGenderProfile.AssignmentGrounded ∧ shonaGenderProfile.BasisGrounded ∧ shonaGenderProfile.AssignmentGrounded

Both profiles' codings agree with WALS where covered.

theorem Carstens2026.xhosa_satisfies_semantic_core : xhosaGenderProfile.SatisfiesSemanticCore

Both profiles satisfy the Semantic Core Generalization ([Kra20] ex. 2/28).

theorem Carstens2026.shona_satisfies_semantic_core : shonaGenderProfile.SatisfiesSemanticCore

def Carstens2026.resolveStacks (s1 s2 : Bantu.NPStack) : Option (List 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. [Car26] (85)–(88): mismatched [3&5] humans → ba-, mismatched [3&5] inanimates → zi-.

Equations

• Carstens2026.resolveStacks s1 s2 = AdamsonAnagnostopoulou2025.resolve (Carstens2026.statusToBundle s1.status) (Carstens2026.statusToBundle s2.status)

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

Criminal (cl3) + policeman (cl5): both [human] core → class 2 ba-. [Car26] (85)a, (86)a.

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

Carrot (cl3) + egg (cl5): both [inanimate] core → class 8 zi-. [Car26] (85)b, (86)b.

theorem Carstens2026.mismatched_7and9_both_human : resolveStacks { visibleClass := 7, coreClass := 1, status := Bantu.GenderStatus.interpretable Bantu.SemanticCore.human } { visibleClass := 9, coreClass := 1, status := Bantu.GenderStatus.interpretable Bantu.SemanticCore.human } = some [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. [Car26] (87)a, (88)a.

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

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

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

Swahili's 5 genders also instantiate the Bantu semantic core system. [Car26] §8 discusses Swahili's GAC (General Animate Concords) as evidence for a [+animate] feature.

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

theorem Carstens2026.three_languages_agree_on_human : Xhosa.Gender.genderA.status = Bantu.GenderStatus.interpretable Bantu.SemanticCore.human ∧ Shona.Gender.genderA.status = Bantu.GenderStatus.interpretable Bantu.SemanticCore.human ∧ Swahili.Gender.genderA.status = Bantu.GenderStatus.interpretable 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
[carstens-2026] §5. 

def Carstens2026.citizenBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

Feature bundle: citizen (class 1, canonical human — no stacking). Structure: [n₁/₂ √CITIZEN]. [Car26] (6)a, (72)a.

Equations

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

def Carstens2026.gangsterBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures 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. [Car26] (28)d, (85)a, (86)a; structure type per (72)b.

Equations

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

def Carstens2026.policemanBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

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

Equations

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

def Carstens2026.hatBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

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

Equations

• Carstens2026.hatBundle = Carstens2026.nP_u

def Carstens2026.carrotBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

Feature bundle: carrot (class 3, inanimate core via stacking). Structure: [n₃/₄ [n₇/₈ √CARROT]]. [Car26] (86)b.

Equations

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

def Carstens2026.eggBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

Feature bundle: egg (class 5, inanimate core via stacking). Structure: [n₅/₆ [n₇/₈ √EGG]]. [Car26] (86)b.

Equations

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

def Carstens2026.elephantBundle : AdamsonAnagnostopoulou2025.AnnotatedFeatures Bantu.SemanticCore

Feature bundle: elephant (class 9, canonical animal — no stacking). Structure: [n₉/₁₀ √ELEPHANT]. [Car26] (49)b, (73)a.

Equations

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

theorem Carstens2026.derivation_1and1_human : AdamsonAnagnostopoulou2025.resolve citizenBundle citizenBundle = some [Bantu.SemanticCore.human]

End-to-end derivation: citizen.1 & president.1 → matching [human]. [Car26] (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 : AdamsonAnagnostopoulou2025.resolve gangsterBundle policemanBundle = some [Bantu.SemanticCore.human]

End-to-end derivation: gangster.3 & policeman.5 → matching [human]. [Car26] (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 : AdamsonAnagnostopoulou2025.resolve carrotBundle eggBundle = some [Bantu.SemanticCore.inanimate]

End-to-end derivation: carrot.3 & egg.5 → matching [inanimate]. [Car26] (86)b: class 8 zi- agreement.

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

theorem Carstens2026.derivation_3and3_default : AdamsonAnagnostopoulou2025.resolve hatBundle hatBundle = none

End-to-end derivation: hat.3 & gun.3 → default. [Car26] (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 : AdamsonAnagnostopoulou2025.resolve elephantBundle elephantBundle = some [Bantu.SemanticCore.animal]

End-to-end derivation: elephant.9 & leopard.9 → matching [animal]. [Car26] (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 : AdamsonAnagnostopoulou2025.resolve citizenBundle (nP Bantu.SemanticCore.inanimate) = none

End-to-end derivation: human + inanimate → default (generally ineffable). [Car26] (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.

[Car26] §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. [Car26] (71): n₁ = i[entity] i[core]; n₂ = i[entity] (for arbitrary members). Core features are more specific.

• classNum : ℕ
• isCore : Bool

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

Equations

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

@[implicit_reducible]

instance Carstens2026.instDecidableEqTwoGrammarFeature : DecidableEq TwoGrammarFeature

Equations

• Carstens2026.instDecidableEqTwoGrammarFeature = Carstens2026.instDecidableEqTwoGrammarFeature.decEq

@[implicit_reducible]

instance Carstens2026.instReprTwoGrammarFeature : Repr TwoGrammarFeature

Equations

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

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

Equations

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

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 : AdamsonAnagnostopoulou2025.AnnotatedFeatures 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. [Car26] (78)a, (79)a, (80)a.

Equations

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

def Carstens2026.divinerFeatures : AdamsonAnagnostopoulou2025.AnnotatedFeatures 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. [Car26] (78)b, (79)b, (80)b.

Equations

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

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

Intersection for train.1a & machine.1a: both layers survive. [Car26] (79)a: &P {1, {7}} ∩ {1, {7}} = {1, {7}}.

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

Intersection for diviner.7 & scholar.7: both layers survive. [Car26] (79)b: &P {7, {1}} ∩ {7, {1}} = {7, {1}}.

theorem Carstens2026.train_highest_wins : AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.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-. [Car26] (79)a.

theorem Carstens2026.train_best_semantic_match : AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.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-. [Car26] (80)a.

theorem Carstens2026.diviner_highest_wins : AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.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-. [Car26] (79)b.

theorem Carstens2026.diviner_best_semantic_match : AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.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-. [Car26] (80)b: 'The fool and the scholar are studying' with ba- agreement.

theorem Carstens2026.two_grammars_differ_train : AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.SelectionGrammar.highestWins TwoGrammarFeature.specificity [{ classNum := 1, isCore := false }, { classNum := 7, isCore := true }] ≠ AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.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. [Car26] (81)a: zi- for [L & M] = BSM; (45)a: ba- for [L & M] = HW.

theorem Carstens2026.two_grammars_differ_diviner : AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.SelectionGrammar.highestWins TwoGrammarFeature.specificity [{ classNum := 7, isCore := false }, { classNum := 1, isCore := true }] ≠ AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.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-).

Coordinate φ-resolution (the &P composition)

Composes the three φ-dimensions for a conjoined DP, each independently: number by lattice join (Number.resolveIn, [Lin83]/[Har14a]), person by hierarchy (Person.resolve, [noyer-1997]), gender by percolation+intersection (resolve, above). Number and person always succeed; gender can fail (→ default). (Formerly Syntax/Minimalist/Agreement/CoordinateResolution.lean, dissolved to its one consumer; the per-dimension operations are the canonical Features/ ones, called directly.)

structure Carstens2026.PhiBundle (G : Type) : Type

A conjunct DP's φ-bundle.

• person : AdamsonAnagnostopoulou2025.AnnotatedFeature Person
• number : AdamsonAnagnostopoulou2025.AnnotatedFeature Number
• gender : AdamsonAnagnostopoulou2025.AnnotatedFeatures G

structure Carstens2026.PhiResolved (G : Type) : Type

Resolved φ-features for a conjoined DP (&P).

• person : Option Person
• number : Option Number
• gender : Option (List G)

def Carstens2026.resolveCoordinate {G : Type} [BEq G] (system : List Number) (dp1 dp2 : PhiBundle G) : PhiResolved G

Resolve all φ-features for two conjoined DPs, each dimension independently: number by Number.resolveIn (coarsened to system), person by Person.resolve, gender by percolation+intersection (resolve).

Equations

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

Bantu coordinate-resolution outcomes

The gender dimension, instantiated with `SemanticCore` via `statusToBundle`, gives
the expected outcomes for conjoined Bantu singular DPs. 

def Carstens2026.bantuDP (s : Bantu.GenderStatus) : PhiBundle 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₂ : Bantu.GenderStatus) : (resolveCoordinate [Number.singular, Number.plural] (bantuDP s₁) (bantuDP s₂)).number = some Number.plural

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

theorem Carstens2026.bantu_coordinate_person (s₁ s₂ : Bantu.GenderStatus) : (resolveCoordinate [Number.singular, Number.plural] (bantuDP s₁) (bantuDP s₂)).person = some Person.third

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

theorem Carstens2026.bantu_coordinate_gender (s₁ s₂ : Bantu.GenderStatus) : (resolveCoordinate [Number.singular, Number.plural] (bantuDP s₁) (bantuDP s₂)).gender = AdamsonAnagnostopoulou2025.resolve (statusToBundle s₁) (statusToBundle s₂)

Gender dimension of composed resolution matches direct resolve.

theorem Carstens2026.xhosa_human_coordinate : resolveCoordinate [Number.singular, Number.plural] (bantuDP (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human)) (bantuDP (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human)) = { person := some Person.third, number := some Number.plural, gender := some [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 : resolveCoordinate [Number.singular, Number.plural] (bantuDP Bantu.GenderStatus.uninterpretable) (bantuDP Bantu.GenderStatus.uninterpretable) = { person := some Person.third, number := some Number.plural, gender := none }

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

Shared mechanism

[carstens-2026] explicitly adopts [adamson-anagnostopoulou-2025]'s
percolation-and-intersection mechanism. Both studies use the same
`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 : Bantu.SemanticCore), (AdamsonAnagnostopoulou2025.resolve (statusToBundle (Bantu.GenderStatus.interpretable c)) (statusToBundle (Bantu.GenderStatus.interpretable c))).isSome = true) ∧ ∀ (f : AdamsonAnagnostopoulou2025.GenderNode), (AdamsonAnagnostopoulou2025.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 ([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 : AdamsonAnagnostopoulou2025.satisfiesMRH [statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.animal), statusToBundle 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 : AdamsonAnagnostopoulou2025.satisfiesMRH [statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate), statusToBundle (Bantu.GenderStatus.interpretable 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 : Bantu.SemanticCore) : AdamsonAnagnostopoulou2025.satisfiesMRH [statusToBundle (Bantu.GenderStatus.interpretable c), statusToBundle (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 : AdamsonAnagnostopoulou2025.resolveN [statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human)] = some [Bantu.SemanticCore.human]

Three [human] conjuncts → matching [human].

theorem Carstens2026.nary_three_inanimates : AdamsonAnagnostopoulou2025.resolveN [statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.inanimate)] = some [Bantu.SemanticCore.inanimate]

Three [inanimate] conjuncts → matching [inanimate].

theorem Carstens2026.nary_three_uninterpretable : AdamsonAnagnostopoulou2025.resolveN [statusToBundle Bantu.GenderStatus.uninterpretable, statusToBundle Bantu.GenderStatus.uninterpretable, statusToBundle Bantu.GenderStatus.uninterpretable] = none

Three uninterpretable conjuncts → default (none).

theorem Carstens2026.nary_mixed_fails : AdamsonAnagnostopoulou2025.resolveN [statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable 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 : AdamsonAnagnostopoulou2025.resolveN [statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle (Bantu.GenderStatus.interpretable Bantu.SemanticCore.human), statusToBundle 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₂ : Bantu.GenderStatus) : AdamsonAnagnostopoulou2025.resolveN [statusToBundle s₁, statusToBundle s₂] = AdamsonAnagnostopoulou2025.resolve (statusToBundle s₁) (statusToBundle s₂)

N-ary subsumes binary for Bantu.

Bridge to [TTML18]: shared classifier N ↔ matching agreement

[TTML18] §2 reads the same conjoined-singular agreement data structurally: matching plural agreement succeeds iff the gender's singular and plural prefixes contain the same classifier N. [Car26]'s diagnostic is semantic: matching succeeds iff the gender has an interpretable core. On the Xhosa lexicon the two classifications coincide — the shared-N pairs (1/2, 7/8, 9/10) are exactly the interpretable genders (A, D, E).

theorem Carstens2026.xhosa_matching_iff_sharesClassifierN (g : Xhosa.Gender) : (AdamsonAnagnostopoulou2025.resolve (statusToBundle g.status) (statusToBundle g.status)).isSome = true ↔ TaraldsenEtAl2018.SharesClassifierN (TaraldsenEtAl2018.xhosaSg g) (TaraldsenEtAl2018.xhosaPl g)

Per Xhosa gender, [Car26]'s matching-agreement diagnostic agrees with [TTML18]'s shared-classifier-N diagnostic.