Typology.Morphology

@cite{bickel-nichols-2013a} @cite{bickel-nichols-2013b} @cite{bickel-nichols-2013c} @cite{nichols-bickel-2013} @cite{nichols-bickel-2013a} @cite{nichols-bickel-2013b} @cite{nichols-bickel-2013c} @cite{nichols-bickel-2013d} @cite{baerman-brown-2013} @cite{baerman-brown-2013a} @cite{dryer-2013-wals} @cite{rubino-2013}

Per-language typological substrate for morphological mechanisms, covering WALS chapters 20--29 (fusion, exponence, synthesis, locus of marking, prefixing/suffixing, reduplication, syncretism) plus thematically-related Ch 21B, 62, 79A, 79B, 80A.

Mirrors the Linglib/Typology/{Possession,Negation,Comparison,Coordination, Modality,Gender,Alignment,ArgumentStructure,Copulas} substrate-extension pattern. Fragment-importable.

What lives here

The morphological types themselves -- Fusion, Flexivity, Exponence, ExponenceScope, VerbSynthesis, LocusOfMarking, PrefixSuffix, Reduplication, LocusClause, LocusPossessive, WholeLanguageMarking, ZeroMarkingAP, CaseSyncretism, VerbalSyncretism, TAMExponence, ActionNominal, SuppletionTA, SuppletionImperative, VerbalNumber -- plus the MorphProfile struct and the fromWALS{20A..80A} converters -- already live in Core/Morphology/MorphProfile.lean (Fragments depend on them directly).

This file adds the WALS-aggregate layer:

• WALSCount row struct + WALSCount.totalOf summer.
• Per-chapter WALS distribution lists (ch20Distribution ... ch80Distribution).
• WALS aggregate sample-size theorems (ch20_total ... ch80_total).
• Corpus-only generalisations: Greenberg's Universal 27 (suffixing dominates), concatenative dominance (Ch 20), reduplication majority (Ch 27), Ch 22 moderate-synthesis dominance.

Out of scope

The 18-language MorphProfile sample and the cross-chapter theorems built on it -- B&N orthogonality (concatenative × flexivity), agglutinating-vs- fusional partition, head-marking-implies-high-synthesis -- live in Phenomena/Morphology/Studies/BickelNichols2013.lean.

@cite{ackerman-malouf-2013}'s LanguageData (10-language E/I-complexity sample) and the LCEC apparatus live in Phenomena/Morphology/Studies/AckermanMalouf2013.lean.

WALSCount + WALSCount.totalOf are imported from Linglib/Data/WALS/Aggregation.lean (shared with the other Typology files that consume WALS distributions).

theorem Typology.Morphology.concatenative_most_common_wals : have concat := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F20A.FusionType) => x.value == Data.WALS.F20A.FusionType.exclusivelyConcatenative) Typology.Morphology.ch20✝).length; have isolating := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F20A.FusionType) => x.value == Data.WALS.F20A.FusionType.exclusivelyIsolating) Typology.Morphology.ch20✝).length; have tonal := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F20A.FusionType) => x.value == Data.WALS.F20A.FusionType.exclusivelyTonal) Typology.Morphology.ch20✝).length; concat > isolating ∧ concat > tonal

WALS Ch 20: exclusively concatenative is the most common single fusion type, exceeding both isolating and tonal.

theorem Typology.Morphology.reduplication_in_majority_wals : have hasRedup := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F27A.ReduplicationType) => x.value != Data.WALS.F27A.ReduplicationType.noProductiveReduplication) Typology.Morphology.ch27✝).length; hasRedup * 2 > Typology.Morphology.ch27✝.length

WALS Ch 27: productive reduplication (full or full+partial) is present in the majority of WALS-sampled languages.

theorem Typology.Morphology.ch22_moderate_dominant : have mid := (List.filter (fun (d : Data.WALS.Datapoint Data.WALS.F22A.InflectionalSynthesis) => d.value == Data.WALS.F22A.InflectionalSynthesis.categoriesPerWord2_3 || d.value == Data.WALS.F22A.InflectionalSynthesis.categoriesPerWord4_5 || d.value == Data.WALS.F22A.InflectionalSynthesis.categoriesPerWord6_7) Typology.Morphology.ch22✝).length; mid * 2 > Typology.Morphology.ch22✝.length

WALS Ch 22: most languages have 2--7 categories per verb word; the extremes (0--1 and 12--13) are rare.