Shared Mayan Fragment Infrastructure

Types and parameters shared across the Mayan language fragments (Q'anjob'al, Chol, Kaqchikel, K'iche', Mam, etc.), following [CMPP14], [Ima20], [Tad93], and [Coo13].

The Mayan Absolutive Parameter is the observable position of absolutive agreement morphemes relative to the verb stem. HIGH-ABS languages place absolutive immediately after the aspect marker (pre-stem; template ASP-ABS-ERG-ROOT-SUFFIX; Highland Guatemala); LOW-ABS languages place it after the stem (post-stem; template ASP-ERG-ROOT-SUFFIX-ABS; Lowland Mexico). Extending [Tad93], [CMPP14] observe that this correlates with extraction asymmetries: HIGH-ABS languages overwhelmingly exhibit syntactic ergativity while LOW-ABS languages do not.

Main declarations

• Mayan.ABSPosition, Mayan.CaseLocus, Mayan.toCaseLocus: the absolutive parameter and its case-locus interpretation.
• Mayan.MarkerSet: the Set A / Set B agreement paradigms.
• Mayan.caseChol, Mayan.caseQanjobalan, Mayan.caseKaqchikel, Mayan.caseKiche, Mayan.caseMam, Mayan.caseTseltalan: per-branch aspect-driven case assignment, with erg…/acc… aspect projections.
• Mayan.VerbForm: transitive vs Agent Focus, and its agreement slots.
• Mayan.ExponentTable, Mayan.ExponentTable.IsThirdSgZero: agreement paradigms over φ-cells and the null-3sg predicate.
• Mayan.MarkerLinearity: prefixal / suffixal / either marker linearity.
• Mayan, Mayan.isStandard, Mayan.caseAt: the language registry and the case-assignment dispatcher.

Implementation notes

The observable ABSPosition receives a theoretical interpretation as CaseLocus, the functional head assigning case to transitive objects: ABS=NOM (HIGH-ABS) has Infl⁰ assign nominative, ABS=DEF (LOW-ABS) has v⁰ assign accusative, with "absolutive" a cover term either way ([Leg08]). Both types assign ergative uniformly (via transitive v⁰) and nominative to intransitive subjects (via Infl⁰).

inductive Mayan : Type

The Mayan languages with consolidated Fragment files.

• Chol : Mayan
• Qanjobal : Mayan
• Kaqchikel : Mayan
• Tseltal : Mayan
• Tsotsil : Mayan
• Mam : Mayan
• Kiche : Mayan
• Yukatek : Mayan

@[implicit_reducible]

instance instDecidableEqMayan : DecidableEq Mayan

Equations

• instDecidableEqMayan x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprMayan.repr : Mayan → ℕ → Std.Format

Equations

• instReprMayan.repr Mayan.Chol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Chol")).group prec✝
• instReprMayan.repr Mayan.Qanjobal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Qanjobal")).group prec✝
• instReprMayan.repr Mayan.Kaqchikel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Kaqchikel")).group prec✝
• instReprMayan.repr Mayan.Tseltal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Tseltal")).group prec✝
• instReprMayan.repr Mayan.Tsotsil prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Tsotsil")).group prec✝
• instReprMayan.repr Mayan.Mam prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Mam")).group prec✝
• instReprMayan.repr Mayan.Kiche prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Kiche")).group prec✝
• instReprMayan.repr Mayan.Yukatek prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.Yukatek")).group prec✝

@[implicit_reducible]

instance instReprMayan : Repr Mayan

Equations

• instReprMayan = { reprPrec := instReprMayan.repr }

Mayan absolutive parameter

inductive 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 Mayan.instDecidableEqABSPosition : DecidableEq ABSPosition

Equations

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

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

Equations

• Mayan.instReprABSPosition.repr Mayan.ABSPosition.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.ABSPosition.high")).group prec✝
• Mayan.instReprABSPosition.repr Mayan.ABSPosition.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.ABSPosition.low")).group prec✝

@[implicit_reducible]

instance Mayan.instReprABSPosition : Repr ABSPosition

Equations

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

Case locus

inductive Mayan.CaseLocus : Type

Abstract case assignment locus for transitive objects.

• absNom: Infl⁰ assigns case to transitive object (HIGH-ABS). [Leg08]'s ABS=NOM.
• absDef: v⁰ assigns case to transitive object (LOW-ABS). [Leg08]'s ABS=DEF.

• absNom : CaseLocus
• absDef : CaseLocus

@[implicit_reducible]

instance Mayan.instDecidableEqCaseLocus : DecidableEq CaseLocus

Equations

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

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

Equations

• Mayan.instReprCaseLocus.repr Mayan.CaseLocus.absNom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.CaseLocus.absNom")).group prec✝
• Mayan.instReprCaseLocus.repr Mayan.CaseLocus.absDef prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.CaseLocus.absDef")).group prec✝

@[implicit_reducible]

instance Mayan.instReprCaseLocus : Repr CaseLocus

Equations

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

def Mayan.toCaseLocus : ABSPosition → CaseLocus

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

Equations

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

Agreement marker paradigms

inductive 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 Mayan.instDecidableEqMarkerSet : DecidableEq MarkerSet

Equations

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

@[implicit_reducible]

instance Mayan.instReprMarkerSet : Repr MarkerSet

Equations

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

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

Equations

• Mayan.instReprMarkerSet.repr Mayan.MarkerSet.setA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.MarkerSet.setA")).group prec✝
• Mayan.instReprMarkerSet.repr Mayan.MarkerSet.setB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.MarkerSet.setB")).group prec✝

Aspect-conditioned case: three branches, two split triggers

Per [AEZM17] and [Koi23] Ch. 2 (citing Campbell & Kaufman 1985), these languages sit in three different major branches: Chol in Greater Tseltalan (Western), Q'anjob'al in Greater Q'anjob'alan (Western), Kaqchikel in K'ichean-Mamean (Eastern). The "extended ergative" non-perfective pattern (Set A on non-perfective subjects) arose independently in all three — convergent grammaticalization of nominalized aspectual constructions, not common inheritance — but the trigger for the split differs.

Cholan (aspect category), per [VA11] §1.9.4, [Ima20] §2.2, [ZM17] §3: Chol, Chontal, and other Cholan languages split by aspect — ergative in perfective, accusative in all non-perfective aspects. Vázquez Álvarez 2011 §1.9.4: "the ergative pattern is split in all non-perfective aspects."

Q'anjob'alan (syntactic dependency), per [MT08] §1.1.1, [Ima20] §2.2, [ZM17] §3 (citing Francisco Pascual 2007): Q'anjob'al, Akateko, Popti', Chuj split in 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 contexts trigger it (Francisco Pascual 2007): aspectless complements, purpose clauses, coordinate clauses, preverbal depictives, resultatives, manner adverbs, and preverbal aspectual/modal auxiliaries (e.g. the progressive lanan). The imperfective chi- IS an aspect marker, so IMP clauses keep canonical ergative; only PROG (matrix lanan, not a preverbal aspect marker) triggers the split. caseQanjobalan approximates the syntactic trigger via .Prog; the other six contexts can't be encoded at this granularity.

Why .gen not .nom?

Both descriptive grammars ([VA11] §1.9.4 for Chol, [MT08] §1.1.1 for Q'anjob'al) characterize the non-perfective alignment as nominative-accusative (Set A as nominative-like). Alignment.extendedErgative.assignCase returns .gen on Coon's view (Set A on non-perfective subjects is genitive licensed by D under nominalization); the morphological identity of Set A with possessive markers makes .gen defensible, but it is a theoretical choice — a descriptive-grammar implementation would return .nom. [ZM17] §3 (p. 235) calls Coon's no-split re-analysis "unconvincing": the split-ergative pattern is the descriptive consensus.

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

Cholan aspect-driven case assignment ([VA11] §1.9.4; [ZM17] §3): ergative in perfective, extended-ergative (accusative-like) in all non-perfective aspects. Used by Chol; presumably also Chontal, Ch'orti', Cholti per the Cholan-branch generalization ([AEZM17]).

Equations

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

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

Q'anjob'alan aspect-driven case assignment ([MT08] §1.1.1; [ZM17] §3): the split is triggered by dependent clauses lacking aspect markers, not by aspect category. This function approximates that via .Prog (the lanan progressive is one of Francisco Pascual 2007's seven split contexts); other non-perfective aspects (e.g. .Imp with the chi- marker) keep canonical ergative. Contrast Cholan, where the IMP mi- marker does trigger the accusative split.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev Mayan.accCaseChol : Features.Prominence.ArgumentRole → 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

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev Mayan.accCaseQanjobalan : Features.Prominence.ArgumentRole → 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

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

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

Kaqchikel (K'ichean-Mamean = Eastern Mayan) aspect-driven case assignment. Per [Ima14] §3.3.1 ("Kaqchikel: ERG=OBJ", p. 122) and [Ima20] §2.2, Kaqchikel shows 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 (ERG/GEN) — the opposite of the Cholan/Q'anjob'alan extended-ergative pattern. Imanishi 2014 derives it from the Unaccusative Requirement on Nominalization plus phase-head ergative Case: the object is the only Case-less DP in the passivized nominalized clause and gets ERG/GEN from D, while the subject is base-generated 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 Kaqchikel-non-perfective generalization; other aspects keep canonical ergative (Imanishi 2014 Table 3.1, p. 95). Per [Ima14] fn. 26 (p. 141), some varieties/consultants reject patterns in [garcia-matzar-rodriguez-guajan-1997]; the claim rests on Imanishi's fieldwork on a specific variety.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev Mayan.accCaseKaqchikel : Features.Prominence.ArgumentRole → 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

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

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

K'iche' (K'ichean) case assignment. Per [Mon17] (Lessons 9, 15), K'iche' is uniformly ergative-absolutive with no aspect-conditioned split — Set A (ERG) cross-references A across all aspects, Set B (ABS) cross-references S and P. This contrasts with its sister Kaqchikel's construction-specific inverted PROG ajin pattern; per [Ima14] fn. 26 p. 141 K'ichean dialectal variation 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

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

@[reducible, inline]

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

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

Equations

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

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

San Juan Atitán Mam (K'ichean-Mamean / Eastern Mayan) case assignment. Per [Sco23] 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, so the tripartite analysis is recoverable only from agreement; per Scott 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 / [ZM17] §4–5) have been characterized as ergative with neutral patterns in dependent clauses, not tripartite; this substrate encodes Scott's SJA Mam analysis. Mam shows no aspect-conditioned split (Scott ch. 3), so the aspect parameter is retained only for shape-uniformity; all aspects map to tripartite.

Equations

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

@[reducible, inline]

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

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

Equations

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

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

Tseltalan (Tseltal, Tsotsil) case assignment.

Per [Pol13a] and [AP25]: 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

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

@[reducible, inline]

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

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

Equations

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

def Mayan.caseYukatek : UD.Aspect → Features.Prominence.ArgumentRole → Case

Yucatecan aspect/status-driven case assignment ([Hof17] p. 692: Set A marks transitive subjects and incompletive intransitive subjects; Set B marks transitive objects and completive intransitive subjects): ergative in the completive (perfective), extended-ergative in the incompletive aspects.

Equations

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

@[reducible, inline]

abbrev Mayan.ergCaseYukatek : Features.Prominence.ArgumentRole → Case

Yucatec completive ergative-absolutive case.

Equations

• Mayan.ergCaseYukatek = Mayan.caseYukatek UD.Aspect.Perf

@[reducible, inline]

abbrev Mayan.accCaseYukatek : Features.Prominence.ArgumentRole → Case

Yucatec incompletive extended-ergative case.

Equations

• Mayan.accCaseYukatek = Mayan.caseYukatek UD.Aspect.Imp

Person-number paradigm

The pan-Mayan person/number agreement paradigm is keyed by the canonical φ-cell Agreement.Cell (the same φ a Pronoun/Word carries): the six cells covering the cross-Mayan consensus (Cholan, K'ichean, Q'anjob'alan, Tseltalan; [KN84] Tables 7-8) are exactly Agreement.Cell.pnCells. Per-language Set A / Set B tables are Agreement.Paradigm String values constructed over those cells, so a controller's Word.agrCell indexes them directly ([Cor98]). Languages with a 1pl inclusive/exclusive split (Chol's -on lojon 1plExcl, [KN84] p. 91) refine at the per-language level.

Verb form (transitive vs Agent Focus)

inductive 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 Mayan.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

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

@[implicit_reducible]

instance Mayan.instReprVerbForm : Repr VerbForm

Equations

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

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

Equations

• Mayan.instReprVerbForm.repr Mayan.VerbForm.transitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbForm.transitive")).group prec✝
• Mayan.instReprVerbForm.repr Mayan.VerbForm.agentFocus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbForm.agentFocus")).group prec✝

def Mayan.VerbForm.hasSetA : VerbForm → Bool

Whether the form bears Set A agreement (ergative cross-reference). Canonical transitive: yes; AF forms "are morphologically intransitive and bear only a Set B (absolutive) affix" ([Pol17] p. 222).

Equations

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

def Mayan.VerbForm.hasAFSuffix : VerbForm → Bool

Whether the form bears a dedicated AF suffix. The exponent is per-language (Kaqchikel -ö or -n [Erl16], Q'anjob'al -on [CMPP14]); its presence tracks the form.

Equations

• Mayan.VerbForm.transitive.hasAFSuffix = false
• Mayan.VerbForm.agentFocus.hasAFSuffix = true

def Mayan.VerbForm.agreementSlots (f : VerbForm) : ℕ

Agreement slots on the verbal complex, derived from the paradigm inventory: Set B is always present; Set A only where the form bears it (transitive: 2, AF: 1).

Equations

• f.agreementSlots = 1 + if f.hasSetA = true then 1 else 0

Exponent tables

@[reducible, inline]

abbrev Mayan.ExponentTable : Type

An exponent table: a descriptive agreement paradigm over canonical φ-cells (Agreement.Cell), mapping each person/number cell to its surface string. Per-language setAExponent/setBExponent populate this; cross-Mayan typology theorems quantify over it.

Equations

• Mayan.ExponentTable = Agreement.Paradigm String

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

Decidable predicate: the third-person singular Set B slot is morphologically null. An invariant of the standard Mayan branches per [KN84] Table 8 (reconstructing to proto-Cholan and proto-Mayan), but not strictly pan-Mayan — SJA Mam's default Set B tz'= surfaces in the 3sg slot per [Sco23] §3.3.2, so mayan_p3sg_abs_null quantifies only over isStandard = true. The predicate is notation-agnostic: "-∅" (suffix-notated Set B: Cholan, Q'anjob'alan, Tseltal, and Tsotsil — whose system also has a prefixal subset, see Tsotsil.setBLinearity), "∅" (prefixal Set B: Kaqchikel and other K'ichean HIGH-ABS), and "∅-" all encode "no overt 3sg exponent". The disjunction form is kernel-decidable, unlike a String.replace normalization.

Equations

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

@[implicit_reducible]

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

Equations

• Mayan.instDecidableIsThirdSgZero e = id inferInstance

Marker linearity

inductive Mayan.MarkerLinearity : Type

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

Tseltalan languages contrast on this dimension: per [AP25] 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 Mayan.instDecidableEqMarkerLinearity : DecidableEq MarkerLinearity

Equations

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

@[implicit_reducible]

instance Mayan.instReprMarkerLinearity : Repr MarkerLinearity

Equations

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

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

Equations

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

Language registry and case dispatcher

def Mayan.all : List Mayan

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

Equations

• Mayan.all = [Mayan.Chol, Mayan.Qanjobal, Mayan.Kaqchikel, Mayan.Tseltal, Mayan.Tsotsil, Mayan.Mam, Mayan.Kiche, Mayan.Yukatek]

def Mayan.isStandard : Mayan → 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 [Sco23], San Juan Atitán Mam is morphologically tripartite (S, A, P each distinct in case and agreement), with Set B 3sg surfacing as the default tz'= rather than null — so mayan_p3sg_abs_null and mayan_perfective_ergative quantify only over isStandard = true. Whether Mam is "really" tripartite vs ergative-with-neutral-objects is contested (cf. England 1983b vs Scott 2023; Zavala 2017 §4 calls Ch'orti' the only tripartite Mayan); the substrate adopts Scott's analysis, recorded in Mam/Agreement.lean.

Equations

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

def Mayan.caseAt : Mayan → UD.Aspect → Features.Prominence.ArgumentRole → 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 Mayan rather than enumerate per-language rfl facts.

Equations

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

Verb templates

inductive Mayan.VerbSlot : Type

A position class in the Mayan verbal complex, in the traditional Mayanist categories (so Set A and Set B stay distinct — a cut Morphology.MorphCategory cannot draw).

• aspect : VerbSlot
• setB : VerbSlot
• setA : VerbSlot
• root : VerbSlot
• status : VerbSlot

@[implicit_reducible]

instance Mayan.instDecidableEqVerbSlot : DecidableEq VerbSlot

Equations

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

@[implicit_reducible]

instance Mayan.instReprVerbSlot : Repr VerbSlot

Equations

• Mayan.instReprVerbSlot = { reprPrec := Mayan.instReprVerbSlot.repr }

def Mayan.instReprVerbSlot.repr : VerbSlot → ℕ → Std.Format

Equations

• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.aspect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.aspect")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.setB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.setB")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.setA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.setA")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.root prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.root")).group prec✝
• Mayan.instReprVerbSlot.repr Mayan.VerbSlot.status prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mayan.VerbSlot.status")).group prec✝

def Mayan.template : Mayan → List VerbSlot

The verbal-complex template, stem-inclusive and left-to-right, in canonical transitive citation form. Per-language morpheme orders as documented in each fragment ([Pre14] (12) for the K'ichean shape, [VA11] §3.4 for Chol, [Pol17] for Tseltalan and the Mam status-suffix loss); Tsotsil's prefixal Set B subset is recorded at Tsotsil.setBLinearity.

Equations

• Mayan.Kaqchikel.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setB, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.status]
• Mayan.Kiche.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setB, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.status]
• Mayan.Qanjobal.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setB, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.status]
• Mayan.Mam.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setB, Mayan.VerbSlot.setA, Mayan.VerbSlot.root]
• Mayan.Chol.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.status, Mayan.VerbSlot.setB]
• Mayan.Yukatek.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.status, Mayan.VerbSlot.setB]
• Mayan.Tseltal.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.setB]
• Mayan.Tsotsil.template = [Mayan.VerbSlot.aspect, Mayan.VerbSlot.setA, Mayan.VerbSlot.root, Mayan.VerbSlot.setB]

def Mayan.templateABSPosition (l : Mayan) : ABSPosition

The absolutive-position classifier derived from the template: HIGH iff Set B precedes the root. absPosition_matches_template in Studies/CoonMateoPedroPreminger2014.lean checks it against the fragments' analytical absPosition values.

Equations

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