Cross-Linguistic Typology of Numeral Systems (WALS Chapters 53--56, 131)

@cite{aikhenvald-2000} @cite{greenberg-1978} @cite{stolz-veselinova-2013}

Typological data on four dimensions of numeral morphology and syntax, drawn from WALS chapters by Stolz & Veselinova (Ch 53) and Gil (Ch 54--56). The data covers ordinal numeral formation, distributive numerals, numeral classifiers, and the relationship between conjunctions and universal quantification.

1. Ordinal Numerals (Ch 53, Stolz & Veselinova): How ordinal numbers are formed from cardinals. The dominant cross-linguistic pattern is for "first" to be suppletive (not derived from "one") while higher ordinals are regular derivations from cardinals. This asymmetry reflects the cognitive and discourse-functional salience of first position.

2. Distributive Numerals (Ch 54, Gil): Whether a language has a dedicated morphological form for distributive numerals ("two each", "three apiece"). Reduplication of the cardinal is the most common strategy among languages that mark distributives (e.g., Turkish iki-ser 'two each', Tagalog dalawa- dalawa 'two-two'). Many languages lack a dedicated form entirely.

3. Numeral Classifiers (Ch 55, Gil): Core types and distribution data live in Phenomena.Classifiers.Typology. This file imports ClassifierStatus from there and uses it in NumeralProfile for cross-dimensional generalizations (Sanches-Slobin, areal concentration).

4. Conjunctions and Universal Quantifiers (Ch 56, Gil): Whether a language uses the same morpheme for 'and' (conjunction) and 'all' / 'every' (universal quantification). Many languages show identity between these forms, suggesting a deep semantic connection between conjunction and universal quantification (both involve exhaustive predication over a set).

theorem Phenomena.Numerals.Typology.ch53_total : Phenomena.Numerals.Typology.ch53✝.length = 321

theorem Phenomena.Numerals.Typology.ch54_total : Phenomena.Numerals.Typology.ch54✝.length = 251

theorem Phenomena.Numerals.Typology.ch55_total : Phenomena.Numerals.Typology.ch55✝.length = 400

theorem Phenomena.Numerals.Typology.ch131_total : Phenomena.Numerals.Typology.ch131✝.length = 196

inductive Phenomena.Numerals.Typology.OrdinalFormation : Type

How a language forms ordinal numerals from cardinal ones (WALS Ch 53).

The key typological variable is whether "first" is suppletive (not derived from "one") and how many of the lowest ordinals show suppletion or irregularity. The pattern "first" suppletive + higher ordinals regular is overwhelmingly dominant.

• firstSuppletion : OrdinalFormation
• firstSecondSuppletion : OrdinalFormation
• allFromCardinals : OrdinalFormation
• various : OrdinalFormation
• noOrdinals : OrdinalFormation

instance Phenomena.Numerals.Typology.instDecidableEqOrdinalFormation : DecidableEq OrdinalFormation

Equations

• Phenomena.Numerals.Typology.instDecidableEqOrdinalFormation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Numerals.Typology.instBEqOrdinalFormation.beq : OrdinalFormation → OrdinalFormation → Bool

Equations

• Phenomena.Numerals.Typology.instBEqOrdinalFormation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Numerals.Typology.instBEqOrdinalFormation : BEq OrdinalFormation

Equations

• Phenomena.Numerals.Typology.instBEqOrdinalFormation = { beq := Phenomena.Numerals.Typology.instBEqOrdinalFormation.beq }

def Phenomena.Numerals.Typology.instReprOrdinalFormation.repr : OrdinalFormation → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instReprOrdinalFormation : Repr OrdinalFormation

Equations

• Phenomena.Numerals.Typology.instReprOrdinalFormation = { reprPrec := Phenomena.Numerals.Typology.instReprOrdinalFormation.repr }

structure Phenomena.Numerals.Typology.OrdinalDistribution : Type

WALS Chapter 53 distribution: language counts per ordinal formation type. Total: 321 languages.

• firstSuppletion : ℕ
• firstSecondSuppletion : ℕ
• allFromCardinals : ℕ
• various : ℕ
• noOrdinals : ℕ

def Phenomena.Numerals.Typology.instReprOrdinalDistribution.repr : OrdinalDistribution → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instReprOrdinalDistribution : Repr OrdinalDistribution

Equations

• Phenomena.Numerals.Typology.instReprOrdinalDistribution = { reprPrec := Phenomena.Numerals.Typology.instReprOrdinalDistribution.repr }

def Phenomena.Numerals.Typology.OrdinalDistribution.total (d : OrdinalDistribution) : ℕ

Equations

• d.total = d.firstSuppletion + d.firstSecondSuppletion + d.allFromCardinals + d.various + d.noOrdinals

def Phenomena.Numerals.Typology.ch53Distribution : OrdinalDistribution

Actual WALS Ch 53 counts.

Equations

• Phenomena.Numerals.Typology.ch53Distribution = { firstSuppletion := 99, firstSecondSuppletion := 45, allFromCardinals := 28, various := 83, noOrdinals := 66 }

inductive Phenomena.Numerals.Typology.DistributiveNumeral : Type

Whether and how a language marks distributive numerals (WALS Ch 54).

Distributive numerals express "N each" or "N apiece" meanings. Languages vary in whether they have a dedicated morphological strategy and, if so, what kind. Reduplication of the cardinal numeral is the most widespread dedicated strategy (e.g., Japanese hito-ri hito-ri, Hungarian két-két).

• noDistributive : DistributiveNumeral
• markedByReduplication : DistributiveNumeral
• markedBySuffix : DistributiveNumeral
• markedByPrefix : DistributiveNumeral
• markedByOtherMeans : DistributiveNumeral

instance Phenomena.Numerals.Typology.instDecidableEqDistributiveNumeral : DecidableEq DistributiveNumeral

Equations

• Phenomena.Numerals.Typology.instDecidableEqDistributiveNumeral x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Numerals.Typology.instBEqDistributiveNumeral.beq : DistributiveNumeral → DistributiveNumeral → Bool

Equations

• Phenomena.Numerals.Typology.instBEqDistributiveNumeral.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Numerals.Typology.instBEqDistributiveNumeral : BEq DistributiveNumeral

Equations

• Phenomena.Numerals.Typology.instBEqDistributiveNumeral = { beq := Phenomena.Numerals.Typology.instBEqDistributiveNumeral.beq }

instance Phenomena.Numerals.Typology.instReprDistributiveNumeral : Repr DistributiveNumeral

Equations

• Phenomena.Numerals.Typology.instReprDistributiveNumeral = { reprPrec := Phenomena.Numerals.Typology.instReprDistributiveNumeral.repr }

def Phenomena.Numerals.Typology.instReprDistributiveNumeral.repr : DistributiveNumeral → ℕ → Std.Format

Equations

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

structure Phenomena.Numerals.Typology.DistributiveDistribution : Type

WALS Chapter 54 distribution: language counts per distributive type. Total: 251 languages.

• noDistributive : ℕ
• reduplication : ℕ
• suffixCount : ℕ
• prefixCount : ℕ
• otherMeans : ℕ

instance Phenomena.Numerals.Typology.instReprDistributiveDistribution : Repr DistributiveDistribution

Equations

• Phenomena.Numerals.Typology.instReprDistributiveDistribution = { reprPrec := Phenomena.Numerals.Typology.instReprDistributiveDistribution.repr }

def Phenomena.Numerals.Typology.instReprDistributiveDistribution.repr : DistributiveDistribution → ℕ → Std.Format

Equations

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

def Phenomena.Numerals.Typology.DistributiveDistribution.total (d : DistributiveDistribution) : ℕ

Equations

• d.total = d.noDistributive + d.reduplication + d.suffixCount + d.prefixCount + d.otherMeans

def Phenomena.Numerals.Typology.ch54Distribution : DistributiveDistribution

Actual WALS Ch 54 counts.

Equations

• Phenomena.Numerals.Typology.ch54Distribution = { noDistributive := 63, reduplication := 85, suffixCount := 34, prefixCount := 19, otherMeans := 50 }

inductive Phenomena.Numerals.Typology.ConjunctionQuantifier : Type

The relationship between 'and' and 'all/every' in a language (WALS Ch 56).

Gil distinguishes languages where the conjunction marker and the universal quantifier share the same form (identity) from those where they are morphologically distinct (differentiation). Identity between 'and' and 'all' reflects a deep connection between conjunction (exhaustive pairing) and universal quantification (exhaustive predication).

• identity : ConjunctionQuantifier
• differentiation : ConjunctionQuantifier

instance Phenomena.Numerals.Typology.instDecidableEqConjunctionQuantifier : DecidableEq ConjunctionQuantifier

Equations

• Phenomena.Numerals.Typology.instDecidableEqConjunctionQuantifier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Numerals.Typology.instBEqConjunctionQuantifier : BEq ConjunctionQuantifier

Equations

• Phenomena.Numerals.Typology.instBEqConjunctionQuantifier = { beq := Phenomena.Numerals.Typology.instBEqConjunctionQuantifier.beq }

def Phenomena.Numerals.Typology.instBEqConjunctionQuantifier.beq : ConjunctionQuantifier → ConjunctionQuantifier → Bool

Equations

• Phenomena.Numerals.Typology.instBEqConjunctionQuantifier.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Numerals.Typology.instReprConjunctionQuantifier.repr : ConjunctionQuantifier → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instReprConjunctionQuantifier : Repr ConjunctionQuantifier

Equations

• Phenomena.Numerals.Typology.instReprConjunctionQuantifier = { reprPrec := Phenomena.Numerals.Typology.instReprConjunctionQuantifier.repr }

structure Phenomena.Numerals.Typology.ConjQuantDistribution : Type

WALS Chapter 56 distribution: language counts per conjunction-quantifier type. Total: 220 languages.

• identity : ℕ
• differentiation : ℕ

instance Phenomena.Numerals.Typology.instReprConjQuantDistribution : Repr ConjQuantDistribution

Equations

• Phenomena.Numerals.Typology.instReprConjQuantDistribution = { reprPrec := Phenomena.Numerals.Typology.instReprConjQuantDistribution.repr }

def Phenomena.Numerals.Typology.instReprConjQuantDistribution.repr : ConjQuantDistribution → ℕ → Std.Format

Equations

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

def Phenomena.Numerals.Typology.ConjQuantDistribution.total (d : ConjQuantDistribution) : ℕ

Equations

• d.total = d.identity + d.differentiation

def Phenomena.Numerals.Typology.ch56Distribution : ConjQuantDistribution

Actual WALS Ch 56 counts.

Equations

• Phenomena.Numerals.Typology.ch56Distribution = { identity := 43, differentiation := 177 }

inductive Phenomena.Numerals.Typology.Region : Type

Areal region, used for areal generalizations about classifier distribution.

• europe : Region
• eastAsia : Region
• southeastAsia : Region
• southAsia : Region
• centralAsia : Region
• westAsia : Region
• africa : Region
• northAmerica : Region
• mesoamerica : Region
• southAmerica : Region
• oceania : Region

instance Phenomena.Numerals.Typology.instDecidableEqRegion : DecidableEq Region

Equations

• Phenomena.Numerals.Typology.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Numerals.Typology.instBEqRegion : BEq Region

Equations

• Phenomena.Numerals.Typology.instBEqRegion = { beq := Phenomena.Numerals.Typology.instBEqRegion.beq }

def Phenomena.Numerals.Typology.instBEqRegion.beq : Region → Region → Bool

Equations

• Phenomena.Numerals.Typology.instBEqRegion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Numerals.Typology.instReprRegion : Repr Region

Equations

• Phenomena.Numerals.Typology.instReprRegion = { reprPrec := Phenomena.Numerals.Typology.instReprRegion.repr }

def Phenomena.Numerals.Typology.instReprRegion.repr : Region → ℕ → Std.Format

Equations

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

inductive Phenomena.Numerals.Typology.PluralMarking : Type

Whether a language has obligatory grammatical plural marking on common nouns. Used for the Sanches-Slobin generalization relating classifiers and plural.

• obligatory : PluralMarking
• optional : PluralMarking
• none : PluralMarking

instance Phenomena.Numerals.Typology.instDecidableEqPluralMarking : DecidableEq PluralMarking

Equations

• Phenomena.Numerals.Typology.instDecidableEqPluralMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Numerals.Typology.instBEqPluralMarking : BEq PluralMarking

Equations

• Phenomena.Numerals.Typology.instBEqPluralMarking = { beq := Phenomena.Numerals.Typology.instBEqPluralMarking.beq }

def Phenomena.Numerals.Typology.instBEqPluralMarking.beq : PluralMarking → PluralMarking → Bool

Equations

• Phenomena.Numerals.Typology.instBEqPluralMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Numerals.Typology.instReprPluralMarking.repr : PluralMarking → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instReprPluralMarking : Repr PluralMarking

Equations

• Phenomena.Numerals.Typology.instReprPluralMarking = { reprPrec := Phenomena.Numerals.Typology.instReprPluralMarking.repr }

inductive Phenomena.Numerals.Typology.NumeralBase : Type

The base of a language's numeral system (WALS Ch 131, Comrie).

Most languages worldwide use a decimal (base-10) system. Vigesimal (base-20) systems are the most common alternative, concentrated in Mesoamerica, West Africa, and the Caucasus. Many "vigesimal" systems are actually hybrid, using base-20 for higher numerals and base-10 within each score.

• decimal : NumeralBase
• vigesimal : NumeralBase
• hybridVigesimalDecimal : NumeralBase
• otherBase : NumeralBase
• bodyPartSystem : NumeralBase
• restricted : NumeralBase

instance Phenomena.Numerals.Typology.instDecidableEqNumeralBase : DecidableEq NumeralBase

Equations

• Phenomena.Numerals.Typology.instDecidableEqNumeralBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Numerals.Typology.instBEqNumeralBase : BEq NumeralBase

Equations

• Phenomena.Numerals.Typology.instBEqNumeralBase = { beq := Phenomena.Numerals.Typology.instBEqNumeralBase.beq }

def Phenomena.Numerals.Typology.instBEqNumeralBase.beq : NumeralBase → NumeralBase → Bool

Equations

• Phenomena.Numerals.Typology.instBEqNumeralBase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Numerals.Typology.instReprNumeralBase.repr : NumeralBase → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instReprNumeralBase : Repr NumeralBase

Equations

• Phenomena.Numerals.Typology.instReprNumeralBase = { reprPrec := Phenomena.Numerals.Typology.instReprNumeralBase.repr }

structure Phenomena.Numerals.Typology.NumeralProfile : Type

A language's numeral typology profile across all four WALS dimensions.

• language : String
• iso : String

  ISO 639-3 code

• ordinal : OrdinalFormation

  Ch 53: Ordinal numeral formation

• distributive : DistributiveNumeral

  Ch 54: Distributive numeral marking

• classifier : Classifiers.Typology.ClassifierStatus

  Ch 55: Numeral classifier status

• conjQuant : ConjunctionQuantifier

  Ch 56: Conjunction-quantifier relationship

• region : Region

  Areal region (for areal generalizations)

• pluralMarking : PluralMarking

  Plural marking on common nouns (for Sanches-Slobin)

• numeralBase : Option NumeralBase

  Ch 131: Numeral base (optional; not all languages surveyed).

instance Phenomena.Numerals.Typology.instReprNumeralProfile : Repr NumeralProfile

Equations

• Phenomena.Numerals.Typology.instReprNumeralProfile = { reprPrec := Phenomena.Numerals.Typology.instReprNumeralProfile.repr }

def Phenomena.Numerals.Typology.instReprNumeralProfile.repr : NumeralProfile → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instBEqNumeralProfile : BEq NumeralProfile

Equations

• Phenomena.Numerals.Typology.instBEqNumeralProfile = { beq := Phenomena.Numerals.Typology.instBEqNumeralProfile.beq }

def Phenomena.Numerals.Typology.instBEqNumeralProfile.beq : NumeralProfile → NumeralProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Numerals.Typology.instBEqNumeralProfile.beq x✝¹ x✝ = false

instance Phenomena.Numerals.Typology.instDecidableEqNumeralProfile : DecidableEq NumeralProfile

Equations

• Phenomena.Numerals.Typology.instDecidableEqNumeralProfile = Phenomena.Numerals.Typology.instDecidableEqNumeralProfile.decEq

def Phenomena.Numerals.Typology.instDecidableEqNumeralProfile.decEq (x✝ x✝¹ : NumeralProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Numerals.Typology.english : NumeralProfile

English: "first" is suppletive (not *one-th), "second" is suppletive (not *two-th), higher ordinals regular (-th suffix). No morphological distributive numerals (*two-each), no numeral classifiers, and conjunction 'and' differs from universal quantifier 'all'. Obligatory plural on nouns.

Equations

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

def Phenomena.Numerals.Typology.mandarin : NumeralProfile

Mandarin Chinese: ordinals formed regularly with di- prefix (di-yi 'first', di-er 'second', etc.) --- no suppletion. No morphological distributive. Obligatory numeral classifiers (san ge ren 'three CL person'). Conjunction 'he' and universal 'dou' are different morphemes, but 'dou' shows quantificational force in both contexts. No grammatical plural on nouns.

Equations

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

def Phenomena.Numerals.Typology.japanese : NumeralProfile

Japanese: ordinals formed with -banme suffix (ichi-banme 'first', ni-banme 'second'). No suppletion. Distributive by reduplication (hitori-hitori 'one by one'). Obligatory numeral classifiers (san-nin 'three-CL.person', ni-hon 'two-CL.long.thing'). Conjunction 'to' differs from universal 'subete'. No grammatical plural on common nouns.

Equations

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

def Phenomena.Numerals.Typology.thai : NumeralProfile

Thai: ordinals formed with thi- prefix (thi-nung 'first', thi-song 'second') --- all regular from cardinals. No morphological distributive. Obligatory numeral classifiers (maa sam tua 'dog three CL.animal'). No grammatical plural on nouns.

Equations

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

def Phenomena.Numerals.Typology.vietnamese : NumeralProfile

Vietnamese: ordinals formed with thu prefix (thu nhat 'first', thu hai 'second') --- regular from cardinals. No morphological distributive. Obligatory classifiers (ba con meo 'three CL cat'). No grammatical plural on nouns.

Equations

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

def Phenomena.Numerals.Typology.turkish : NumeralProfile

Turkish: "birinci" 'first' derived regularly from "bir" 'one' via -inci suffix (all ordinals formed by -inci or -unci suffix). Distributive numerals by suffix -er or -ar (iki-ser 'two each'). No obligatory numeral classifiers, but optional classifiers exist (iki tane kitap 'two CL book'). 'Ve' (and) differs from 'hepsi' or 'butun' (all). Obligatory plural with -ler or -lar.

Equations

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

def Phenomena.Numerals.Typology.korean : NumeralProfile

Korean: ordinals use native Korean numerals + -jjae suffix (cheot-jjae 'first' partially suppletive). Distributive by suffix -ssik (du-ssik 'two each'). Optional numeral classifiers (se myeong-ui haksaeng 'three CL student'). 'Gwa/wa' (and) differs from 'modu' (all). Optional plural marking with -deul.

Equations

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

def Phenomena.Numerals.Typology.hindi : NumeralProfile

Hindi: ordinals show "first" (pehla) suppletive, higher ordinals regular with -vam suffix (dusra 'second' also partially suppletive). Distributive by reduplication (do-do 'two-two'). No numeral classifiers. 'Aur' (and) differs from 'sab' (all). Obligatory plural marking.

Equations

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

def Phenomena.Numerals.Typology.bengali : NumeralProfile

Bengali: ordinals formed with -tho suffix, but "first" (prothom) is suppletive. Distributive by reduplication. Optional classifiers (tin-ta boi 'three-CL book', but bare tin boi also grammatical). 'Ebong' (and) differs from 'sob' (all). Optional plural.

Equations

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

def Phenomena.Numerals.Typology.burmese : NumeralProfile

Burmese: ordinals formed regularly with prefix (pa-hta-ma 'first' from inherited Pali, but modern ordinals use prefix tha-). Numeral classifiers obligatory (lu thon yauk 'person three CL'). No morphological distributive form. No grammatical plural on nouns.

Equations

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

def Phenomena.Numerals.Typology.hungarian : NumeralProfile

Hungarian: "first" (elso) is suppletive, higher ordinals regular with -dik suffix (masodik 'second', harmadik 'third'). Distributive by reduplication (ket-ket 'two-two'). No numeral classifiers. 'Es' (and) differs from 'minden' (all/every). Obligatory plural with -k.

Equations

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

def Phenomena.Numerals.Typology.russian : NumeralProfile

Russian: "first" (pervyj) is suppletive, "second" (vtoroj) also suppletive, higher ordinals from cardinals with suffix (tretij 'third', chetvertyj 'fourth'). No morphological distributive (uses prepositional phrase 'po + dative'). No numeral classifiers. 'I' (and) differs from 'vse' (all). Obligatory plural marking.

Equations

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

def Phenomena.Numerals.Typology.yoruba : NumeralProfile

Yoruba: ordinals formed with -(i)keji prefix system, varying patterns across the paradigm. No morphological distributive. No numeral classifiers. Conjunction 'ati' and universal quantifier 'gbogbo' are distinct. Plural marked optionally (awon).

Equations

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

def Phenomena.Numerals.Typology.swahili : NumeralProfile

Swahili: ordinals formed with -a prefix + cardinal (wa-kwanza 'first' has distinct root, but -a-pili 'second' etc. are regular). No morphological distributive. No numeral classifiers (noun class system serves a different function). 'Na' (and) differs from '-ote' (all). Obligatory plural via noun class prefixes.

Equations

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

def Phenomena.Numerals.Typology.tagalog : NumeralProfile

Tagalog: ordinals with pang- prefix (pang-una 'first' from una 'precede', pang-alawa 'second'). Distributive by reduplication (dalawa-dalawa 'two-two'). No obligatory numeral classifiers (linkers na/ng serve different function). 'At' (and) and 'lahat' (all) are differentiated. Optional plural (mga).

Equations

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

def Phenomena.Numerals.Typology.georgian : NumeralProfile

Georgian: ordinals formed with me-...-e circumfix (me-or-e 'second', me-sam-e 'third'). "First" (p'irveli) is suppletive. Distributive by suffix -agan (or-agan 'two each'). No numeral classifiers. 'Da' (and) differs from 'q'vela' (all). Obligatory plural.

Equations

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

def Phenomena.Numerals.Typology.finnish : NumeralProfile

Finnish: ordinals formed regularly with -(n)s suffix (ensimmainen 'first' is suppletive, toinen 'second' from eri 'different', kolmas 'third' etc. regular). No morphological distributive. No classifiers. 'Ja' (and) differs from 'kaikki' (all). Obligatory plural with -t.

Equations

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

def Phenomena.Numerals.Typology.tzeltal : NumeralProfile

Tzeltal (Mayan, Mesoamerica): ordinals not productively formed. Numeral classifiers obligatory (distinct from Mayan noun classifiers). No morphological distributive. Conjunction and universal quantifier are differentiated. No obligatory plural on nouns.

Equations

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

def Phenomena.Numerals.Typology.indonesian : NumeralProfile

Malay/Indonesian: ordinals with ke- prefix (ke-satu 'first' regular, pertama 'first' from Skt also used). No morphological distributive. Obligatory numeral classifiers (tiga orang murid 'three CL student'). 'Dan' (and) differs from 'semua' (all). Optional plural by reduplication.

Equations

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

def Phenomena.Numerals.Typology.allLanguages : List NumeralProfile

All language profiles in our sample.

Equations

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

theorem Phenomena.Numerals.Typology.suppletive_first_dominant : ch53Distribution.firstSuppletion + ch53Distribution.firstSecondSuppletion > ch53Distribution.allFromCardinals

Suppletive "first" is the dominant ordinal formation strategy (WALS Ch 53). Languages with suppletive "first" (alone or with suppletive "second") outnumber languages where all ordinals derive regularly from cardinals.

theorem Phenomena.Numerals.Typology.first_suppletion_most_common : ch53Distribution.firstSuppletion > ch53Distribution.firstSecondSuppletion ∧ ch53Distribution.firstSuppletion > ch53Distribution.allFromCardinals ∧ ch53Distribution.firstSuppletion > ch53Distribution.noOrdinals

"First" suppletion alone is the single most common ordinal pattern.

theorem Phenomena.Numerals.Typology.most_languages_have_ordinals : ch53Distribution.firstSuppletion + ch53Distribution.firstSecondSuppletion + ch53Distribution.allFromCardinals + ch53Distribution.various > ch53Distribution.noOrdinals * 3

Languages with some form of ordinal formation (regular or suppletive) outnumber languages lacking ordinals entirely. Most languages have ordinals.

theorem Phenomena.Numerals.Typology.distributive_majority_has_marking : ch54Distribution.reduplication + ch54Distribution.suffixCount + ch54Distribution.prefixCount + ch54Distribution.otherMeans > ch54Distribution.noDistributive

Languages with dedicated distributive numeral forms outnumber those without, but neither is a negligible minority.

theorem Phenomena.Numerals.Typology.reduplication_most_common_distributive : ch54Distribution.reduplication > ch54Distribution.suffixCount ∧ ch54Distribution.reduplication > ch54Distribution.prefixCount ∧ ch54Distribution.reduplication > ch54Distribution.otherMeans ∧ ch54Distribution.reduplication > ch54Distribution.noDistributive

Reduplication is the single most common distributive strategy, outnumbering any other individual morphological means.

theorem Phenomena.Numerals.Typology.differentiation_dominant : ch56Distribution.differentiation > ch56Distribution.identity

Differentiation between 'and' and 'all' is the dominant pattern (WALS Ch 56). Most languages use distinct morphemes for conjunction and universal quantification.

theorem Phenomena.Numerals.Typology.differentiation_supermajority : ch56Distribution.differentiation * 4 > ch56Distribution.total * 3

Differentiation accounts for more than three-quarters of the sample.

theorem Phenomena.Numerals.Typology.identity_nonnegligible : ch56Distribution.identity * 6 ≥ ch56Distribution.total

Identity between 'and' and 'all' is a non-negligible minority pattern, attested in roughly a fifth of languages (43 out of 220).

def Phenomena.Numerals.Typology.NumeralProfile.hasObligatoryClassifiers (p : NumeralProfile) : Bool

Does a language have obligatory numeral classifiers?

Equations

• p.hasObligatoryClassifiers = (p.classifier == Phenomena.Classifiers.Typology.ClassifierStatus.obligatory)

def Phenomena.Numerals.Typology.NumeralProfile.hasClassifiers (p : NumeralProfile) : Bool

Does a language have any numeral classifiers (obligatory or optional)?

Equations

• p.hasClassifiers = (p.classifier != Phenomena.Classifiers.Typology.ClassifierStatus.absent)

def Phenomena.Numerals.Typology.NumeralProfile.hasObligatoryPlural (p : NumeralProfile) : Bool

Does a language have obligatory plural marking on common nouns?

Equations

• p.hasObligatoryPlural = (p.pluralMarking == Phenomena.Numerals.Typology.PluralMarking.obligatory)

def Phenomena.Numerals.Typology.NumeralProfile.hasFirstSuppletion (p : NumeralProfile) : Bool

Does a language form "first" by suppletion?

Equations

• p.hasFirstSuppletion = (p.ordinal == Phenomena.Numerals.Typology.OrdinalFormation.firstSuppletion || p.ordinal == Phenomena.Numerals.Typology.OrdinalFormation.firstSecondSuppletion)

def Phenomena.Numerals.Typology.NumeralProfile.hasDistributive (p : NumeralProfile) : Bool

Does a language have a morphological distributive numeral form?

Equations

• p.hasDistributive = (p.distributive != Phenomena.Numerals.Typology.DistributiveNumeral.noDistributive)

def Phenomena.Numerals.Typology.NumeralProfile.isEastSoutheastAsian (p : NumeralProfile) : Bool

Is a language in the East/Southeast Asian region?

Equations

• p.isEastSoutheastAsian = (p.region == Phenomena.Numerals.Typology.Region.eastAsia || p.region == Phenomena.Numerals.Typology.Region.southeastAsia)

theorem Phenomena.Numerals.Typology.classifier_implies_no_obligatory_plural : have withObligatoryClassifiers := List.filter (fun (x : NumeralProfile) => x.hasObligatoryClassifiers) allLanguages; (withObligatoryClassifiers.all fun (p : NumeralProfile) => !p.hasObligatoryPlural) = true

Sanches-Slobin generalization: Classifier languages tend to lack obligatory plural marking on nouns. In our sample, every language with obligatory classifiers lacks obligatory plural.

The theoretical explanation: classifiers already individuate entities for counting, making obligatory plural morphology redundant.

theorem Phenomena.Numerals.Typology.obligatory_plural_implies_no_obligatory_classifier : have withObligatoryPlural := List.filter (fun (x : NumeralProfile) => x.hasObligatoryPlural) allLanguages; (withObligatoryPlural.all fun (p : NumeralProfile) => !p.hasObligatoryClassifiers) = true

Converse of Sanches-Slobin: every language in our sample with obligatory plural marking lacks obligatory classifiers. (This is the contrapositive, independently verifiable on the data.)

theorem Phenomena.Numerals.Typology.classifiers_areal_concentration : have obligatory := List.filter (fun (x : NumeralProfile) => x.hasObligatoryClassifiers) allLanguages; (obligatory.all fun (p : NumeralProfile) => p.region == Region.eastAsia || p.region == Region.southeastAsia || p.region == Region.mesoamerica) = true

Numeral classifiers concentrate in East and Southeast Asia in our sample: every obligatory-classifier language in our sample is in East Asia, Southeast Asia, or Mesoamerica.

theorem Phenomena.Numerals.Typology.eastasian_classifier_langs_regular_ordinals : have eastAsianClassifier := List.filter (fun (p : NumeralProfile) => p.isEastSoutheastAsian && p.hasObligatoryClassifiers && p.ordinal != OrdinalFormation.various) allLanguages; (eastAsianClassifier.all fun (p : NumeralProfile) => p.ordinal == OrdinalFormation.allFromCardinals) = true

In our sample, East/Southeast Asian languages with obligatory classifiers all form ordinals regularly from cardinals (no suppletion of "first"). This is consistent with the observation that agglutinative numeral morphology in these languages extends uniformly to ordinals.

theorem Phenomena.Numerals.Typology.european_first_suppletion : have european := List.filter (fun (p : NumeralProfile) => p.region == Region.europe) allLanguages; (european.all fun (x : NumeralProfile) => x.hasFirstSuppletion) = true

European languages in our sample all show suppletive "first" (either alone or with suppletive "second"). No European language in our sample derives "first" regularly from "one".

theorem Phenomena.Numerals.Typology.japanese_has_both_classifier_and_distributive : (japanese.hasObligatoryClassifiers && decide (japanese.hasDistributive = true)) = true

Japanese is a notable exception to any strict complementarity between obligatory classifiers and distributive morphology: it has both obligatory classifiers and distributive-by-reduplication (hito-ri hito-ri).

theorem Phenomena.Numerals.Typology.most_obligatory_classifier_no_distributive : have obligCl := List.filter (fun (x : NumeralProfile) => x.hasObligatoryClassifiers) allLanguages; have withoutDist := List.filter (fun (p : NumeralProfile) => !p.hasDistributive) obligCl; withoutDist.length > obligCl.length / 2

In our sample, the majority of obligatory-classifier languages lack morphological distributive forms. Japanese is the sole exception.

inductive Phenomena.Numerals.Typology.SuppletionCutoff : Type

@cite{greenberg-1978}'s implicational universal for ordinal suppletion: if a language has a suppletive ordinal for numeral N, then it has suppletive ordinals for all numerals less than N. Equivalently: suppletion cuts off at some point in the sequence 1st, 2nd, 3rd,... and all ordinals above the cutoff are regular.

The WALS data captures the coarsest version: suppletion is most likely for "first", less likely for "second", and rare beyond that. Our inductive type captures three attested cutoff points (none, first-only, first+second).

• none : SuppletionCutoff
• first : SuppletionCutoff
• firstAndSecond : SuppletionCutoff

instance Phenomena.Numerals.Typology.instDecidableEqSuppletionCutoff : DecidableEq SuppletionCutoff

Equations

• Phenomena.Numerals.Typology.instDecidableEqSuppletionCutoff x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Numerals.Typology.instBEqSuppletionCutoff.beq : SuppletionCutoff → SuppletionCutoff → Bool

Equations

• Phenomena.Numerals.Typology.instBEqSuppletionCutoff.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Numerals.Typology.instBEqSuppletionCutoff : BEq SuppletionCutoff

Equations

• Phenomena.Numerals.Typology.instBEqSuppletionCutoff = { beq := Phenomena.Numerals.Typology.instBEqSuppletionCutoff.beq }

def Phenomena.Numerals.Typology.instReprSuppletionCutoff.repr : SuppletionCutoff → ℕ → Std.Format

Equations

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

instance Phenomena.Numerals.Typology.instReprSuppletionCutoff : Repr SuppletionCutoff

Equations

• Phenomena.Numerals.Typology.instReprSuppletionCutoff = { reprPrec := Phenomena.Numerals.Typology.instReprSuppletionCutoff.repr }

def Phenomena.Numerals.Typology.SuppletionCutoff.rank : SuppletionCutoff → ℕ

Numeric rank for the suppletion cutoff (higher = more suppletion).

Equations

• Phenomena.Numerals.Typology.SuppletionCutoff.none.rank = 0
• Phenomena.Numerals.Typology.SuppletionCutoff.first.rank = 1
• Phenomena.Numerals.Typology.SuppletionCutoff.firstAndSecond.rank = 2

def Phenomena.Numerals.Typology.OrdinalFormation.suppletionCutoff : OrdinalFormation → Option SuppletionCutoff

Map ordinal formation type to suppletion cutoff. Languages with 'various' or 'no ordinals' patterns are excluded from the hierarchy.

Equations

• Phenomena.Numerals.Typology.OrdinalFormation.allFromCardinals.suppletionCutoff = some Phenomena.Numerals.Typology.SuppletionCutoff.none
• Phenomena.Numerals.Typology.OrdinalFormation.firstSuppletion.suppletionCutoff = some Phenomena.Numerals.Typology.SuppletionCutoff.first
• Phenomena.Numerals.Typology.OrdinalFormation.firstSecondSuppletion.suppletionCutoff = some Phenomena.Numerals.Typology.SuppletionCutoff.firstAndSecond
• Phenomena.Numerals.Typology.OrdinalFormation.various.suppletionCutoff = none
• Phenomena.Numerals.Typology.OrdinalFormation.noOrdinals.suppletionCutoff = none

theorem Phenomena.Numerals.Typology.suppletion_hierarchy_ordering : SuppletionCutoff.none.rank < SuppletionCutoff.first.rank ∧ SuppletionCutoff.first.rank < SuppletionCutoff.firstAndSecond.rank

The hierarchy is consistent: rank of each cutoff increases monotonically.

theorem Phenomena.Numerals.Typology.suppletion_frequency_matches_hierarchy : ch53Distribution.firstSuppletion > ch53Distribution.firstSecondSuppletion ∧ ch53Distribution.firstSecondSuppletion > ch53Distribution.allFromCardinals

In our sample, the WALS aggregate confirms the hierarchy: languages with "first"-only suppletion are more numerous than those with "first+second" suppletion, which in turn are more numerous than those with no suppletion at all. This reflects the implicational scale: suppletion at higher numerals is rarer.

theorem Phenomena.Numerals.Typology.english_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "eng") = some english.ordinal

theorem Phenomena.Numerals.Typology.bengali_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "ben") = some bengali.ordinal

theorem Phenomena.Numerals.Typology.burmese_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "brm") = some burmese.ordinal

theorem Phenomena.Numerals.Typology.finnish_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "fin") = some finnish.ordinal

theorem Phenomena.Numerals.Typology.georgian_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "geo") = some georgian.ordinal

theorem Phenomena.Numerals.Typology.japanese_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "jpn") = some japanese.ordinal

theorem Phenomena.Numerals.Typology.mandarin_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "mnd") = some mandarin.ordinal

theorem Phenomena.Numerals.Typology.russian_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "rus") = some russian.ordinal

theorem Phenomena.Numerals.Typology.indonesian_ch53 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ x.value) (Core.WALS.F53A.lookup "ind") = some indonesian.ordinal

theorem Phenomena.Numerals.Typology.english_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "eng") = some english.distributive

theorem Phenomena.Numerals.Typology.bengali_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "ben") = some bengali.distributive

theorem Phenomena.Numerals.Typology.finnish_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "fin") = some finnish.distributive

theorem Phenomena.Numerals.Typology.hindi_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "hin") = some hindi.distributive

theorem Phenomena.Numerals.Typology.hungarian_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "hun") = some hungarian.distributive

theorem Phenomena.Numerals.Typology.indonesian_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "ind") = some indonesian.distributive

theorem Phenomena.Numerals.Typology.korean_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "kor") = some korean.distributive

theorem Phenomena.Numerals.Typology.mandarin_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "mnd") = some mandarin.distributive

theorem Phenomena.Numerals.Typology.thai_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "tha") = some thai.distributive

theorem Phenomena.Numerals.Typology.turkish_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "tur") = some turkish.distributive

theorem Phenomena.Numerals.Typology.vietnamese_ch54 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ x.value) (Core.WALS.F54A.lookup "vie") = some vietnamese.distributive

theorem Phenomena.Numerals.Typology.english_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "eng") = some english.classifier

theorem Phenomena.Numerals.Typology.burmese_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "brm") = some burmese.classifier

theorem Phenomena.Numerals.Typology.finnish_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "fin") = some finnish.classifier

theorem Phenomena.Numerals.Typology.georgian_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "geo") = some georgian.classifier

theorem Phenomena.Numerals.Typology.hindi_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "hin") = some hindi.classifier

theorem Phenomena.Numerals.Typology.japanese_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "jpn") = some japanese.classifier

theorem Phenomena.Numerals.Typology.mandarin_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "mnd") = some mandarin.classifier

theorem Phenomena.Numerals.Typology.russian_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "rus") = some russian.classifier

theorem Phenomena.Numerals.Typology.swahili_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "swa") = some swahili.classifier

theorem Phenomena.Numerals.Typology.tagalog_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "tag") = some tagalog.classifier

theorem Phenomena.Numerals.Typology.thai_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "tha") = some thai.classifier

theorem Phenomena.Numerals.Typology.tzeltal_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "tze") = some tzeltal.classifier

theorem Phenomena.Numerals.Typology.turkish_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "tur") = some turkish.classifier

theorem Phenomena.Numerals.Typology.vietnamese_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "vie") = some vietnamese.classifier

theorem Phenomena.Numerals.Typology.yoruba_ch55 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A x.value) (Core.WALS.F55A.lookup "yor") = some yoruba.classifier

theorem Phenomena.Numerals.Typology.english_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "eng") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.japanese_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "jpn") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.mandarin_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "mnd") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.hindi_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "hin") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.russian_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "rus") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.finnish_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "fin") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.turkish_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "tur") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.hungarian_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "hun") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.korean_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "kor") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.thai_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "tha") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.vietnamese_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "vie") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.indonesian_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "ind") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.swahili_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "swa") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.burmese_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "brm") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.tagalog_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "tag") = some NumeralBase.decimal

theorem Phenomena.Numerals.Typology.georgian_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "geo") = some NumeralBase.hybridVigesimalDecimal

theorem Phenomena.Numerals.Typology.yoruba_ch131 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ x.value) (Core.WALS.F131A.lookup "yor") = some NumeralBase.vigesimal

theorem Phenomena.Numerals.Typology.ch53_firstSuppletion_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ d.value == OrdinalFormation.firstSuppletion) Phenomena.Numerals.Typology.ch53✝).length = 122

Ch 53 distribution from WALS data: firstSuppletion count (WALS "First, two-th, three-th" + "First, two, three" both map to firstSuppletion).

theorem Phenomena.Numerals.Typology.ch53_firstSecondSuppletion_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ d.value == OrdinalFormation.firstSecondSuppletion) Phenomena.Numerals.Typology.ch53✝).length = 61

theorem Phenomena.Numerals.Typology.ch53_allFromCardinals_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ d.value == OrdinalFormation.allFromCardinals) Phenomena.Numerals.Typology.ch53✝).length = 41

theorem Phenomena.Numerals.Typology.ch53_noOrdinals_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ d.value == OrdinalFormation.noOrdinals) Phenomena.Numerals.Typology.ch53✝).length = 33

theorem Phenomena.Numerals.Typology.ch53_various_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F53A.OrdinalNumerals) => Phenomena.Numerals.Typology.fromWALS53A✝ d.value == OrdinalFormation.various) Phenomena.Numerals.Typology.ch53✝).length = 64

theorem Phenomena.Numerals.Typology.ch53_exhaustive : 122 + 61 + 41 + 33 + 64 = Phenomena.Numerals.Typology.ch53✝.length

Ch 53: Mapped categories are exhaustive — all 321 languages are accounted for.

theorem Phenomena.Numerals.Typology.ch54_reduplication_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ d.value == DistributiveNumeral.markedByReduplication) Phenomena.Numerals.Typology.ch54✝).length = 85

Ch 54 distribution from WALS data: reduplication is the most common strategy.

theorem Phenomena.Numerals.Typology.ch54_noDistributive_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ d.value == DistributiveNumeral.noDistributive) Phenomena.Numerals.Typology.ch54✝).length = 62

theorem Phenomena.Numerals.Typology.ch54_suffix_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ d.value == DistributiveNumeral.markedBySuffix) Phenomena.Numerals.Typology.ch54✝).length = 32

theorem Phenomena.Numerals.Typology.ch54_prefix_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ d.value == DistributiveNumeral.markedByPrefix) Phenomena.Numerals.Typology.ch54✝).length = 23

theorem Phenomena.Numerals.Typology.ch54_otherMeans_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F54A.DistributiveNumerals) => Phenomena.Numerals.Typology.fromWALS54A✝ d.value == DistributiveNumeral.markedByOtherMeans) Phenomena.Numerals.Typology.ch54✝).length = 49

theorem Phenomena.Numerals.Typology.ch54_exhaustive : 85 + 62 + 32 + 23 + 49 = Phenomena.Numerals.Typology.ch54✝.length

Ch 54: Mapped categories are exhaustive — all 251 languages are accounted for.

theorem Phenomena.Numerals.Typology.ch55_absent_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A d.value == Classifiers.Typology.ClassifierStatus.absent) Phenomena.Numerals.Typology.ch55✝).length = Classifiers.Typology.ch55Distribution.absent

Ch 55 distribution from WALS data: all three categories match exactly.

theorem Phenomena.Numerals.Typology.ch55_optional_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A d.value == Classifiers.Typology.ClassifierStatus.optional) Phenomena.Numerals.Typology.ch55✝).length = Classifiers.Typology.ch55Distribution.optional

theorem Phenomena.Numerals.Typology.ch55_obligatory_count : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F55A.NumeralClassifiers) => Classifiers.Typology.fromWALS55A d.value == Classifiers.Typology.ClassifierStatus.obligatory) Phenomena.Numerals.Typology.ch55✝).length = Classifiers.Typology.ch55Distribution.obligatory

theorem Phenomena.Numerals.Typology.ch131_decimal_dominant : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ d.value == NumeralBase.decimal) Phenomena.Numerals.Typology.ch131✝).length > Phenomena.Numerals.Typology.ch131✝¹.length / 2

Ch 131: Decimal is the dominant numeral base worldwide.

theorem Phenomena.Numerals.Typology.ch131_vigesimal_nonnegligible : (List.filter (fun (d : Core.WALS.Datapoint Core.WALS.F131A.NumeralBases) => Phenomena.Numerals.Typology.fromWALS131A✝ d.value == NumeralBase.vigesimal || Phenomena.Numerals.Typology.fromWALS131A✝¹ d.value == NumeralBase.hybridVigesimalDecimal) Phenomena.Numerals.Typology.ch131✝).length > 20

Ch 131: Pure vigesimal and hybrid vigesimal-decimal together.