Yukatek Maya Verb Classes and Status System

@cite{bohnemeyer-2004} @cite{lucy-1994}

Yukatek Maya has a typologically rare split-intransitive pattern of argument marking controlled by overt aspect-mood marking. The system comprises five verb stem classes distinguished by their status inflection patterns (allomorphy of aspect-mood suffixes).

Verb Stem Classes

Class	Event type	Examples
active	process	walk, sing, dance, sneeze
inactive	state change	die, burst, enter, exit
inchoative	state change (stative root + -tal)	blacken, shrink, sink
positional	state change (spatial config.)	sit, stand, hang, be round
transitive active	transitive	hit, chip, eat

Status Categories

Status marking encodes both viewpoint aspect and modal assertiveness (@cite{bohnemeyer-2004} Table 2):

• completive: +perfective, +assertive → ergative (S = U)
• subjunctive: +perfective, −assertive → ergative (S = U)
• incompletive: −perfective, +assertive → accusative (S = A)
• imperative: directive mood

The split in argument marking is associated with the aspectual value: perfective status → S marked like U (ergative); imperfective status → S marked like A (accusative).

inductive Fragments.Mayan.Yukatek.VerbStemClass : Type

The five verb stem classes of Yukatek Maya, distinguished by status inflection patterns (@cite{bohnemeyer-2004} Table 3; @cite{lucy-1994}).

• active : VerbStemClass
• inactive : VerbStemClass
• inchoative : VerbStemClass
• positional : VerbStemClass
• transitiveActive : VerbStemClass

instance Fragments.Mayan.Yukatek.instDecidableEqVerbStemClass : DecidableEq VerbStemClass

Equations

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

instance Fragments.Mayan.Yukatek.instBEqVerbStemClass : BEq VerbStemClass

Equations

• Fragments.Mayan.Yukatek.instBEqVerbStemClass = { beq := Fragments.Mayan.Yukatek.instBEqVerbStemClass.beq }

def Fragments.Mayan.Yukatek.instBEqVerbStemClass.beq : VerbStemClass → VerbStemClass → Bool

Equations

• Fragments.Mayan.Yukatek.instBEqVerbStemClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Yukatek.instReprVerbStemClass : Repr VerbStemClass

Equations

• Fragments.Mayan.Yukatek.instReprVerbStemClass = { reprPrec := Fragments.Mayan.Yukatek.instReprVerbStemClass.repr }

def Fragments.Mayan.Yukatek.instReprVerbStemClass.repr : VerbStemClass → ℕ → Std.Format

Equations

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

def Fragments.Mayan.Yukatek.VerbStemClass.eventType : VerbStemClass → Semantics.Lexical.Verb.EventStructure.EventType

Event type encoded by each verb stem class. Active stems encode processes; all others encode state changes.

@cite{bohnemeyer-2004} §5: degree achievement verbs regularly appear in the inactive and inchoative classes despite being atelic. Their event structure encodes state change — the process/state-change distinction, not telicity, motivates class membership.

Equations

• Fragments.Mayan.Yukatek.VerbStemClass.active.eventType = Semantics.Lexical.Verb.EventStructure.EventType.process
• Fragments.Mayan.Yukatek.VerbStemClass.inactive.eventType = Semantics.Lexical.Verb.EventStructure.EventType.stateChange
• Fragments.Mayan.Yukatek.VerbStemClass.inchoative.eventType = Semantics.Lexical.Verb.EventStructure.EventType.stateChange
• Fragments.Mayan.Yukatek.VerbStemClass.positional.eventType = Semantics.Lexical.Verb.EventStructure.EventType.stateChange
• Fragments.Mayan.Yukatek.VerbStemClass.transitiveActive.eventType = Semantics.Lexical.Verb.EventStructure.EventType.stateChange

def Fragments.Mayan.Yukatek.VerbStemClass.isIntransitive : VerbStemClass → Bool

Whether a verb stem class is intransitive.

Equations

• Fragments.Mayan.Yukatek.VerbStemClass.transitiveActive.isIntransitive = false
• x✝.isIntransitive = true

inductive Fragments.Mayan.Yukatek.StatusCategory : Type

The four status categories of Yukatek Maya, encoding viewpoint aspect and modal assertiveness (@cite{bohnemeyer-2004} Table 2).

• completive : StatusCategory
• subjunctive : StatusCategory
• incompletive : StatusCategory
• imperative : StatusCategory

instance Fragments.Mayan.Yukatek.instDecidableEqStatusCategory : DecidableEq StatusCategory

Equations

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

def Fragments.Mayan.Yukatek.instBEqStatusCategory.beq : StatusCategory → StatusCategory → Bool

Equations

• Fragments.Mayan.Yukatek.instBEqStatusCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mayan.Yukatek.instBEqStatusCategory : BEq StatusCategory

Equations

• Fragments.Mayan.Yukatek.instBEqStatusCategory = { beq := Fragments.Mayan.Yukatek.instBEqStatusCategory.beq }

def Fragments.Mayan.Yukatek.instReprStatusCategory.repr : StatusCategory → ℕ → Std.Format

Equations

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

instance Fragments.Mayan.Yukatek.instReprStatusCategory : Repr StatusCategory

Equations

• Fragments.Mayan.Yukatek.instReprStatusCategory = { reprPrec := Fragments.Mayan.Yukatek.instReprStatusCategory.repr }

def Fragments.Mayan.Yukatek.StatusCategory.viewpointAspect : StatusCategory → Option Semantics.Tense.Aspect.Core.ViewpointAspectB

Aspectual value of a status category. Completive and subjunctive are perfective; incompletive is imperfective. Imperative has no clear aspectual value.

Equations

• Fragments.Mayan.Yukatek.StatusCategory.completive.viewpointAspect = some Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective
• Fragments.Mayan.Yukatek.StatusCategory.subjunctive.viewpointAspect = some Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective
• Fragments.Mayan.Yukatek.StatusCategory.incompletive.viewpointAspect = some Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective
• Fragments.Mayan.Yukatek.StatusCategory.imperative.viewpointAspect = none

def Fragments.Mayan.Yukatek.StatusCategory.isAssertive : StatusCategory → Bool

Whether the status category is assertive (modal component).

Equations

• Fragments.Mayan.Yukatek.StatusCategory.completive.isAssertive = true
• Fragments.Mayan.Yukatek.StatusCategory.incompletive.isAssertive = true
• x✝.isAssertive = false

def Fragments.Mayan.Yukatek.sArgumentMarker : StatusCategory → Option MarkerSet

Which marker set cross-references the sole argument (S) of an intransitive verb, given the status category.

@cite{bohnemeyer-2004} Table 2:

• Perfective status (completive/subjunctive): S = U → set-B (ergative)
• Imperfective status (incompletive): S = A → set-A (accusative)
• Imperative: not discussed in the split analysis (Table 2 omits it)

Equations

• Fragments.Mayan.Yukatek.sArgumentMarker Fragments.Mayan.Yukatek.StatusCategory.completive = some Fragments.Mayan.MarkerSet.setB
• Fragments.Mayan.Yukatek.sArgumentMarker Fragments.Mayan.Yukatek.StatusCategory.subjunctive = some Fragments.Mayan.MarkerSet.setB
• Fragments.Mayan.Yukatek.sArgumentMarker Fragments.Mayan.Yukatek.StatusCategory.incompletive = some Fragments.Mayan.MarkerSet.setA
• Fragments.Mayan.Yukatek.sArgumentMarker Fragments.Mayan.Yukatek.StatusCategory.imperative = none

theorem Fragments.Mayan.Yukatek.perfective_ergative : sArgumentMarker StatusCategory.completive = some MarkerSet.setB ∧ sArgumentMarker StatusCategory.subjunctive = some MarkerSet.setB

The split: perfective → set-B (ergative), imperfective → set-A (accusative).

theorem Fragments.Mayan.Yukatek.imperfective_accusative : sArgumentMarker StatusCategory.incompletive = some MarkerSet.setA

structure Fragments.Mayan.Yukatek.YukatekVerb : Type

A Yukatek verb entry for the split intransitivity analysis. Records stem class and causation type of the intransitive base.

• gloss : String
• stemClass : VerbStemClass
• causationType : Semantics.Lexical.Verb.EventStructure.CausationType

instance Fragments.Mayan.Yukatek.instBEqYukatekVerb : BEq YukatekVerb

Equations

• Fragments.Mayan.Yukatek.instBEqYukatekVerb = { beq := Fragments.Mayan.Yukatek.instBEqYukatekVerb.beq }

def Fragments.Mayan.Yukatek.instBEqYukatekVerb.beq : YukatekVerb → YukatekVerb → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Mayan.Yukatek.instBEqYukatekVerb.beq x✝¹ x✝ = false

def Fragments.Mayan.Yukatek.instReprYukatekVerb.repr : YukatekVerb → ℕ → Std.Format

Equations

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

instance Fragments.Mayan.Yukatek.instReprYukatekVerb : Repr YukatekVerb

Equations

• Fragments.Mayan.Yukatek.instReprYukatekVerb = { reprPrec := Fragments.Mayan.Yukatek.instReprYukatekVerb.repr }

def Fragments.Mayan.Yukatek.meyah : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.meyah = { gloss := "work", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.internal }

def Fragments.Mayan.Yukatek.baaxal : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.baaxal = { gloss := "play", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.internal }

def Fragments.Mayan.Yukatek.balak : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.balak = { gloss := "roll", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.peek : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.tsiirin : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.tsiirin = { gloss := "buzz", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.kim : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.kim = { gloss := "die", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.luub : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.luub = { gloss := "fall", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.booxTal : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.chichanTal : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.kaan : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.naak : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.naak = { gloss := "ascend", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.kulTal : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.waalTal : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.haan : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.haan = { gloss := "eat", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.internal }

def Fragments.Mayan.Yukatek.chiik : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.chiik = { gloss := "shake", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.haarax : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.haarax = { gloss := "slide", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.huuy : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.huuy = { gloss := "stir", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.mosoon : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.mosoon = { gloss := "whirl", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.pirik : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.pirik = { gloss := "flick", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.walak : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.nikich : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.nikich = { gloss := "squeak", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.active, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.chilTal : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.xolTal : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.lab : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.tiil : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.tsuuk : YukatekVerb

Equations

• Fragments.Mayan.Yukatek.tsuuk = { gloss := "rot", stemClass := Fragments.Mayan.Yukatek.VerbStemClass.inactive, causationType := Semantics.Lexical.Verb.EventStructure.CausationType.external }

def Fragments.Mayan.Yukatek.haats : YukatekVerb

Equations

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

def Fragments.Mayan.Yukatek.VerbStemClass.toTemplate : VerbStemClass → Semantics.Lexical.Verb.EventStructure.Template

Map Yukatek verb stem classes to R&H event structure templates. This connects the language-specific classification to the theory-level decomposition in EventStructure.lean.

• Active → activity [x ACT]
• Inactive/inchoative → achievement [BECOME [x ⟨STATE⟩]]
• Positional → achievement (externally-caused spatial config.)
• Transitive active → accomplishment [[x ACT] CAUSE [BECOME [y ⟨STATE⟩]]]

Equations

• Fragments.Mayan.Yukatek.VerbStemClass.active.toTemplate = Semantics.Lexical.Verb.EventStructure.Template.activity
• Fragments.Mayan.Yukatek.VerbStemClass.inactive.toTemplate = Semantics.Lexical.Verb.EventStructure.Template.achievement
• Fragments.Mayan.Yukatek.VerbStemClass.inchoative.toTemplate = Semantics.Lexical.Verb.EventStructure.Template.achievement
• Fragments.Mayan.Yukatek.VerbStemClass.positional.toTemplate = Semantics.Lexical.Verb.EventStructure.Template.achievement
• Fragments.Mayan.Yukatek.VerbStemClass.transitiveActive.toTemplate = Semantics.Lexical.Verb.EventStructure.Template.accomplishment

theorem Fragments.Mayan.Yukatek.eventType_consistent (c : VerbStemClass) : c.eventType = c.toTemplate.eventType

The stem class → template mapping preserves event type: VerbStemClass.eventType agrees with Template.eventType ∘ toTemplate.

def Fragments.Mayan.Yukatek.yukatekSplit : Core.SplitErgativity StatusCategory

Yukatek split-ergative system, parameterized by status category. Perfective status (completive/subjunctive) triggers ergative alignment; imperfective status (incompletive) triggers accusative alignment. Imperative is treated as ergative (completive-like default).

This instantiates the same Core.SplitErgativity type used by Hindi and Georgian, enabling cross-linguistic comparison.

Equations

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

theorem Fragments.Mayan.Yukatek.yukatek_completive_erg : yukatekSplit.alignment StatusCategory.completive = Core.AlignmentFamily.ergative

theorem Fragments.Mayan.Yukatek.yukatek_subjunctive_erg : yukatekSplit.alignment StatusCategory.subjunctive = Core.AlignmentFamily.ergative

theorem Fragments.Mayan.Yukatek.yukatek_incompletive_acc : yukatekSplit.alignment StatusCategory.incompletive = Core.AlignmentFamily.accusative

theorem Fragments.Mayan.Yukatek.yukatek_hindi_same_split : yukatekSplit.alignment StatusCategory.completive = Core.hindiSplit.alignment Core.Aspect.perfective ∧ yukatekSplit.alignment StatusCategory.incompletive = Core.hindiSplit.alignment Core.Aspect.imperfective

Yukatek and Hindi share the same split conditioning: perfective → ergative, imperfective → accusative. This is @cite{bohnemeyer-2004}'s core insight that a single linking-by-viewpoint mechanism underlies both systems.