Morphosyntactic Alignment Typology (WALS Chapters 98--100)

@cite{comrie-1978} @cite{comrie-2013} @cite{dixon-1994} @cite{dryer-haspelmath-2013} @cite{dixon-1972} @cite{haspelmath-2021}

Formalizes three chapters from the World Atlas of Language Structures (WALS) covering morphosyntactic alignment -- the way languages mark the core grammatical relations S (sole argument of intransitive), A (agent of transitive), and P (patient of transitive):

• Chapter 98: Alignment of Case Marking of Full Noun Phrases. How full NPs are case-marked for S, A, P roles.
• Chapter 99: Alignment of Case Marking of Pronouns. Same dimension but restricted to pronominal arguments, which frequently diverge from full NP marking.
• Chapter 100: Alignment of Verbal Person Marking. How person agreement on the verb distinguishes S, A, P.

Alignment Types

Five alignment patterns recur across all three domains:

• Neutral: S = A = P (no case/agreement distinction at all)
• Accusative: S = A vs P (subject grouped together, patient marked)
• Ergative: S = P vs A (absolutive grouped together, agent marked)
• Tripartite: S ≠ A ≠ P (all three distinctly marked)
• Active (or split-S): S splits into agent-like (= A) and patient-like (= P)

Key Generalizations

Accusative alignment dominates cross-linguistically in all three domains. However, the three domains frequently diverge within a single language -- the phenomenon of split ergativity. @cite{dixon-1994} established the generalization that ergative case marking is more common for full NPs than for pronouns: many "ergative" languages are ergative for NPs but accusative for pronouns (e.g., Dyirbal, many Australian languages). Tripartite and active systems are typologically rare.

inductive Phenomena.Alignment.Typology.AlignmentType : Type

Morphosyntactic alignment type for case marking or verbal person marking.

These five categories classify how a language groups the three core grammatical relations S, A, P:

• S = sole argument of an intransitive verb ("The man fell")
• A = agent-like argument of a transitive verb ("The man hit the dog")
• P = patient-like argument of a transitive verb ("The man hit the dog")

The alignment determines which relations receive the same morphological treatment (case marking or agreement pattern).

• neutral : AlignmentType

  Neutral (S = A = P): no morphological distinction among the three relations. Common in isolating languages (e.g., Mandarin, Thai).

• accusative : AlignmentType

  Accusative (S = A ≠ P): subject and agent grouped as "nominative", patient distinctly marked as "accusative". The most common pattern worldwide (e.g., English, Latin, Russian, Japanese).

• ergative : AlignmentType

  Ergative (S = P ≠ A): absolutive groups S and P, while A receives distinct "ergative" marking (e.g., Basque, Dyirbal NPs, Hindi perfective).

• tripartite : AlignmentType

  Tripartite (S ≠ A ≠ P): all three relations distinctly marked. Extremely rare (e.g., Nez Perce pronouns, some Australian languages).

• active : AlignmentType

  Active / split-S: intransitive S is split -- agent-like S patterns with A, patient-like S patterns with P. The split is typically lexically or semantically determined (e.g., Georgian, Guarani).

instance Phenomena.Alignment.Typology.instDecidableEqAlignmentType : DecidableEq AlignmentType

Equations

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

instance Phenomena.Alignment.Typology.instBEqAlignmentType : BEq AlignmentType

Equations

• Phenomena.Alignment.Typology.instBEqAlignmentType = { beq := Phenomena.Alignment.Typology.instBEqAlignmentType.beq }

def Phenomena.Alignment.Typology.instBEqAlignmentType.beq : AlignmentType → AlignmentType → Bool

Equations

• Phenomena.Alignment.Typology.instBEqAlignmentType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Alignment.Typology.instReprAlignmentType.repr : AlignmentType → Nat → Std.Format

Equations

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

instance Phenomena.Alignment.Typology.instReprAlignmentType : Repr AlignmentType

Equations

• Phenomena.Alignment.Typology.instReprAlignmentType = { reprPrec := Phenomena.Alignment.Typology.instReprAlignmentType.repr }

instance Phenomena.Alignment.Typology.instInhabitedAlignmentType : Inhabited AlignmentType

Equations

• Phenomena.Alignment.Typology.instInhabitedAlignmentType = { default := Phenomena.Alignment.Typology.AlignmentType.neutral }

def Phenomena.Alignment.Typology.AlignmentType.marksAgent : AlignmentType → Bool

Whether this alignment type marks the agent (A) distinctly from S.

Equations

• Phenomena.Alignment.Typology.AlignmentType.ergative.marksAgent = true
• Phenomena.Alignment.Typology.AlignmentType.tripartite.marksAgent = true
• x✝.marksAgent = false

def Phenomena.Alignment.Typology.AlignmentType.marksPatient : AlignmentType → Bool

Whether this alignment type marks the patient (P) distinctly from S.

Equations

• Phenomena.Alignment.Typology.AlignmentType.accusative.marksPatient = true
• Phenomena.Alignment.Typology.AlignmentType.tripartite.marksPatient = true
• x✝.marksPatient = false

def Phenomena.Alignment.Typology.AlignmentType.isNomAcc : AlignmentType → Bool

Whether this alignment groups S with A (nominative-accusative pattern).

Equations

• Phenomena.Alignment.Typology.AlignmentType.accusative.isNomAcc = true
• x✝.isNomAcc = false

def Phenomena.Alignment.Typology.AlignmentType.isAbsErg : AlignmentType → Bool

Whether this alignment groups S with P (absolutive-ergative pattern).

Equations

• Phenomena.Alignment.Typology.AlignmentType.ergative.isAbsErg = true
• x✝.isAbsErg = false

theorem Phenomena.Alignment.Typology.ch98_total : Phenomena.Alignment.Typology.ch98✝.length = 190

theorem Phenomena.Alignment.Typology.ch99_total : Phenomena.Alignment.Typology.ch99✝.length = 172

theorem Phenomena.Alignment.Typology.ch100_total : Phenomena.Alignment.Typology.ch100✝.length = 380

theorem Phenomena.Alignment.Typology.ch98_neutral_modal : have neutral := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.neutral) Phenomena.Alignment.Typology.ch98✝).length; neutral > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.nominativeAccusative) Phenomena.Alignment.Typology.ch98✝¹).length ∧ neutral > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.ergativeAbsolutive) Phenomena.Alignment.Typology.ch98✝²).length

Ch 98: Neutral marking is the most common for full NPs (many languages lack case marking on NPs entirely).

theorem Phenomena.Alignment.Typology.ch98_accusative_gt_ergative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.nominativeAccusative) Phenomena.Alignment.Typology.ch98✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.ergativeAbsolutive) Phenomena.Alignment.Typology.ch98✝¹).length

Ch 98: Among languages with case marking on NPs, accusative outnumbers ergative.

theorem Phenomena.Alignment.Typology.ch99_accusative_gt_ergative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => x.value == Core.WALS.F99A.PronounCaseAlignment.nominativeAccusative) Phenomena.Alignment.Typology.ch99✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => x.value == Core.WALS.F99A.PronounCaseAlignment.ergativeAbsolutive) Phenomena.Alignment.Typology.ch99✝¹).length

Ch 99: Accusative alignment outnumbers ergative for pronouns, though neutral is the most common category (many languages lack distinct pronoun case forms).

theorem Phenomena.Alignment.Typology.ch100_accusative_dominant : have acc := (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => x.value == Core.WALS.F100A.VerbalPersonAlignment.accusative) Phenomena.Alignment.Typology.ch100✝).length; acc > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => x.value == Core.WALS.F100A.VerbalPersonAlignment.neutral) Phenomena.Alignment.Typology.ch100✝¹).length ∧ acc > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => x.value == Core.WALS.F100A.VerbalPersonAlignment.ergative) Phenomena.Alignment.Typology.ch100✝²).length ∧ acc > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => x.value == Core.WALS.F100A.VerbalPersonAlignment.active) Phenomena.Alignment.Typology.ch100✝³).length

Ch 100: Accusative alignment is the most common for verbal person marking.

theorem Phenomena.Alignment.Typology.ch98_tripartite_rare : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.tripartite) Phenomena.Alignment.Typology.ch98✝).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.ergativeAbsolutive) Phenomena.Alignment.Typology.ch98✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.activeInactive) Phenomena.Alignment.Typology.ch98✝²).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => x.value == Core.WALS.F98A.NPCaseAlignment.ergativeAbsolutive) Phenomena.Alignment.Typology.ch98✝³).length

Ch 98: Tripartite and active-inactive alignments are the rarest for full NPs.

theorem Phenomena.Alignment.Typology.ch99_tripartite_rare : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => x.value == Core.WALS.F99A.PronounCaseAlignment.tripartite) Phenomena.Alignment.Typology.ch99✝).length < (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => x.value == Core.WALS.F99A.PronounCaseAlignment.ergativeAbsolutive) Phenomena.Alignment.Typology.ch99✝¹).length

Ch 99: Tripartite is also rare for pronouns.

structure Phenomena.Alignment.Typology.AlignmentProfile : Type

A language's alignment profile, combining classifications from all three WALS alignment chapters.

This structure records a single language's position in each of the three typological dimensions: case marking on full NPs (Ch 98), case marking on pronouns (Ch 99), and verbal person marking (Ch 100). Languages frequently have different alignment types in different domains -- this is the phenomenon of split ergativity.

• name : String

  Language name

• iso639 : String

  ISO 639-3 code

• npAlignment : AlignmentType

  Ch 98: Alignment of case marking of full NPs

• pronAlignment : AlignmentType

  Ch 99: Alignment of case marking of pronouns

• verbAlignment : AlignmentType

  Ch 100: Alignment of verbal person marking

• notes : String

  Notes on the alignment system

def Phenomena.Alignment.Typology.instReprAlignmentProfile.repr : AlignmentProfile → Nat → Std.Format

Equations

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

instance Phenomena.Alignment.Typology.instReprAlignmentProfile : Repr AlignmentProfile

Equations

• Phenomena.Alignment.Typology.instReprAlignmentProfile = { reprPrec := Phenomena.Alignment.Typology.instReprAlignmentProfile.repr }

instance Phenomena.Alignment.Typology.instDecidableEqAlignmentProfile : DecidableEq AlignmentProfile

Equations

• Phenomena.Alignment.Typology.instDecidableEqAlignmentProfile = Phenomena.Alignment.Typology.instDecidableEqAlignmentProfile.decEq

def Phenomena.Alignment.Typology.instDecidableEqAlignmentProfile.decEq (x✝ x✝¹ : AlignmentProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Alignment.Typology.instBEqAlignmentProfile : BEq AlignmentProfile

Equations

• Phenomena.Alignment.Typology.instBEqAlignmentProfile = { beq := Phenomena.Alignment.Typology.instBEqAlignmentProfile.beq }

def Phenomena.Alignment.Typology.instBEqAlignmentProfile.beq : AlignmentProfile → AlignmentProfile → Bool

Equations

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

def Phenomena.Alignment.Typology.AlignmentProfile.caseUniform (p : AlignmentProfile) : Bool

Whether NP and pronoun alignment match (no split ergativity in case).

Equations

• p.caseUniform = (p.npAlignment == p.pronAlignment)

def Phenomena.Alignment.Typology.AlignmentProfile.dixonSplit (p : AlignmentProfile) : Bool

Whether the language shows the classic NP-ergative / pronoun-accusative split (Dixon's generalization).

Equations

• p.dixonSplit = (p.npAlignment == Phenomena.Alignment.Typology.AlignmentType.ergative && p.pronAlignment == Phenomena.Alignment.Typology.AlignmentType.accusative)

def Phenomena.Alignment.Typology.AlignmentProfile.fullyUniform (p : AlignmentProfile) : Bool

Whether all three domains have the same alignment.

Equations

• p.fullyUniform = (p.npAlignment == p.pronAlignment && p.pronAlignment == p.verbAlignment)

def Phenomena.Alignment.Typology.AlignmentProfile.hasAnyErgative (p : AlignmentProfile) : Bool

Whether the language has any ergative alignment in any domain.

Equations

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

def Phenomena.Alignment.Typology.AlignmentProfile.accusativeCase (p : AlignmentProfile) : Bool

Whether the language has accusative alignment in all case-marking domains (NPs and pronouns).

Equations

• p.accusativeCase = (p.npAlignment == Phenomena.Alignment.Typology.AlignmentType.accusative && p.pronAlignment == Phenomena.Alignment.Typology.AlignmentType.accusative)

def Phenomena.Alignment.Typology.english : AlignmentProfile

English: accusative case marking on pronouns (I/me, he/him), no case on full NPs (neutral), and accusative verb agreement (verb agrees with subject = S/A grouping).

Equations

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

def Phenomena.Alignment.Typology.hindiUrdu : AlignmentProfile

Hindi-Urdu: split-ergative. Ergative case marking (-ne on A) in perfective aspect for both NPs and pronouns. Accusative alignment in imperfective. WALS codes the dominant pattern as ergative for NPs, accusative for pronouns (the pronoun forms are less consistently ergative). Verb agreement is neutral (agrees with unmarked argument).

Equations

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

def Phenomena.Alignment.Typology.basque : AlignmentProfile

Basque: consistently ergative across all three domains. Ergative case (-k) marks A on both NPs and pronouns. Verb agreement cross-references S/P (absolutive) and A (ergative) with distinct slots -- ergative alignment in agreement.

Equations

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

def Phenomena.Alignment.Typology.dyirbal : AlignmentProfile

Dyirbal (Pama-Nyungan, Australia): the textbook case of split ergativity. Full NPs have ergative case marking, but 1st/2nd person pronouns follow accusative alignment. Verb has no person agreement (neutral).

Equations

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

def Phenomena.Alignment.Typology.georgian : AlignmentProfile

Georgian: active (split-S) alignment. The verb agreement system shows an active pattern: some intransitive S arguments pattern like A, others like P, depending on the verb class (unergative vs. unaccusative). Case marking is also active in some series.

Equations

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

def Phenomena.Alignment.Typology.tagalog : AlignmentProfile

Tagalog: neutral case marking on NPs and pronouns (the Philippine voice system does not straightforwardly map to accusative/ergative alignment). Verbal person marking is also neutral in the WALS sense.

Equations

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

def Phenomena.Alignment.Typology.japanese : AlignmentProfile

Japanese: accusative case marking on NPs (ga nom, o acc) and pronouns. No verb person agreement (neutral).

Equations

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

def Phenomena.Alignment.Typology.latin : AlignmentProfile

Latin: accusative case marking on both NPs and pronouns (nominative vs. accusative). Verb agreement is accusative (agrees with S/A).

Equations

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

def Phenomena.Alignment.Typology.russian : AlignmentProfile

Russian: accusative alignment across all three domains. Nominative marks S/A, accusative marks P (with animacy-conditioned syncretism). Verb agrees with S/A.

Equations

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

def Phenomena.Alignment.Typology.mandarin : AlignmentProfile

Mandarin Chinese: neutral alignment in all three domains. No morphological case marking, no verb person agreement. Grammatical relations encoded by word order.

Equations

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

def Phenomena.Alignment.Typology.turkish : AlignmentProfile

Turkish: accusative case marking on NPs (with differential object marking) and pronouns. Verb agreement is accusative (agrees with S/A).

Equations

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

def Phenomena.Alignment.Typology.tongan : AlignmentProfile

Tongan (Austronesian): ergative case marking on NPs. Pronouns are also ergative. No verb person agreement (neutral).

Equations

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

def Phenomena.Alignment.Typology.guarani : AlignmentProfile

Guarani (Tupian): active (split-S) case marking and verb agreement. The set of prefixes used on the verb depends on whether the S argument is agent-like or patient-like.

Equations

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

def Phenomena.Alignment.Typology.samoan : AlignmentProfile

Samoan (Austronesian): ergative case marking on full NPs (ergative particle e before A). Pronouns have accusative alignment. Verb agreement is neutral.

Equations

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

def Phenomena.Alignment.Typology.german : AlignmentProfile

German: accusative case marking on NPs and pronouns (nom/acc distinction). Verb agreement is accusative (agrees with S/A).

Equations

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

def Phenomena.Alignment.Typology.swahili : AlignmentProfile

Swahili (Bantu): neutral case marking (no morphological case on NPs or pronouns). Verb agreement is accusative (subject prefixes cross-reference S/A).

Equations

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

def Phenomena.Alignment.Typology.tibetan : AlignmentProfile

Tibetan (Central, Lhasa): ergative case marking on NPs and pronouns (ergative particles -gis and -kyis on A). Verb is neutral (no person agreement).

Equations

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

def Phenomena.Alignment.Typology.nezPerce : AlignmentProfile

Nez Perce (Sahaptian): tripartite case marking on NPs (nominative for S, ergative for A, accusative for P -- all three distinctly marked). Pronouns are also tripartite. Verb agreement is accusative.

Equations

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

def Phenomena.Alignment.Typology.finnish : AlignmentProfile

Finnish: accusative case marking on NPs and pronouns (nominative for S/A, partitive/accusative for P). Verb agreement is accusative (agrees with S/A).

Equations

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

def Phenomena.Alignment.Typology.warlpiri : AlignmentProfile

Warlpiri (Pama-Nyungan, Australia): ergative case marking on full NPs (ergative -ngku and -rlu on A). Pronouns have accusative alignment (nom and acc). Verb agreement is neutral (no person marking on verb in the standard analysis).

Equations

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

def Phenomena.Alignment.Typology.dargwa : AlignmentProfile

Dargwa (Tanti; Nakh-Dagestanian): consistently ergative across all three domains. Ergative -li marks A on both full NPs and pronouns (@cite{sumbatova-2021} §4.4.3). Gender agreement on the verb is controlled by the absolutive argument (ergative alignment). Person agreement follows a hierarchical pattern (1,2 > 3; abs > erg) but the primary dimension is ergative. No tense-conditioned or animacy-conditioned split.

Equations

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

def Phenomena.Alignment.Typology.yukatek : AlignmentProfile

Yukatek Maya (Yucatecan Mayan): aspect-conditioned split-intransitive system. In perfective clauses (completive/subjunctive status), S is cross-referenced by set-B markers (ergative pattern). In imperfective clauses (incompletive status), S is cross-referenced by set-A markers (accusative pattern). Transitive marking is not affected by the split.

@cite{bohnemeyer-2004}: the split is not conditioned by lexical verb class (not split-S or fluid-S) but by viewpoint aspect, making it a typologically rare case of aspect-conditioned split intransitivity. WALS codes Yukatek verbal person marking as "split" (F100A).

Equations

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

def Phenomena.Alignment.Typology.allProfiles : List AlignmentProfile

All alignment profiles in our sample.

Equations

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

theorem Phenomena.Alignment.Typology.allProfiles_count : allProfiles.length = 22

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

All ISO 639-3 codes are non-empty.

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

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

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

No duplicate ISO codes (each language appears once).

Spot-checks that each language has the expected alignment values.

theorem Phenomena.Alignment.Typology.english_np_neutral : english.npAlignment = AlignmentType.neutral

theorem Phenomena.Alignment.Typology.basque_np_ergative : basque.npAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.japanese_np_accusative : japanese.npAlignment = AlignmentType.accusative

theorem Phenomena.Alignment.Typology.georgian_np_active : georgian.npAlignment = AlignmentType.active

theorem Phenomena.Alignment.Typology.nezPerce_np_tripartite : nezPerce.npAlignment = AlignmentType.tripartite

theorem Phenomena.Alignment.Typology.dyirbal_np_ergative : dyirbal.npAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.english_pron_accusative : english.pronAlignment = AlignmentType.accusative

theorem Phenomena.Alignment.Typology.basque_pron_ergative : basque.pronAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.dyirbal_pron_accusative : dyirbal.pronAlignment = AlignmentType.accusative

theorem Phenomena.Alignment.Typology.tagalog_pron_neutral : tagalog.pronAlignment = AlignmentType.neutral

theorem Phenomena.Alignment.Typology.basque_verb_ergative : basque.verbAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.latin_verb_accusative : latin.verbAlignment = AlignmentType.accusative

theorem Phenomena.Alignment.Typology.japanese_verb_neutral : japanese.verbAlignment = AlignmentType.neutral

theorem Phenomena.Alignment.Typology.georgian_verb_active : georgian.verbAlignment = AlignmentType.active

theorem Phenomena.Alignment.Typology.dargwa_np_ergative : dargwa.npAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.dargwa_pron_ergative : dargwa.pronAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.dargwa_verb_ergative : dargwa.verbAlignment = AlignmentType.ergative

theorem Phenomena.Alignment.Typology.yukatek_np_neutral : yukatek.npAlignment = AlignmentType.neutral

theorem Phenomena.Alignment.Typology.yukatek_pron_neutral : yukatek.pronAlignment = AlignmentType.neutral

theorem Phenomena.Alignment.Typology.yukatek_verb_active : yukatek.verbAlignment = AlignmentType.active

theorem Phenomena.Alignment.Typology.dyirbal_is_dixon_split : dyirbal.dixonSplit = true

theorem Phenomena.Alignment.Typology.hindiUrdu_is_dixon_split : hindiUrdu.dixonSplit = true

theorem Phenomena.Alignment.Typology.warlpiri_is_dixon_split : warlpiri.dixonSplit = true

theorem Phenomena.Alignment.Typology.samoan_is_dixon_split : samoan.dixonSplit = true

theorem Phenomena.Alignment.Typology.basque_fully_uniform : basque.fullyUniform = true

theorem Phenomena.Alignment.Typology.dargwa_fully_uniform : dargwa.fullyUniform = true

theorem Phenomena.Alignment.Typology.mandarin_fully_uniform : mandarin.fullyUniform = true

theorem Phenomena.Alignment.Typology.latin_fully_uniform : latin.fullyUniform = true

Generalization 1: Accusative is the most common alignment for pronouns.

Across WALS Ch 99, accusative (83) outnumbers all other pronoun alignment types. In our sample, accusative pronoun marking is likewise the most frequent pattern.

theorem Phenomena.Alignment.Typology.gen1_accusative_most_common_pronouns : (List.filter (fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.accusative) allProfiles).length ≥ (List.filter (fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.ergative) allProfiles).length

Generalization 2: Ergative NP marking is more common than ergative

pronoun marking (Dixon's generalization).

@cite{dixon-1994} established that in the animacy/nominal hierarchy, ergative case marking is more likely to appear on full NPs than on pronouns. In our sample, more languages have ergative NP alignment than ergative pronoun alignment.

theorem Phenomena.Alignment.Typology.gen2_dixon_generalization : (List.filter (fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.ergative) allProfiles).length > (List.filter (fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.ergative) allProfiles).length

Generalization 3: Split ergativity -- ergative NPs with accusative

pronouns.

Many "ergative" languages show a split: NPs are ergative but pronouns are accusative. This pattern is attested multiple times in our sample (Dyirbal, Hindi-Urdu, Samoan, Warlpiri).

theorem Phenomena.Alignment.Typology.gen3_split_ergativity_attested : (List.filter (fun (p : AlignmentProfile) => p.dixonSplit) allProfiles).length ≥ 4

Generalization 4: No language has accusative NPs with ergative pronouns.

The reverse of Dixon's split (accusative NPs, ergative pronouns) is predicted not to occur. Our sample confirms this: whenever pronouns are ergative, NPs are at least ergative too.

theorem Phenomena.Alignment.Typology.gen4_no_reverse_dixon : (allProfiles.all fun (p : AlignmentProfile) => if (p.pronAlignment == AlignmentType.ergative) = true then p.npAlignment == AlignmentType.ergative || p.npAlignment == AlignmentType.tripartite else true) = true

Generalization 5: Tripartite alignment is extremely rare.

In WALS Ch 98, only 2 out of 190 languages have tripartite NP alignment. In our sample, only Nez Perce is tripartite for NPs.

theorem Phenomena.Alignment.Typology.gen5_tripartite_rare_nps : (List.filter (fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.tripartite) allProfiles).length ≤ 1

theorem Phenomena.Alignment.Typology.gen5_tripartite_rare_pronouns : (List.filter (fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.tripartite) allProfiles).length ≤ 1

Generalization 6: Active alignment is rare for case marking.

Active (split-S) systems are uncommon for case marking. In our sample, only Georgian shows active case marking on NPs and pronouns.

theorem Phenomena.Alignment.Typology.gen6_active_rare_case : (List.filter (fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.active) allProfiles).length ≤ 2

Generalization 6a: Aspect-conditioned split intransitivity.

Yukatek Maya and Georgian both show active (split-S) verbal person marking. In both languages, the split is conditioned by viewpoint aspect: perfective triggers ergative-like marking, imperfective triggers accusative-like marking. @cite{bohnemeyer-2004} argues this reduces to a single linking-by-viewpoint mechanism projected from the causal chain of subevents in event structure.

theorem Phenomena.Alignment.Typology.gen6a_aspect_split_languages : (List.filter (fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.active) allProfiles).length ≥ 2

theorem Phenomena.Alignment.Typology.gen6a_yukatek_and_georgian_both_active : yukatek.verbAlignment = AlignmentType.active ∧ georgian.verbAlignment = AlignmentType.active

Generalization 7: Languages with ergative NP marking tend to have

ergative or neutral verbal person marking.

When NP case is ergative, the verb agreement is typically either ergative (like Basque) or neutral (like Dyirbal, Tibetan). Accusative verb agreement with ergative NP case is uncommon.

theorem Phenomena.Alignment.Typology.gen7_erg_np_verb_pattern : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.ergative) = true then p.verbAlignment == AlignmentType.ergative || p.verbAlignment == AlignmentType.neutral || p.verbAlignment == AlignmentType.accusative else true) = true

Generalization 8: All five alignment types are attested for NPs.

Our sample covers every WALS alignment category for full NPs.

theorem Phenomena.Alignment.Typology.gen8_all_np_types_attested : (((((allProfiles.any fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.neutral) && allProfiles.any fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.accusative) && allProfiles.any fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.ergative) && allProfiles.any fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.tripartite) && decide ((allProfiles.any fun (p : AlignmentProfile) => p.npAlignment == AlignmentType.active) = true)) = true

Generalization 9: All five alignment types are attested for pronouns.

theorem Phenomena.Alignment.Typology.gen9_all_pron_types_attested : (((((allProfiles.any fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.neutral) && allProfiles.any fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.accusative) && allProfiles.any fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.ergative) && allProfiles.any fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.tripartite) && decide ((allProfiles.any fun (p : AlignmentProfile) => p.pronAlignment == AlignmentType.active) = true)) = true

Generalization 10: Four of the five alignment types are attested for

verbal person marking. Tripartite verb agreement is exceedingly rare cross-linguistically (WALS Ch 100 lists only 5 out of 378 languages) and is not represented in our sample.

theorem Phenomena.Alignment.Typology.gen10_verb_types_attested : ((((allProfiles.any fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.neutral) && allProfiles.any fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.accusative) && allProfiles.any fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.ergative) && decide ((allProfiles.any fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.active) = true)) = true

theorem Phenomena.Alignment.Typology.gen10_tripartite_verb_unattested : (allProfiles.all fun (p : AlignmentProfile) => p.verbAlignment != AlignmentType.tripartite) = true

Generalization 11: Neutral NP alignment implies neutral or accusative

pronoun alignment.

Languages without case marking on NPs (neutral) either also lack case marking on pronouns (neutral) or have accusative pronoun case (like English, where case survives only on pronouns). They never have ergative pronoun case without NP case.

theorem Phenomena.Alignment.Typology.gen11_neutral_np_pronoun : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.neutral) = true then p.pronAlignment == AlignmentType.neutral || p.pronAlignment == AlignmentType.accusative else true) = true

Generalization 12: Fully uniform alignment is common.

Many languages have the same alignment type across all three domains. This includes languages like Basque (uniformly ergative), Mandarin (uniformly neutral), Latin/Russian/Turkish (uniformly accusative), and Georgian (uniformly active).

theorem Phenomena.Alignment.Typology.gen12_uniform_common : (List.filter (fun (p : AlignmentProfile) => p.fullyUniform) allProfiles).length ≥ 5

Generalization 13: Accusative verb agreement is the dominant pattern

among languages that have verb agreement.

Among languages with non-neutral verb alignment, accusative agreement (verb agrees with S/A, i.e., subject agreement) is the most common.

theorem Phenomena.Alignment.Typology.gen13_accusative_verb_dominant : (List.filter (fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.accusative) allProfiles).length > (List.filter (fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.ergative) allProfiles).length ∧ (List.filter (fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.accusative) allProfiles).length > (List.filter (fun (p : AlignmentProfile) => p.verbAlignment == AlignmentType.active) allProfiles).length

def Phenomena.Alignment.Typology.ergativeNpCount : Nat

Number of languages with ergative NP alignment.

Equations

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

def Phenomena.Alignment.Typology.ergativePronCount : Nat

Number of languages with ergative pronoun alignment.

Equations

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

def Phenomena.Alignment.Typology.dixonSplitCount : Nat

Number of languages with Dixon-split ergativity.

Equations

• Phenomena.Alignment.Typology.dixonSplitCount = (List.filter (fun (p : Phenomena.Alignment.Typology.AlignmentProfile) => p.dixonSplit) Phenomena.Alignment.Typology.allProfiles).length

def Phenomena.Alignment.Typology.uniformCount : Nat

Number of fully uniform languages.

Equations

• Phenomena.Alignment.Typology.uniformCount = (List.filter (fun (p : Phenomena.Alignment.Typology.AlignmentProfile) => p.fullyUniform) Phenomena.Alignment.Typology.allProfiles).length

theorem Phenomena.Alignment.Typology.ergativeNp_is_8 : ergativeNpCount = 8

theorem Phenomena.Alignment.Typology.ergativePron_is_4 : ergativePronCount = 4

theorem Phenomena.Alignment.Typology.dixonSplit_is_4 : dixonSplitCount = 4

theorem Phenomena.Alignment.Typology.uniform_is_10 : uniformCount = 10

theorem Phenomena.Alignment.Typology.neutral_np_not_ergative : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.neutral) = true then !p.npAlignment.marksAgent else true) = true

Languages with no case on NPs should not have ergative NP alignment.

theorem Phenomena.Alignment.Typology.tripartite_marks_both : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.tripartite) = true then p.npAlignment.marksAgent && p.npAlignment.marksPatient else true) = true

Languages with tripartite case mark both A and P.

theorem Phenomena.Alignment.Typology.ergative_marks_agent_only : AlignmentType.ergative.marksAgent = true ∧ AlignmentType.ergative.marksPatient = false

Ergative alignment marks agent but not patient (S = P grouping).

theorem Phenomena.Alignment.Typology.accusative_marks_patient_only : AlignmentType.accusative.marksPatient = true ∧ AlignmentType.accusative.marksAgent = false

Accusative alignment marks patient but not agent (S = A grouping).

theorem Phenomena.Alignment.Typology.accusative_np_implies_accusative_pron : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.accusative) = true then p.pronAlignment == AlignmentType.accusative else true) = true

In our sample, every language with accusative NP case also has accusative pronoun case. (Accusative alignment does not split across the NP/pronoun divide the way ergative does.)

theorem Phenomena.Alignment.Typology.tripartite_np_implies_tripartite_pron : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.tripartite) = true then p.pronAlignment == AlignmentType.tripartite else true) = true

No language has tripartite NP alignment without also having tripartite pronoun alignment (in our sample).

theorem Phenomena.Alignment.Typology.active_np_implies_active_pron : (allProfiles.all fun (p : AlignmentProfile) => if (p.npAlignment == AlignmentType.active) = true then p.pronAlignment == AlignmentType.active else true) = true

Active NP alignment implies active pronoun alignment in our sample.

theorem Phenomena.Alignment.Typology.english_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "eng") = some english.npAlignment

theorem Phenomena.Alignment.Typology.japanese_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "jpn") = some japanese.npAlignment

theorem Phenomena.Alignment.Typology.russian_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "rus") = some russian.npAlignment

theorem Phenomena.Alignment.Typology.mandarin_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "mnd") = some mandarin.npAlignment

theorem Phenomena.Alignment.Typology.turkish_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "tur") = some turkish.npAlignment

theorem Phenomena.Alignment.Typology.german_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "ger") = some german.npAlignment

theorem Phenomena.Alignment.Typology.swahili_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "swa") = some swahili.npAlignment

theorem Phenomena.Alignment.Typology.tagalog_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "tag") = some tagalog.npAlignment

theorem Phenomena.Alignment.Typology.nezPerce_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "nez") = some nezPerce.npAlignment

theorem Phenomena.Alignment.Typology.finnish_ch98 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F98A.NPCaseAlignment) => Phenomena.Alignment.Typology.fromWALS98A✝ x.value) (Core.WALS.F98A.lookup "fin") = some finnish.npAlignment

theorem Phenomena.Alignment.Typology.english_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "eng") = some english.pronAlignment

theorem Phenomena.Alignment.Typology.japanese_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "jpn") = some japanese.pronAlignment

theorem Phenomena.Alignment.Typology.russian_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "rus") = some russian.pronAlignment

theorem Phenomena.Alignment.Typology.mandarin_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "mnd") = some mandarin.pronAlignment

theorem Phenomena.Alignment.Typology.turkish_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "tur") = some turkish.pronAlignment

theorem Phenomena.Alignment.Typology.german_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "ger") = some german.pronAlignment

theorem Phenomena.Alignment.Typology.swahili_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "swa") = some swahili.pronAlignment

theorem Phenomena.Alignment.Typology.tagalog_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "tag") = some tagalog.pronAlignment

theorem Phenomena.Alignment.Typology.nezPerce_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "nez") = some nezPerce.pronAlignment

theorem Phenomena.Alignment.Typology.finnish_ch99 : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F99A.PronounCaseAlignment) => Phenomena.Alignment.Typology.fromWALS99A✝ x.value) (Core.WALS.F99A.lookup "fin") = some finnish.pronAlignment

theorem Phenomena.Alignment.Typology.english_ch100 : ((Core.WALS.F100A.lookup "eng").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some english.verbAlignment

theorem Phenomena.Alignment.Typology.russian_ch100 : ((Core.WALS.F100A.lookup "rus").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some russian.verbAlignment

theorem Phenomena.Alignment.Typology.mandarin_ch100 : ((Core.WALS.F100A.lookup "mnd").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some mandarin.verbAlignment

theorem Phenomena.Alignment.Typology.turkish_ch100 : ((Core.WALS.F100A.lookup "tur").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some turkish.verbAlignment

theorem Phenomena.Alignment.Typology.german_ch100 : ((Core.WALS.F100A.lookup "ger").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some german.verbAlignment

theorem Phenomena.Alignment.Typology.swahili_ch100 : ((Core.WALS.F100A.lookup "swa").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some swahili.verbAlignment

theorem Phenomena.Alignment.Typology.tagalog_ch100 : ((Core.WALS.F100A.lookup "tag").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some tagalog.verbAlignment

theorem Phenomena.Alignment.Typology.basque_ch100 : ((Core.WALS.F100A.lookup "bsq").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some basque.verbAlignment

theorem Phenomena.Alignment.Typology.finnish_ch100 : ((Core.WALS.F100A.lookup "fin").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some finnish.verbAlignment

theorem Phenomena.Alignment.Typology.japanese_ch100 : ((Core.WALS.F100A.lookup "jpn").bind fun (x : Core.WALS.Datapoint Core.WALS.F100A.VerbalPersonAlignment) => Phenomena.Alignment.Typology.fromWALS100A✝ x.value) = some japanese.verbAlignment

Silverstein's Hierarchy

@cite{silverstein-1976} predicts that ergative marking targets the less prominent end of the animacy/definiteness scale. More prominent NPs (pronouns, 1st/2nd person) get accusative treatment; less prominent NPs (full NPs, 3rd person, inanimate) get ergative treatment.

The silverstein function encodes this as a threshold-based predicate over prominence values, and its monotonicity property captures the implicational nature of the hierarchy: if a less-prominent NP gets accusative treatment, all more-prominent NPs do too.

The dyirbalSplit instantiates Core.SplitErgativity for Dyirbal's animacy-conditioned split, connecting the split mechanism to the dyirbal alignment profile above.

• Silverstein, M. (1976). Hierarchy of features and ergativity. In Dixon, R. M. W. (ed.), Grammatical Categories in Australian Languages. AIAS.

def Phenomena.Alignment.Typology.silverstein (threshold npProminence : Nat) : Core.AlignmentFamily

Silverstein's hierarchy: NPs at or above the prominence threshold get accusative alignment; those below get ergative.

Equations

• Phenomena.Alignment.Typology.silverstein threshold npProminence = if npProminence ≥ threshold then Core.AlignmentFamily.accusative else Core.AlignmentFamily.ergative

theorem Phenomena.Alignment.Typology.silverstein_monotone (threshold p₁ p₂ : Nat) (h_ge : p₁ ≥ p₂) (h_acc : silverstein threshold p₂ = Core.AlignmentFamily.accusative) : silverstein threshold p₁ = Core.AlignmentFamily.accusative

Silverstein is monotone: if prominence p₁ ≥ p₂ and p₂ gets accusative, then p₁ gets accusative. (Higher prominence → more likely accusative.)

theorem Phenomena.Alignment.Typology.silverstein_predicts_dixon : silverstein 1 0 = Core.AlignmentFamily.ergative ∧ silverstein 1 1 = Core.AlignmentFamily.accusative

Silverstein predicts Dixon's generalization: with threshold 1, full NPs (prominence 0) get ergative, pronouns (prominence 1) get accusative — exactly the NP-ergative / pronoun-accusative split.

def Phenomena.Alignment.Typology.dyirbalSplit : Core.SplitErgativity Core.Prominence.AnimacyLevel

Dyirbal-style split by animacy: human/animate → accusative, inanimate → ergative (@cite{dixon-1972}, @cite{blake-1994} Ch. 4).

Equations

• Phenomena.Alignment.Typology.dyirbalSplit = { ergCondition := fun (a : Core.Prominence.AnimacyLevel) => a == Core.Prominence.AnimacyLevel.inanimate }

theorem Phenomena.Alignment.Typology.dyirbal_human_acc : dyirbalSplit.alignment Core.Prominence.AnimacyLevel.human = Core.AlignmentFamily.accusative

theorem Phenomena.Alignment.Typology.dyirbal_inanimate_erg : dyirbalSplit.alignment Core.Prominence.AnimacyLevel.inanimate = Core.AlignmentFamily.ergative

theorem Phenomena.Alignment.Typology.dyirbal_split_matches_np : Phenomena.Alignment.Typology.toAlignmentType✝ (dyirbalSplit.alignment Core.Prominence.AnimacyLevel.inanimate) = dyirbal.npAlignment

The Dyirbal split matches the Dyirbal alignment profile: inanimate NPs get ergative alignment (matching dyirbal.npAlignment).

theorem Phenomena.Alignment.Typology.dyirbal_split_matches_pron : Phenomena.Alignment.Typology.toAlignmentType✝ (dyirbalSplit.alignment Core.Prominence.AnimacyLevel.human) = dyirbal.pronAlignment

Human/animate arguments get accusative alignment (matching dyirbal.pronAlignment).

Ditransitive alignment classifies how a language codes R (recipient) and T (theme) relative to the monotransitive roles A and P.

The terminology follows @cite{haspelmath-2005}:
- **Indirective**: T = P, R distinctly marked (like accusative for
  monotransitives: the "subject-like" argument is unmarked)
- **Secundative**: R = P, T distinctly marked (like ergative for
  monotransitives: the "object-like" argument is unmarked)
- **Neutral**: R = T = P (no distinction among objects)
- **Tripartite**: R ≠ T ≠ P (all three distinctly marked)

Haspelmath's key observation: indirective is to ditransitives what
accusative is to monotransitives; secundative is to ditransitives
what ergative is to monotransitives. 

inductive Phenomena.Alignment.Typology.DitransitiveAlignment : Type

Ditransitive alignment type. Classifies how R (recipient) and T (theme) are coded relative to the monotransitive P.

• neutral : DitransitiveAlignment

  Neutral (R = T = P): no distinction among non-agent arguments

• indirective : DitransitiveAlignment

  Indirective (T = P ≠ R): R is distinctly marked, T patterns with P. Analogous to accusative alignment. E.g., English "give the book TO Mary".

• secundative : DitransitiveAlignment

  Secundative (R = P ≠ T): T is distinctly marked, R patterns with P. Analogous to ergative alignment. E.g., many Bantu applicatives.

• tripartite : DitransitiveAlignment

  Tripartite (R ≠ T ≠ P): all three roles distinctly marked

instance Phenomena.Alignment.Typology.instDecidableEqDitransitiveAlignment : DecidableEq DitransitiveAlignment

Equations

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

instance Phenomena.Alignment.Typology.instBEqDitransitiveAlignment : BEq DitransitiveAlignment

Equations

• Phenomena.Alignment.Typology.instBEqDitransitiveAlignment = { beq := Phenomena.Alignment.Typology.instBEqDitransitiveAlignment.beq }

def Phenomena.Alignment.Typology.instBEqDitransitiveAlignment.beq : DitransitiveAlignment → DitransitiveAlignment → Bool

Equations

• Phenomena.Alignment.Typology.instBEqDitransitiveAlignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Alignment.Typology.instReprDitransitiveAlignment.repr : DitransitiveAlignment → Nat → Std.Format

Equations

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

instance Phenomena.Alignment.Typology.instReprDitransitiveAlignment : Repr DitransitiveAlignment

Equations

• Phenomena.Alignment.Typology.instReprDitransitiveAlignment = { reprPrec := Phenomena.Alignment.Typology.instReprDitransitiveAlignment.repr }

def Phenomena.Alignment.Typology.DitransitiveAlignment.marksR : DitransitiveAlignment → Bool

Whether this ditransitive alignment marks R distinctly from P.

Equations

• Phenomena.Alignment.Typology.DitransitiveAlignment.indirective.marksR = true
• Phenomena.Alignment.Typology.DitransitiveAlignment.tripartite.marksR = true
• x✝.marksR = false

def Phenomena.Alignment.Typology.DitransitiveAlignment.marksT : DitransitiveAlignment → Bool

Whether this ditransitive alignment marks T distinctly from P.

Equations

• Phenomena.Alignment.Typology.DitransitiveAlignment.secundative.marksT = true
• Phenomena.Alignment.Typology.DitransitiveAlignment.tripartite.marksT = true
• x✝.marksT = false

structure Phenomena.Alignment.Typology.DitransitiveProfile : Type

A language's ditransitive alignment profile.

• name : String
• iso639 : String
• alignment : DitransitiveAlignment
• notes : String

instance Phenomena.Alignment.Typology.instReprDitransitiveProfile : Repr DitransitiveProfile

Equations

• Phenomena.Alignment.Typology.instReprDitransitiveProfile = { reprPrec := Phenomena.Alignment.Typology.instReprDitransitiveProfile.repr }

def Phenomena.Alignment.Typology.instReprDitransitiveProfile.repr : DitransitiveProfile → Nat → Std.Format

Equations

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

instance Phenomena.Alignment.Typology.instDecidableEqDitransitiveProfile : DecidableEq DitransitiveProfile

Equations

• Phenomena.Alignment.Typology.instDecidableEqDitransitiveProfile = Phenomena.Alignment.Typology.instDecidableEqDitransitiveProfile.decEq

def Phenomena.Alignment.Typology.instDecidableEqDitransitiveProfile.decEq (x✝ x✝¹ : DitransitiveProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Alignment.Typology.instBEqDitransitiveProfile.beq : DitransitiveProfile → DitransitiveProfile → Bool

Equations

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

instance Phenomena.Alignment.Typology.instBEqDitransitiveProfile : BEq DitransitiveProfile

Equations

• Phenomena.Alignment.Typology.instBEqDitransitiveProfile = { beq := Phenomena.Alignment.Typology.instBEqDitransitiveProfile.beq }

def Phenomena.Alignment.Typology.ditrans_english : DitransitiveProfile

English: indirective (T = P, R marked with "to"). "give the book to Mary" vs. "give Mary the book" (double-object alternation, but prepositional dative is the indirective base).

Equations

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

def Phenomena.Alignment.Typology.ditrans_german : DitransitiveProfile

German: indirective (T = ACC, R = DAT).

Equations

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

def Phenomena.Alignment.Typology.ditrans_latin : DitransitiveProfile

Latin: indirective (T = ACC, R = DAT).

Equations

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

def Phenomena.Alignment.Typology.ditrans_japanese : DitransitiveProfile

Japanese: indirective (T = o, R = ni).

Equations

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

def Phenomena.Alignment.Typology.ditrans_swahili : DitransitiveProfile

Swahili: secundative (R = P, T distinctly marked via applicative).

Equations

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

def Phenomena.Alignment.Typology.ditrans_mandarin : DitransitiveProfile

Mandarin: neutral (R and T both unmarked, distinguished by order).

Equations

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

def Phenomena.Alignment.Typology.allDitransProfiles : List DitransitiveProfile

Equations

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

theorem Phenomena.Alignment.Typology.ditrans_indirective_attested : (allDitransProfiles.any fun (p : DitransitiveProfile) => p.alignment == DitransitiveAlignment.indirective) = true

Indirective alignment is attested.

theorem Phenomena.Alignment.Typology.ditrans_secundative_attested : (allDitransProfiles.any fun (p : DitransitiveProfile) => p.alignment == DitransitiveAlignment.secundative) = true

Secundative alignment is attested.

theorem Phenomena.Alignment.Typology.ditrans_neutral_attested : (allDitransProfiles.any fun (p : DitransitiveProfile) => p.alignment == DitransitiveAlignment.neutral) = true

Neutral ditransitive alignment is attested.

theorem Phenomena.Alignment.Typology.ditrans_indirective_more_common : (List.filter (fun (p : DitransitiveProfile) => p.alignment == DitransitiveAlignment.indirective) allDitransProfiles).length > (List.filter (fun (p : DitransitiveProfile) => p.alignment == DitransitiveAlignment.secundative) allDitransProfiles).length

Indirective is more common than secundative (parallel to accusative being more common than ergative for monotransitives).

Bridge: Fragment grammatical descriptions ↔ Typology classifications

These theorems verify that the inline AlignmentProfile entries are consistent with the grammatical facts described in each language's Fragment directory. The Fragment describes what the language does (e.g., agent gets ERG, patient gets ABS); the Typology classifies that pattern (e.g., ergative NP alignment). Bridge theorems ensure the classification faithfully reflects the grammar.

Languages without Fragment directories rely on WALS grounding (above) instead.

theorem Phenomena.Alignment.Typology.dargwa_fragment_bridge : Fragments.Dargwa.Case.agentCase = Core.Case.erg ∧ Fragments.Dargwa.Case.patientCase = Core.Case.abs ∧ dargwa.npAlignment = AlignmentType.ergative

Dargwa: Fragment says A=ERG, S/P=ABS → Typology says ergative NP alignment. The classification follows from the case facts.

theorem Phenomena.Alignment.Typology.dargwa_alignment_family_bridge : Phenomena.Alignment.Typology.toAlignmentType✝ Fragments.Dargwa.Case.alignment = dargwa.npAlignment

Dargwa: Fragment says alignment family is ergative → Typology profile is consistently ergative.

theorem Phenomena.Alignment.Typology.japanese_fragment_bridge : (Fragments.Japanese.Case.caseInventory.any fun (x : Core.Case) => x == Core.Case.nom) = true ∧ (Fragments.Japanese.Case.caseInventory.any fun (x : Core.Case) => x == Core.Case.acc) = true ∧ japanese.npAlignment = AlignmentType.accusative

Japanese: Fragment case inventory contains NOM and ACC → Typology says accusative NP alignment.

theorem Phenomena.Alignment.Typology.hindi_fragment_bridge : Core.hindiSplit.alignment Core.Aspect.perfective = Core.AlignmentFamily.ergative ∧ Phenomena.Alignment.Typology.toAlignmentType✝ (Core.hindiSplit.alignment Core.Aspect.perfective) = hindiUrdu.npAlignment

Hindi: Fragment split-ergative system perfective→ERG matches Typology's ergative NP alignment (the dominant/WALS-coded pattern).

theorem Phenomena.Alignment.Typology.hindi_split_bridge : Core.hindiSplit.alignment Core.Aspect.imperfective = Core.AlignmentFamily.accusative ∧ Phenomena.Alignment.Typology.toAlignmentType✝ (Core.hindiSplit.alignment Core.Aspect.imperfective) = hindiUrdu.pronAlignment

Hindi: Fragment split-ergative system imperfective→ACC matches Typology's accusative pronoun alignment.