Taraldsen, Taraldsen Medová & Langa (2018)

@cite{taraldsen-et-al-2018}

"Class prefixes as specifiers in Southern Bantu." Natural Language & Linguistic Theory 36:1339–1394.

Core claims

1. Bantu class prefixes are phrasal specifiers, not heads.
2. Each prefix lexicalizes a nanosyntactic tree: [# Nx] (plural) or just [Nx] (singular), where # is the number head and Nx is a classifier-like nominal head.
3. "Strong" classes (1/2, 7/8) share the same N between singular and plural; "weak" classes (3/4, 5/6, 9/10) have distinct Ns (N₄ ≠ N₃, N₆ ≠ N₅). This is the paper's central empirical finding from agreement with conjoined subjects (§2.1–2.6).
4. The Foot Condition constrains prefix insertion and derives nP stacking (double prefix constructions in Changana/Rhonga).
5. The specifier analysis unifies Bantu class prefixes with classifiers on the @cite{aikhenvald-2000} continuum.

Formalization

• §1: NCFeature — nominal feature inventory (number, classifier)
• §2: Class prefix entries as TreeLexEntry NCFeature
• §3: Tree-based spellout verification
• §4: Strong vs weak classes — the core N₄ ≠ N₃ distinction
• §5: Foot Condition and why weak classes can't spell out
• §6: Pluralization derivation — the backtracking algorithm
• §7: Stacking-agreement correlation (central bridge theorem)
• §8: DM vs Nanosyntax comparison on SC prefixes
• §9: Agreement-classifier bridge (@cite{carstens-2026})
• §10: NPStack derivation from stacking analysis
• §11: NPStack–stacking bridge (canonical ↔ direct spellout)
• §12: NounClass alignment (Fragment enums ↔ study Nats)

inductive TaraldsenEtAl2018.NCFeature : Type

Nominal features on the Bantu nanosyntactic fseq. num = number head (#); cls n = classifier head Nn.

@cite{taraldsen-et-al-2018}: class prefixes spell out phrasal trees built from these features. Singular prefixes lexicalize just Nx; plural prefixes lexicalize [# Nx].

• num : NCFeature
• cls : ℕ → NCFeature

def TaraldsenEtAl2018.instDecidableEqNCFeature.decEq (x✝ x✝¹ : NCFeature) : Decidable (x✝ = x✝¹)

Equations

• TaraldsenEtAl2018.instDecidableEqNCFeature.decEq TaraldsenEtAl2018.NCFeature.num TaraldsenEtAl2018.NCFeature.num = isTrue ⋯
• TaraldsenEtAl2018.instDecidableEqNCFeature.decEq TaraldsenEtAl2018.NCFeature.num (TaraldsenEtAl2018.NCFeature.cls a) = isFalse ⋯
• TaraldsenEtAl2018.instDecidableEqNCFeature.decEq (TaraldsenEtAl2018.NCFeature.cls a) TaraldsenEtAl2018.NCFeature.num = isFalse ⋯
• TaraldsenEtAl2018.instDecidableEqNCFeature.decEq (TaraldsenEtAl2018.NCFeature.cls a) (TaraldsenEtAl2018.NCFeature.cls b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance TaraldsenEtAl2018.instDecidableEqNCFeature : DecidableEq NCFeature

Equations

• TaraldsenEtAl2018.instDecidableEqNCFeature = TaraldsenEtAl2018.instDecidableEqNCFeature.decEq

@[implicit_reducible]

instance TaraldsenEtAl2018.instBEqNCFeature : BEq NCFeature

Equations

• TaraldsenEtAl2018.instBEqNCFeature = { beq := TaraldsenEtAl2018.instBEqNCFeature.beq }

def TaraldsenEtAl2018.instBEqNCFeature.beq : NCFeature → NCFeature → Bool

Equations

• TaraldsenEtAl2018.instBEqNCFeature.beq TaraldsenEtAl2018.NCFeature.num TaraldsenEtAl2018.NCFeature.num = true
• TaraldsenEtAl2018.instBEqNCFeature.beq (TaraldsenEtAl2018.NCFeature.cls a) (TaraldsenEtAl2018.NCFeature.cls b) = (a == b)
• TaraldsenEtAl2018.instBEqNCFeature.beq x✝¹ x✝ = false

def TaraldsenEtAl2018.instReprNCFeature.repr : NCFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TaraldsenEtAl2018.instReprNCFeature : Repr NCFeature

Equations

• TaraldsenEtAl2018.instReprNCFeature = { reprPrec := TaraldsenEtAl2018.instReprNCFeature.repr }

def TaraldsenEtAl2018.cl1Sg : Morphology.Nanosyntax.TreeLexEntry NCFeature

Singular class prefixes: each lexicalizes just Nx. @cite{taraldsen-et-al-2018} (60)–(61): singular prefixes are specifiers of nP, spelling out the classifier head N alone.

Equations

• TaraldsenEtAl2018.cl1Sg = { tree := Morphology.Nanosyntax.NanoTree.leaf (TaraldsenEtAl2018.NCFeature.cls 1), exponent := "um", morphType := Morphology.Nanosyntax.MorphType.prefix }

def TaraldsenEtAl2018.cl3Sg : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

• TaraldsenEtAl2018.cl3Sg = { tree := Morphology.Nanosyntax.NanoTree.leaf (TaraldsenEtAl2018.NCFeature.cls 3), exponent := "um", morphType := Morphology.Nanosyntax.MorphType.prefix }

def TaraldsenEtAl2018.cl5Sg : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

• TaraldsenEtAl2018.cl5Sg = { tree := Morphology.Nanosyntax.NanoTree.leaf (TaraldsenEtAl2018.NCFeature.cls 5), exponent := "ili", morphType := Morphology.Nanosyntax.MorphType.prefix }

def TaraldsenEtAl2018.cl7Sg : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

• TaraldsenEtAl2018.cl7Sg = { tree := Morphology.Nanosyntax.NanoTree.leaf (TaraldsenEtAl2018.NCFeature.cls 7), exponent := "isi", morphType := Morphology.Nanosyntax.MorphType.prefix }

def TaraldsenEtAl2018.cl9Sg : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

• TaraldsenEtAl2018.cl9Sg = { tree := Morphology.Nanosyntax.NanoTree.leaf (TaraldsenEtAl2018.NCFeature.cls 9), exponent := "in", morphType := Morphology.Nanosyntax.MorphType.prefix }

def TaraldsenEtAl2018.cl2Pl : Morphology.Nanosyntax.TreeLexEntry NCFeature

Plural class prefixes: each lexicalizes [# Nx]. @cite{taraldsen-et-al-2018} (60)–(61), (77), (83): plural prefixes are specifiers of #P, spelling out [number + classifier].

Critical: "strong" classes (2, 8) share the same N with their singular counterparts (N₁, N₇). "Weak" classes (4, 6, 10) contain DISTINCT Ns: N₄ ≠ N₃, N₆ ≠ N₅, N₁₀ ≠ N₉. This is the paper's central empirical finding from agreement with conjoined subjects (@cite{taraldsen-et-al-2018} §2).

Equations

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

def TaraldsenEtAl2018.cl4Pl : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

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

def TaraldsenEtAl2018.cl6Pl : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

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

def TaraldsenEtAl2018.cl8Pl : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

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

def TaraldsenEtAl2018.cl10Pl : Morphology.Nanosyntax.TreeLexEntry NCFeature

Equations

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

def TaraldsenEtAl2018.xhosaClassPrefixes : List (Morphology.Nanosyntax.TreeLexEntry NCFeature)

Equations

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

theorem TaraldsenEtAl2018.spellout_cl1_sg : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 1)) = some "um"

Singular: target N1 -> "um" (cl1Sg wins, smallest match).

theorem TaraldsenEtAl2018.spellout_cl2_pl : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 1)]) = some "aba"

Plural: target [# N1] -> "aba" (cl2Pl matches — strong class).

theorem TaraldsenEtAl2018.spellout_cl5_sg : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 5)) = some "ili"

Singular: target N5 -> "ili".

theorem TaraldsenEtAl2018.spellout_cl6_pl : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 6)]) = some "ama"

Plural: target [# N6] -> "ama" (weak class — N₆ ≠ N₅).

theorem TaraldsenEtAl2018.spellout_cl7_sg : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 7)) = some "isi"

Singular: target N7 -> "isi".

theorem TaraldsenEtAl2018.spellout_cl8_pl : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 7)]) = some "izi"

Plural: target [# N7] -> "izi" (strong class).

theorem TaraldsenEtAl2018.spellout_cl2_sg_none : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 2)) = none

No prefix matches an unlexicalized N (class 2 has no singular form).

def TaraldsenEtAl2018.sharesClassifierN (sgEntry plEntry : Morphology.Nanosyntax.TreeLexEntry NCFeature) : Bool

Whether a singular-plural class pair shares the same classifier N. @cite{taraldsen-et-al-2018} §2: strong classes (1/2, 7/8) share Ns; weak classes (3/4, 5/6, 9/10) have distinct Ns. The evidence comes from agreement with conjoined singular subjects: a conjunction of two class X singulars triggers plural class Y agreement iff the plural prefix for Y contains the same N as X.

Equations

• TaraldsenEtAl2018.sharesClassifierN sgEntry plEntry = (sgEntry.tree.foot == plEntry.tree.foot)

theorem TaraldsenEtAl2018.cl1_cl2_share_N : sharesClassifierN cl1Sg cl2Pl = true

Classes 1/2 share N₁ — strong class pair. A conjunction of two class 1 singular nouns triggers class 2 plural agreement because ba ↔ [# N₁] and the singular m ↔ [N₁] share the same N₁.

theorem TaraldsenEtAl2018.cl7_cl8_share_N : sharesClassifierN cl7Sg cl8Pl = true

Classes 7/8 share N₇ — strong class pair.

theorem TaraldsenEtAl2018.cl3_cl4_distinct_N : sharesClassifierN cl3Sg cl4Pl = false

Classes 3/4 do NOT share Ns — weak class pair. @cite{taraldsen-et-al-2018} §2.1–2.4: a conjunction of two class 3 singular nouns does NOT trigger class 4 agreement. The plural prefix mi contains N₄, distinct from the N₃ in the singular prefix mu.

theorem TaraldsenEtAl2018.cl5_cl6_distinct_N : sharesClassifierN cl5Sg cl6Pl = false

Classes 5/6 do NOT share Ns — weak class pair. @cite{taraldsen-et-al-2018} §2.5: a conjunction of two class 5 singular nouns does NOT trigger class 6 agreement. The plural prefix ma contains N₆, distinct from the N₅ in class 5.

theorem TaraldsenEtAl2018.cl9_cl10_distinct_N : sharesClassifierN cl9Sg cl10Pl = false

Classes 9/10 do NOT share Ns — weak class pair (in Changana/Rhonga; in Xhosa the class 10 prefix = class 8).

theorem TaraldsenEtAl2018.cl2_foot_is_n1 : cl2Pl.tree.foot = NCFeature.cls 1

The foot of cl2Pl ("aba") is N₁.

theorem TaraldsenEtAl2018.cl4_foot_is_n4 : cl4Pl.tree.foot = NCFeature.cls 4

The foot of cl4Pl ("imi") is N₄ — NOT N₃. This is the key structural fact: imi requires N₄ to be present in the syntactic structure. Since N₄ ≠ N₃, imi cannot spell out a structure built from a class 3 noun.

theorem TaraldsenEtAl2018.foot_met_strong_cl2 : Morphology.Nanosyntax.footConditionMet cl2Pl (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 1)]) = true

Strong class: "aba" CAN spell out [# N₁] because its foot (N₁) is present in the target. No stacking needed.

theorem TaraldsenEtAl2018.foot_met_strong_cl8 : Morphology.Nanosyntax.footConditionMet cl8Pl (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 7)]) = true

Strong class: "izi" CAN spell out [# N₇].

theorem TaraldsenEtAl2018.foot_not_met_weak_cl4 : Morphology.Nanosyntax.footConditionMet cl4Pl (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 3)]) = false

Weak class: "imi" CANNOT spell out a structure containing only N₃. The Foot Condition requires N₄ (the foot of imi's stored tree), but the target [# N₃] contains only N₃. This forces backtracking, producing stacking — e.g., mi-mu-twa 'thorns' (class 4-3) in Changana/Rhonga.

theorem TaraldsenEtAl2018.foot_not_met_weak_cl6 : Morphology.Nanosyntax.footConditionMet cl6Pl (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 5)]) = false

Weak class: "ama" CANNOT spell out a structure containing only N₅. Same logic: N₆ ≠ N₅.

theorem TaraldsenEtAl2018.no_spellout_forces_stacking_cl3 : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 3)]) = none

The stacking prediction: for weak classes, no entry in the lexicon can spell out the target [# N_sg]. The derivation must backtrack, splitting the structure and building a Specifier — producing the stacking pattern observed in Changana/Rhonga. @cite{taraldsen-et-al-2018} §4.2, prediction derived from (77)–(83).

Contrast with strong classes (§3) where spellout succeeds directly.

theorem TaraldsenEtAl2018.no_spellout_forces_stacking_cl5 : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 5)]) = none

theorem TaraldsenEtAl2018.no_spellout_forces_stacking_cl9 : Morphology.Nanosyntax.treeSpellout xhosaClassPrefixes (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 9)]) = none

inductive TaraldsenEtAl2018.PluralizationResult : Type

Result of pluralizing a Bantu noun. @cite{taraldsen-et-al-2018} §4.2 derives two outcomes:

• direct: one plural prefix replaces the singular (strong class).
• stacked: the plural prefix stacks on top of the singular prefix (weak class), producing double prefix constructions.

• direct : String → PluralizationResult
• stacked : String → String → PluralizationResult

@[implicit_reducible]

instance TaraldsenEtAl2018.instDecidableEqPluralizationResult : DecidableEq PluralizationResult

Equations

• TaraldsenEtAl2018.instDecidableEqPluralizationResult = TaraldsenEtAl2018.instDecidableEqPluralizationResult.decEq

def TaraldsenEtAl2018.instDecidableEqPluralizationResult.decEq (x✝ x✝¹ : PluralizationResult) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TaraldsenEtAl2018.instDecidableEqPluralizationResult.decEq (TaraldsenEtAl2018.PluralizationResult.direct a) (TaraldsenEtAl2018.PluralizationResult.stacked a_1 a_2) = isFalse ⋯
• TaraldsenEtAl2018.instDecidableEqPluralizationResult.decEq (TaraldsenEtAl2018.PluralizationResult.stacked a a_1) (TaraldsenEtAl2018.PluralizationResult.direct a_2) = isFalse ⋯

@[implicit_reducible]

instance TaraldsenEtAl2018.instBEqPluralizationResult : BEq PluralizationResult

Equations

• TaraldsenEtAl2018.instBEqPluralizationResult = { beq := TaraldsenEtAl2018.instBEqPluralizationResult.beq }

def TaraldsenEtAl2018.instBEqPluralizationResult.beq : PluralizationResult → PluralizationResult → Bool

Equations

• TaraldsenEtAl2018.instBEqPluralizationResult.beq (TaraldsenEtAl2018.PluralizationResult.direct a) (TaraldsenEtAl2018.PluralizationResult.direct b) = (a == b)
• TaraldsenEtAl2018.instBEqPluralizationResult.beq (TaraldsenEtAl2018.PluralizationResult.stacked a a_1) (TaraldsenEtAl2018.PluralizationResult.stacked b b_1) = (a == b && a_1 == b_1)
• TaraldsenEtAl2018.instBEqPluralizationResult.beq x✝¹ x✝ = false

def TaraldsenEtAl2018.instReprPluralizationResult.repr : PluralizationResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TaraldsenEtAl2018.instReprPluralizationResult : Repr PluralizationResult

Equations

• TaraldsenEtAl2018.instReprPluralizationResult = { reprPrec := TaraldsenEtAl2018.instReprPluralizationResult.repr }

def TaraldsenEtAl2018.PluralizationResult.isStacked : PluralizationResult → Bool

Equations

• (TaraldsenEtAl2018.PluralizationResult.direct a).isStacked = false
• (TaraldsenEtAl2018.PluralizationResult.stacked a a_1).isStacked = true

def TaraldsenEtAl2018.derivePlural (entries : List (Morphology.Nanosyntax.TreeLexEntry NCFeature)) (sgCls plCls : ℕ) : Option PluralizationResult

Derive the plural form for a noun with singular class sgCls.

Models @cite{taraldsen-et-al-2018} §4.2 cyclic derivation:

1. Noun N_Y merges with classifier N_sgCls → [N_sgCls N_Y].
2. Number head # merges → target [# N_sgCls].
3. Try spellout of [# N_sgCls]. If some entry's tree contains this target, the plural prefix directly replaces the singular (strong class path — e.g., ba replaces m for cl 1→2).
4. If no entry matches: the Foot Condition blocks lexicalization (§5). Backtrack (Starke's last resort): form [# N_plCls] as a Specifier merged with N_Y, producing a stacked structure (weak class path — e.g., mi-mu for cl 3→4).

Equations

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

theorem TaraldsenEtAl2018.cl1_plural_direct : derivePlural xhosaClassPrefixes 1 2 = some (PluralizationResult.direct "aba")

Strong class 1/2: direct pluralization. ba ↔ [# N₁] matches the target [# N₁], so the derivation succeeds in one step.

theorem TaraldsenEtAl2018.cl7_plural_direct : derivePlural xhosaClassPrefixes 7 8 = some (PluralizationResult.direct "izi")

Strong class 7/8: direct pluralization.

theorem TaraldsenEtAl2018.cl3_plural_stacked : derivePlural xhosaClassPrefixes 3 4 = some (PluralizationResult.stacked "imi" "um")

Weak class 3/4: stacking. No entry matches [# N₃] (because the only class 4 entry has [# N₄] and N₄ ≠ N₃), so the derivation backtracks: mi ↔ [# N₄] stacks on top of um ↔ [N₃]. Produces the Changana/Rhonga form mi-mu-twa 'thorns'.

theorem TaraldsenEtAl2018.cl5_plural_stacked : derivePlural xhosaClassPrefixes 5 6 = some (PluralizationResult.stacked "ama" "ili")

Weak class 5/6: stacking. ama ↔ [# N₆] on top of ili ↔ [N₅]. Produces Rhonga ma-rhi-tu 'words'.

theorem TaraldsenEtAl2018.cl9_plural_stacked : derivePlural xhosaClassPrefixes 9 10 = some (PluralizationResult.stacked "iin" "in")

Weak class 9/10: stacking. iin ↔ [# N₁₀] on top of in ↔ [N₉]. Produces Rhonga ti-yi-n-dlu 'houses'.

def TaraldsenEtAl2018.isPluralEntry (e : Morphology.Nanosyntax.TreeLexEntry NCFeature) : Bool

Whether an entry is a plural prefix (has # at root). Structurally, plural entries are [# N_X] (node with num label); singular entries are [N_X] (leaf).

Equations

• TaraldsenEtAl2018.isPluralEntry e = match e.tree with | Morphology.Nanosyntax.NanoTree.node f a => f == TaraldsenEtAl2018.NCFeature.num | Morphology.Nanosyntax.NanoTree.leaf a => false

theorem TaraldsenEtAl2018.singular_entries_not_plural : ([cl1Sg, cl3Sg, cl5Sg, cl7Sg, cl9Sg].all fun (x : Morphology.Nanosyntax.TreeLexEntry NCFeature) => !isPluralEntry x) = true

All singular prefixes lack #.

theorem TaraldsenEtAl2018.plural_entries_have_number : ([cl2Pl, cl4Pl, cl6Pl, cl8Pl, cl10Pl].all fun (x : Morphology.Nanosyntax.TreeLexEntry NCFeature) => isPluralEntry x) = true

All plural prefixes have # at root.

theorem TaraldsenEtAl2018.stacking_iff_distinct_N_general (entries : List (Morphology.Nanosyntax.TreeLexEntry NCFeature)) (sg pl : Morphology.Nanosyntax.TreeLexEntry NCFeature) (s pN plCls : ℕ) (hSgTree : sg.tree = Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls s)) (hPlTree : pl.tree = Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls pN)]) (hDirect : (Morphology.Nanosyntax.treeSpellout entries (Morphology.Nanosyntax.NanoTree.node NCFeature.num [Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls s)])).isNone = !s == pN) (r : PluralizationResult) (hr : derivePlural entries s plCls = some r) : r.isStacked = !sharesClassifierN sg pl

The paper's central prediction, proved structurally: for any lexicon where direct spellout of [# N_s] succeeds iff s = pN, stacking occurs iff the classifier Ns are distinct.

The three class-number parameters:

• s: the singular class N (e.g., N₁ for class 1)
• pN: the N inside the plural entry's tree (e.g., N₁ for strong class 2, N₄ for weak class 4)
• plCls: the plural class number used in derivePlural (e.g., 2, 4)

For strong classes, pN = s (shared N): cl2Pl has N₁ = cl1Sg's N. For weak classes, pN ≠ s (distinct Ns): cl4Pl has N₄ ≠ cl3Sg's N₃.

The proof chains three structural insights:

• Algorithm: derivePlural stacks iff direct spellout fails (derivePlural_isStacked_eq)
• Lexicon: direct spellout fails iff s ≠ pN (hDirect)
• Entries: sharesClassifierN = (s = pN) for standard-form entries (definitional from NanoTree.foot)

@cite{taraldsen-et-al-2018}: the correlation between agreement failure and stacking is not stipulated — it is derived from distinct Ns in the lexical entries.

theorem TaraldsenEtAl2018.stacking_cl1_cl2 (r : PluralizationResult) (hr : derivePlural xhosaClassPrefixes 1 2 = some r) : r.isStacked = !sharesClassifierN cl1Sg cl2Pl

Strong class 1/2: no stacking (shared N₁).

theorem TaraldsenEtAl2018.stacking_cl7_cl8 (r : PluralizationResult) (hr : derivePlural xhosaClassPrefixes 7 8 = some r) : r.isStacked = !sharesClassifierN cl7Sg cl8Pl

Strong class 7/8: no stacking (shared N₇).

theorem TaraldsenEtAl2018.stacking_cl3_cl4 (r : PluralizationResult) (hr : derivePlural xhosaClassPrefixes 3 4 = some r) : r.isStacked = !sharesClassifierN cl3Sg cl4Pl

Weak class 3/4: stacking (N₄ ≠ N₃).

theorem TaraldsenEtAl2018.stacking_cl5_cl6 (r : PluralizationResult) (hr : derivePlural xhosaClassPrefixes 5 6 = some r) : r.isStacked = !sharesClassifierN cl5Sg cl6Pl

Weak class 5/6: stacking (N₆ ≠ N₅).

theorem TaraldsenEtAl2018.stacking_cl9_cl10 (r : PluralizationResult) (hr : derivePlural xhosaClassPrefixes 9 10 = some r) : r.isStacked = !sharesClassifierN cl9Sg cl10Pl

Weak class 9/10: stacking (N₁₀ ≠ N₉).

structure TaraldsenEtAl2018.ClassPairing : Type

A singular-plural class pairing in Bantu.

• sgEntry : Morphology.Nanosyntax.TreeLexEntry NCFeature
• plEntry : Morphology.Nanosyntax.TreeLexEntry NCFeature
• sgClass : ℕ
• plClass : ℕ

def TaraldsenEtAl2018.classPairings : List ClassPairing

All five Xhosa class pairings: 2 strong + 3 weak.

Equations

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

theorem TaraldsenEtAl2018.stacking_outer_is_plural : (classPairings.all fun (p : ClassPairing) => match derivePlural xhosaClassPrefixes p.sgClass p.plClass with | some (PluralizationResult.stacked outer a) => xhosaClassPrefixes.any fun (e : Morphology.Nanosyntax.TreeLexEntry NCFeature) => e.exponent == outer && isPluralEntry e | x => true) = true

In stacked forms, the outer prefix is always from a plural entry (has # at root). Singular prefixes never appear as the outer layer in stacking. @cite{taraldsen-et-al-2018} §4.5: "while plural prefixes may stack on top of singular prefixes, we have found no cases where a singular prefix stacks on top of a plural prefix." This follows from the derivation: stacking is triggered by failure to lexicalize #, so the outer Specifier always contains #.

theorem TaraldsenEtAl2018.all_pairings_derive : (classPairings.all fun (p : ClassPairing) => (derivePlural xhosaClassPrefixes p.sgClass p.plClass).isSome) = true

Every class pairing produces a valid derivation (no failures).

def TaraldsenEtAl2018.scPrefixDM : List (Morphology.DM.VI.FeatureVI ℕ String)

DM Vocabulary Items for Xhosa SC prefixes. Each class maps to a single feature. The Subset Principle selects the item whose features are all present in the target (largest match).

Equations

• TaraldsenEtAl2018.scPrefixDM = [{ features := [1], exponent := "u" }, { features := [2], exponent := "ba" }, { features := [7], exponent := "si" }, { features := [8], exponent := "zi" }]

def TaraldsenEtAl2018.scPrefixNano : List (Morphology.Nanosyntax.TreeLexEntry NCFeature)

Nanosyntax entries for the same SC prefixes using tree-based spellout. Each class feature is a leaf on the nanosyntactic tree.

Equations

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

theorem TaraldsenEtAl2018.dm_nano_agree_cl1 : Morphology.DM.VI.subsetPrinciple scPrefixDM [1] = some "u" ∧ Morphology.Nanosyntax.treeSpellout scPrefixNano (Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 1)) = some "u"

DM and Nanosyntax agree: class 1 SC prefix = "u".

theorem TaraldsenEtAl2018.dm_nano_agree_cl2 : Morphology.DM.VI.subsetPrinciple scPrefixDM [2] = some "ba" ∧ Morphology.Nanosyntax.treeSpellout scPrefixNano (Morphology.Nanosyntax.NanoTree.leaf (NCFeature.cls 2)) = some "ba"

DM and Nanosyntax agree: class 2 SC prefix = "ba".

theorem TaraldsenEtAl2018.agreement_resolve_iff_core (s : Fragments.Bantu.GenderStatus) : (Minimalist.Agreement.GenderResolution.resolve (Carstens2026.statusToBundle s) (Carstens2026.statusToBundle s)).isSome = s.core.isSome

Combining @cite{carstens-2026}'s agreement diagnostic with the classifier analysis: matching agreement (resolve succeeds) iff the gender has a semantic core — identifying it as a semantically motivated, classifier-like noun class.

This theorem bridges two phenomena: genders where conjoined singulars allow matching plural agreement (@cite{carstens-2026}) are exactly those whose class prefixes have classifier-like semantic content (@cite{taraldsen-et-al-2018}).

theorem TaraldsenEtAl2018.xhosa_on_classifier_continuum : Typology.NounCategorizationSystem.isNounClassType Aikhenvald2000.xhosa.classifierType = true ∧ Aikhenvald2000.xhosa.HasAgreement

Xhosa sits at the noun-class pole of the @cite{aikhenvald-2000} classifier-to-noun-class continuum.

def TaraldsenEtAl2018.treeToNPStack (visibleClass coreClass : ℕ) (status : Fragments.Bantu.GenderStatus) : Fragments.Bantu.NPStack

Derive an NPStack from a tree-based analysis. The visible class is the outermost N; the core class is the innermost (= foot). When visible = core, the noun is canonical (strong class); when they differ, stacking has occurred because the plural prefix contains a different N (@cite{taraldsen-et-al-2018} §4).

Equations

• TaraldsenEtAl2018.treeToNPStack visibleClass coreClass status = { visibleClass := visibleClass, coreClass := coreClass, status := status }

theorem TaraldsenEtAl2018.canonical_cl1_matches : treeToNPStack 1 1 (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human) = Fragments.Xhosa.humanCanonical

Canonical class 1 [human] noun: visible = core = 1 (strong class).

theorem TaraldsenEtAl2018.stacked_cl3_matches : treeToNPStack 3 1 (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human) = Fragments.Xhosa.humanInClass3

Stacked [human] noun in class 3: visible = 3, core = 1. Stacking occurs because N₃ ≠ N₄ (cl3_cl4_distinct_N): the class 4 plural prefix cannot directly spell out [# N₃] (no_spellout_forces_stacking_cl3), so derivePlural backtracks (cl3_plural_stacked), placing class 3's prefix on top.

theorem TaraldsenEtAl2018.stacked_cl5_matches : treeToNPStack 5 1 (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human) = Fragments.Xhosa.humanInClass5

Stacked [human] noun in class 5: visible = 5, core = 1.

theorem TaraldsenEtAl2018.canonical_cl9_matches : treeToNPStack 9 9 (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.animal) = Fragments.Xhosa.animalCanonical

Canonical [animal] noun: visible = core = 9.

theorem TaraldsenEtAl2018.canonical_does_not_stack : (treeToNPStack 1 1 (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)).isCanonical = true

Canonical nouns (strong classes) don't stack.

theorem TaraldsenEtAl2018.stacked_is_not_canonical : (treeToNPStack 3 1 (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human)).isCanonical = false

Stacked nouns (weak class contexts) are not in their canonical class.

theorem TaraldsenEtAl2018.stacked_implies_not_canonical (vis core : ℕ) (st : Fragments.Bantu.GenderStatus) (hStack : vis ≠ core) : (treeToNPStack vis core st).isCanonical = false

Stacking (from derivePlural) implies non-canonical NPStack. If derivePlural produces .stacked, the noun cannot be in its canonical class (visibleClass ≠ coreClass).

theorem TaraldsenEtAl2018.direct_implies_canonical (cls : ℕ) (st : Fragments.Bantu.GenderStatus) : (treeToNPStack cls cls st).isCanonical = true

Direct pluralization (from derivePlural) is consistent with canonical NPStack (visibleClass = coreClass).

theorem TaraldsenEtAl2018.nounclass_numbers_align : Fragments.Xhosa.NounClass.cl1.classNumber = 1 ∧ Fragments.Xhosa.NounClass.cl3.classNumber = 3 ∧ Fragments.Xhosa.NounClass.cl5.classNumber = 5 ∧ Fragments.Xhosa.NounClass.cl7.classNumber = 7 ∧ Fragments.Xhosa.NounClass.cl9.classNumber = 9

The Xhosa NounClass enum produces the same class numbers used in the nanosyntactic entries. This ensures that Fragment data and the nanosyntactic analysis share a common namespace.

theorem TaraldsenEtAl2018.gender_singular_aligns : Fragments.Xhosa.Gender.genderA.singularClass.classNumber = 1 ∧ Fragments.Xhosa.Gender.genderB.singularClass.classNumber = 3 ∧ Fragments.Xhosa.Gender.genderC.singularClass.classNumber = 5 ∧ Fragments.Xhosa.Gender.genderD.singularClass.classNumber = 7 ∧ Fragments.Xhosa.Gender.genderE.singularClass.classNumber = 9

Gender singular classes match the singular class numbers used in prefix entries.

theorem TaraldsenEtAl2018.gender_plural_aligns : Fragments.Xhosa.Gender.genderA.pluralClass.classNumber = 2 ∧ Fragments.Xhosa.Gender.genderB.pluralClass.classNumber = 4 ∧ Fragments.Xhosa.Gender.genderC.pluralClass.classNumber = 6 ∧ Fragments.Xhosa.Gender.genderD.pluralClass.classNumber = 8 ∧ Fragments.Xhosa.Gender.genderE.pluralClass.classNumber = 10

Gender plural classes match the plural class numbers used in derivePlural.