Building verbs in Chuj

[Coo19]'s analysis of Chuj verb stems: roots determine internal arguments, the four v/Voice⁰ heads (Ø, -ch, -j, -w) determine external arguments. The root lexicon lives in Fragments/Mayan/Chuj/RootClasses.lean, the attested examples in Data.Examples.Coon2019.

Main declarations

• Chuj.RootClass.toClassification — Coon's coordinates for the root classes, as a derived projection.
• selects, isGrammatical — each head's selection condition on the root coordinates; the paradigm table is derived, not stipulated (isGrammatical_table), and checked against the attested data (paradigm_predicts_attestation).
• vØ, v_w, v_ch, v_j — the voice heads, on substrate Voice.Flavor cells; the agent diagnostics and the -aj distribution are derived from their parametric semantics.

Root-class coordinates

def Chuj.RootClass.toClassification : RootClass → Verb.Root.Classification

[Coo19]'s coordinates for each root class ((3), p. 37), as a derived projection off the class label. The changeType column is a representative placeholder — Coon's classes mix change-of-state and non-change roots (p. 60), and [BEJ+21] subdivides √TV on exactly this axis.

Equations

• One or more equations did not get rendered due to their size.
• Chuj.RootClass.pos.toClassification = { valency := ∅, changeType := Verb.Root.ChangeType.propertyConcept, denotationType := some (Intensional.Ty.e ⇒ Intensional.Ty.s ⇒ Intensional.Ty.d) }
• Chuj.RootClass.nom.toClassification = { valency := ∅, changeType := Verb.Root.ChangeType.propertyConcept, denotationType := some (Intensional.Ty.e ⇒ Intensional.Ty.t) }

def Coon2019.unaccusative (r : Verb.Root.Classification) : Bool

A root is unaccusative when it takes an internal argument but does not license transitive Voice (§3.3).

Equations

• Coon2019.unaccusative r = (r.valency == {ArgumentStructure.ArgPosition.internal} && !r.licensesTransitiveVoice)

Selection and the paradigm

def Coon2019.selects (vs : Chuj.VoiceSuffix) (r : Verb.Root.Classification) : Bool

The selection condition each voice suffix imposes on the root's coordinates: the Ø slot covers transitive vØ (requires transitive licensing) and the null intransitive v (selects unaccusatives); the passives -ch and -j presuppose a transitive stem; -w introduces an external argument and rejects exactly the unaccusative class (p. 45).

Equations

• Coon2019.selects Chuj.VoiceSuffix.null r = (r.licensesTransitiveVoice || Coon2019.unaccusative r)
• Coon2019.selects Chuj.VoiceSuffix.ch r = r.licensesTransitiveVoice
• Coon2019.selects Chuj.VoiceSuffix.j r = r.licensesTransitiveVoice
• Coon2019.selects Chuj.VoiceSuffix.w r = !Coon2019.unaccusative r

def Coon2019.isGrammatical (rc : Chuj.RootClass) (vs : Chuj.VoiceSuffix) : Bool

A root class forms a grammatical stem with a voice suffix exactly when the suffix selects the class's coordinates. Does not cover derived transitive stems in -ej, which all four classes form (§2.2), or the isolated -j forms on non-transitive roots (ex. (71), p. 71).

Equations

• Coon2019.isGrammatical rc vs = Coon2019.selects vs rc.toClassification

theorem Coon2019.isGrammatical_table : (∀ (vs : Chuj.VoiceSuffix), isGrammatical Chuj.RootClass.tv vs = true) ∧ (∀ (vs : Chuj.VoiceSuffix), isGrammatical Chuj.RootClass.itv vs = (vs == Chuj.VoiceSuffix.null)) ∧ (∀ (vs : Chuj.VoiceSuffix), isGrammatical Chuj.RootClass.pos vs = (vs == Chuj.VoiceSuffix.w)) ∧ ∀ (vs : Chuj.VoiceSuffix), isGrammatical Chuj.RootClass.nom vs = (vs == Chuj.VoiceSuffix.w)

Coon's paradigm table, derived: √TV takes all four voices, √ITV only null v, √POS and √NOM only -w.

theorem Coon2019.every_class_verbalizes (rc : Chuj.RootClass) : ∃ (vs : Chuj.VoiceSuffix), isGrammatical rc vs = true

Every root class verbalizes under some v/Voice⁰ head: categorization is free at category grain (DistributedMorphology.same_root_different_category); the paradigm gaps are flavor-level selection (selects).

def Chuj.VoiceSuffix.categorizer : VoiceSuffix → DistributedMorphology.Categorizer

Each v/Voice⁰ head is a verbal categorizer in the DM sense ([Coo19] treats all four as bundled v/Voice⁰).

Equations

• x✝.categorizer = DistributedMorphology.Categorizer.v

def Coon2019.formsBareTransitive (rc : Chuj.RootClass) : Bool

A root class forms bare transitive stems exactly when it licenses transitive Voice (§2.2, p. 41).

Equations

• Coon2019.formsBareTransitive rc = rc.toClassification.licensesTransitiveVoice

Paradigm data (§§2–5)

Attested examples live in Data/Examples/Coon2019.json (generated module Data.Examples.Coon2019); each row carries the root form and [Coo19]'s voice segmentation as paperFeatures.

def Coon2019.readVoice : String → Option Chuj.VoiceSuffix

Parse a row's voice feature.

Equations

• Coon2019.readVoice "null" = some Chuj.VoiceSuffix.null
• Coon2019.readVoice "ch" = some Chuj.VoiceSuffix.ch
• Coon2019.readVoice "j" = some Chuj.VoiceSuffix.j
• Coon2019.readVoice "w" = some Chuj.VoiceSuffix.w
• Coon2019.readVoice x✝ = none

def Coon2019.rowRoot (e : Data.Examples.LinguisticExample) : Option Chuj.ChujRoot

The root a row attests, looked up in the fragment lexicon by its rootForm feature.

Equations

• Coon2019.rowRoot e = do let f ← e.feature? "rootForm" List.find? (fun (x : Chuj.ChujRoot) => x.form == f) Chuj.allRoots

def Coon2019.paradigmData : List (Chuj.RootClass × Chuj.VoiceSuffix × Bool)

Root class, voice, and grammaticality for each attestation row; the adverb-diagnostic rows are excluded.

Equations

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

theorem Coon2019.paradigmData_complete : paradigmData.length = 8

All eight attestation rows survive the adapter.

theorem Coon2019.paradigm_predicts_attestation : (paradigmData.all fun (x : Chuj.RootClass × Chuj.VoiceSuffix × Bool) => match x with | (rc, vs, g) => isGrammatical rc vs == g) = true

The derived paradigm agrees with the recorded judgment of every attested example.

Minimalist voice heads (ex. (78))

def Coon2019.vØ : Minimalist.Voice.Head

Active transitive v/Voice⁰ (Ø): introduces overt agent in Spec,VoiceP, assigns ergative case, phase head (v*).

Equations

• Coon2019.vØ = { flavor := Minimalist.Voice.Flavor.agentive, hasD := true }

def Coon2019.v_w : Minimalist.Voice.Head

Agentive intransitive v/Voice⁰ (-w): overt agent, absolutive case (p. 54) — the substrate's .antipassive cell, non-phasal by default. Verbalizes √NOM and √POS, forms √TV antipassives, and models the null intransitive v/Voice⁰ of √ITV (p. 40).

Equations

• Coon2019.v_w = { flavor := Minimalist.Voice.Flavor.antipassive, hasD := true }

def Coon2019.v_ch : Minimalist.Voice.Head

Passive v/Voice⁰ (-ch): implicit, existentially bound agent (pp. 68–69) — the substrate's .impersonal cell [−D, +∃x]. Agent adverbs and by-phrases confirm the agent's semantic presence.

Equations

• Coon2019.v_ch = { flavor := Minimalist.Voice.Flavor.impersonal, hasD := false }

def Coon2019.v_j : Minimalist.Voice.Head

Agentless passive v/Voice⁰ (-j): verbalizes the stem, introduces no external argument, overt or implicit (p. 70). hasD := false diverges from .nonThematic's [+D] SE cell (v_j_not_dCoherent).

Equations

• Coon2019.v_j = { flavor := Minimalist.Voice.Flavor.nonThematic, hasD := false }

def Coon2019.toVoiceHead : Chuj.VoiceSuffix → Minimalist.Voice.Head

Map each voice suffix to its Minimalist Head.

Equations

• Coon2019.toVoiceHead Chuj.VoiceSuffix.null = Coon2019.vØ
• Coon2019.toVoiceHead Chuj.VoiceSuffix.ch = Coon2019.v_ch
• Coon2019.toVoiceHead Chuj.VoiceSuffix.j = Coon2019.v_j
• Coon2019.toVoiceHead Chuj.VoiceSuffix.w = Coon2019.v_w

Voice head properties

theorem Coon2019.agent_presence : vØ.AssignsTheta ∧ v_w.AssignsTheta ∧ ¬v_ch.AssignsTheta ∧ v_ch.params.assignsTheta? = some true

Ø and -w project an overt θ-marked agent; -ch's agent is present only in the broad params.assignsTheta? sense.

theorem Coon2019.v_j_no_theta : ¬v_j.AssignsTheta ∧ v_j.params.assignsTheta? = some false

-j has no agent in any sense (p. 70).

theorem Coon2019.ch_j_params_contrast : v_ch.params.extArgSemantics = some Minimalist.Voice.ExternalArgSemantics.thematicExistential ∧ v_j.params.assignsTheta? = some false

-ch's agent is existentially bound, -j's is absent (§4.1).

theorem Coon2019.only_vØ_is_phase : vØ.IsPhasal ∧ ¬v_w.IsPhasal ∧ ¬v_ch.IsPhasal ∧ ¬v_j.IsPhasal

Only Ø is a phase head (assigns ergative case).

theorem Coon2019.v_j_not_dCoherent : vØ.DCoherent ∧ v_w.DCoherent ∧ v_ch.DCoherent ∧ ¬v_j.DCoherent

Ø, -w, and -ch are [D]-coherent; -j diverges from .nonThematic's SE-type [+D] cell.

Derived diagnostics (§4.1)

The agent diagnostics are predictions read off the heads' parametric semantics, checked against the attested minimal pair (adverb_pair_predicted).

def Chuj.VoiceSuffix.participantFate (vs : VoiceSuffix) : Voice.ParticipantFate

The fate of the external argument, read off the head's parametric semantics (§4.1).

Equations

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

def Coon2019.agentAdverbOK (vs : Chuj.VoiceSuffix) : Bool

Agent-oriented adverbs are predicted grammatical exactly where the head supplies an agent, overt or implicit (§4.1).

Equations

• Coon2019.agentAdverbOK vs = ((Coon2019.toVoiceHead vs).params.assignsTheta? == some true)

def Coon2019.byPhraseOK (vs : Chuj.VoiceSuffix) : Bool

Agentive by-phrases are predicted grammatical exactly where the head's agent is implicit (§4.1); with an overt agent the by-phrase has nothing to identify.

Equations

• Coon2019.byPhraseOK vs = ((Coon2019.toVoiceHead vs).params.extArgSemantics == some Minimalist.Voice.ExternalArgSemantics.thematicExistential)

theorem Coon2019.adverb_pair_predicted : agentAdverbOK Chuj.VoiceSuffix.ch = (Examples.ex_63a.judgment != Features.Judgment.ungrammatical) ∧ agentAdverbOK Chuj.VoiceSuffix.j = (Examples.ex_67a.judgment != Features.Judgment.ungrammatical)

agentAdverbOK predicts the (63a)/(67a) minimal pair.

theorem Coon2019.passive_contrast : agentAdverbOK Chuj.VoiceSuffix.ch = true ∧ byPhraseOK Chuj.VoiceSuffix.ch = true ∧ agentAdverbOK Chuj.VoiceSuffix.j = false ∧ byPhraseOK Chuj.VoiceSuffix.j = false

Both passives lack an overt external argument, but -ch has an implicit agent and -j none, and both diagnostics track the difference.

-aj distribution (§4.2)

-aj marks an implicit argument on a √TV stem — an overt reflex of Existential Closure ([Die92]) per [Coo19] (p. 73).

inductive Coon2019.AntipassiveType : Type

The two antipassive (-w) subtypes: absolutive (implicit theme, ex. (55b–c)) vs incorporation (overt bare-NP theme, ex. (54a)).

• absolutive : AntipassiveType

  Theme is implicit (suppressed).

• incorporation : AntipassiveType

  Theme is an overt bare NP (incorporated).

@[instance_reducible]

instance Coon2019.instDecidableEqAntipassiveType : DecidableEq AntipassiveType

Equations

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

def Coon2019.instReprAntipassiveType.repr : AntipassiveType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Coon2019.instReprAntipassiveType : Repr AntipassiveType

Equations

• Coon2019.instReprAntipassiveType = { reprPrec := Coon2019.instReprAntipassiveType.repr }

def Coon2019.triggersAj (v : Minimalist.Voice.Head) (implicitInternal : Bool) : Bool

-aj surfaces when the stem has an implicit argument: the existentially bound agent of -ch, or the suppressed theme of the absolutive antipassive.

Equations

• Coon2019.triggersAj v implicitInternal = (v.params.extArgSemantics == some Minimalist.Voice.ExternalArgSemantics.thematicExistential || implicitInternal)

def Coon2019.ajOnPassive (vs : Chuj.VoiceSuffix) : Bool

-aj on stems in passive/agentless contexts (-w is handled by ajOnAntipassive).

Equations

• Coon2019.ajOnPassive vs = Coon2019.triggersAj (Coon2019.toVoiceHead vs) false

def Coon2019.ajOnAntipassive (apt : AntipassiveType) : Bool

-aj on antipassive (-w) stems: present exactly in the absolutive subtype.

Equations

• Coon2019.ajOnAntipassive apt = Coon2019.triggersAj Coon2019.v_w (apt == Coon2019.AntipassiveType.absolutive)

theorem Coon2019.ch_aj_passive : ajOnPassive Chuj.VoiceSuffix.ch = true

The -ch passive triggers -aj: its agent is implicit (ex. (58), p. 66).

theorem Coon2019.no_implicit_external : ajOnPassive Chuj.VoiceSuffix.null = false ∧ ajOnPassive Chuj.VoiceSuffix.w = false ∧ ajOnPassive Chuj.VoiceSuffix.j = false

Ø, -w, and -j alone trigger no -aj: none has an implicit external argument.

theorem Coon2019.aj_antipassive_split : ajOnAntipassive AntipassiveType.absolutive = true ∧ ajOnAntipassive AntipassiveType.incorporation = false

The absolutive antipassive triggers -aj: its theme is implicit (ex. (55b–c), p. 65); the incorporation antipassive does not — its theme is an overt bare NP (ex. (54a), p. 64).

-aj is not a morphome

The -aj piece shared by -chaj and -waj is one meaningful exponent — an Existential Closure reflex ([Coo19], p. 73) — not an arbitrary marker of a stem class: its distribution over the stem cells is exactly the implicit-argument class predicted by triggersAj.

inductive Coon2019.StemCell : Type

The five √TV stem shapes: the four voice slots, with -w split by antipassive subtype (ex. (78), p. 76; table (58), p. 66).

• active : StemCell

  The Ø transitive stem.

• passive : StemCell

  The -chaj passive.

• agentless : StemCell

  The -ji agentless passive.

• absolutiveAP : StemCell

  The -waj absolutive antipassive.

• incorporationAP : StemCell

  The -wi incorporation antipassive.

@[instance_reducible]

instance Coon2019.instDecidableEqStemCell : DecidableEq StemCell

Equations

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

def Coon2019.instReprStemCell.repr : StemCell → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Coon2019.instReprStemCell.repr Coon2019.StemCell.active prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemCell.active")).group prec✝
• Coon2019.instReprStemCell.repr Coon2019.StemCell.passive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemCell.passive")).group prec✝
• Coon2019.instReprStemCell.repr Coon2019.StemCell.agentless prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemCell.agentless")).group prec✝

@[instance_reducible]

instance Coon2019.instReprStemCell : Repr StemCell

Equations

• Coon2019.instReprStemCell = { reprPrec := Coon2019.instReprStemCell.repr }

def Coon2019.StemCell.voice : StemCell → Chuj.VoiceSuffix

The voice suffix of each stem cell.

Equations

• Coon2019.StemCell.active.voice = Chuj.VoiceSuffix.null
• Coon2019.StemCell.passive.voice = Chuj.VoiceSuffix.ch
• Coon2019.StemCell.agentless.voice = Chuj.VoiceSuffix.j
• Coon2019.StemCell.absolutiveAP.voice = Chuj.VoiceSuffix.w
• Coon2019.StemCell.incorporationAP.voice = Chuj.VoiceSuffix.w

def Coon2019.StemCell.implicitInternal : StemCell → Bool

Whether the cell's theme is implicit.

Equations

• Coon2019.StemCell.absolutiveAP.implicitInternal = true
• x✝.implicitInternal = false

inductive Coon2019.StemPiece : Type

The exponent pieces of [Coo19]'s stem decomposition (table (58), p. 66).

• ch : StemPiece

  The passive piece -ch.

• j : StemPiece

  The agentless-passive piece -j.

• w : StemPiece

  The antipassive/verbalizer piece -w.

• aj : StemPiece

  The Existential Closure reflex -aj.

@[instance_reducible]

instance Coon2019.instDecidableEqStemPiece : DecidableEq StemPiece

Equations

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

def Coon2019.instReprStemPiece.repr : StemPiece → ℕ → Std.Format

Equations

• Coon2019.instReprStemPiece.repr Coon2019.StemPiece.ch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemPiece.ch")).group prec✝
• Coon2019.instReprStemPiece.repr Coon2019.StemPiece.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemPiece.j")).group prec✝
• Coon2019.instReprStemPiece.repr Coon2019.StemPiece.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemPiece.w")).group prec✝
• Coon2019.instReprStemPiece.repr Coon2019.StemPiece.aj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Coon2019.StemPiece.aj")).group prec✝

@[instance_reducible]

instance Coon2019.instReprStemPiece : Repr StemPiece

Equations

• Coon2019.instReprStemPiece = { reprPrec := Coon2019.instReprStemPiece.repr }

def Coon2019.StemCell.pieces : StemCell → List StemPiece

The attested pieces of each stem cell (status suffixes omitted).

Equations

• Coon2019.StemCell.active.pieces = []
• Coon2019.StemCell.passive.pieces = [Coon2019.StemPiece.ch, Coon2019.StemPiece.aj]
• Coon2019.StemCell.agentless.pieces = [Coon2019.StemPiece.j]
• Coon2019.StemCell.absolutiveAP.pieces = [Coon2019.StemPiece.w, Coon2019.StemPiece.aj]
• Coon2019.StemCell.incorporationAP.pieces = [Coon2019.StemPiece.w]

theorem Coon2019.mem_ajCells_iff (c : StemCell) : c ∈ Morphology.exponentCells StemCell.pieces StemPiece.aj ↔ triggersAj (toVoiceHead c.voice) c.implicitInternal = true

A cell bears the -aj piece exactly when its configuration has an implicit argument.

theorem Coon2019.aj_not_morphomic : Morphology.exponentCells StemCell.pieces StemPiece.aj = {c : StemCell | triggersAj (toVoiceHead c.voice) c.implicitInternal = true}

The -aj bearer set is the semantically characterized implicit-argument class — the sharing across passive and antipassive is not an arbitrary kernel.

Event decomposition

def Coon2019.resultLower : List Minimalist.VerbHead

Lower event structure for result roots: cause + change + result state.

Equations

• Coon2019.resultLower = [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE]

def Coon2019.activityLower : List Minimalist.VerbHead

Lower event structure for activity roots (√TV PC, √ITV, √NOM): no sub-eventive decomposition below Voice.

Equations

• Coon2019.activityLower = []

def Coon2019.positionalLower : List Minimalist.VerbHead

Lower event structure for positional roots (√POS): stative.

Equations

• Coon2019.positionalLower = [Minimalist.VerbHead.vBE]

theorem Coon2019.tv_res_active : Minimalist.isCausative (Minimalist.Voice.buildDecomposition vØ resultLower) = true

Active transitives built from result roots are causative.

theorem Coon2019.tv_res_passive_ch : Minimalist.hasCause (Minimalist.Voice.buildDecomposition v_ch resultLower) = true ∧ v_ch.params.assignsTheta? = some true

In the -ch passive of a result root, CAUSE persists and the agent stays semantically present, but no specifier is projected.

theorem Coon2019.tv_res_agentless : Minimalist.isInchoative (Minimalist.Voice.buildDecomposition v_j resultLower) = true

The -j form of a result root is a pure change of state — an inchoative (p. 70).

theorem Coon2019.itv_intransitive : Minimalist.isActivity (Minimalist.Voice.buildDecomposition v_w activityLower) = true

Intransitive roots with their v/Voice⁰ head form activities (p. 40).

theorem Coon2019.pos_agentive : Minimalist.Voice.buildDecomposition v_w positionalLower = [Minimalist.VerbHead.vDO, Minimalist.VerbHead.vBE]

Positional roots verbalized by -w describe an agent assuming a position ((23), p. 48).

theorem Coon2019.nom_agentive : Minimalist.isActivity (Minimalist.Voice.buildDecomposition v_w activityLower) = true

Nominal roots verbalized by -w form activities ((16b), p. 45).

Root-class contrasts

theorem Coon2019.tv_itv_same_type_different_voice : Chuj.RootClass.tv.toClassification.denotationType = Chuj.RootClass.itv.toClassification.denotationType ∧ Chuj.RootClass.tv.toClassification.valency = Chuj.RootClass.itv.toClassification.valency ∧ Chuj.RootClass.tv.toClassification.licensesTransitiveVoice ≠ Chuj.RootClass.itv.toClassification.licensesTransitiveVoice

√TV and √ITV share semantic type and valency ([Dav97]; §3.3); transitive-Voice licensing alone separates them.

theorem Coon2019.salience_of_root_classes : Chuj.RootClass.tv.toClassification.salienceClass = some ArgumentStructure.SalienceClass.agentPatient ∧ Chuj.RootClass.itv.toClassification.salienceClass = none ∧ Chuj.RootClass.pos.toClassification.salienceClass = none ∧ Chuj.RootClass.nom.toClassification.salienceClass = none

Only √TV determines a salience class — agent-patient, the cell of [Luc94]'s Yucatec =∅ roots; the intransitive classes are underdetermined.