Dixon (1994): Ergativity — typology + Silverstein hierarchy + ditransitives

[Dix94] [Dix72] [Sil76] [Bla94b] [Com78] [Com13a] [Has05] [Has21] [Boh04] [Sum21]

R. M. W. Dixon. Ergativity. Cambridge University Press, 1994. The canonical typological reference for ergative alignment + split ergativity, covering [Sil76]'s prominence hierarchy and [Dix72]'s Dyirbal split-ergative analysis.

This study file holds:

1. The 22-language exemplar sample spanning all five AlignmentType values across the three WALS dimensions (Ch 98/99/100).
2. Cross-linguistic generalisations including Dixon's NP-vs-pronoun ergativity asymmetry, the absence of reverse-Dixon splits, and the rarity of tripartite/active patterns.
3. Silverstein's hierarchy as a threshold-based prominence function with monotonicity proven, and the Dyirbal split as a specific instance.
4. Ditransitive alignment ([Has05]): the 6-language indirective/secundative/neutral sample.
5. Fragment bridges: theorems verifying the per-language alignment classifications match the Fragment grammatical descriptions.
6. Bridges to Syntax/Case/Alignment: theorems verifying marksAgent/marksPatient projections agree with the case-assignment functions on canonical S/A/P inputs.

WALS aggregate distribution theorems are kept with the WALS data, not here. Per-language Fragment-vs-WALS data-equality theorems are deliberately absent — see feedback_no_per_lang_wals_grounding_in_studies for the rationale.

structure Dixon1994.AlignmentProfile : Type

A language's morphosyntactic alignment across the three case/agreement domains (WALS Chs 98/99/100). The bundled per-language record for the exemplar sample below; lives here with its data and analysis (relocated out of the dissolved Typology/Alignment.lean — its only consumers are this file and Comrie1989, which imports it).

• name : String

  Language name.

• iso639 : String

  ISO 639-3 code.

• npAlignment : Alignment.AlignmentType

  Ch 98: alignment of case marking of full NPs.

• pronAlignment : Alignment.AlignmentType

  Ch 99: alignment of case marking of pronouns.

• verbAlignment : Alignment.AlignmentType

  Ch 100: alignment of verbal person marking.

• notes : String

  Notes on the alignment system.

@[implicit_reducible]

instance Dixon1994.instReprAlignmentProfile : Repr AlignmentProfile

Equations

• Dixon1994.instReprAlignmentProfile = { reprPrec := Dixon1994.instReprAlignmentProfile.repr }

def Dixon1994.instReprAlignmentProfile.repr : AlignmentProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dixon1994.instDecidableEqAlignmentProfile : DecidableEq AlignmentProfile

Equations

• Dixon1994.instDecidableEqAlignmentProfile = Dixon1994.instDecidableEqAlignmentProfile.decEq

def Dixon1994.instDecidableEqAlignmentProfile.decEq (x✝ x✝¹ : AlignmentProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Dixon1994.AlignmentProfile.dixonSplit (p : AlignmentProfile) : Bool

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

Equations

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

def Dixon1994.AlignmentProfile.fullyUniform (p : AlignmentProfile) : Bool

Whether all three alignment domains agree.

Equations

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

def Dixon1994.english : AlignmentProfile

English: accusative case marking on pronouns (I/me, he/him), no case on full NPs (neutral), and accusative verb agreement.

Equations

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

def Dixon1994.hindiUrdu : AlignmentProfile

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

Equations

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

def Dixon1994.basque : AlignmentProfile

Basque: consistently ergative across all three domains.

Equations

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

def Dixon1994.dyirbal : AlignmentProfile

Dyirbal (Pama-Nyungan, Australia): the textbook case of split ergativity. NPs ergative, 1st/2nd person pronouns accusative. No verb person agreement.

Equations

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

def Dixon1994.georgian : AlignmentProfile

Georgian: active (split-S) alignment determined by verb class.

Equations

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

def Dixon1994.tagalog : AlignmentProfile

Tagalog: WALS codes Philippine voice system as neutral.

Equations

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

def Dixon1994.japanese : AlignmentProfile

Japanese: accusative NPs and pronouns; no verb agreement.

Equations

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

def Dixon1994.latin : AlignmentProfile

Latin: accusative NPs, pronouns, verb agreement.

Equations

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

def Dixon1994.russian : AlignmentProfile

Russian: accusative across all three domains.

Equations

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

def Dixon1994.mandarin : AlignmentProfile

Mandarin Chinese: neutral across all three.

Equations

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

def Dixon1994.turkish : AlignmentProfile

Turkish: accusative.

Equations

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

def Dixon1994.tongan : AlignmentProfile

Tongan (Austronesian): ergative on NPs and pronouns; no verb agreement.

Equations

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

def Dixon1994.guarani : AlignmentProfile

Guarani (Tupian): active verb agreement with split-S prefixes.

Equations

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

def Dixon1994.samoan : AlignmentProfile

Samoan: ergative NPs (e before A), accusative pronouns.

Equations

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

def Dixon1994.german : AlignmentProfile

German: accusative.

Equations

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

def Dixon1994.swahili : AlignmentProfile

Swahili (Bantu): no case, accusative verb agreement (subject prefix).

Equations

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

def Dixon1994.tibetan : AlignmentProfile

Tibetan (Lhasa): ergative NPs and pronouns; no verb agreement.

Equations

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

def Dixon1994.nezPerce : AlignmentProfile

Nez Perce: tripartite NPs and pronouns (distinct nom, erg, acc); accusative verb agreement.

Equations

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

def Dixon1994.finnish : AlignmentProfile

Finnish: accusative.

Equations

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

def Dixon1994.warlpiri : AlignmentProfile

Warlpiri (Pama-Nyungan): split-ergative — ergative NPs, accusative pronouns; no verb agreement.

Equations

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

def Dixon1994.dargwa : AlignmentProfile

Dargwa (Tanti; [Sum21]): consistently ergative across all three domains.

Equations

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

def Dixon1994.yukatek : AlignmentProfile

Yukatek Maya ([Boh04]): aspect-conditioned split intransitivity — perfective triggers ergative-like marking, imperfective triggers accusative-like marking.

Equations

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

def Dixon1994.allProfiles : List AlignmentProfile

All 22 alignment profiles.

Equations

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

theorem Dixon1994.allProfiles_count : allProfiles.length = 22

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

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

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

theorem Dixon1994.sample_counts : (List.filter (fun (p : AlignmentProfile) => p.npAlignment == Alignment.AlignmentType.ergative) allProfiles).length = 8 ∧ (List.filter (fun (p : AlignmentProfile) => p.pronAlignment == Alignment.AlignmentType.ergative) allProfiles).length = 4 ∧ (List.filter (fun (x : AlignmentProfile) => x.dixonSplit) allProfiles).length = 4 ∧ (List.filter (fun (x : AlignmentProfile) => x.fullyUniform) allProfiles).length = 10

Sample distribution counts.

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

Accusative is the most common alignment for pronouns ([Dix94]'s prominence hierarchy prediction).

theorem Dixon1994.dixon_generalization : (List.filter (fun (p : AlignmentProfile) => p.npAlignment == Alignment.AlignmentType.ergative) allProfiles).length > (List.filter (fun (p : AlignmentProfile) => p.pronAlignment == Alignment.AlignmentType.ergative) allProfiles).length

[Dix94]'s generalisation: ergative case marking is more common on full NPs than on pronouns.

theorem Dixon1994.split_ergativity_attested : (List.filter (fun (p : AlignmentProfile) => p.dixonSplit) allProfiles).length ≥ 4

Split ergativity (NP-ergative + pronoun-accusative) is attested in multiple languages (Dyirbal, Hindi-Urdu, Samoan, Warlpiri).

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

The reverse-Dixon pattern (accusative NPs + ergative pronouns) is predicted not to occur. The sample confirms it: whenever pronouns are ergative, NPs are at least ergative too.

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

Tripartite NP alignment is rare: only Nez Perce in the sample.

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

Tripartite pronoun alignment is equally rare.

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

Active alignment is rare for case marking: only Georgian in the sample.

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

Aspect-conditioned split intransitivity ([Boh04]): Yukatek Maya and Georgian both show active verbal person marking.

theorem Dixon1994.yukatek_and_georgian_both_active : yukatek.verbAlignment = Alignment.AlignmentType.active ∧ georgian.verbAlignment = Alignment.AlignmentType.active

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

Languages with ergative NP marking tend to have ergative or neutral verbal person marking (or accusative as a third option).

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

All five alignment types are attested for NPs.

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

All five alignment types are attested for pronouns.

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

Four of the five alignment types are attested for verbal person marking; tripartite verb agreement is exceedingly rare cross-linguistically and not represented here.

theorem Dixon1994.tripartite_verb_unattested : (allProfiles.all fun (p : AlignmentProfile) => p.verbAlignment != Alignment.AlignmentType.tripartite) = true

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

Neutral NP alignment implies neutral or accusative pronoun alignment (English-style: case survives only on pronouns). Never ergative.

theorem Dixon1994.uniform_common : (List.filter (fun (p : AlignmentProfile) => p.fullyUniform) allProfiles).length ≥ 5

Fully uniform alignment is common (Basque, Mandarin, Latin, Russian, Turkish, Georgian, etc.).

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

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

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

Every language with accusative NP case also has accusative pronoun case in the sample. Accusative does not split across NP/pronoun like ergative.

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

No language has tripartite NP without tripartite pronoun in the sample.

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

Active NP alignment implies active pronoun alignment in the sample.

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

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

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

Languages with tripartite case mark both A and P.

theorem Dixon1994.ergative_marks_agent_only : Alignment.AlignmentType.ergative.marksAgent = (true = true) ∧ Alignment.AlignmentType.ergative.marksPatient = (false = true)

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

theorem Dixon1994.accusative_marks_patient_only : Alignment.AlignmentType.accusative.marksPatient = (true = true) ∧ Alignment.AlignmentType.accusative.marksAgent = (false = true)

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

[Sil76] 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.

def Dixon1994.silverstein (threshold npProminence : ℕ) : Features.AlignmentFamily

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

Equations

• Dixon1994.silverstein threshold npProminence = if npProminence ≥ threshold then Features.AlignmentFamily.accusative else Features.AlignmentFamily.ergative

theorem Dixon1994.silverstein_monotone (threshold p₁ p₂ : ℕ) (h_ge : p₁ ≥ p₂) (h_acc : silverstein threshold p₂ = Features.AlignmentFamily.accusative) : silverstein threshold p₁ = Features.AlignmentFamily.accusative

Silverstein is monotone: if prominence p₁ ≥ p₂ and p₂ gets accusative, then p₁ gets accusative.

theorem Dixon1994.silverstein_predicts_dixon : silverstein 1 0 = Features.AlignmentFamily.ergative ∧ silverstein 1 1 = Features.AlignmentFamily.accusative

Silverstein predicts Dixon's generalisation: with threshold 1, full NPs (prominence 0) get ergative, pronouns (prominence 1) get accusative.

def Dixon1994.dyirbalSplit : Alignment.SplitErgativity Features.Prominence.AnimacyLevel

[Dix72] Dyirbal split: human/animate → accusative, inanimate → ergative.

Equations

• Dixon1994.dyirbalSplit = { ergCondition := fun (a : Features.Prominence.AnimacyLevel) => a == Features.Prominence.AnimacyLevel.inanimate }

theorem Dixon1994.dyirbal_human_acc : dyirbalSplit.alignment Features.Prominence.AnimacyLevel.human = Features.AlignmentFamily.accusative

theorem Dixon1994.dyirbal_inanimate_erg : dyirbalSplit.alignment Features.Prominence.AnimacyLevel.inanimate = Features.AlignmentFamily.ergative

theorem Dixon1994.dyirbal_split_matches_np : Dixon1994.toAlignmentType✝ (dyirbalSplit.alignment Features.Prominence.AnimacyLevel.inanimate) = dyirbal.npAlignment

Dyirbal split matches the Dyirbal alignment profile: inanimate NPs get ergative alignment.

theorem Dixon1994.dyirbal_split_matches_pron : Dixon1994.toAlignmentType✝ (dyirbalSplit.alignment Features.Prominence.AnimacyLevel.human) = dyirbal.pronAlignment

Human/animate arguments get accusative alignment.

def Dixon1994.ditrans_english : Alignment.DitransitiveProfile

Equations

• Dixon1994.ditrans_english = { name := "English", iso639 := "eng", alignment := Alignment.DitransitiveAlignment.indirective, notes := "T = P (acc); R marked with 'to'" }

def Dixon1994.ditrans_german : Alignment.DitransitiveProfile

Equations

• Dixon1994.ditrans_german = { name := "German", iso639 := "deu", alignment := Alignment.DitransitiveAlignment.indirective, notes := "T = accusative; R = dative" }

def Dixon1994.ditrans_latin : Alignment.DitransitiveProfile

Equations

• Dixon1994.ditrans_latin = { name := "Latin", iso639 := "lat", alignment := Alignment.DitransitiveAlignment.indirective, notes := "T = accusative; R = dative" }

def Dixon1994.ditrans_japanese : Alignment.DitransitiveProfile

Equations

• Dixon1994.ditrans_japanese = { name := "Japanese", iso639 := "jpn", alignment := Alignment.DitransitiveAlignment.indirective, notes := "T = o (accusative); R = ni (dative)" }

def Dixon1994.ditrans_swahili : Alignment.DitransitiveProfile

Equations

• Dixon1994.ditrans_swahili = { name := "Swahili", iso639 := "swh", alignment := Alignment.DitransitiveAlignment.secundative, notes := "R = P in applicative; T marked differently" }

def Dixon1994.ditrans_mandarin : Alignment.DitransitiveProfile

Equations

• Dixon1994.ditrans_mandarin = { name := "Mandarin", iso639 := "cmn", alignment := Alignment.DitransitiveAlignment.neutral, notes := "R and T both unmarked; order distinguishes" }

def Dixon1994.allDitransProfiles : List Alignment.DitransitiveProfile

Equations

• Dixon1994.allDitransProfiles = [Dixon1994.ditrans_english, Dixon1994.ditrans_german, Dixon1994.ditrans_latin, Dixon1994.ditrans_japanese, Dixon1994.ditrans_swahili, Dixon1994.ditrans_mandarin]

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

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

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

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

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

Theorems verifying that the inline AlignmentProfile entries are consistent with the grammatical facts described in each language's Fragment directory.

theorem Dixon1994.dargwa_fragment_bridge : Dargwa.Case.agentCase = Case.erg ∧ Dargwa.Case.patientCase = Case.abs ∧ dargwa.npAlignment = Alignment.AlignmentType.ergative

Dargwa: Fragment says A=ERG, S/P=ABS → Typology says ergative NP alignment.

theorem Dixon1994.dargwa_alignment_family_bridge : Dixon1994.toAlignmentType✝ Dargwa.Case.alignment = dargwa.npAlignment

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

theorem Dixon1994.japanese_fragment_bridge : Case.nom ∈ Japanese.Case.caseInventory ∧ Case.acc ∈ Japanese.Case.caseInventory ∧ japanese.npAlignment = Alignment.AlignmentType.accusative

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

theorem Dixon1994.hindi_fragment_bridge : Alignment.hindiSplit.alignment Alignment.Aspect.perfective = Features.AlignmentFamily.ergative ∧ Dixon1994.toAlignmentType✝ (Alignment.hindiSplit.alignment Alignment.Aspect.perfective) = hindiUrdu.npAlignment

Hindi: Fragment split-ergative system perfective → ERG matches Typology's ergative NP alignment.

theorem Dixon1994.hindi_split_bridge : Alignment.hindiSplit.alignment Alignment.Aspect.imperfective = Features.AlignmentFamily.accusative ∧ Dixon1994.toAlignmentType✝ (Alignment.hindiSplit.alignment Alignment.Aspect.imperfective) = hindiUrdu.pronAlignment

Hindi: Fragment imperfective → ACC matches Typology's accusative pronoun alignment.

The typology classifier AlignmentType (substrate) and the case-assignment functions _root_.Alignment.X.assignCase (Syntax/Case/Alignment.lean) are two views of the same alignment dimension. The bridge theorems confirm that the typology's marksAgent/marksPatient Bool projections agree pointwise with what the case-assignment functions actually do on the canonical S/A/P inputs.

theorem Dixon1994.ergative_function_marks_A : ((Alignment.ergative.assignCase Features.Prominence.ArgumentRole.A != Alignment.ergative.assignCase Features.Prominence.ArgumentRole.S) = true) = Alignment.AlignmentType.ergative.marksAgent

theorem Dixon1994.ergative_function_does_not_mark_P : ((Alignment.ergative.assignCase Features.Prominence.ArgumentRole.P != Alignment.ergative.assignCase Features.Prominence.ArgumentRole.S) = true) = Alignment.AlignmentType.ergative.marksPatient

theorem Dixon1994.accusative_function_marks_P : ((Alignment.nominativeAccusative.assignCase Features.Prominence.ArgumentRole.P != Alignment.nominativeAccusative.assignCase Features.Prominence.ArgumentRole.S) = true) = Alignment.AlignmentType.accusative.marksPatient

theorem Dixon1994.accusative_function_does_not_mark_A : ((Alignment.nominativeAccusative.assignCase Features.Prominence.ArgumentRole.A != Alignment.nominativeAccusative.assignCase Features.Prominence.ArgumentRole.S) = true) = Alignment.AlignmentType.accusative.marksAgent

theorem Dixon1994.extendedErgative_groups_S_with_A_like_accusative : Alignment.extendedErgative.assignCase Features.Prominence.ArgumentRole.S = Alignment.extendedErgative.assignCase Features.Prominence.ArgumentRole.A ∧ Alignment.extendedErgative.assignCase Features.Prominence.ArgumentRole.A ≠ Alignment.nominativeAccusative.assignCase Features.Prominence.ArgumentRole.A

Extended ergative is non-canonical (no AlignmentType constructor): it groups S with A like accusative does, but marks them with GEN rather than NOM. The Cholan non-perfective pattern is captured by the function only.