Number: nominal plurality typology (WALS Chs 33-36)

[DH13b] (Chs 33-36)

Type-level enums + per-language profile struct for nominal and pronominal plurality across [DH13b] chapters 33–36.

Schema

• PluralCoding (Ch 33): how plurality is morphologically realized
• PluralOccurrence (Ch 34): when plural marking occurs (animacy + obligatoriness)
• Pronoun.Plurality (Ch 35): how independent pronouns encode number — the canonical type lives in Syntax/Pronoun/WALS.lean; this file bundles it
• AssociativePlural (Ch 36): "X and associates" construction
• PluralityProfile: per-language bundle of the four

Per-language data lives in Fragments/{Lang}/Plurals.lean. Raw WALS distributions live in Data/WALS/Features/F3{3..6}A.lean — count any strategy directly via F3XA.allData.countP (·.value == ...) rather than re-tabulating here. Corbett 2000 Number refines several of these (general number, dual/trial/paucal inventory, facultative number, Smith-Stark animacy hierarchy, clusivity); those distinctions are formalized in Features/Number.lean, Features/Person.lean, and Studies/Corbett2000.lean rather than here.

Layer discipline

This file is substrate: enums, profile struct, predicates, WALS converters. No Fragment imports.

inductive Morphology.Number.PluralCoding : Type

WALS Ch 33: how plurality is morphologically coded on full nouns. Nine values cross morphological strategy with absence-of-marking.

• prefix : PluralCoding

  Plural prefix (e.g., Swahili wa-toto 'children').

• suffix : PluralCoding

  Plural suffix (e.g., English dog-s).

• stemChange : PluralCoding

  Stem-internal vowel change (e.g., Maricopa humar/humaar).

• tone : PluralCoding

  Tonal change (e.g., Ngiti kamà/kámá 'chief/chiefs').

• reduplication : PluralCoding

  Complete reduplication (e.g., Indonesian rumah-rumah).

• mixedMorphological : PluralCoding

  Two or more methods, none primary (e.g., Arabic).

• pluralWord : PluralCoding

  Separate word in NP (e.g., Hawaiian mau, Mandarin 些).

• pluralClitic : PluralCoding

  NP-level clitic (e.g., Cayuvava me=).

• noPlural : PluralCoding

  No indication of plurality.

@[implicit_reducible]

instance Morphology.Number.instDecidableEqPluralCoding : DecidableEq PluralCoding

Equations

• Morphology.Number.instDecidableEqPluralCoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.Number.instReprPluralCoding : Repr PluralCoding

Equations

• Morphology.Number.instReprPluralCoding = { reprPrec := Morphology.Number.instReprPluralCoding.repr }

def Morphology.Number.instReprPluralCoding.repr : PluralCoding → ℕ → Std.Format

Equations

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

inductive Morphology.Number.PluralOccurrence : Type

WALS Ch 34: when plural marking occurs on full nouns. Cross of animacy scope (none / human-only / all) and obligatoriness (optional / obligatory).

• noNominalPlural : PluralOccurrence

  No nominal plural at all.

• humanOnlyOptional : PluralOccurrence

  Plural only on human nouns, optional.

• humanOnlyObligatory : PluralOccurrence

  Plural only on human nouns, obligatory.

• allNounsAlwaysOptional : PluralOccurrence

  Plural on all nouns, always optional.

• allNounsOptionalInanimates : PluralOccurrence

  Plural on all nouns, obligatory for human, optional for inanimate.

• allNounsAlwaysObligatory : PluralOccurrence

  Plural on all nouns, always obligatory.

@[implicit_reducible]

instance Morphology.Number.instDecidableEqPluralOccurrence : DecidableEq PluralOccurrence

Equations

• Morphology.Number.instDecidableEqPluralOccurrence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.Number.instReprPluralOccurrence : Repr PluralOccurrence

Equations

• Morphology.Number.instReprPluralOccurrence = { reprPrec := Morphology.Number.instReprPluralOccurrence.repr }

def Morphology.Number.instReprPluralOccurrence.repr : PluralOccurrence → ℕ → Std.Format

Equations

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

inductive Morphology.Number.AssociativePlural : Type

WALS Ch 36: associative plural marking ("X and associates"). The typological split is between marker-overlap with additive plural vs dedicated associative form.

• sameAsAdditive : AssociativePlural

  Marker also used for additive plural (e.g., Zulu, Turkish).

• uniqueAffixal : AssociativePlural

  Dedicated affix (e.g., Hungarian -ek).

• uniquePeriphrastic : AssociativePlural

  Dedicated free/clitic marker (e.g., Tagalog, Japanese -tachi).

• absent : AssociativePlural

  No productive associative plural (e.g., Russian, English).

@[implicit_reducible]

instance Morphology.Number.instDecidableEqAssociativePlural : DecidableEq AssociativePlural

Equations

• Morphology.Number.instDecidableEqAssociativePlural x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.Number.instReprAssociativePlural.repr : AssociativePlural → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Number.instReprAssociativePlural : Repr AssociativePlural

Equations

• Morphology.Number.instReprAssociativePlural = { reprPrec := Morphology.Number.instReprAssociativePlural.repr }

structure Morphology.Number.PluralityProfile : Type

A language's plurality profile across [DH13b] Chs 33-36.

• language : String

  Language name (matches LanguageProfile.name when bundled).

• iso : String

  ISO 639-3 code (matches LanguageProfile.iso when bundled).

• coding : PluralCoding

  Ch 33: how plurality is coded on nouns.

• occurrence : PluralOccurrence

  Ch 34: when plural marking occurs.

• pronounPlurality : Pronoun.Plurality

  Ch 35: pronoun plurality type (canonical type in Syntax/Pronoun/WALS.lean).

• associativePlural : AssociativePlural

  Ch 36: associative plural strategy.

@[implicit_reducible]

instance Morphology.Number.instReprPluralityProfile : Repr PluralityProfile

Equations

• Morphology.Number.instReprPluralityProfile = { reprPrec := Morphology.Number.instReprPluralityProfile.repr }

def Morphology.Number.instReprPluralityProfile.repr : PluralityProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.Number.instDecidableEqPluralityProfile : DecidableEq PluralityProfile

Equations

• Morphology.Number.instDecidableEqPluralityProfile = Morphology.Number.instDecidableEqPluralityProfile.decEq

def Morphology.Number.instDecidableEqPluralityProfile.decEq (x✝ x✝¹ : PluralityProfile) : Decidable (x✝ = x✝¹)

Equations

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