Maddieson 2013: WALS phonology chapters ↔ PHOIBLE 2.0 bridges

[Mad13] [MMcC19] [DH13a]

Cross-dataset bridge theorems verifying that PHOIBLE 2.0 inventories are consistent with the WALS Maddieson chapter classifications, for the 16 languages currently covered by Fragments/{Lang}/Phonology.lean.

Inventories are accessed via Fragments (not Data directly), per linglib's pattern that per-language data flows through Fragment files.

Why this study file exists

The dissolved Phenomena/Phonology/Typology.lean carried a 16-language hand-curated PhonProfile sample with ~80 xxx_chN grounding theorems testing each language against WALS — vacuous round-trips (each value matches its own WALS lookup). Dropped in the dissolution.

This file replaces the bridge work with substantive WALS↔PHOIBLE cross-dataset verification: each language's PHOIBLE consonant count is checked against the WALS Maddieson Ch 1 bin it falls into. Where PHOIBLE and WALS disagree at the bin level, the disagreement is documented (PHOIBLE often counts more segments under finer transcription).

Maddieson's WALS Ch 1 bin definitions

WALS Ch 1 (consonant inventory size) bins, per the chapter text:

• small : 6–14 consonants
• moderatelySmall : 15–18
• average : 19–25
• moderatelyLarge : 26–33
• large : 34+

Note: these bins come from Maddieson's UPSID counts. PHOIBLE 2.0 has finer transcription and broader source coverage, so per-language counts can differ even when both are well-formed inventories.

Featural double-coding (deferred)

WALS Ch 7 (glottalized consonants) could derive from a PHOIBLE inventory

• a presence-of-[+constricted glottis] predicate (Linglib/Phonology/Segmental/Defs.lean). Same for Ch 8 ([+lateral]), Ch 9 ([+nasal, +dorsal]), Ch 11 ([+front, +round]). Bridge theorems of that form are deferred — would require a uniform "inventory has any phoneme with feature F" helper.

inductive Maddieson2013.CInventorySize : Type

Consonant inventory size, WALS Ch 1 ([Mad13]). Maddieson's UPSID-based bins; the sole consumer is inWALS1ABin below, so this classification lives with the paper that uses it.

• small : CInventorySize
• moderatelySmall : CInventorySize
• average : CInventorySize
• moderatelyLarge : CInventorySize
• large : CInventorySize

@[implicit_reducible]

instance Maddieson2013.instDecidableEqCInventorySize : DecidableEq CInventorySize

Equations

• Maddieson2013.instDecidableEqCInventorySize x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Maddieson2013.instReprCInventorySize : Repr CInventorySize

Equations

• Maddieson2013.instReprCInventorySize = { reprPrec := Maddieson2013.instReprCInventorySize.repr }

def Maddieson2013.instReprCInventorySize.repr : CInventorySize → ℕ → Std.Format

Equations

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

def Maddieson2013.inWALS1ABin (bin : CInventorySize) (n : ℕ) : Bool

Whether a consonant count falls in the WALS Ch 1 bin for a given CInventorySize. Uses Maddieson's bin boundaries. Returns Bool; decide resolves the comparisons concretely.

Equations

• Maddieson2013.inWALS1ABin Maddieson2013.CInventorySize.small n = decide (6 ≤ n ∧ n ≤ 14)
• Maddieson2013.inWALS1ABin Maddieson2013.CInventorySize.moderatelySmall n = decide (15 ≤ n ∧ n ≤ 18)
• Maddieson2013.inWALS1ABin Maddieson2013.CInventorySize.average n = decide (19 ≤ n ∧ n ≤ 25)
• Maddieson2013.inWALS1ABin Maddieson2013.CInventorySize.moderatelyLarge n = decide (26 ≤ n ∧ n ≤ 33)
• Maddieson2013.inWALS1ABin Maddieson2013.CInventorySize.large n = decide (34 ≤ n)

theorem Maddieson2013.english_consonants : English.Phonology.phonemeInventory.consonantCount = 27

theorem Maddieson2013.german_consonants : German.Phonology.phonemeInventory.consonantCount = 23

theorem Maddieson2013.finnish_consonants : Finnish.Phonology.phonemeInventory.consonantCount = 25

theorem Maddieson2013.turkish_consonants : Turkish.Phonology.phonemeInventory.consonantCount = 24

theorem Maddieson2013.russian_consonants : Russian.Phonology.phonemeInventory.consonantCount = 33

theorem Maddieson2013.french_consonants : French.Phonology.phonemeInventory.consonantCount = 23

theorem Maddieson2013.spanish_consonants : Spanish.Phonology.phonemeInventory.consonantCount = 20

theorem Maddieson2013.japanese_consonants : Japanese.Phonology.phonemeInventory.consonantCount = 27

theorem Maddieson2013.mandarin_consonants : Mandarin.Phonology.phonemeInventory.consonantCount = 27

theorem Maddieson2013.hindi_consonants : HindiUrdu.Phonology.phonemeInventory.consonantCount = 71

theorem Maddieson2013.georgian_consonants : Georgian.Phonology.phonemeInventory.consonantCount = 29

theorem Maddieson2013.hungarian_consonants : Hungarian.Phonology.phonemeInventory.consonantCount = 50

theorem Maddieson2013.swahili_consonants : Swahili.Phonology.phonemeInventory.consonantCount = 31

theorem Maddieson2013.yoruba_consonants : Yoruba.Phonology.phonemeInventory.consonantCount = 18

theorem Maddieson2013.maori_consonants : Maori.Phonology.phonemeInventory.consonantCount = 10

theorem Maddieson2013.zulu_consonants : Zulu.Phonology.phonemeInventory.consonantCount = 35

theorem Maddieson2013.english_phoible_in_moderatelyLarge : inWALS1ABin CInventorySize.moderatelyLarge English.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.german_phoible_in_average : inWALS1ABin CInventorySize.average German.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.finnish_phoible_in_average : inWALS1ABin CInventorySize.average Finnish.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.turkish_phoible_in_average : inWALS1ABin CInventorySize.average Turkish.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.russian_phoible_in_moderatelyLarge : inWALS1ABin CInventorySize.moderatelyLarge Russian.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.french_phoible_in_average : inWALS1ABin CInventorySize.average French.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.spanish_phoible_in_average : inWALS1ABin CInventorySize.average Spanish.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.japanese_phoible_in_moderatelyLarge : inWALS1ABin CInventorySize.moderatelyLarge Japanese.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.mandarin_phoible_in_moderatelyLarge : inWALS1ABin CInventorySize.moderatelyLarge Mandarin.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.hindi_phoible_in_large : inWALS1ABin CInventorySize.large HindiUrdu.Phonology.phonemeInventory.consonantCount = true

Hindi: PHOIBLE's "hind1269" Hindi-Urdu has 71 consonants (the breathy-aspirated × voiced/voiceless × place series produces a very large inventory) — falls in WALS large (34+).

theorem Maddieson2013.georgian_phoible_in_moderatelyLarge : inWALS1ABin CInventorySize.moderatelyLarge Georgian.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.hungarian_phoible_in_large : inWALS1ABin CInventorySize.large Hungarian.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.swahili_phoible_in_moderatelyLarge : inWALS1ABin CInventorySize.moderatelyLarge Swahili.Phonology.phonemeInventory.consonantCount = true

theorem Maddieson2013.yoruba_phoible_in_moderatelySmall : inWALS1ABin CInventorySize.moderatelySmall Yoruba.Phonology.phonemeInventory.consonantCount = true

Yoruba: 18 consonants — exceptionally small, falls in WALS moderatelySmall (15–18).

theorem Maddieson2013.maori_phoible_in_small : inWALS1ABin CInventorySize.small Maori.Phonology.phonemeInventory.consonantCount = true

Maori: 10 consonants — exceptionally small (Polynesian-typical). WALS small (6–14).

theorem Maddieson2013.zulu_phoible_in_large : inWALS1ABin CInventorySize.large Zulu.Phonology.phonemeInventory.consonantCount = true

Zulu: 35 consonants (clicks + ejectives + breathy series) puts it in WALS large (34+).

theorem Maddieson2013.batch_bin_distribution : inWALS1ABin CInventorySize.small Maori.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.moderatelySmall Yoruba.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.average German.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.average Finnish.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.average Turkish.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.average French.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.average Spanish.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.average Mandarin.Phonology.phonemeInventory.consonantCount = false ∧ inWALS1ABin CInventorySize.moderatelyLarge English.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.moderatelyLarge Japanese.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.moderatelyLarge Mandarin.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.moderatelyLarge Russian.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.moderatelyLarge Georgian.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.moderatelyLarge Swahili.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.large HindiUrdu.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.large Hungarian.Phonology.phonemeInventory.consonantCount = true ∧ inWALS1ABin CInventorySize.large Zulu.Phonology.phonemeInventory.consonantCount = true

Of the 16 PHOIBLE-canonical inventories: 1 small, 1 moderatelySmall, 6 average, 5 moderatelyLarge, 3 large. The 0 moderatelySmall finding inverts WALS Maddieson's modal-average count for the same 16 ISOs — PHOIBLE's finer transcription pulls several moderatelySmall-in-WALS languages up into average.