Shared Mayan Fragment Infrastructure

@cite{coon-mateo-pedro-preminger-2014} @cite{imanishi-2020} @cite{tada-1993} @cite{coon-2013}

Types and parameters shared across Mayan language fragments (Q'anjob'al, Chol, Kaqchikel, K'iche', Mam, etc.).

The Mayan Absolutive Parameter

The position of absolutive agreement morphemes relative to the verb stem is an observable morphological parameter:

• HIGH-ABS: absolutive immediately follows the aspect marker (pre-stem). Template: ASP-ABS-ERG-ROOT-SUFFIX. Highland Guatemala languages.
• LOW-ABS: absolutive follows the verb stem (post-stem). Template: ASP-ERG-ROOT-SUFFIX-ABS. Lowland Mexico languages.

@cite{coon-mateo-pedro-preminger-2014} observe (extending @cite{tada-1993}) that this correlates with extraction asymmetries: overwhelmingly, HIGH-ABS languages exhibit syntactic ergativity while LOW-ABS languages do not.

Case Locus (theoretical interpretation)

The observable ABSPosition receives a theoretical interpretation in terms of which functional head assigns case to the transitive object:

• ABS=NOM (HIGH-ABS): Infl⁰ assigns case (= nominative) to transitive objects. "Absolutive" is a cover term for nominative.
• ABS=DEF (LOW-ABS): v⁰ assigns case (= accusative) to transitive objects. "Absolutive" is a cover term for accusative.

Both types assign ergative uniformly (via transitive v⁰) and nominative to intransitive subjects (via Infl⁰).

inductive Fragments.Mayan.ABSPosition : Type

The position of absolutive agreement morphemes relative to the verb stem. Observable from the linear order of morphemes in the verb-aspect complex — no theoretical commitment required.

• high : ABSPosition
• low : ABSPosition

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqABSPosition : DecidableEq ABSPosition

Equations

• Fragments.Mayan.instDecidableEqABSPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mayan.instReprABSPosition : Repr ABSPosition

Equations

• Fragments.Mayan.instReprABSPosition = { reprPrec := Fragments.Mayan.instReprABSPosition.repr }

def Fragments.Mayan.instReprABSPosition.repr : ABSPosition → ℕ → Std.Format

Equations

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

inductive Fragments.Mayan.CaseLocus : Type

Abstract case assignment locus for transitive objects.

• absNom: Infl⁰ assigns case to transitive object (HIGH-ABS). @cite{legate-2008}'s ABS=NOM.
• absDef: v⁰ assigns case to transitive object (LOW-ABS). @cite{legate-2008}'s ABS=DEF.

• absNom : CaseLocus
• absDef : CaseLocus

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqCaseLocus : DecidableEq CaseLocus

Equations

• Fragments.Mayan.instDecidableEqCaseLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mayan.instReprCaseLocus : Repr CaseLocus

Equations

• Fragments.Mayan.instReprCaseLocus = { reprPrec := Fragments.Mayan.instReprCaseLocus.repr }

def Fragments.Mayan.instReprCaseLocus.repr : CaseLocus → ℕ → Std.Format

Equations

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

def Fragments.Mayan.toCaseLocus : ABSPosition → CaseLocus

Map the observable morphological parameter to the theoretical case-assignment locus.

Equations

• Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.high = Fragments.Mayan.CaseLocus.absNom
• Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.low = Fragments.Mayan.CaseLocus.absDef

inductive Fragments.Mayan.MarkerSet : Type

The two agreement marker paradigms found in Mayan languages. Set A and set B are the traditional Mayanist labels for the two cross-referencing paradigms on the verb.

These are framework-agnostic descriptive labels — they do not commit to an analysis of the markers as ergative, accusative, nominative, or absolutive.

• setA : MarkerSet

  Set A: cross-references ergative arguments (transitive agent) and genitives (possessors). Ergative and genitive are homophonous.

• setB : MarkerSet

  Set B: cross-references absolutive arguments (intransitive subject and, in ergative alignment, transitive patient).

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqMarkerSet : DecidableEq MarkerSet

Equations

• Fragments.Mayan.instDecidableEqMarkerSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mayan.instReprMarkerSet : Repr MarkerSet

Equations

• Fragments.Mayan.instReprMarkerSet = { reprPrec := Fragments.Mayan.instReprMarkerSet.repr }

def Fragments.Mayan.instReprMarkerSet.repr : MarkerSet → ℕ → Std.Format

Equations

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

Three different major Mayan branches; two different cut-off patterns

Per @cite{aissen-england-zavala-2017} (Routledge handbook) and @cite{koizumi-2023} Ch. 2 (citing Campbell & Kaufman 1985), the canonical Mayan family classification places these languages in three different major branches:

• Chol → Cholan group → Greater Tseltalan (Western Mayan)
• Q'anjob'al → Q'anjob'al group → Greater Q'anjob'alan (Western Mayan)
• Kaqchikel → K'ichean group → K'ichean-Mamean (Eastern Mayan)

The "extended ergative" non-perfective pattern arose independently in three different major branches — convergent grammaticalization of nominalized aspectual constructions, not common inheritance.

But while the surface alignment is similar (Set A on subjects in non-perfective contexts), the trigger for the split differs:

Cholan trigger (aspect category) — per @cite{vazquez-alvarez-2011} §1.9.4, @cite{imanishi-2020} §2.2, and @cite{zavala-maldonado-2017} §3:

Chol, Chontal, and other Cholan languages exhibit aspect-based split ergativity. The split is triggered by aspect category: ergative in perfective, accusative in all non-perfective aspects (imperfective, progressive, etc.). Per Vázquez Álvarez 2011 §1.9.4: "the ergative pattern is split in all non-perfective aspects."

Q'anjob'alan trigger (syntactic dependency) — per @cite{mateo-toledo-2008} §1.1.1, @cite{imanishi-2020} §2.2, and @cite{zavala-maldonado-2017} §3 (citing Francisco Pascual 2007):

Q'anjob'al, Akateko, Popti', Chuj, etc. exhibit a syntactic split triggered by dependent clauses lacking aspect markers — NOT by aspect category. Mateo Toledo 2008 §1.1.1: "split ergativity occurs in any clause without an overt preverbal aspect marker." Seven syntactic constructions trigger the split (per Francisco Pascual 2007), including: aspectless complements, purpose clauses, coordinate clauses, preverbal depictives, preverbal resultatives, preverbal manner adverbs, and preverbal aspectual/modal auxiliaries (e.g., the progressive lanan). The Q'anjob'al imperfective marker chi- IS an aspect marker, so IMP clauses keep canonical ergative — only PROG (which uses lanan matrix predicate, not a preverbal aspect marker) triggers the split.

The Aspect-indexed function below approximates the syntactic trigger via .Prog for Q'anjob'alan; the other 6 syntactic-dependency contexts can't be encoded at this granularity.

Why .gen not .nom?

Both descriptive grammars (@cite{vazquez-alvarez-2011} §1.9.4 for Chol, @cite{mateo-toledo-2008} §1.1.1 for Q'anjob'al) characterize the non-perfective alignment as nominative-accusative (Set A as nominative-like). The substrate's Alignment.extendedErgative.assignCase returns .gen (from Coon's analytical view: Set A on subjects in non-perfective is genitive licensed by D under nominalization). The morphological identity of Set A with possessive markers across Mayan makes .gen analytically defensible, but it's a theoretical choice; a descriptive-grammar implementation would return .nom.

@cite{zavala-maldonado-2017} §3 (p. 235) calls Coon's no-split re-analysis "unconvincing" — the split-ergative pattern is the descriptive consensus, with Coon's nominalization analysis being one analytical framing among several.

def Fragments.Mayan.caseChol : UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

Cholan aspect-driven case assignment.

Per @cite{vazquez-alvarez-2011} §1.9.4 + @cite{zavala-maldonado-2017} §3: ergative in perfective; accusative-like (extended-ergative) in ALL non-perfective aspects (imperfective, progressive, prospective, habitual, iterative). Used by Chol; presumably also Chontal, Ch'orti', Cholti per the Cholan-branch generalization in @cite{aissen-england-zavala-2017}.

Equations

• Fragments.Mayan.caseChol UD.Aspect.Perf x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseChol UD.Aspect.Imp x✝ = Alignment.extendedErgative.assignCase x✝
• Fragments.Mayan.caseChol UD.Aspect.Prog x✝ = Alignment.extendedErgative.assignCase x✝
• Fragments.Mayan.caseChol UD.Aspect.Prosp x✝ = Alignment.extendedErgative.assignCase x✝
• Fragments.Mayan.caseChol UD.Aspect.Hab x✝ = Alignment.extendedErgative.assignCase x✝
• Fragments.Mayan.caseChol UD.Aspect.Iter x✝ = Alignment.extendedErgative.assignCase x✝

def Fragments.Mayan.caseQanjobalan : UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

Q'anjob'alan aspect-driven case assignment.

Per @cite{mateo-toledo-2008} §1.1.1 + @cite{zavala-maldonado-2017} §3: split is triggered by dependent clauses lacking aspect markers, not by aspect category. The aspect-indexed function below approximates this with .Prog (since the progressive uses the lanan matrix predicate construction, which is one of the seven split-triggering syntactic contexts per Francisco Pascual 2007). Other non-perfective aspects (.Imp with chi- marker, etc.) keep the canonical ergative pattern — they ARE aspect-marked.

DIFFERS FROM CHOLAN: Chol's IMP mi- marker triggers the accusative split (per Vázquez Álvarez 2011 §1.9.4); Q'anjob'al's IMP chi- does NOT (per Mateo Toledo 2008 §1.1.1).

Equations

• Fragments.Mayan.caseQanjobalan UD.Aspect.Prog x✝ = Alignment.extendedErgative.assignCase x✝
• Fragments.Mayan.caseQanjobalan UD.Aspect.Perf x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseQanjobalan UD.Aspect.Imp x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseQanjobalan UD.Aspect.Prosp x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseQanjobalan UD.Aspect.Hab x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseQanjobalan UD.Aspect.Iter x✝ = Alignment.ergative.assignCase x✝

@[reducible, inline]

abbrev Fragments.Mayan.ergCaseChol : Features.Prominence.ArgumentRole → Core.Case

Perfective projection of caseChol. Equals Alignment.ergative.assignCase by definition.

Equations

• Fragments.Mayan.ergCaseChol = Fragments.Mayan.caseChol UD.Aspect.Perf

@[reducible, inline]

abbrev Fragments.Mayan.accCaseChol : Features.Prominence.ArgumentRole → Core.Case

Non-perfective (imperfective-and-up) projection of caseChol. Equals Alignment.extendedErgative.assignCase by definition. Reflects Chol's pattern of split in all non-perfective aspects.

Equations

• Fragments.Mayan.accCaseChol = Fragments.Mayan.caseChol UD.Aspect.Imp

@[reducible, inline]

abbrev Fragments.Mayan.ergCaseQanjobalan : Features.Prominence.ArgumentRole → Core.Case

Perfective projection of caseQanjobalan. Equals Alignment.ergative.assignCase by definition.

Equations

• Fragments.Mayan.ergCaseQanjobalan = Fragments.Mayan.caseQanjobalan UD.Aspect.Perf

@[reducible, inline]

abbrev Fragments.Mayan.accCaseQanjobalan : Features.Prominence.ArgumentRole → Core.Case

Progressive projection of caseQanjobalan. Equals Alignment.extendedErgative.assignCase by definition. Reflects Q'anjob'al's lanan-construction trigger; other non-perfective aspects in Q'anjob'al keep canonical ergative.

Equations

• Fragments.Mayan.accCaseQanjobalan = Fragments.Mayan.caseQanjobalan UD.Aspect.Prog

def Fragments.Mayan.caseKaqchikel : UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

Kaqchikel (K'ichean / K'ichean-Mamean = Eastern Mayan) aspect-driven case assignment.

Per @cite{imanishi-2014} §3.3.1 ("Kaqchikel: ERG=OBJ", p. 122) and @cite{imanishi-2020} §2.2: Kaqchikel exhibits a cross-linguistically rare INVERTED alignment in PROG sentences with the ajin matrix predicate — the OBJECT (not the subject) is cross-referenced by Set A (ergative/genitive). This is the OPPOSITE of the Cholan/Q'anjob'alan extended-ergative pattern.

Imanishi 2014 derives this from the Unaccusative Requirement on Nominalization + phase head ergative Case: the object becomes the only Case-less DP in the passivized nominalized clause and receives ERG/GEN from D as phase head. The subject is base-generated outside (in matrix Spec-PredP headed by ajin) and gets ABS from Infl.

The pattern is construction-specific (PROG ajin and certain embedding-verb constructions), not a broader Kaqchikel-non-perfective generalization. Other aspects in Kaqchikel (perfective, imperfective) keep canonical ergative alignment per Imanishi 2014 Table 3.1 (p. 95).

Dialectal variation: per @cite{imanishi-2014} fn. 26 (p. 141), some Kaqchikel varieties / consultants don't accept all the patterns documented in @cite{garcia-matzar-rodriguez-guajan-1997}. The inverted-pattern claim is grounded in Imanishi's primary fieldwork on a specific Kaqchikel variety.

Equations

• Fragments.Mayan.caseKaqchikel UD.Aspect.Prog x✝ = Alignment.invertedErgative.assignCase x✝
• Fragments.Mayan.caseKaqchikel UD.Aspect.Perf x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseKaqchikel UD.Aspect.Imp x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseKaqchikel UD.Aspect.Prosp x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseKaqchikel UD.Aspect.Hab x✝ = Alignment.ergative.assignCase x✝
• Fragments.Mayan.caseKaqchikel UD.Aspect.Iter x✝ = Alignment.ergative.assignCase x✝

@[reducible, inline]

abbrev Fragments.Mayan.ergCaseKaqchikel : Features.Prominence.ArgumentRole → Core.Case

Perfective projection of caseKaqchikel. Equals Alignment.ergative.assignCase by definition. Kaqchikel perfective is canonical ergative (A → ERG, S/P → ABS).

Equations

• Fragments.Mayan.ergCaseKaqchikel = Fragments.Mayan.caseKaqchikel UD.Aspect.Perf

@[reducible, inline]

abbrev Fragments.Mayan.accCaseKaqchikel : Features.Prominence.ArgumentRole → Core.Case

Progressive projection of caseKaqchikel. Equals Alignment.invertedErgative.assignCase by definition. The construction-specific inverted pattern (S/A → ABS, P → ERG/GEN) documented by Imanishi 2014/2020 for Kaqchikel ajin-progressive sentences.

Equations

• Fragments.Mayan.accCaseKaqchikel = Fragments.Mayan.caseKaqchikel UD.Aspect.Prog

def Fragments.Mayan.caseKiche : UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

K'iche' (K'ichean) case assignment.

Per @cite{mondloch-2017} (Lessons 9, 15): K'iche' is a uniformly ergative-absolutive language without an aspect-conditioned split — Set A (ergative) cross-references A across all aspects; Set B (absolutive) cross-references S and P. This contrasts with its sister Kaqchikel, which has the construction-specific inverted pattern in PROG ajin. Per @cite{imanishi-2014} fn. 26 p. 141, dialectal variation in K'ichean languages is non-trivial, but Mondloch documents no analogous K'iche' split. The aspect parameter is retained for shape-uniformity with the other Mayan case* functions; all aspects map to canonical ergative.

Equations

• Fragments.Mayan.caseKiche x✝¹ x✝ = Alignment.ergative.assignCase x✝

@[reducible, inline]

abbrev Fragments.Mayan.ergCaseKiche : Features.Prominence.ArgumentRole → Core.Case

K'iche' ergative-absolutive case (uniform across aspects). Equals Alignment.ergative.assignCase by definition.

Equations

• Fragments.Mayan.ergCaseKiche = Fragments.Mayan.caseKiche UD.Aspect.Perf

def Fragments.Mayan.caseMam : UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

San Juan Atitán Mam (K'ichean-Mamean / Eastern Mayan) case assignment.

Per @cite{scott-2023} ch. 3: SJA Mam is morphologically tripartite — A → ERG (Set A on Voice), P → ACC (no agreement; overt pronoun required), S → ABS (Set B on Infl). Mam lacks independent DP case morphology; the tripartite analysis is recoverable only from agreement patterns. Per Scott's analysis (ch. 3 §3.4), the underlying abstract Cases are nonetheless distinct: ERG (inherent from Voice), ACC (structural from Voice), ABS (structural from Infl).

Other Mam dialects (notably Ixtahuacán Mam per England 1983b / @cite{zavala-maldonado-2017} §4–5) have been characterized as ergative with neutral patterns in dependent clauses, NOT tripartite. This substrate encodes Scott's SJA Mam analysis; alternative-dialect fragments would need a different parameterization.

Mam shows no aspect-conditioned alignment split (per Scott ch. 3, the tripartite pattern is uniform). The aspect parameter is retained for shape-uniformity with the other Mayan case* functions; all aspects map to tripartite.

Equations

• Fragments.Mayan.caseMam x✝¹ x✝ = Alignment.tripartite.assignCase x✝

@[reducible, inline]

abbrev Fragments.Mayan.ergCaseMam : Features.Prominence.ArgumentRole → Core.Case

SJA Mam tripartite case (uniform across aspects). Equals Alignment.tripartite.assignCase by definition.

Equations

• Fragments.Mayan.ergCaseMam = Fragments.Mayan.caseMam UD.Aspect.Perf

def Fragments.Mayan.caseTseltalan : UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

Tseltalan (Tseltal, Tsotsil) case assignment.

Per @cite{polian-2013} and @cite{aissen-polian-2025}: Tseltalan languages are uniformly ergative-absolutive with no aspect- conditioned split (in contrast with their Cholan cousins). The aspect parameter is retained for shape-uniformity with the other Mayan case* functions.

Equations

• Fragments.Mayan.caseTseltalan x✝¹ x✝ = Alignment.ergative.assignCase x✝

@[reducible, inline]

abbrev Fragments.Mayan.ergCaseTseltalan : Features.Prominence.ArgumentRole → Core.Case

Tseltalan ergative-absolutive case (uniform across aspects). Equals Alignment.ergative.assignCase by definition.

Equations

• Fragments.Mayan.ergCaseTseltalan = Fragments.Mayan.caseTseltalan UD.Aspect.Perf

inductive Fragments.Mayan.PersonNumber : Type

The pan-Mayan person/number agreement paradigm.

Six values cover the consensus across Cholan, K'ichean, Q'anjob'alan, and Tseltalan agreement morphology (@cite{kaufman-norman-1984} Tables 7-8 reconstruct this paradigm to proto-Cholan with -∅ 3sg invariant). Languages with an inclusive/exclusive distinction in 1pl (Chol's -on lojon 1plExcl per @cite{kaufman-norman-1984} p. 91) accommodate the refinement at the per-language level.

• p1sg : PersonNumber
• p2sg : PersonNumber
• p3sg : PersonNumber
• p1pl : PersonNumber
• p2pl : PersonNumber
• p3pl : PersonNumber

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqPersonNumber : DecidableEq PersonNumber

Equations

• Fragments.Mayan.instDecidableEqPersonNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mayan.instReprPersonNumber.repr : PersonNumber → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.instReprPersonNumber : Repr PersonNumber

Equations

• Fragments.Mayan.instReprPersonNumber = { reprPrec := Fragments.Mayan.instReprPersonNumber.repr }

def Fragments.Mayan.PersonNumber.person : PersonNumber → Features.Prominence.PersonLevel

Project the person component (independent of number).

Equations

• Fragments.Mayan.PersonNumber.p1sg.person = Features.Prominence.PersonLevel.first
• Fragments.Mayan.PersonNumber.p1pl.person = Features.Prominence.PersonLevel.first
• Fragments.Mayan.PersonNumber.p2sg.person = Features.Prominence.PersonLevel.second
• Fragments.Mayan.PersonNumber.p2pl.person = Features.Prominence.PersonLevel.second
• Fragments.Mayan.PersonNumber.p3sg.person = Features.Prominence.PersonLevel.third
• Fragments.Mayan.PersonNumber.p3pl.person = Features.Prominence.PersonLevel.third

def Fragments.Mayan.PersonNumber.isPlural : PersonNumber → Bool

Is this a plural form?

Equations

• Fragments.Mayan.PersonNumber.p1sg.isPlural = false
• Fragments.Mayan.PersonNumber.p2sg.isPlural = false
• Fragments.Mayan.PersonNumber.p3sg.isPlural = false
• Fragments.Mayan.PersonNumber.p1pl.isPlural = true
• Fragments.Mayan.PersonNumber.p2pl.isPlural = true
• Fragments.Mayan.PersonNumber.p3pl.isPlural = true

def Fragments.Mayan.PersonNumber.all : List PersonNumber

All six values, useful for decide-checked drift sentries.

Equations

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

inductive Fragments.Mayan.VerbForm : Type

The two verb forms relevant to Mayan agreement morphology. Used by HIGH-ABS languages with an Agent Focus alternation (Q'anjob'al, Kaqchikel) and trivially by LOW-ABS languages (where .agentFocus is unattested).

• transitive : VerbForm
• agentFocus : VerbForm

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

• Fragments.Mayan.instDecidableEqVerbForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mayan.instReprVerbForm : Repr VerbForm

Equations

• Fragments.Mayan.instReprVerbForm = { reprPrec := Fragments.Mayan.instReprVerbForm.repr }

def Fragments.Mayan.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

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

def Fragments.Mayan.VerbForm.hasSetA : VerbForm → Bool

Whether the form bears Set A agreement (ergative cross-reference). Canonical transitive: yes. AF: no (the agent loses Set A under @cite{coon-mateo-pedro-preminger-2014}'s analysis).

Equations

• Fragments.Mayan.VerbForm.transitive.hasSetA = true
• Fragments.Mayan.VerbForm.agentFocus.hasSetA = false

@[reducible, inline]

abbrev Fragments.Mayan.ExponentTable : Type

An exponent table mapping each person/number value to its surface string realization. Per-language setAExponent and setBExponent populate this; cross-Mayan typology theorems quantify over it.

Equations

• Fragments.Mayan.ExponentTable = (Fragments.Mayan.PersonNumber → String)

def Fragments.Mayan.ExponentTable.IsThirdSgZero (e : ExponentTable) : Prop

Decidable predicate: the third-person singular slot is morphologically null. An invariant of the standard Mayan branches per @cite{kaufman-norman-1984} Table 8 — Set B 3sg null reconstructs to proto-Cholan and proto-Mayan. Not strictly pan-Mayan: SJA Mam's default Set B tz'= surfaces in the 3sg slot per @cite{scott-2023} §3.3.2; the cross-Mayan theorem mayan_p3sg_abs_null quantifies only over MayanLang.isStandard = true. The predicate is notation-agnostic — surface notation varies by linearity: "-∅" for suffixal Set B (Cholan, Q'anjob'alan, Tseltal, Tsotsil), "∅" for prefixal Set B (Kaqchikel and other K'ichean HIGH-ABS languages), "∅-" for prefixal-with-trailing-dash convention. All resolve to the same morphological claim: no overt 3sg exponent. The disjunction form is kernel-decidable (unlike a String.replace normalization, which is opaque to decide).

Equations

• e.IsThirdSgZero = (e Fragments.Mayan.PersonNumber.p3sg = "-∅" ∨ e Fragments.Mayan.PersonNumber.p3sg = "∅" ∨ e Fragments.Mayan.PersonNumber.p3sg = "∅-")

@[implicit_reducible]

instance Fragments.Mayan.instDecidableIsThirdSgZero (e : ExponentTable) : Decidable e.IsThirdSgZero

Equations

• Fragments.Mayan.instDecidableIsThirdSgZero e = id inferInstance

inductive Fragments.Mayan.MarkerLinearity : Type

The morphological linearity of an agreement marker on the verb stem.

Tseltalan languages contrast on this dimension: per @cite{aissen-polian-2025} Table 1, Tseltal Set B is consistently suffixal, while Tsotsil Set B is prefixal-or-suffixal depending on dialect and morphosyntactic context. Cholan and Q'anjob'alan Set B are uniformly suffixal. Set A is uniformly prefixal across all formalised Mayan languages — a candidate cross-Mayan invariant.

• prefixal : MarkerLinearity
• suffixal : MarkerLinearity
• either : MarkerLinearity

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqMarkerLinearity : DecidableEq MarkerLinearity

Equations

• Fragments.Mayan.instDecidableEqMarkerLinearity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mayan.instReprMarkerLinearity.repr : MarkerLinearity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.instReprMarkerLinearity : Repr MarkerLinearity

Equations

• Fragments.Mayan.instReprMarkerLinearity = { reprPrec := Fragments.Mayan.instReprMarkerLinearity.repr }

inductive Fragments.Mayan.MayanLang : Type

The Mayan languages with consolidated Fragment files. Yukatek has substrate work pending and is not yet in the registry; it'll be added once caseYukatek and the consolidated Agreement.lean shape are in place.

• Chol : MayanLang
• Qanjobal : MayanLang
• Kaqchikel : MayanLang
• Tseltal : MayanLang
• Tsotsil : MayanLang
• Mam : MayanLang
• Kiche : MayanLang

@[implicit_reducible]

instance Fragments.Mayan.instDecidableEqMayanLang : DecidableEq MayanLang

Equations

• Fragments.Mayan.instDecidableEqMayanLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mayan.instReprMayanLang : Repr MayanLang

Equations

• Fragments.Mayan.instReprMayanLang = { reprPrec := Fragments.Mayan.instReprMayanLang.repr }

def Fragments.Mayan.instReprMayanLang.repr : MayanLang → ℕ → Std.Format

Equations

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

def Fragments.Mayan.MayanLang.all : List MayanLang

All registered Mayan languages, useful for cross-Mayan typology theorems quantified by ∀ lang ∈ MayanLang.all.

Equations

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

def Fragments.Mayan.MayanLang.isStandard : MayanLang → Bool

The Mayan languages with the standard ergative-absolutive base (perfective ergative; Set B 3sg null per K&N reconstruction).

Mam is the exception: per @cite{scott-2023}, San Juan Atitán Mam is morphologically tripartite (S, A, P each receive distinct case and agreement), and its Set B 3sg surfaces as the default tz'= form rather than null. The substrate exposes this as a falsification of pan-Mayan invariants when Mam is in scope — mayan_p3sg_abs_null and mayan_perfective_ergative quantify only over isStandard = true languages.

Whether Mam is "really" tripartite vs ergative-with-neutral-objects is a contested analytical question (cf. England 1983b vs Scott 2023; Zavala 2017 §4 calls Ch'orti' the only tripartite Mayan). The substrate adopts Scott's analysis as recorded in Mam/Agreement.lean.

Equations

• Fragments.Mayan.MayanLang.Mam.isStandard = false
• x✝.isStandard = true

def Fragments.Mayan.caseAt : MayanLang → UD.Aspect → Features.Prominence.ArgumentRole → Core.Case

Aspect-driven case assignment dispatched by language. Routes to the existing per-branch case* substrate functions; the dispatcher is the consolidation point that lets cross-Mayan theorems quantify over MayanLang rather than enumerate per-language rfl facts.

Equations

• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Chol x✝¹ x✝ = Fragments.Mayan.caseChol x✝¹ x✝
• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Qanjobal x✝¹ x✝ = Fragments.Mayan.caseQanjobalan x✝¹ x✝
• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Kaqchikel x✝¹ x✝ = Fragments.Mayan.caseKaqchikel x✝¹ x✝
• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Tseltal x✝¹ x✝ = Fragments.Mayan.caseTseltalan x✝¹ x✝
• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Tsotsil x✝¹ x✝ = Fragments.Mayan.caseTseltalan x✝¹ x✝
• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Mam x✝¹ x✝ = Fragments.Mayan.caseMam x✝¹ x✝
• Fragments.Mayan.caseAt Fragments.Mayan.MayanLang.Kiche x✝¹ x✝ = Fragments.Mayan.caseKiche x✝¹ x✝