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

@cite{dixon-1994} @cite{dixon-1972} @cite{silverstein-1976} @cite{blake-1994} @cite{comrie-1978} @cite{comrie-2013} @cite{haspelmath-2005} @cite{haspelmath-2021} @cite{bohnemeyer-2004} @cite{sumbatova-2021}

R. M. W. Dixon. Ergativity. Cambridge University Press, 1994. The canonical typological reference for ergative alignment + split ergativity, covering @cite{silverstein-1976}'s prominence hierarchy and @cite{dixon-1972}'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 (@cite{haspelmath-2005}): 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 Theories/Syntax/Case/Alignment: theorems verifying marksAgent/marksPatient projections agree with the case-assignment functions on canonical S/A/P inputs.

WALS aggregate distribution theorems live in Linglib/Typology/Alignment.lean. Per-language Fragment-vs-WALS data-equality theorems are deliberately absent — see feedback_no_per_lang_wals_grounding_in_studies for the rationale.

def Phenomena.Alignment.Studies.Dixon1994.english : Typology.Alignment.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 Phenomena.Alignment.Studies.Dixon1994.hindiUrdu : Typology.Alignment.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 Phenomena.Alignment.Studies.Dixon1994.basque : Typology.Alignment.AlignmentProfile

Basque: consistently ergative across all three domains.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.dyirbal : Typology.Alignment.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 Phenomena.Alignment.Studies.Dixon1994.georgian : Typology.Alignment.AlignmentProfile

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

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.tagalog : Typology.Alignment.AlignmentProfile

Tagalog: WALS codes Philippine voice system as neutral.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.japanese : Typology.Alignment.AlignmentProfile

Japanese: accusative NPs and pronouns; no verb agreement.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.latin : Typology.Alignment.AlignmentProfile

Latin: accusative NPs, pronouns, verb agreement.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.russian : Typology.Alignment.AlignmentProfile

Russian: accusative across all three domains.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.mandarin : Typology.Alignment.AlignmentProfile

Mandarin Chinese: neutral across all three.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.turkish : Typology.Alignment.AlignmentProfile

Turkish: accusative.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.tongan : Typology.Alignment.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 Phenomena.Alignment.Studies.Dixon1994.guarani : Typology.Alignment.AlignmentProfile

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

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.samoan : Typology.Alignment.AlignmentProfile

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

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.german : Typology.Alignment.AlignmentProfile

German: accusative.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.swahili : Typology.Alignment.AlignmentProfile

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

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.tibetan : Typology.Alignment.AlignmentProfile

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

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.nezPerce : Typology.Alignment.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 Phenomena.Alignment.Studies.Dixon1994.finnish : Typology.Alignment.AlignmentProfile

Finnish: accusative.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.warlpiri : Typology.Alignment.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 Phenomena.Alignment.Studies.Dixon1994.dargwa : Typology.Alignment.AlignmentProfile

Dargwa (Tanti; @cite{sumbatova-2021}): consistently ergative across all three domains.

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.yukatek : Typology.Alignment.AlignmentProfile

Yukatek Maya (@cite{bohnemeyer-2004}): 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 Phenomena.Alignment.Studies.Dixon1994.allProfiles : List Typology.Alignment.AlignmentProfile

All 22 alignment profiles.

Equations

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

theorem Phenomena.Alignment.Studies.Dixon1994.allProfiles_count : allProfiles.length = 22

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

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

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

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

Sample distribution counts.

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

Accusative is the most common alignment for pronouns (@cite{dixon-1994}'s prominence hierarchy prediction).

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

@cite{dixon-1994}'s generalisation: ergative case marking is more common on full NPs than on pronouns.

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

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

theorem Phenomena.Alignment.Studies.Dixon1994.no_reverse_dixon : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => if (p.pronAlignment == Typology.Alignment.AlignmentType.ergative) = true then p.npAlignment == Typology.Alignment.AlignmentType.ergative || p.npAlignment == Typology.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 Phenomena.Alignment.Studies.Dixon1994.tripartite_rare_nps : (List.filter (fun (p : Typology.Alignment.AlignmentProfile) => p.npAlignment == Typology.Alignment.AlignmentType.tripartite) allProfiles).length ≤ 1

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

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

Tripartite pronoun alignment is equally rare.

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

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

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

Aspect-conditioned split intransitivity (@cite{bohnemeyer-2004}): Yukatek Maya and Georgian both show active verbal person marking.

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

theorem Phenomena.Alignment.Studies.Dixon1994.erg_np_verb_pattern : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => if (p.npAlignment == Typology.Alignment.AlignmentType.ergative) = true then p.verbAlignment == Typology.Alignment.AlignmentType.ergative || p.verbAlignment == Typology.Alignment.AlignmentType.neutral || p.verbAlignment == Typology.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 Phenomena.Alignment.Studies.Dixon1994.all_np_types_attested : (((((allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.npAlignment == Typology.Alignment.AlignmentType.neutral) && allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.npAlignment == Typology.Alignment.AlignmentType.accusative) && allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.npAlignment == Typology.Alignment.AlignmentType.ergative) && allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.npAlignment == Typology.Alignment.AlignmentType.tripartite) && decide ((allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.npAlignment == Typology.Alignment.AlignmentType.active) = true)) = true

All five alignment types are attested for NPs.

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

All five alignment types are attested for pronouns.

theorem Phenomena.Alignment.Studies.Dixon1994.verb_types_attested : ((((allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.verbAlignment == Typology.Alignment.AlignmentType.neutral) && allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.verbAlignment == Typology.Alignment.AlignmentType.accusative) && allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.verbAlignment == Typology.Alignment.AlignmentType.ergative) && decide ((allProfiles.any fun (p : Typology.Alignment.AlignmentProfile) => p.verbAlignment == Typology.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 Phenomena.Alignment.Studies.Dixon1994.tripartite_verb_unattested : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => p.verbAlignment != Typology.Alignment.AlignmentType.tripartite) = true

theorem Phenomena.Alignment.Studies.Dixon1994.neutral_np_pronoun : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => if (p.npAlignment == Typology.Alignment.AlignmentType.neutral) = true then p.pronAlignment == Typology.Alignment.AlignmentType.neutral || p.pronAlignment == Typology.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 Phenomena.Alignment.Studies.Dixon1994.uniform_common : (List.filter (fun (p : Typology.Alignment.AlignmentProfile) => p.fullyUniform) allProfiles).length ≥ 5

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

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

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

theorem Phenomena.Alignment.Studies.Dixon1994.accusative_np_implies_accusative_pron : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => if (p.npAlignment == Typology.Alignment.AlignmentType.accusative) = true then p.pronAlignment == Typology.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 Phenomena.Alignment.Studies.Dixon1994.tripartite_np_implies_tripartite_pron : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => if (p.npAlignment == Typology.Alignment.AlignmentType.tripartite) = true then p.pronAlignment == Typology.Alignment.AlignmentType.tripartite else true) = true

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

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

Active NP alignment implies active pronoun alignment in the sample.

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

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

theorem Phenomena.Alignment.Studies.Dixon1994.tripartite_marks_both : (allProfiles.all fun (p : Typology.Alignment.AlignmentProfile) => if (p.npAlignment == Typology.Alignment.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.Studies.Dixon1994.ergative_marks_agent_only : Typology.Alignment.AlignmentType.ergative.marksAgent = true ∧ Typology.Alignment.AlignmentType.ergative.marksPatient = false

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

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

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

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

def Phenomena.Alignment.Studies.Dixon1994.silverstein (threshold npProminence : ℕ) : Core.AlignmentFamily

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

Equations

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

theorem Phenomena.Alignment.Studies.Dixon1994.silverstein_monotone (threshold p₁ p₂ : ℕ) (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.

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

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

def Phenomena.Alignment.Studies.Dixon1994.dyirbalSplit : Core.SplitErgativity Features.Prominence.AnimacyLevel

@cite{dixon-1972} Dyirbal split: human/animate → accusative, inanimate → ergative.

Equations

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

theorem Phenomena.Alignment.Studies.Dixon1994.dyirbal_human_acc : dyirbalSplit.alignment Features.Prominence.AnimacyLevel.human = Core.AlignmentFamily.accusative

theorem Phenomena.Alignment.Studies.Dixon1994.dyirbal_inanimate_erg : dyirbalSplit.alignment Features.Prominence.AnimacyLevel.inanimate = Core.AlignmentFamily.ergative

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

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

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

Human/animate arguments get accusative alignment.

def Phenomena.Alignment.Studies.Dixon1994.ditrans_english : Typology.Alignment.DitransitiveProfile

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.ditrans_german : Typology.Alignment.DitransitiveProfile

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.ditrans_latin : Typology.Alignment.DitransitiveProfile

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.ditrans_japanese : Typology.Alignment.DitransitiveProfile

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.ditrans_swahili : Typology.Alignment.DitransitiveProfile

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.ditrans_mandarin : Typology.Alignment.DitransitiveProfile

Equations

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

def Phenomena.Alignment.Studies.Dixon1994.allDitransProfiles : List Typology.Alignment.DitransitiveProfile

Equations

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

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

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

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

theorem Phenomena.Alignment.Studies.Dixon1994.ditrans_indirective_more_common : (List.filter (fun (p : Typology.Alignment.DitransitiveProfile) => p.alignment == Typology.Alignment.DitransitiveAlignment.indirective) allDitransProfiles).length > (List.filter (fun (p : Typology.Alignment.DitransitiveProfile) => p.alignment == Typology.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 Phenomena.Alignment.Studies.Dixon1994.dargwa_fragment_bridge : Fragments.Dargwa.Case.agentCase = UD.Case.erg ∧ Fragments.Dargwa.Case.patientCase = UD.Case.abs ∧ dargwa.npAlignment = Typology.Alignment.AlignmentType.ergative

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

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

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

theorem Phenomena.Alignment.Studies.Dixon1994.japanese_fragment_bridge : UD.Case.nom ∈ Fragments.Japanese.Case.caseInventory ∧ UD.Case.acc ∈ Fragments.Japanese.Case.caseInventory ∧ japanese.npAlignment = Typology.Alignment.AlignmentType.accusative

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

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

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

theorem Phenomena.Alignment.Studies.Dixon1994.hindi_split_bridge : Core.hindiSplit.alignment Core.Aspect.imperfective = Core.AlignmentFamily.accusative ∧ Phenomena.Alignment.Studies.Dixon1994.toAlignmentType✝ (Core.hindiSplit.alignment Core.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 (Theories/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 Phenomena.Alignment.Studies.Dixon1994.ergative_function_marks_A : (Alignment.ergative.assignCase Features.Prominence.ArgumentRole.A != Alignment.ergative.assignCase Features.Prominence.ArgumentRole.S) = Typology.Alignment.AlignmentType.ergative.marksAgent

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

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

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

theorem Phenomena.Alignment.Studies.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.