Case Typology (WALS Chapters 49--52)

@cite{dryer-haspelmath-2013} @cite{iggesen-2013} @cite{stolz-veselinova-2013}

Formalizes four chapters from the World Atlas of Language Structures (WALS) covering the typology of case systems:

• Chapter 49: Number of Cases -- how many morphological cases a language has, from zero to ten or more.
• Chapter 50: Asymmetrical Case-Marking -- whether case marking is conditioned by NP properties (animacy, definiteness, pronoun status). Also known as Differential Case Marking.
• Chapter 51: Position of Case Affixes -- whether case markers are suffixes, prefixes, tonal, or mixed.
• Chapter 52: Comitatives and Instrumentals -- whether comitative ('with X') and instrumental ('by means of X') are marked identically or distinctly.

Each chapter is encoded as an inductive type with distributions derived from generated WALS data (Ch 49--51) or hand-coded counts (Ch 52). Language profiles combine all four dimensions, and typological generalizations are verified over the sample by native_decide.

inductive Phenomena.Case.Typology.CaseCount : Type

Number-of-cases categories (WALS Ch. 49, @cite{iggesen-2013}).

Languages are classified by the number of morphological case distinctions in their nominal paradigm. "No morphological case-marking" means the language has no affixal or clitic case at all (e.g., Mandarin, Thai).

• none : CaseCount
• two : CaseCount
• threeFour : CaseCount
• fiveSeven : CaseCount
• eightNine : CaseCount
• tenPlus : CaseCount

instance Phenomena.Case.Typology.instDecidableEqCaseCount : DecidableEq CaseCount

Equations

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

def Phenomena.Case.Typology.instBEqCaseCount.beq : CaseCount → CaseCount → Bool

Equations

• Phenomena.Case.Typology.instBEqCaseCount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Typology.instBEqCaseCount : BEq CaseCount

Equations

• Phenomena.Case.Typology.instBEqCaseCount = { beq := Phenomena.Case.Typology.instBEqCaseCount.beq }

instance Phenomena.Case.Typology.instReprCaseCount : Repr CaseCount

Equations

• Phenomena.Case.Typology.instReprCaseCount = { reprPrec := Phenomena.Case.Typology.instReprCaseCount.repr }

def Phenomena.Case.Typology.instReprCaseCount.repr : CaseCount → Nat → Std.Format

Equations

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

instance Phenomena.Case.Typology.instInhabitedCaseCount : Inhabited CaseCount

Equations

• Phenomena.Case.Typology.instInhabitedCaseCount = { default := Phenomena.Case.Typology.CaseCount.none }

def Phenomena.Case.Typology.CaseCount.lowerBound : CaseCount → Nat

Numeric lower bound for each CaseCount category.

Equations

• Phenomena.Case.Typology.CaseCount.none.lowerBound = 0
• Phenomena.Case.Typology.CaseCount.two.lowerBound = 2
• Phenomena.Case.Typology.CaseCount.threeFour.lowerBound = 3
• Phenomena.Case.Typology.CaseCount.fiveSeven.lowerBound = 5
• Phenomena.Case.Typology.CaseCount.eightNine.lowerBound = 8
• Phenomena.Case.Typology.CaseCount.tenPlus.lowerBound = 10

def Phenomena.Case.Typology.CaseCount.contains (cc : CaseCount) (n : Nat) : Bool

Whether a raw case count falls in a given CaseCount category.

Equations

• Phenomena.Case.Typology.CaseCount.none.contains n = (n == 0)
• Phenomena.Case.Typology.CaseCount.two.contains n = (n == 2)
• Phenomena.Case.Typology.CaseCount.threeFour.contains n = (decide (n ≥ 3) && decide (n ≤ 4))
• Phenomena.Case.Typology.CaseCount.fiveSeven.contains n = (decide (n ≥ 5) && decide (n ≤ 7))
• Phenomena.Case.Typology.CaseCount.eightNine.contains n = (decide (n ≥ 8) && decide (n ≤ 9))
• Phenomena.Case.Typology.CaseCount.tenPlus.contains n = decide (n ≥ 10)

theorem Phenomena.Case.Typology.ch49_total : Phenomena.Case.Typology.ch49✝.length = 261

Chapter 49 total sample size (from generated data).

inductive Phenomena.Case.Typology.AsymmetricalCaseMarking : Type

Asymmetrical (differential) case-marking types (WALS Ch. 50, @cite{iggesen-2013}).

Differential case marking (DCM) means that case marking on a noun phrase depends on properties of that NP -- its animacy, definiteness, or whether it is a full noun vs. a pronoun. For example, in Hindi-Urdu the accusative marker -ko appears on animate/definite objects but not inanimate/indefinite ones.

• noCase : AsymmetricalCaseMarking
• borderlineOnly : AsymmetricalCaseMarking
• noAsymmetry : AsymmetricalCaseMarking
• animacyOnly : AsymmetricalCaseMarking
• definitenessOnly : AsymmetricalCaseMarking
• pronounOnly : AsymmetricalCaseMarking
• twoConditions : AsymmetricalCaseMarking
• threeConditions : AsymmetricalCaseMarking

instance Phenomena.Case.Typology.instDecidableEqAsymmetricalCaseMarking : DecidableEq AsymmetricalCaseMarking

Equations

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

instance Phenomena.Case.Typology.instBEqAsymmetricalCaseMarking : BEq AsymmetricalCaseMarking

Equations

• Phenomena.Case.Typology.instBEqAsymmetricalCaseMarking = { beq := Phenomena.Case.Typology.instBEqAsymmetricalCaseMarking.beq }

def Phenomena.Case.Typology.instBEqAsymmetricalCaseMarking.beq : AsymmetricalCaseMarking → AsymmetricalCaseMarking → Bool

Equations

• Phenomena.Case.Typology.instBEqAsymmetricalCaseMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Case.Typology.instReprAsymmetricalCaseMarking.repr : AsymmetricalCaseMarking → Nat → Std.Format

Equations

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

instance Phenomena.Case.Typology.instReprAsymmetricalCaseMarking : Repr AsymmetricalCaseMarking

Equations

• Phenomena.Case.Typology.instReprAsymmetricalCaseMarking = { reprPrec := Phenomena.Case.Typology.instReprAsymmetricalCaseMarking.repr }

instance Phenomena.Case.Typology.instInhabitedAsymmetricalCaseMarking : Inhabited AsymmetricalCaseMarking

Equations

• Phenomena.Case.Typology.instInhabitedAsymmetricalCaseMarking = { default := Phenomena.Case.Typology.AsymmetricalCaseMarking.noCase }

def Phenomena.Case.Typology.AsymmetricalCaseMarking.hasDCM : AsymmetricalCaseMarking → Bool

Whether this type involves any differential case marking.

Equations

• Phenomena.Case.Typology.AsymmetricalCaseMarking.noCase.hasDCM = false
• Phenomena.Case.Typology.AsymmetricalCaseMarking.borderlineOnly.hasDCM = false
• Phenomena.Case.Typology.AsymmetricalCaseMarking.noAsymmetry.hasDCM = false
• x✝.hasDCM = true

def Phenomena.Case.Typology.AsymmetricalCaseMarking.conditionCount : AsymmetricalCaseMarking → Nat

Number of conditioning factors (0--3).

Equations

• Phenomena.Case.Typology.AsymmetricalCaseMarking.noCase.conditionCount = 0
• Phenomena.Case.Typology.AsymmetricalCaseMarking.borderlineOnly.conditionCount = 0
• Phenomena.Case.Typology.AsymmetricalCaseMarking.noAsymmetry.conditionCount = 0
• Phenomena.Case.Typology.AsymmetricalCaseMarking.animacyOnly.conditionCount = 1
• Phenomena.Case.Typology.AsymmetricalCaseMarking.definitenessOnly.conditionCount = 1
• Phenomena.Case.Typology.AsymmetricalCaseMarking.pronounOnly.conditionCount = 1
• Phenomena.Case.Typology.AsymmetricalCaseMarking.twoConditions.conditionCount = 2
• Phenomena.Case.Typology.AsymmetricalCaseMarking.threeConditions.conditionCount = 3

theorem Phenomena.Case.Typology.ch50_total : Phenomena.Case.Typology.ch50✝.length = 261

Chapter 50 total sample size (from generated data).

inductive Phenomena.Case.Typology.CaseAffixPosition : Type

Position of case affixes (WALS Ch. 51, @cite{iggesen-2013}).

Classifies where the case morpheme sits relative to the nominal stem. Languages with no case affixes at all (either no case or case expressed only by adpositions) are distinguished from those with suffixes, prefixes, tonal marking, or mixed strategies.

• noAffixes : CaseAffixPosition
• suffixesOnly : CaseAffixPosition
• prefixesOnly : CaseAffixPosition
• toneOnly : CaseAffixPosition
• bothSuffixPrefix : CaseAffixPosition

instance Phenomena.Case.Typology.instDecidableEqCaseAffixPosition : DecidableEq CaseAffixPosition

Equations

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

instance Phenomena.Case.Typology.instBEqCaseAffixPosition : BEq CaseAffixPosition

Equations

• Phenomena.Case.Typology.instBEqCaseAffixPosition = { beq := Phenomena.Case.Typology.instBEqCaseAffixPosition.beq }

def Phenomena.Case.Typology.instBEqCaseAffixPosition.beq : CaseAffixPosition → CaseAffixPosition → Bool

Equations

• Phenomena.Case.Typology.instBEqCaseAffixPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Typology.instReprCaseAffixPosition : Repr CaseAffixPosition

Equations

• Phenomena.Case.Typology.instReprCaseAffixPosition = { reprPrec := Phenomena.Case.Typology.instReprCaseAffixPosition.repr }

def Phenomena.Case.Typology.instReprCaseAffixPosition.repr : CaseAffixPosition → Nat → Std.Format

Equations

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

instance Phenomena.Case.Typology.instInhabitedCaseAffixPosition : Inhabited CaseAffixPosition

Equations

• Phenomena.Case.Typology.instInhabitedCaseAffixPosition = { default := Phenomena.Case.Typology.CaseAffixPosition.noAffixes }

def Phenomena.Case.Typology.CaseAffixPosition.hasBoundCase : CaseAffixPosition → Bool

Whether this position type involves bound morphology.

Equations

• Phenomena.Case.Typology.CaseAffixPosition.noAffixes.hasBoundCase = false
• x✝.hasBoundCase = true

def Phenomena.Case.Typology.CaseAffixPosition.hasSuffix : CaseAffixPosition → Bool

Whether suffixal case marking is present.

Equations

• Phenomena.Case.Typology.CaseAffixPosition.suffixesOnly.hasSuffix = true
• Phenomena.Case.Typology.CaseAffixPosition.bothSuffixPrefix.hasSuffix = true
• x✝.hasSuffix = false

theorem Phenomena.Case.Typology.ch51_total : Phenomena.Case.Typology.ch51✝.length = 1031

Chapter 51 total sample size (from generated data).

inductive Phenomena.Case.Typology.ComitativeInstrumental : Type

Comitative-instrumental syncretism (WALS Ch. 52, @cite{stolz-veselinova-2013}).

In many languages the marker for 'with X' (comitative: accompaniment) and 'by means of X' (instrumental: means/instrument) is the same morpheme. For example, Russian uses the instrumental case (-om, -oj) for both "I went with Ivan" and "I cut it with a knife". Other languages distinguish them, e.g. Japanese -to (comitative) vs. -de (instrumental).

• identity : ComitativeInstrumental
• differentiation : ComitativeInstrumental
• mixed : ComitativeInstrumental

instance Phenomena.Case.Typology.instDecidableEqComitativeInstrumental : DecidableEq ComitativeInstrumental

Equations

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

def Phenomena.Case.Typology.instBEqComitativeInstrumental.beq : ComitativeInstrumental → ComitativeInstrumental → Bool

Equations

• Phenomena.Case.Typology.instBEqComitativeInstrumental.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Typology.instBEqComitativeInstrumental : BEq ComitativeInstrumental

Equations

• Phenomena.Case.Typology.instBEqComitativeInstrumental = { beq := Phenomena.Case.Typology.instBEqComitativeInstrumental.beq }

def Phenomena.Case.Typology.instReprComitativeInstrumental.repr : ComitativeInstrumental → Nat → Std.Format

Equations

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

instance Phenomena.Case.Typology.instReprComitativeInstrumental : Repr ComitativeInstrumental

Equations

• Phenomena.Case.Typology.instReprComitativeInstrumental = { reprPrec := Phenomena.Case.Typology.instReprComitativeInstrumental.repr }

instance Phenomena.Case.Typology.instInhabitedComitativeInstrumental : Inhabited ComitativeInstrumental

Equations

• Phenomena.Case.Typology.instInhabitedComitativeInstrumental = { default := Phenomena.Case.Typology.ComitativeInstrumental.identity }

def Phenomena.Case.Typology.ComitativeInstrumental.isSyncretic : ComitativeInstrumental → Bool

Whether the language uses the same morpheme for both functions.

Equations

• Phenomena.Case.Typology.ComitativeInstrumental.identity.isSyncretic = true
• x✝.isSyncretic = false

theorem Phenomena.Case.Typology.ch52_total : Phenomena.Case.Typology.ch52✝.length = 322

Chapter 52 total sample size.

theorem Phenomena.Case.Typology.ch49_no_case_modal : have noCases := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => x.value == Core.WALS.F49A.CaseCount.noMorphologicalCaseMarking) Phenomena.Case.Typology.ch49✝).length; noCases > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => x.value == Core.WALS.F49A.CaseCount.cases2) Phenomena.Case.Typology.ch49✝¹).length ∧ noCases > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => x.value == Core.WALS.F49A.CaseCount.cases6_7) Phenomena.Case.Typology.ch49✝²).length

Ch 49: Languages with no case are the modal category.

theorem Phenomena.Case.Typology.ch49_case_languages_majority : have noCases := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => x.value == Core.WALS.F49A.CaseCount.noMorphologicalCaseMarking) Phenomena.Case.Typology.ch49✝).length; Phenomena.Case.Typology.ch49✝¹.length - noCases > noCases

Ch 49: Case-bearing languages (2+ cases) outnumber caseless ones.

theorem Phenomena.Case.Typology.ch50_asymmetry_common : have symmetrical := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F50A.AsymmetricalCaseMarking) => x.value == Core.WALS.F50A.AsymmetricalCaseMarking.symmetrical) Phenomena.Case.Typology.ch50✝).length; have additive := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F50A.AsymmetricalCaseMarking) => x.value == Core.WALS.F50A.AsymmetricalCaseMarking.additiveQuantitativelyAsymmetrical) Phenomena.Case.Typology.ch50✝¹).length; have subtractive := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F50A.AsymmetricalCaseMarking) => x.value == Core.WALS.F50A.AsymmetricalCaseMarking.subtractiveQuantitativelyAsymmetrical) Phenomena.Case.Typology.ch50✝²).length; have qualitative := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F50A.AsymmetricalCaseMarking) => x.value == Core.WALS.F50A.AsymmetricalCaseMarking.qualitativelyAsymmetrical) Phenomena.Case.Typology.ch50✝³).length; have syncretism := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F50A.AsymmetricalCaseMarking) => x.value == Core.WALS.F50A.AsymmetricalCaseMarking.syncretismInRelevantNpTypes) Phenomena.Case.Typology.ch50✝⁴).length; additive + subtractive + qualitative + syncretism > symmetrical

Ch 50: Languages with some asymmetrical case-marking outnumber those with purely symmetrical case.

theorem Phenomena.Case.Typology.ch51_suffix_dominant : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F51A.CaseAffixPosition) => x.value == Core.WALS.F51A.CaseAffixPosition.caseSuffixes) Phenomena.Case.Typology.ch51✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F51A.CaseAffixPosition) => x.value == Core.WALS.F51A.CaseAffixPosition.casePrefixes) Phenomena.Case.Typology.ch51✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F51A.CaseAffixPosition) => x.value == Core.WALS.F51A.CaseAffixPosition.caseSuffixes) Phenomena.Case.Typology.ch51✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F51A.CaseAffixPosition) => x.value == Core.WALS.F51A.CaseAffixPosition.postpositionalClitics) Phenomena.Case.Typology.ch51✝³).length

Ch 51: Suffixal case is the dominant strategy among case-marking languages.

theorem Phenomena.Case.Typology.ch52_differentiation_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F52A.ComitativesAndInstrumentals) => x.value == Core.WALS.F52A.ComitativesAndInstrumentals.differentiation) Phenomena.Case.Typology.ch52✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F52A.ComitativesAndInstrumentals) => x.value == Core.WALS.F52A.ComitativesAndInstrumentals.identity) Phenomena.Case.Typology.ch52✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F52A.ComitativesAndInstrumentals) => x.value == Core.WALS.F52A.ComitativesAndInstrumentals.differentiation) Phenomena.Case.Typology.ch52✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F52A.ComitativesAndInstrumentals) => x.value == Core.WALS.F52A.ComitativesAndInstrumentals.mixed) Phenomena.Case.Typology.ch52✝³).length

Ch 52: Differentiation is the majority pattern.

structure Phenomena.Case.Typology.CaseProfile : Type

A language's case profile, combining classifications from all four WALS case chapters.

This structure records a single language's position in each of the four typological dimensions. The rawCaseCount field stores the actual number of morphological cases (not just the WALS bin), enabling finer-grained generalizations.

• name : String

  Language name

• iso639 : String

  ISO 639-3 code

• caseCount : CaseCount

  Ch 49: Number of cases (WALS category)

• rawCaseCount : Nat

  Actual number of morphological cases

• asymmetry : AsymmetricalCaseMarking

  Ch 50: Asymmetrical case-marking type

• affixPosition : CaseAffixPosition

  Ch 51: Position of case affixes

• comitativeInstr : ComitativeInstrumental

  Ch 52: Comitative-instrumental relation

def Phenomena.Case.Typology.instReprCaseProfile.repr : CaseProfile → Nat → Std.Format

Equations

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

instance Phenomena.Case.Typology.instReprCaseProfile : Repr CaseProfile

Equations

• Phenomena.Case.Typology.instReprCaseProfile = { reprPrec := Phenomena.Case.Typology.instReprCaseProfile.repr }

def Phenomena.Case.Typology.instDecidableEqCaseProfile.decEq (x✝ x✝¹ : CaseProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Case.Typology.instDecidableEqCaseProfile : DecidableEq CaseProfile

Equations

• Phenomena.Case.Typology.instDecidableEqCaseProfile = Phenomena.Case.Typology.instDecidableEqCaseProfile.decEq

def Phenomena.Case.Typology.instBEqCaseProfile.beq : CaseProfile → CaseProfile → Bool

Equations

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

instance Phenomena.Case.Typology.instBEqCaseProfile : BEq CaseProfile

Equations

• Phenomena.Case.Typology.instBEqCaseProfile = { beq := Phenomena.Case.Typology.instBEqCaseProfile.beq }

def Phenomena.Case.Typology.CaseProfile.rawCountConsistent (p : CaseProfile) : Bool

Whether the raw case count is consistent with the WALS bin.

Equations

• p.rawCountConsistent = p.caseCount.contains p.rawCaseCount

def Phenomena.Case.Typology.CaseProfile.crossChapterConsistent (p : CaseProfile) : Bool

Whether the profile is internally consistent across chapters: no-case in Ch 49 should align with no-case in Ch 50 and no-affixes in Ch 51.

Equations

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

def Phenomena.Case.Typology.finnish : CaseProfile

Finnish: 15 morphological cases (nom, gen, acc, part, iness, elat, illat, adess, ablat, allat, ess, transl, instruct, comit, abes). Suffixal. No DCM. Comitative and instrumental are distinct cases.

Equations

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

def Phenomena.Case.Typology.hungarian : CaseProfile

Hungarian: 18 morphological cases (nom, acc, dat, instrum, causal-final, translative, terminative, essive-formal, essive-modal, inessive, elative, illative, superessive, delative, sublative, adessive, ablative, allative). Suffixal agglutinative. Comitative (-val, -vel) = instrumental.

Equations

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

def Phenomena.Case.Typology.turkish : CaseProfile

Turkish: 6 cases (nom, acc, gen, dat, loc, abl). Suffixal agglutinative. Differential object marking: definite objects take -I, indefinite do not.

Equations

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

def Phenomena.Case.Typology.latin : CaseProfile

Latin: 6 cases (nom, acc, gen, dat, abl, voc; locative vestigial). Suffixal fusional. No asymmetrical case-marking. Comitative (cum + abl) vs. instrumental (plain abl) are technically distinct strategies.

Equations

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

def Phenomena.Case.Typology.russian : CaseProfile

Russian: 6 cases (nom, acc, gen, dat, instrum, prep/loc). Suffixal fusional. Differential accusative: animate nouns take genitive form in accusative, inanimates keep nominative form.

Equations

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

def Phenomena.Case.Typology.german : CaseProfile

German: 4 cases (nom, acc, gen, dat). Suffixal fusional with articles carrying most case marking. No systematic DCM. Comitative (mit + dat) and instrumental (mit + dat) use the same marker.

Equations

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

def Phenomena.Case.Typology.japanese : CaseProfile

Japanese: case particles (ga, o, ni, no, de, e, to, kara, made,...). Postpositional clitics rather than affixes in WALS's classification. Differential object marking with -o conditioned by specificity/topicality. Comitative -to vs. instrumental -de are distinct.

Equations

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

def Phenomena.Case.Typology.english : CaseProfile

English: 2-case system surviving only in pronouns (nom/acc: I/me, he/him, she/her, we/us, they/them). No case affixes on nouns. Comitative 'with' and instrumental 'with' are identical.

Equations

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

def Phenomena.Case.Typology.korean : CaseProfile

Korean: case particles (-i/ga nom, -(l)eul acc, -ui gen, -e dat/loc, -eseo loc/source, -(eu)ro instr/dir, -wa/gwa comit). Particles are postpositional clitics. Optional object marking conditioned by definiteness/topicality. Comitative -wa and instrumental -(eu)ro are distinct.

Equations

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

def Phenomena.Case.Typology.mandarin : CaseProfile

Mandarin Chinese: no morphological case. Fixed SVO word order encodes grammatical relations. No case markers, no DCM, comitative and instrumental expressed by distinct prepositions (he 'with-COM' vs. yong 'with-INSTR').

Equations

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

def Phenomena.Case.Typology.hindiUrdu : CaseProfile

Hindi-Urdu: 3 cases (direct, oblique, vocative). Postpositional system with -ne (ergative), -ko (accusative/dative), -se (instrumental/ ablative), -me (locative). Differential object marking: -ko appears on animate/specific objects. Comitative -ke saath vs. instrumental -se are distinct.

Equations

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

def Phenomena.Case.Typology.arabic : CaseProfile

Arabic (Modern Standard): 3 cases (nom -u, acc -a, gen -i). Suffixal. Full case marking on indefinite nouns (tanwin); definite nouns often show reduced marking in spoken varieties, but MSA maintains it. Comitative (maʕa) and instrumental (bi-) are distinct.

Equations

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

def Phenomena.Case.Typology.georgian : CaseProfile

Georgian: 7 cases (nom, erg, dat, gen, instrum, adverbial, vocative). Suffixal agglutinative. Split-ergative system conditioned by tense/aspect (not NP properties), so no DCM in the WALS sense. Instrumental -it and comitative -tan are distinct.

Equations

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

def Phenomena.Case.Typology.quechua : CaseProfile

Quechua (Cusco): 12+ cases (nom, acc -ta, gen -pa or -q, dat -man, loc -pi, abl -manta, instrum -wan, comit -wan, limit -kama, causal -rayku, benef -paq, topic -qa,...). Suffixal agglutinative. Comitative and instrumental both use -wan (identity).

Equations

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

def Phenomena.Case.Typology.basque : CaseProfile

Basque: ergative-absolutive system with 11+ cases (abs, erg, dat, gen, comit -ekin, instrum -z, iness, allat, ablat, destinat, motivat). Suffixal. Differential ergative marking in some analyses. Comitative -ekin and instrumental -z are distinct.

Equations

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

def Phenomena.Case.Typology.tamil : CaseProfile

Tamil: 8 cases (nom, acc, dat, gen, instrum, loc, ablat, sociative/ comitative). Suffixal agglutinative. Differential object marking: accusative -ai on animate/definite objects. Comitative -ootu and instrumental -aal are distinct.

Equations

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

def Phenomena.Case.Typology.allProfiles : List CaseProfile

All language profiles in our sample.

Equations

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

theorem Phenomena.Case.Typology.allProfiles_count : allProfiles.length = 16

theorem Phenomena.Case.Typology.finnish_ch49 : ((Core.WALS.F49A.lookup "fin").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some finnish.caseCount

theorem Phenomena.Case.Typology.hungarian_ch49 : ((Core.WALS.F49A.lookup "hun").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some hungarian.caseCount

theorem Phenomena.Case.Typology.turkish_ch49 : ((Core.WALS.F49A.lookup "tur").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some turkish.caseCount

theorem Phenomena.Case.Typology.russian_ch49 : ((Core.WALS.F49A.lookup "rus").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some russian.caseCount

theorem Phenomena.Case.Typology.german_ch49 : ((Core.WALS.F49A.lookup "ger").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some german.caseCount

theorem Phenomena.Case.Typology.japanese_ch49 : ((Core.WALS.F49A.lookup "jpn").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some japanese.caseCount

theorem Phenomena.Case.Typology.english_ch49 : ((Core.WALS.F49A.lookup "eng").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some english.caseCount

theorem Phenomena.Case.Typology.korean_ch49 : ((Core.WALS.F49A.lookup "kor").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some korean.caseCount

theorem Phenomena.Case.Typology.mandarin_ch49 : ((Core.WALS.F49A.lookup "mnd").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some mandarin.caseCount

theorem Phenomena.Case.Typology.georgian_ch49 : ((Core.WALS.F49A.lookup "geo").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some georgian.caseCount

theorem Phenomena.Case.Typology.basque_ch49 : ((Core.WALS.F49A.lookup "bsq").bind fun (x : Core.WALS.Datapoint Core.WALS.F49A.CaseCount) => Phenomena.Case.Typology.fromWALS49A✝ x.value) = some basque.caseCount

Every language's raw case count falls within its declared WALS category.

theorem Phenomena.Case.Typology.finnish_raw_consistent : finnish.rawCountConsistent = true

theorem Phenomena.Case.Typology.hungarian_raw_consistent : hungarian.rawCountConsistent = true

theorem Phenomena.Case.Typology.turkish_raw_consistent : turkish.rawCountConsistent = true

theorem Phenomena.Case.Typology.latin_raw_consistent : latin.rawCountConsistent = true

theorem Phenomena.Case.Typology.russian_raw_consistent : russian.rawCountConsistent = true

theorem Phenomena.Case.Typology.german_raw_consistent : german.rawCountConsistent = true

theorem Phenomena.Case.Typology.japanese_raw_consistent : japanese.rawCountConsistent = true

theorem Phenomena.Case.Typology.english_raw_consistent : english.rawCountConsistent = true

theorem Phenomena.Case.Typology.korean_raw_consistent : korean.rawCountConsistent = true

theorem Phenomena.Case.Typology.mandarin_raw_consistent : mandarin.rawCountConsistent = true

theorem Phenomena.Case.Typology.hindiUrdu_raw_consistent : hindiUrdu.rawCountConsistent = true

theorem Phenomena.Case.Typology.arabic_raw_consistent : arabic.rawCountConsistent = true

theorem Phenomena.Case.Typology.georgian_raw_consistent : georgian.rawCountConsistent = true

theorem Phenomena.Case.Typology.quechua_raw_consistent : quechua.rawCountConsistent = true

theorem Phenomena.Case.Typology.basque_raw_consistent : basque.rawCountConsistent = true

theorem Phenomena.Case.Typology.tamil_raw_consistent : tamil.rawCountConsistent = true

theorem Phenomena.Case.Typology.all_raw_consistent : (allProfiles.all fun (x : CaseProfile) => x.rawCountConsistent) = true

All raw case counts are consistent with their WALS bins.

Cross-chapter consistency: no-case in Ch 49 aligns with noCase in Ch 50 and noAffixes in Ch 51; case-bearing languages do not have noCase in Ch 50.

theorem Phenomena.Case.Typology.mandarin_cross_consistent : mandarin.crossChapterConsistent = true

theorem Phenomena.Case.Typology.english_cross_consistent : english.crossChapterConsistent = true

theorem Phenomena.Case.Typology.finnish_cross_consistent : finnish.crossChapterConsistent = true

theorem Phenomena.Case.Typology.all_cross_consistent : (allProfiles.all fun (x : CaseProfile) => x.crossChapterConsistent) = true

All profiles are cross-chapter consistent.

Generalization 1: Case-rich languages are overwhelmingly suffixal.

Among the world's languages, suffixal case marking is far more common than prefixal. In our sample, every language with case affixes uses suffixes (either exclusively or in combination with prefixes). This reflects the strong universal preference documented by @cite{hawkins-1983} and @cite{dryer-1992}.

theorem Phenomena.Case.Typology.case_rich_are_suffixal : (allProfiles.all fun (p : CaseProfile) => if (p.caseCount != CaseCount.none && p.affixPosition.hasBoundCase) = true then p.affixPosition.hasSuffix else true) = true

Generalization 2: No prefixal-only case in our sample.

No language in our sample uses exclusively prefixal case marking. Cross-linguistically, prefixal-only case is very rare (WALS Ch 51 reports only 7 out of 261 languages).

theorem Phenomena.Case.Typology.no_prefix_only : (allProfiles.all fun (p : CaseProfile) => p.affixPosition != CaseAffixPosition.prefixesOnly) = true

Generalization 3: DCM is conditioned by animacy or definiteness.

Among languages with differential case marking in our sample, the conditioning factors are animacy, definiteness, or pronoun status -- never some other property like gender or number alone.

theorem Phenomena.Case.Typology.dcm_conditions_limited : (allProfiles.all fun (p : CaseProfile) => if p.asymmetry.hasDCM = true then p.asymmetry == AsymmetricalCaseMarking.animacyOnly || p.asymmetry == AsymmetricalCaseMarking.definitenessOnly || p.asymmetry == AsymmetricalCaseMarking.pronounOnly || p.asymmetry == AsymmetricalCaseMarking.twoConditions || p.asymmetry == AsymmetricalCaseMarking.threeConditions else true) = true

Generalization 4: Comitative-instrumental identity is common but

not universal. Identity (syncretism) and differentiation both occur across language families.

theorem Phenomena.Case.Typology.both_comit_instr_patterns_attested : ((allProfiles.any fun (p : CaseProfile) => p.comitativeInstr == ComitativeInstrumental.identity) && decide ((allProfiles.any fun (p : CaseProfile) => p.comitativeInstr == ComitativeInstrumental.differentiation) = true)) = true

Generalization 5: No-case languages have no asymmetrical marking.

By definition, if there is no morphological case, there can be no asymmetrical (differential) case marking.

theorem Phenomena.Case.Typology.no_case_no_asymmetry : (allProfiles.all fun (p : CaseProfile) => if (p.caseCount == CaseCount.none) = true then p.asymmetry == AsymmetricalCaseMarking.noCase else true) = true

Generalization 6: No-case languages have no case affixes.

Again by definition: without morphological case, there are no case affixes to position.

theorem Phenomena.Case.Typology.no_case_no_affixes : (allProfiles.all fun (p : CaseProfile) => if (p.caseCount == CaseCount.none) = true then p.affixPosition == CaseAffixPosition.noAffixes else true) = true

Generalization 7: 10+-case languages all have suffixal case.

Highly agglutinative case-rich systems (Finnish, Hungarian, Quechua, Basque) uniformly use suffixes. No case-rich language uses prefixes only or tone only.

theorem Phenomena.Case.Typology.ten_plus_all_suffixal : (allProfiles.all fun (p : CaseProfile) => if (p.caseCount == CaseCount.tenPlus) = true then p.affixPosition == CaseAffixPosition.suffixesOnly else true) = true

Generalization 8: Languages with 2 cases tend toward asymmetrical

marking.

When a language has only two cases, case marking often applies differentially (to pronouns only, or conditioned by definiteness). English is the classic example: only pronouns show nominative/accusative.

theorem Phenomena.Case.Typology.two_case_tends_asymmetric : (allProfiles.all fun (p : CaseProfile) => if (p.caseCount == CaseCount.two) = true then p.asymmetry.hasDCM || p.asymmetry == AsymmetricalCaseMarking.pronounOnly else true) = true

Generalization 9: Comitative-instrumental identity correlates with

case-rich systems.

Among our case-rich languages (5+ cases), those with identity include Hungarian, Russian, Turkish, Quechua -- all agglutinative or fusional languages where an instrumental case doubles for comitative.

theorem Phenomena.Case.Typology.identity_in_case_rich : (List.filter (fun (p : CaseProfile) => decide (p.rawCaseCount ≥ 5) && p.comitativeInstr == ComitativeInstrumental.identity) allProfiles).length ≥ 3

Generalization 10: All CaseCount bins are attested in the sample.

Our 16-language sample covers every WALS Chapter 49 category.

theorem Phenomena.Case.Typology.all_case_counts_attested : ((((((allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.none) && allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.two) && allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.threeFour) && allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.fiveSeven) && allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.eightNine) && decide ((allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.tenPlus) = true)) = true

Spot-checks that each language has the expected WALS category values.

theorem Phenomena.Case.Typology.finnish_tenPlus : finnish.caseCount = CaseCount.tenPlus

theorem Phenomena.Case.Typology.hungarian_tenPlus : hungarian.caseCount = CaseCount.tenPlus

theorem Phenomena.Case.Typology.turkish_fiveSeven : turkish.caseCount = CaseCount.fiveSeven

theorem Phenomena.Case.Typology.latin_fiveSeven : latin.caseCount = CaseCount.fiveSeven

theorem Phenomena.Case.Typology.russian_fiveSeven : russian.caseCount = CaseCount.fiveSeven

theorem Phenomena.Case.Typology.german_threeFour : german.caseCount = CaseCount.threeFour

theorem Phenomena.Case.Typology.english_two : english.caseCount = CaseCount.two

theorem Phenomena.Case.Typology.mandarin_none : mandarin.caseCount = CaseCount.none

theorem Phenomena.Case.Typology.russian_animacy_dcm : russian.asymmetry = AsymmetricalCaseMarking.animacyOnly

theorem Phenomena.Case.Typology.turkish_definiteness_dcm : turkish.asymmetry = AsymmetricalCaseMarking.definitenessOnly

theorem Phenomena.Case.Typology.english_pronoun_dcm : english.asymmetry = AsymmetricalCaseMarking.pronounOnly

theorem Phenomena.Case.Typology.hindiUrdu_two_cond : hindiUrdu.asymmetry = AsymmetricalCaseMarking.twoConditions

theorem Phenomena.Case.Typology.english_no_affixes : english.affixPosition = CaseAffixPosition.noAffixes

theorem Phenomena.Case.Typology.finnish_suffixes : finnish.affixPosition = CaseAffixPosition.suffixesOnly

theorem Phenomena.Case.Typology.mandarin_no_affixes : mandarin.affixPosition = CaseAffixPosition.noAffixes

theorem Phenomena.Case.Typology.russian_com_instr_identity : russian.comitativeInstr = ComitativeInstrumental.identity

theorem Phenomena.Case.Typology.japanese_com_instr_diff : japanese.comitativeInstr = ComitativeInstrumental.differentiation

theorem Phenomena.Case.Typology.case_count_ordering : mandarin.rawCaseCount < english.rawCaseCount ∧ english.rawCaseCount < arabic.rawCaseCount ∧ arabic.rawCaseCount < german.rawCaseCount ∧ german.rawCaseCount < turkish.rawCaseCount ∧ turkish.rawCaseCount < korean.rawCaseCount ∧ korean.rawCaseCount < japanese.rawCaseCount ∧ japanese.rawCaseCount < basque.rawCaseCount ∧ basque.rawCaseCount < quechua.rawCaseCount ∧ quechua.rawCaseCount < finnish.rawCaseCount ∧ finnish.rawCaseCount < hungarian.rawCaseCount

Raw case counts are ordered as expected: Finnish < Hungarian at the top, Mandarin and English at the bottom.

def Phenomena.Case.Typology.caselessCount : Nat

Number of caseless languages in our sample.

Equations

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

def Phenomena.Case.Typology.dcmCount : Nat

Number of DCM languages in our sample.

Equations

• Phenomena.Case.Typology.dcmCount = (List.filter (fun (p : Phenomena.Case.Typology.CaseProfile) => p.asymmetry.hasDCM) Phenomena.Case.Typology.allProfiles).length

def Phenomena.Case.Typology.suffixalCount : Nat

Number of suffixal-case languages in our sample.

Equations

• Phenomena.Case.Typology.suffixalCount = (List.filter (fun (p : Phenomena.Case.Typology.CaseProfile) => p.affixPosition.hasSuffix) Phenomena.Case.Typology.allProfiles).length

def Phenomena.Case.Typology.comitIdentityCount : Nat

Number of comitative-instrumental identity languages.

Equations

• Phenomena.Case.Typology.comitIdentityCount = (List.filter (fun (p : Phenomena.Case.Typology.CaseProfile) => p.comitativeInstr.isSyncretic) Phenomena.Case.Typology.allProfiles).length

theorem Phenomena.Case.Typology.caseless_is_1 : caselessCount = 1

theorem Phenomena.Case.Typology.dcm_is_7 : dcmCount = 7

theorem Phenomena.Case.Typology.suffixal_is_14 : suffixalCount = 14

theorem Phenomena.Case.Typology.comit_identity_is_6 : comitIdentityCount = 6

theorem Phenomena.Case.Typology.all_iso_nonempty : (allProfiles.all fun (p : CaseProfile) => decide (p.iso639.length > 0)) = true

All ISO 639-3 codes are non-empty.

theorem Phenomena.Case.Typology.all_iso_length_3 : (allProfiles.all fun (p : CaseProfile) => p.iso639.length == 3) = true

All ISO 639-3 codes are exactly 3 characters (standard length).

theorem Phenomena.Case.Typology.iso_codes_unique : (List.map (fun (x : CaseProfile) => x.iso639) allProfiles).eraseDups.length = allProfiles.length

No duplicate ISO codes (each language appears once).

theorem Phenomena.Case.Typology.dcm_implies_case : (allProfiles.all fun (p : CaseProfile) => if p.asymmetry.hasDCM = true then decide (p.rawCaseCount ≥ 2) else true) = true

Languages with DCM (Ch 50) all have at least 2 cases (Ch 49).

theorem Phenomena.Case.Typology.affixes_imply_case : (allProfiles.all fun (p : CaseProfile) => if p.affixPosition.hasBoundCase = true then decide (p.rawCaseCount ≥ 2) else true) = true

Languages with case affixes (Ch 51) all have at least 2 cases (Ch 49).

theorem Phenomena.Case.Typology.rich_case_profile_exists : (allProfiles.any fun (p : CaseProfile) => p.caseCount == CaseCount.tenPlus && p.asymmetry == AsymmetricalCaseMarking.noAsymmetry && p.affixPosition == CaseAffixPosition.suffixesOnly) = true

No language with 10+ cases uses identity for comitative-instrumental in our sample that also has no DCM and uses suffixes. This checks a three-way conjunction across chapters.

theorem Phenomena.Case.Typology.ch49_ch50_same_sample : Phenomena.Case.Typology.ch49✝.length = Phenomena.Case.Typology.ch50✝.length

Ch 49 and Ch 50 share the same 261-language sample.

@cite{aissen-2003} DOM Hierarchy

Formalizes the bidimensional DOM predictions from:

• Aissen, J. (2003). Differential Object Marking: Iconicity vs. Economy. Natural Language & Linguistic Theory 21(3): 435--483.

The prominence scales (AnimacyLevel, DefinitenessLevel) and their orderings are defined in Core.Prominence and re-exported here. DOM is the P-flagging specialization of the general differential marking framework.

@[reducible, inline]

abbrev Phenomena.Case.Typology.DOMProfile : Type

A DOM (Differential Object Marking) profile: a DifferentialMarkingProfile specialized to role P + channel flagging.

Each cell (a, d) records whether an object with animacy level a and definiteness level d obligatorily receives an overt DOM marker (e.g., Spanish a, Turkish -(y)I, Hindi -ko).

DOM is the P-flagging instance of @cite{just-2024}'s general differential marking framework. Monotonicity (isMonotone), isAnimacyOnly, and isDefinitenessOnly are all inherited from DifferentialMarkingProfile.

Equations

• Phenomena.Case.Typology.DOMProfile = Core.Prominence.DifferentialMarkingProfile

def Phenomena.Case.Typology.spanishDOM : DOMProfile

Spanish: a-marking for human direct objects regardless of definiteness. One-dimensional (animacy-based), cutoff between human and animate.

Equations

• Phenomena.Case.Typology.spanishDOM = Core.Prominence.DifferentialMarkingProfile.animacyCutoffP "Spanish" Core.Prominence.MarkingChannel.flagging Core.Prominence.AnimacyLevel.human

def Phenomena.Case.Typology.russianDOM : DOMProfile

Russian: animate accusative (genitive form used as accusative for animate nouns). One-dimensional (animacy-based), cutoff between animate and inanimate.

Equations

• Phenomena.Case.Typology.russianDOM = Core.Prominence.DifferentialMarkingProfile.animacyCutoffP "Russian" Core.Prominence.MarkingChannel.flagging Core.Prominence.AnimacyLevel.animate

def Phenomena.Case.Typology.turkishDOM : DOMProfile

Turkish: -(y)I marking for definite direct objects regardless of animacy. One-dimensional (definiteness-based), cutoff between definite and indefinite specific.

Equations

• Phenomena.Case.Typology.turkishDOM = Core.Prominence.DifferentialMarkingProfile.definitenessCutoffP "Turkish" Core.Prominence.MarkingChannel.flagging Core.Prominence.DefinitenessLevel.definite

def Phenomena.Case.Typology.hebrewDOM : DOMProfile

Hebrew: ʔet marking for definite direct objects regardless of animacy. Same one-dimensional definiteness cutoff as Turkish.

Equations

• Phenomena.Case.Typology.hebrewDOM = Core.Prominence.DifferentialMarkingProfile.definitenessCutoffP "Hebrew" Core.Prominence.MarkingChannel.flagging Core.Prominence.DefinitenessLevel.definite

def Phenomena.Case.Typology.persianDOM : DOMProfile

Persian: -rā marking for definite direct objects. One-dimensional (definiteness-based) for obligatory marking; optional extension to specific indefinite animates. Modeled here with the definiteness-based obligatory core.

Equations

• Phenomena.Case.Typology.persianDOM = Core.Prominence.DifferentialMarkingProfile.definitenessCutoffP "Persian" Core.Prominence.MarkingChannel.flagging Core.Prominence.DefinitenessLevel.definite

def Phenomena.Case.Typology.catalanDOM : DOMProfile

Catalan: a-marking restricted to personal pronouns. The most restrictive DOM pattern attested: only the highest cell on the definiteness scale receives marking.

Equations

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

def Phenomena.Case.Typology.hindiDOM : DOMProfile

Hindi-Urdu: -ko marking conditioned by BOTH animacy and definiteness. Two-dimensional DOM with a staircase cutoff:

• Human objects: marked when indefinite specific or more prominent
• Animate objects: marked when definite or more prominent
• Inanimate objects: not obligatorily marked

This captures the obligatory marking core. Optional/variable marking extends further down the staircase at the boundary cells.

Equations

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

def Phenomena.Case.Typology.noDOMProfile : DOMProfile

No DOM: no differential marking (either no case at all, or uniform case on all objects). Trivially monotone.

Equations

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

def Phenomena.Case.Typology.allDOMProfiles : List DOMProfile

All DOM profiles in the sample.

Equations

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

theorem Phenomena.Case.Typology.allDOMProfiles_count : allDOMProfiles.length = 8

Each language's DOM pattern forms an upper set in the bidimensional animacy × definiteness grid — Aissen's central prediction.

theorem Phenomena.Case.Typology.spanish_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone spanishDOM = true

theorem Phenomena.Case.Typology.russian_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone russianDOM = true

theorem Phenomena.Case.Typology.turkish_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone turkishDOM = true

theorem Phenomena.Case.Typology.hebrew_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone hebrewDOM = true

theorem Phenomena.Case.Typology.persian_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone persianDOM = true

theorem Phenomena.Case.Typology.catalan_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone catalanDOM = true

theorem Phenomena.Case.Typology.hindi_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone hindiDOM = true

theorem Phenomena.Case.Typology.no_dom_monotone : Core.Prominence.DifferentialMarkingProfile.isMonotone noDOMProfile = true

theorem Phenomena.Case.Typology.dom_monotonicity_universal : (allDOMProfiles.all fun (x : DOMProfile) => Core.Prominence.DifferentialMarkingProfile.isMonotone x) = true

Aissen's DOM monotonicity universal: all attested DOM patterns in the sample form upper sets in the bidimensional animacy × definiteness grid. No language marks a less-prominent object while leaving a more-prominent one unmarked.

Verify that the one-dimensional profiles are indeed one-dimensional, and that Hindi is genuinely two-dimensional.

theorem Phenomena.Case.Typology.spanish_animacy_only : Core.Prominence.DifferentialMarkingProfile.isAnimacyOnly spanishDOM = true

theorem Phenomena.Case.Typology.russian_animacy_only : Core.Prominence.DifferentialMarkingProfile.isAnimacyOnly russianDOM = true

theorem Phenomena.Case.Typology.turkish_definiteness_only : Core.Prominence.DifferentialMarkingProfile.isDefinitenessOnly turkishDOM = true

theorem Phenomena.Case.Typology.hebrew_definiteness_only : Core.Prominence.DifferentialMarkingProfile.isDefinitenessOnly hebrewDOM = true

theorem Phenomena.Case.Typology.persian_definiteness_only : Core.Prominence.DifferentialMarkingProfile.isDefinitenessOnly persianDOM = true

theorem Phenomena.Case.Typology.catalan_definiteness_only : Core.Prominence.DifferentialMarkingProfile.isDefinitenessOnly catalanDOM = true

theorem Phenomena.Case.Typology.hindi_not_animacy_only : Core.Prominence.DifferentialMarkingProfile.isAnimacyOnly hindiDOM = false

Hindi DOM depends on both animacy and definiteness — it cannot be reduced to a single scale.

theorem Phenomena.Case.Typology.hindi_not_definiteness_only : Core.Prominence.DifferentialMarkingProfile.isDefinitenessOnly hindiDOM = false

Consequences of monotonicity: higher prominence on one dimension implies at least as much marking, holding the other dimension constant.

theorem Phenomena.Case.Typology.human_dominates_animate : (allDOMProfiles.all fun (p : DOMProfile) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => if p.marks Core.Prominence.AnimacyLevel.animate d = true then p.marks Core.Prominence.AnimacyLevel.human d else true) = true

In all sample languages, human objects are never less marked than animate objects at the same definiteness level.

theorem Phenomena.Case.Typology.animate_dominates_inanimate : (allDOMProfiles.all fun (p : DOMProfile) => Core.Prominence.DefinitenessLevel.all.all fun (d : Core.Prominence.DefinitenessLevel) => if p.marks Core.Prominence.AnimacyLevel.inanimate d = true then p.marks Core.Prominence.AnimacyLevel.animate d else true) = true

In all sample languages, animate objects are never less marked than inanimate objects at the same definiteness level.

theorem Phenomena.Case.Typology.pronoun_dominates_properName : (allDOMProfiles.all fun (p : DOMProfile) => Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => if p.marks a Core.Prominence.DefinitenessLevel.properName = true then p.marks a Core.Prominence.DefinitenessLevel.personalPronoun else true) = true

In all sample languages, pronouns are never less marked than proper names at the same animacy level.

theorem Phenomena.Case.Typology.definite_dominates_indefiniteSpecific : (allDOMProfiles.all fun (p : DOMProfile) => Core.Prominence.AnimacyLevel.all.all fun (a : Core.Prominence.AnimacyLevel) => if p.marks a Core.Prominence.DefinitenessLevel.indefiniteSpecific = true then p.marks a Core.Prominence.DefinitenessLevel.definite else true) = true

In all sample languages, definite NPs are never less marked than indefinite specific NPs at the same animacy level.

The most prominent cell (human, pronoun) is always marked when any DOM exists; the least prominent cell (inanimate, non-specific) is never marked in our sample.

theorem Phenomena.Case.Typology.top_cell_marked_if_any : (allDOMProfiles.all fun (p : DOMProfile) => if (Core.Prominence.AnimacyLevel.all.any fun (a : Core.Prominence.AnimacyLevel) => Core.Prominence.DefinitenessLevel.all.any fun (d : Core.Prominence.DefinitenessLevel) => p.marks a d) = true then p.marks Core.Prominence.AnimacyLevel.human Core.Prominence.DefinitenessLevel.personalPronoun else true) = true

If any cell is marked, the most prominent cell (human, pronoun) is also marked.

theorem Phenomena.Case.Typology.bottom_cell_unmarked : (allDOMProfiles.all fun (p : DOMProfile) => p.marks Core.Prominence.AnimacyLevel.inanimate Core.Prominence.DefinitenessLevel.nonSpecific == false) = true

The least prominent cell (inanimate, non-specific) is unmarked in all DOM languages in the sample.

theorem Phenomena.Case.Typology.grid_size : Core.Prominence.AnimacyLevel.all.length * Core.Prominence.DefinitenessLevel.all.length = 15

The bidimensional grid has 3 × 5 = 15 cells per language.

def Phenomena.Case.Typology.totalMarkedCells : Nat

Total marked cells across all sample languages.

Equations

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

theorem Phenomena.Case.Typology.total_marked_cells_value : totalMarkedCells = 52

Marked cells: Spanish (5) + Russian (10) + Turkish (9) + Hebrew (9) + Persian (9) + Catalan (3) + Hindi (7) + NoDOM (0) = 52.