Documentation

Linglib.Phenomena.Ergativity.MayanAlignment

Cross-Mayan Alignment Typology #

@cite{kaufman-norman-1984} @cite{coon-mateo-pedro-preminger-2014} @cite{aissen-polian-2025} @cite{polian-2013}

Cross-Mayan typology theorems quantified over Fragments.Mayan.MayanLang, made statable by the per-language Fragment shape consolidation (Phases 1–6 of the Mayan agreement refactor). Each theorem replaces what previously had to be enumerated as parallel rfl facts in per-paper Studies.

What this file is anchored on #

Why this is not in Phenomena/Ergativity/Typology.lean #

The directory rule (feedback_no_phenomena_typology_lean) bans recreating Phenomena/X/Typology.lean files; cross-linguistic theorems anchored on a documented empirical pattern instead live in a topically-named file. This file is anchored on Tada's Generalization plus the pan-Mayan agreement-paradigm invariants — a recognised empirical literature, not an editorial synthesis.

source
def Phenomena.Ergativity.MayanAlignment.setBExponentOf :
Fragments.Mayan.MayanLang → Fragments.Mayan.ExponentTable

Set B exponent table indexed by Mayan language. Routes to the per-language setBExponent defined in each Fragment. Return type is Fragments.Mayan.ExponentTable (not the unfolded function type) to enable .IsThirdSgZero dot-notation.

Equations
Instances For
    source
    def Phenomena.Ergativity.MayanAlignment.setAExponentOf :
    Fragments.Mayan.MayanLang → Fragments.Mayan.ExponentTable

    Set A exponent table (canonical / pre-consonantal allomorph) indexed by Mayan language.

    Equations
    Instances For
      source
      def Phenomena.Ergativity.MayanAlignment.setALinearityOf :
      Fragments.Mayan.MayanLang → Fragments.Mayan.MarkerLinearity

      Set A linearity (uniformly prefixal across Mayan; see theorem below).

      Equations
      Instances For
        source
        def Phenomena.Ergativity.MayanAlignment.setBLinearityOf :
        Fragments.Mayan.MayanLang → Fragments.Mayan.MarkerLinearity

        Set B linearity. Varies across Mayan: suffixal in Cholan, Q'anjob'alan, and Tseltal; prefixal in Kaqchikel and K'iche' (HIGH-ABS K'ichean) and Mam (HIGH-ABS pre-stem on Infl); either in Tsotsil (dialectally and morphosyntactically conditioned).

        Equations
        Instances For
          source
          def Phenomena.Ergativity.MayanAlignment.absPositionOf :
          Fragments.Mayan.MayanLang → Fragments.Mayan.ABSPosition

          Absolutive structural position (HIGH-ABS / LOW-ABS) indexed by Mayan language. The substantive parameter for Tada's Generalization.

          Equations
          Instances For
            source
            theorem Phenomena.Ergativity.MayanAlignment.mayan_p3sg_abs_null (lang : Fragments.Mayan.MayanLang) (h : lang.isStandard = true) :
            (setBExponentOf lang).IsThirdSgZero

            Pan-Mayan Set B 3sg invariant (standard languages): across the formalised Mayan languages with the standard ergative-absolutive base (Cholan, Q'anjob'alan, Tseltalan, K'ichean — i.e., all except Mam), the third-person singular Set B exponent is morphologically null. Replaces parallel per-language rfl facts with one universally-quantified theorem.

            Notation differs by linearity ("-∅" for suffixal Set B, "∅" for prefixal); IsThirdSgZero is notation-agnostic.

            Mam exception: per @cite{scott-2023}, San Juan Atitán Mam's Set B 3sg surfaces as the default tz'= form (not null) — see mam_set_b_3sg_not_null below. This theorem hypothesizes lang.isStandard = true to scope around the exception.

            source
            theorem Phenomena.Ergativity.MayanAlignment.mam_set_b_3sg_not_null :
            ¬(setBExponentOf Fragments.Mayan.MayanLang.Mam).IsThirdSgZero

            The Mam exception to the pan-Mayan Set B 3sg null invariant: Mam's default Set B tz'= surfaces in the 3sg slot, not a null morpheme.

            source
            theorem Phenomena.Ergativity.MayanAlignment.mayan_set_a_uniformly_prefixal (lang : Fragments.Mayan.MayanLang) :
            setALinearityOf lang = Fragments.Mayan.MarkerLinearity.prefixal

            Pan-Mayan Set A linearity invariant: Set A markers are prefixal across all formalised Mayan languages. The morphological-position pan-Mayan claim corresponding to the structural-position invariant that ergative is licensed by the highest functional head in the verbal extended projection.

            source
            theorem Phenomena.Ergativity.MayanAlignment.mayan_perfective_ergative (lang : Fragments.Mayan.MayanLang) (h : lang.isStandard = true) (r : Features.Prominence.ArgumentRole) :
            Fragments.Mayan.caseAt lang UD.Aspect.Perf r = Alignment.ergative.assignCase r

            Pan-Mayan perfective alignment invariant (standard languages): in perfective aspect, every formalised Mayan language with the standard ergative-absolutive base assigns case canonically ergatively (A → ERG, S/P → ABS), regardless of any aspect-conditioned splits in non-perfective aspects.

            Mam exception: per @cite{scott-2023}, Mam is morphologically tripartite — caseMam .Perf .P = .acc, not .abs. The substrate surfaces this falsification when Mam is in scope; this theorem hypothesizes lang.isStandard = true to scope around it. See mam_is_tripartite_in_perfective for the contrast.

            source
            theorem Phenomena.Ergativity.MayanAlignment.mam_is_tripartite_in_perfective :
            Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Mam UD.Aspect.Perf Features.Prominence.ArgumentRole.P = Alignment.tripartite.assignCase Features.Prominence.ArgumentRole.P

            The Mam exception to pan-Mayan ergative perfective alignment: caseMam .Perf .P = .acc (tripartite, not ergative).