Numeral typology — substrate types and WALS data

@cite{wals-2013} (Chs 53, 54, 55, 56, 131) @cite{aikhenvald-2000} @cite{greenberg-1978} @cite{stolz-veselinova-2013}

Type-level enums + per-language profile struct for numeral systems across @cite{wals-2013} chapters 53–56 (Gil, Comrie) and 131: ordinal formation, distributive numerals, numeral classifiers, conjunction-quantifier identity, numeral base. Plus WALS distribution data, the principal cross-linguistic generalizations, and the Greenberg suppletion hierarchy for ordinal formation.

ClassifierStatus (WALS Ch 55) and fromWALS55A live in Typology/ClassifierSystem.lean and are re-imported here.

Schema

• OrdinalFormation (Ch 53): ordinal numeral formation
• DistributiveNumeral (Ch 54): distributive marking strategy
• ConjunctionQuantifier (Ch 56): identity of 'and' and 'all'
• Region: areal grouping (for cross-linguistic generalizations)
• PluralMarking: nominal plural status (Sanches-Slobin)
• NumeralBase (Ch 131): decimal/vigesimal/etc.
• NumeralProfile: per-language bundle

Per-language data lives in Fragments/{Lang}/Numerals.lean.

inductive Typology.OrdinalFormation : Type

WALS Ch 53: how a language forms ordinal numerals from cardinals. The dominant pattern is "first" suppletive + higher ordinals regular.

• firstSuppletion : OrdinalFormation

  "first" is suppletive, "second" onward regular (e.g., English).

• firstSecondSuppletion : OrdinalFormation

  "first" and "second" suppletive, "third" onward regular.

• allFromCardinals : OrdinalFormation

  All ordinals derived regularly from cardinals.

• various : OrdinalFormation

  Mixed strategies, no single dominant pattern.

• noOrdinals : OrdinalFormation

  No productive ordinal formation reported.

@[implicit_reducible]

instance Typology.instDecidableEqOrdinalFormation : DecidableEq OrdinalFormation

Equations

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

@[implicit_reducible]

instance Typology.instReprOrdinalFormation : Repr OrdinalFormation

Equations

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

def Typology.instReprOrdinalFormation.repr : OrdinalFormation → Nat → Std.Format

Equations

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

inductive Typology.DistributiveNumeral : Type

WALS Ch 54: whether and how a language marks distributive numerals ("N each" / "N apiece"). Reduplication is the most widespread dedicated strategy.

• noDistributive : DistributiveNumeral

  No dedicated distributive numeral form.

• markedByReduplication : DistributiveNumeral

  Cardinal is reduplicated (e.g., Turkish iki-şer, Tagalog dalawa-dalawa).

• markedBySuffix : DistributiveNumeral

  Suffix creates distributive (e.g., Georgian -agan).

• markedByPrefix : DistributiveNumeral

  Prefix creates distributive.

• markedByOtherMeans : DistributiveNumeral

  Other strategies (particles, circumfix, etc.).

@[implicit_reducible]

instance Typology.instDecidableEqDistributiveNumeral : DecidableEq DistributiveNumeral

Equations

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

@[implicit_reducible]

instance Typology.instReprDistributiveNumeral : Repr DistributiveNumeral

Equations

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

def Typology.instReprDistributiveNumeral.repr : DistributiveNumeral → Nat → Std.Format

Equations

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

inductive Typology.ConjunctionQuantifier : Type

WALS Ch 56 (Gil): relationship between 'and' and 'all/every'. Identity reflects a deep connection between conjunction (exhaustive pairing) and universal quantification (exhaustive predication).

• identity : ConjunctionQuantifier

  Same morpheme for 'and' and 'all' (e.g., Mandarin dou, Tagalog lahat).

• differentiation : ConjunctionQuantifier

  Different morphemes (e.g., English and/all, Japanese to/subete).

@[implicit_reducible]

instance Typology.instDecidableEqConjunctionQuantifier : DecidableEq ConjunctionQuantifier

Equations

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

@[implicit_reducible]

instance Typology.instReprConjunctionQuantifier : Repr ConjunctionQuantifier

Equations

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

def Typology.instReprConjunctionQuantifier.repr : ConjunctionQuantifier → Nat → Std.Format

Equations

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

inductive Typology.Region : Type

Areal region — used for areal generalizations about classifier distribution (e.g., Sanches-Slobin's classifier-belt observation).

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

@[implicit_reducible]

instance Typology.instDecidableEqRegion : DecidableEq Region

Equations

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

@[implicit_reducible]

instance Typology.instReprRegion : Repr Region

Equations

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

def Typology.instReprRegion.repr : Region → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Typology.instReprRegion.repr Typology.Region.europe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.europe")).group prec✝
• Typology.instReprRegion.repr Typology.Region.eastAsia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.eastAsia")).group prec✝
• Typology.instReprRegion.repr Typology.Region.southAsia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.southAsia")).group prec✝
• Typology.instReprRegion.repr Typology.Region.centralAsia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.centralAsia")).group prec✝
• Typology.instReprRegion.repr Typology.Region.westAsia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.westAsia")).group prec✝
• Typology.instReprRegion.repr Typology.Region.africa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.africa")).group prec✝
• Typology.instReprRegion.repr Typology.Region.northAmerica prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.northAmerica")).group prec✝
• Typology.instReprRegion.repr Typology.Region.mesoamerica prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.mesoamerica")).group prec✝
• Typology.instReprRegion.repr Typology.Region.southAmerica prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.southAmerica")).group prec✝
• Typology.instReprRegion.repr Typology.Region.oceania prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Typology.Region.oceania")).group prec✝

inductive Typology.PluralMarking : Type

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

• obligatory : PluralMarking

  Plural marking required (e.g., English, Spanish).

• optional : PluralMarking

  Plural marking available but not required (e.g., Korean).

• none : PluralMarking

  No grammatical plural on nouns (e.g., Mandarin, Japanese).

@[implicit_reducible]

instance Typology.instDecidableEqPluralMarking : DecidableEq PluralMarking

Equations

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

def Typology.instReprPluralMarking.repr : PluralMarking → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprPluralMarking : Repr PluralMarking

Equations

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

inductive Typology.NumeralBase : Type

WALS Ch 131 (Comrie): the base of a language's numeral system. Most languages use a decimal (base-10) system.

• decimal : NumeralBase

  Base 10 (e.g., English, Mandarin, Swahili).

• vigesimal : NumeralBase

  Pure base 20 (e.g., Ainu, Chukchi).

• hybridVigesimalDecimal : NumeralBase

  Mixed base-20 / base-10 (e.g., French, Basque, Georgian).

• otherBase : NumeralBase

  Base 5, 6, or other (rare).

• bodyPartSystem : NumeralBase

  Extended body-part counting system (e.g., Eipo).

• restricted : NumeralBase

  Restricted numeral system (few numerals, no productive base).

@[implicit_reducible]

instance Typology.instDecidableEqNumeralBase : DecidableEq NumeralBase

Equations

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

def Typology.instReprNumeralBase.repr : NumeralBase → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprNumeralBase : Repr NumeralBase

Equations

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

structure Typology.NumeralProfile : Type

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

• areal region + plural-marking status.

• language : String
• iso : String

  ISO 639-3 code.

• ordinal : OrdinalFormation

  Ch 53: ordinal numeral formation.

• distributive : DistributiveNumeral

  Ch 54: distributive numeral marking.

• classifier : 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).

@[implicit_reducible]

instance Typology.instReprNumeralProfile : Repr NumeralProfile

Equations

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

def Typology.instReprNumeralProfile.repr : NumeralProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instDecidableEqNumeralProfile : DecidableEq NumeralProfile

Equations

• Typology.instDecidableEqNumeralProfile = Typology.instDecidableEqNumeralProfile.decEq

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

Equations

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

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

Does a language have obligatory numeral classifiers?

Equations

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

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

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

Equations

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

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

Does a language have obligatory plural marking on common nouns?

Equations

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

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

Does a language form "first" by suppletion?

Equations

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

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

Does a language have a morphological distributive numeral form?

Equations

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

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

Is a language in the East/Southeast Asian region?

Equations

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

def Typology.fromWALS53A : Data.WALS.F53A.OrdinalNumerals → OrdinalFormation

Convert WALS 53A ordinal numeral values to the substrate enum. WALS distinguishes eight subtypes; we collapse them into five categories. "First, two-th, three-th" and "First, two, three" both map to firstSuppletion (only "first" suppletive). "One, two, three" and "First/one-th, …" map to various.

Equations

• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.none = Typology.OrdinalFormation.noOrdinals
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.oneTwoThree = Typology.OrdinalFormation.various
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.firstTwoThree = Typology.OrdinalFormation.firstSuppletion
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.oneThTwoThThreeTh = Typology.OrdinalFormation.allFromCardinals
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.firstOneThTwoThThreeTh = Typology.OrdinalFormation.various
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.firstTwoThThreeTh = Typology.OrdinalFormation.firstSuppletion
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.firstSecondThreeTh = Typology.OrdinalFormation.firstSecondSuppletion
• Typology.fromWALS53A Data.WALS.F53A.OrdinalNumerals.various = Typology.OrdinalFormation.various

def Typology.fromWALS54A : Data.WALS.F54A.DistributiveNumerals → DistributiveNumeral

Convert WALS 54A distributive numeral values to the substrate enum. Word-level and mixed strategies collapse into markedByOtherMeans.

Equations

• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.noDistributiveNumerals = Typology.DistributiveNumeral.noDistributive
• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.markedByReduplication = Typology.DistributiveNumeral.markedByReduplication
• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.markedByPrefix = Typology.DistributiveNumeral.markedByPrefix
• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.markedBySuffix = Typology.DistributiveNumeral.markedBySuffix
• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.markedByPrecedingWord = Typology.DistributiveNumeral.markedByOtherMeans
• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.markedByFollowingWord = Typology.DistributiveNumeral.markedByOtherMeans
• Typology.fromWALS54A Data.WALS.F54A.DistributiveNumerals.markedByMixedOrOtherStrategies = Typology.DistributiveNumeral.markedByOtherMeans

def Typology.fromWALS131A : Data.WALS.F131A.NumeralBases → NumeralBase

Convert WALS 131A numeral base values to the substrate enum (one-to-one).

Equations

• Typology.fromWALS131A Data.WALS.F131A.NumeralBases.decimal = Typology.NumeralBase.decimal
• Typology.fromWALS131A Data.WALS.F131A.NumeralBases.pureVigesimal = Typology.NumeralBase.vigesimal
• Typology.fromWALS131A Data.WALS.F131A.NumeralBases.hybridVigesimalDecimal = Typology.NumeralBase.hybridVigesimalDecimal
• Typology.fromWALS131A Data.WALS.F131A.NumeralBases.otherBase = Typology.NumeralBase.otherBase
• Typology.fromWALS131A Data.WALS.F131A.NumeralBases.extendedBodyPartSystem = Typology.NumeralBase.bodyPartSystem
• Typology.fromWALS131A Data.WALS.F131A.NumeralBases.restricted = Typology.NumeralBase.restricted

structure Typology.OrdinalDistribution : Type

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

• firstSuppletion : Nat
• firstSecondSuppletion : Nat
• allFromCardinals : Nat
• various : Nat
• noOrdinals : Nat

def Typology.instReprOrdinalDistribution.repr : OrdinalDistribution → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprOrdinalDistribution : Repr OrdinalDistribution

Equations

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

def Typology.OrdinalDistribution.total (d : OrdinalDistribution) : Nat

Equations

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

def Typology.ch53Distribution : OrdinalDistribution

WALS Ch 53 counts (321 languages).

Equations

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

structure Typology.DistributiveDistribution : Type

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

• noDistributive : Nat
• reduplication : Nat
• suffixCount : Nat
• prefixCount : Nat
• otherMeans : Nat

def Typology.instReprDistributiveDistribution.repr : DistributiveDistribution → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.instReprDistributiveDistribution : Repr DistributiveDistribution

Equations

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

def Typology.DistributiveDistribution.total (d : DistributiveDistribution) : Nat

Equations

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

def Typology.ch54Distribution : DistributiveDistribution

WALS Ch 54 counts (251 languages).

Equations

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

structure Typology.ConjQuantDistribution : Type

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

• identity : Nat
• differentiation : Nat

@[implicit_reducible]

instance Typology.instReprConjQuantDistribution : Repr ConjQuantDistribution

Equations

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

def Typology.instReprConjQuantDistribution.repr : ConjQuantDistribution → Nat → Std.Format

Equations

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

def Typology.ConjQuantDistribution.total (d : ConjQuantDistribution) : Nat

Equations

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

def Typology.ch56Distribution : ConjQuantDistribution

WALS Ch 56 counts (220 languages).

Equations

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

theorem 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 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 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.

theorem 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 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 Typology.differentiation_dominant : ch56Distribution.differentiation > ch56Distribution.identity

Differentiation between 'and' and 'all' is the dominant pattern (WALS Ch 56).

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

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

theorem 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).

inductive 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.

• none : SuppletionCutoff

  No suppletive ordinals (all regular from cardinals).

• first : SuppletionCutoff

  Only "first" is suppletive.

• firstAndSecond : SuppletionCutoff

  "first" and "second" are suppletive.

@[implicit_reducible]

instance Typology.instDecidableEqSuppletionCutoff : DecidableEq SuppletionCutoff

Equations

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

@[implicit_reducible]

instance Typology.instReprSuppletionCutoff : Repr SuppletionCutoff

Equations

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

def Typology.instReprSuppletionCutoff.repr : SuppletionCutoff → Nat → Std.Format

Equations

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

def Typology.SuppletionCutoff.rank : SuppletionCutoff → Nat

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

Equations

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

def 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

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

theorem 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 Typology.suppletion_frequency_matches_hierarchy : ch53Distribution.firstSuppletion > ch53Distribution.firstSecondSuppletion ∧ ch53Distribution.firstSecondSuppletion > ch53Distribution.allFromCardinals

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