Chuj Verb Building: Empirical Data and Bridge Theorems

@cite{coon-2019}

Minimalist analysis and bridge theorems for @cite{coon-2019} "Building verbs in Chuj: Consequences for the nature of roots." Journal of Linguistics 55(1): 35–81.

Theory-neutral data (root classes, voice morphology, paradigm grammaticality, -aj distribution, agent diagnostics, root lexicon) lives in the Chuj fragment (Fragments/Chuj/VerbBuilding.lean). This file provides:

Paradigm examples (§§1–2)

Glossed Chuj sentences with root, voice suffix, and grammaticality.

Minimalist analysis (§§3–9)

Voice heads as Minimalist.VoiceHead instances, event decomposition via buildDecomposition, existential closure (-aj), and division of labor / causative alternation proved from the Voice–root split.

Bridge theorems (§§10–16)

Connect the fragment's theory-neutral types (CRootClass, ChujVoiceSuffix, isGrammatical, etc.) to Minimalist VoiceHead properties and to the @cite{beavers-etal-2021} root typology.

Chuj fragment bridge (§§10–15)

1. Root class ↔ Root arity: CRootClass maps to RootClassification values. √TV = selectsTheme, others = noTheme.
2. Voice suffix ↔ VoiceHead: theta assignment, D feature, phase head.
3. Paradigm predictions: isGrammatical matches data attestation.
4. -aj predictions: hasImplicitExternal / triggersAj match -aj distribution.
5. Agent diagnostics: assignsTheta matches agent adverb / by-phrase.
6. Division of labor: formsBareTransitive aligns with arity.

Root typology bridge

The chronologically-later @cite{beavers-etal-2021} paper hosts the bridge content connecting Coon's Chuj root classes to the cross-linguistic CoS typology (relocated to Phenomena/Causation/Studies/BeaversEtAl2021.lean §§8-14 per the chronological-dependency rule — Coon 2019 < Beavers 2021, so only the later paper may reference the earlier).

structure Coon2019.ChujExample : Type

A glossed Chuj example sentence.

• exNumber : ℕ

  Example number in the paper

• page : ℕ

  Page number

• chuj : String

  Chuj form

• english : String

  English translation

• verb : Fragments.Chuj.ChujRoot

  Root used (from the Chuj fragment lexicon)

• voice : Fragments.Chuj.ChujVoiceSuffix

  Voice suffix

• grammatical : Bool

  Whether the example is grammatical

@[implicit_reducible]

instance Coon2019.instReprChujExample : Repr ChujExample

Equations

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

def Coon2019.instReprChujExample.repr : ChujExample → ℕ → Std.Format

Equations

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

def Coon2019.ex10a : ChujExample

(10a) Active transitive: √TV + Ø (§2.2, p. 41).

Equations

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

def Coon2019.ex7a : ChujExample

(7a) √ITV + null v (§2.1, p. 40).

Equations

• Coon2019.ex7a = { exNumber := 7, page := 40, chuj := "Ix-onh-way-i", english := "We slept.", verb := Fragments.Chuj.way, voice := Fragments.Chuj.ChujVoiceSuffix.null, grammatical := true }

def Coon2019.ex23a : ChujExample

(23a) √POS + -w (§3, p. 48).

Equations

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

def Coon2019.ex16b : ChujExample

(16b) √NOM + -w (§2.5, p. 45).

Equations

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

def Coon2019.ex62 : ChujExample

(62) √TV + -chaj (passive, §4.1.1, p. 68).

Equations

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

def Coon2019.ex59 : ChujExample

(59) √TV + -j (agentless passive, §4.1.2, p. 67).

Equations

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

def Coon2019.ex63a : ChujExample

(63a) Agent adverb with -chaj: grammatical (§4.1.1, p. 68).

Equations

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

def Coon2019.ex67a : ChujExample

(67a) Agent adverb with -j: ungrammatical (§4.1.2, p. 70).

Equations

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

def Coon2019.ex54a : ChujExample

(54a) √TV + -w incorporation antipassive (§4, p. 64).

Equations

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

def Coon2019.ex55 : ChujExample

(55b) √TV + -w absolutive antipassive (§4, p. 65).

Equations

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

theorem Coon2019.examples_grammaticality : ex10a.grammatical = true ∧ ex7a.grammatical = true ∧ ex23a.grammatical = true ∧ ex16b.grammatical = true ∧ ex62.grammatical = true ∧ ex59.grammatical = true ∧ ex63a.grammatical = true ∧ ex67a.grammatical = false ∧ ex54a.grammatical = true ∧ ex55.grammatical = true

Grammatical examples are predicted grammatical; ungrammatical examples are predicted ungrammatical.

def Coon2019.vØ : Minimalist.VoiceHead

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

Equations

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

def Coon2019.v_w : Minimalist.VoiceHead

Agentive intransitive v/Voice⁰ (-w): introduces overt agent in Spec,VoiceP but assigns absolutive (not ergative) case (p. 54). Merges directly with root — cannot attach to derived stems (p. 54, (34b)). Used with √NOM and √POS to verbalize roots, and with √TV in incorporation antipassives (where the theme is a bare NP). Also models the null intransitive v/Voice⁰ for √ITV roots (p. 40): both introduce an agent and assign absolutive, differing only in overt (-w) vs null morphological realization.

Equations

• Coon2019.v_w = { flavor := Minimalist.VoiceFlavor.agentive, hasD := true, phaseOverride := some false }

def Coon2019.v_ch : Minimalist.VoiceHead

Passive v/Voice⁰ (-ch): assigns θ-role to an implicit (existentially bound) external argument (p. 68–69). Agent-oriented adverbs and by-phrases are licensed, confirming semantic presence of agent. Only combines with √TV roots.

Equations

• Coon2019.v_ch = { flavor := Minimalist.VoiceFlavor.agentive, hasD := false, phaseOverride := some false }

def Coon2019.v_j : Minimalist.VoiceHead

Agentless passive v/Voice⁰ (-j): verbalizes stem but introduces no external argument — neither overt nor implicit (p. 70: "does not assign a thematic role and does not merge an external argument"). No agent-oriented adverbs, no agentive by-phrases. Used with √TV (agentless passive) and non-transitive roots (inchoative/stative readings).

Equations

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

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.agentive_voices_assign_theta : vØ.AssignsTheta ∧ v_w.AssignsTheta ∧ v_ch.AssignsTheta

All three agentive voices (Ø, -w, -ch) assign a θ-role.

theorem Coon2019.v_j_no_theta : ¬v_j.AssignsTheta

-j does NOT assign a θ-role: agentless (p. 70).

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.tv_res_active : Minimalist.isCausative (Minimalist.buildDecomposition vØ resultLower) = true

√TV result + Ø → causative [vDO, vGO, vBE] (active transitive).

theorem Coon2019.tv_res_passive_ch : Minimalist.isCausative (Minimalist.buildDecomposition v_ch resultLower) = true

√TV result + -ch → causative [vDO, vGO, vBE] (passive with implicit agent). Event structure is still causative — the agent is semantically present.

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

√TV result + -j → inchoative [vGO, vBE] (agentless passive / anticausative). No agent at all — the event is a pure change-of-state (p. 70).

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

√ITV + v/Voice⁰ → activity [vDO] (intransitive). Uses v_w, which shares formal properties with the null intransitive v/Voice⁰ for √ITV (both are agentive, non-ERG-assigning; p. 40).

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

√POS + -w → [vDO, vBE]: agent assumes a position (agentive stative). (p. 48, (23)): chot-w-i "The frog hopped."

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

√NOM + -w → activity [vDO] (denominal agentive intransitive). (p. 45, (16b)): chanhal-w-i "I danced."

def Coon2019.hasImplicitExternal (v : Minimalist.VoiceHead) : Bool

Does this Voice head have an implicit (existentially bound) external argument? True when Voice assigns θ but has no overt specifier.

Equations

• Coon2019.hasImplicitExternal v = (decide v.AssignsTheta && !v.hasD)

def Coon2019.triggersAj (v : Minimalist.VoiceHead) (implicitInternal : Bool) : Bool

-aj (Existential Closure) surfaces when there is any implicit argument: implicit external (from Voice, as in -ch) or implicit internal (from theme suppression in absolutive antipassive -w-aj).

implicitInternal is true when a √TV root's theme is not filled by an overt DP (absolutive antipassive, not incorporation antipassive).

Equations

• Coon2019.triggersAj v implicitInternal = (Coon2019.hasImplicitExternal v || implicitInternal)

theorem Coon2019.ch_triggers_aj : hasImplicitExternal v_ch = true

-ch always triggers -aj (implicit external agent; p. 69).

theorem Coon2019.vØ_no_implicit : hasImplicitExternal vØ = false

Ø never has an implicit external (agent is overt ERG DP).

theorem Coon2019.v_w_no_implicit : hasImplicitExternal v_w = false

-w never has an implicit external (agent is overt ABS DP; p. 54).

theorem Coon2019.v_j_no_implicit : hasImplicitExternal v_j = false

-j has no implicit external (there is no agent at all, not even implicit; p. 70: "no thematic agent, implicit or otherwise").

theorem Coon2019.ch_aj_passive : triggersAj v_ch false = true

-ch-aj: passive of √TV with implicit agent (ex. (58), p. 66).

theorem Coon2019.w_aj_antipassive : triggersAj v_w true = true

-w-aj: absolutive antipassive (√TV theme is implicit; ex. (58), p. 66).

theorem Coon2019.w_incorporation_no_aj : triggersAj v_w false = false

-w incorporation antipassive: theme is overt bare NP → no -aj (ex. (58), p. 66; cf. (26b), p. 50).

theorem Coon2019.w_cross_class : Minimalist.isActivity (Minimalist.buildDecomposition v_w activityLower) = true ∧ Minimalist.buildDecomposition v_w positionalLower = [Minimalist.VerbHead.vDO, Minimalist.VerbHead.vBE] ∧ Minimalist.isActivity (Minimalist.buildDecomposition v_w activityLower) = true

-w serves the same structural function across three root classes: it merges directly with the root, verbalizes it, and introduces an agent without assigning ERG (p. 54–56). The only difference is the root's lower event structure.

theorem Coon2019.minimalist_division_of_labor : Minimalist.isCausative (Minimalist.buildDecomposition vØ resultLower) = true ∧ Minimalist.isInchoative (Minimalist.buildDecomposition v_j resultLower) = true ∧ Fragments.Chuj.rootTV_res.arity.hasInternalArg = true ∧ Fragments.Chuj.rootITV.arity.hasInternalArg = false

Division of labor (@cite{coon-2019}, ex. (2)/(77), p. 75): the root determines whether a theme is present; Voice determines whether an agent is present. Same root with different Voice → different event type; same Voice with different root → same external argument status.

theorem Coon2019.chuj_causative_alternation_result : (Minimalist.isCausative (Minimalist.buildDecomposition vØ resultLower) = true ↔ vØ.AssignsTheta) ∧ (Minimalist.isCausative (Minimalist.buildDecomposition v_w resultLower) = true ↔ v_w.AssignsTheta) ∧ (Minimalist.isCausative (Minimalist.buildDecomposition v_ch resultLower) = true ↔ v_ch.AssignsTheta) ∧ (Minimalist.isCausative (Minimalist.buildDecomposition v_j resultLower) = true ↔ v_j.AssignsTheta)

The causative alternation in Chuj is determined by Voice, not by the root (instantiation of voice_determines_causativity_go_be for Chuj heads). For result roots, causativity tracks exactly with θ-assignment.

def Coon2019.toFragmentRoot : Fragments.Chuj.CRootClass → RootClassification

Map the phenomena's root class to the fragment's RootClassification. This connects theory-neutral distributional classes to the theoretically analyzed RootClassification structure. √TV maps to rootTV_res as a representative — the choice between rootTV_res and rootTV_pc is arbitrary for arity (both are selectsTheme); only changeType differs.

Equations

• Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.tv = Fragments.Chuj.rootTV_res
• Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.itv = Fragments.Chuj.rootITV
• Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.pos = Fragments.Chuj.rootPOS
• Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.nom = Fragments.Chuj.rootNOM

theorem Coon2019.root_class_arity_alignment : (toFragmentRoot Fragments.Chuj.CRootClass.tv).arity = RootArity.selectsTheme ∧ (toFragmentRoot Fragments.Chuj.CRootClass.itv).arity = RootArity.noTheme ∧ (toFragmentRoot Fragments.Chuj.CRootClass.pos).arity = RootArity.noTheme ∧ (toFragmentRoot Fragments.Chuj.CRootClass.nom).arity = RootArity.noTheme

√TV maps to a theme-selecting root; all others map to non-theme roots. This is the formal content of the observation that only √TV forms bare transitive stems (§2.2).

theorem Coon2019.bare_transitive_iff_theme (rc : Fragments.Chuj.CRootClass) : Fragments.Chuj.formsBareTransitive rc = (toFragmentRoot rc).arity.hasInternalArg

The data's formsBareTransitive matches the fragment's hasInternalArg. Only roots that select a theme can form bare transitive stems.

def Coon2019.toVoiceHead : Fragments.Chuj.ChujVoiceSuffix → Minimalist.VoiceHead

Map the phenomena's voice suffix to the Minimalist VoiceHead.

Equations

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

theorem Coon2019.theta_alignment (vs : Fragments.Chuj.ChujVoiceSuffix) : vs.hasAgent = true ↔ (toVoiceHead vs).AssignsTheta

Theta assignment matches: the data's hasAgent agrees with the fragment's AssignsTheta for all four voice suffixes.

theorem Coon2019.d_feature_alignment : (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.null).hasD = true ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.w).hasD = true ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch).hasD = false ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j).hasD = false

External argument status matches D feature: overt external arg ↔ hasD = true.

theorem Coon2019.phase_head_alignment : (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.null).IsPhasal ∧ ¬(toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch).IsPhasal ∧ ¬(toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j).IsPhasal ∧ ¬(toVoiceHead Fragments.Chuj.ChujVoiceSuffix.w).IsPhasal

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

theorem Coon2019.agent_adverb_matches_theta (vs : Fragments.Chuj.ChujVoiceSuffix) : Fragments.Chuj.agentAdverbOK vs = true ↔ (toVoiceHead vs).AssignsTheta

The data's agent adverb diagnostic matches the fragment's theta assignment. Agent-oriented adverbs require a theta-role-bearing Voice head.

theorem Coon2019.passive_contrast : (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch).AssignsTheta ∧ Fragments.Chuj.agentAdverbOK Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ Fragments.Chuj.byPhraseOK Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ ¬(toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j).AssignsTheta ∧ Fragments.Chuj.agentAdverbOK Fragments.Chuj.ChujVoiceSuffix.j = false ∧ Fragments.Chuj.byPhraseOK Fragments.Chuj.ChujVoiceSuffix.j = false

The -ch vs -j contrast is the critical test: both are passives (no overt external arg), but they differ in theta assignment. The agent diagnostic data confirms the fragment's distinction.

theorem Coon2019.aj_passive_matches_implicit (vs : Fragments.Chuj.ChujVoiceSuffix) : Fragments.Chuj.ajOnPassive vs = hasImplicitExternal (toVoiceHead vs)

The data's -aj on passives matches the fragment's hasImplicitExternal. -aj appears when there is an implicit (but not absent) external argument.

theorem Coon2019.aj_full_distribution : triggersAj v_ch false = true ∧ Fragments.Chuj.ajOnPassive Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ triggersAj v_j false = false ∧ Fragments.Chuj.ajOnPassive Fragments.Chuj.ChujVoiceSuffix.j = false ∧ triggersAj v_w true = true ∧ Fragments.Chuj.ajOnAntipassive Fragments.Chuj.AntipassiveType.absolutive = true ∧ triggersAj v_w false = false ∧ Fragments.Chuj.ajOnAntipassive Fragments.Chuj.AntipassiveType.incorporation = false

The fragment's triggersAj predicts the data's full -aj distribution:

• -ch (implicit ext) → -aj
• -j (no ext) → no -aj
• -w absolutive (implicit int) → -aj
• -w incorporation (overt int) → no -aj

theorem Coon2019.event_decomposition_matches_data : Minimalist.isCausative (Minimalist.buildDecomposition vØ resultLower) = true ∧ Minimalist.isInchoative (Minimalist.buildDecomposition v_j resultLower) = true ∧ Minimalist.isCausative (Minimalist.buildDecomposition v_ch resultLower) = true ∧ Minimalist.isActivity (Minimalist.buildDecomposition v_w activityLower) = true

The fragment predicts correct event decompositions for each root×voice combination attested in the data.

√TV result + Ø → causative (active transitive) √TV result + -j → inchoative (agentless passive / anticausative) √TV result + -ch → causative (passive with implicit agent) √ITV + -w → activity (intransitive)

theorem Coon2019.division_of_labor_matches_data : Fragments.Chuj.formsBareTransitive Fragments.Chuj.CRootClass.tv = true ∧ Fragments.Chuj.rootTV_res.arity.hasInternalArg = true ∧ Fragments.Chuj.formsBareTransitive Fragments.Chuj.CRootClass.itv = false ∧ Fragments.Chuj.rootITV.arity.hasInternalArg = false ∧ Fragments.Chuj.ChujVoiceSuffix.null.extArgStatus = Fragments.Chuj.ExtArgStatus.overt_erg ∧ Fragments.Chuj.ChujVoiceSuffix.ch.extArgStatus = Fragments.Chuj.ExtArgStatus.implicit ∧ Fragments.Chuj.ChujVoiceSuffix.j.extArgStatus = Fragments.Chuj.ExtArgStatus.absent

The core empirical claim (ex. (2)/(77), p. 75): roots determine internal arguments, Voice determines external arguments.

The data confirms this in two ways:

1. Theme persistence: √TV always has an internal arg regardless of Voice
2. Voice determines agent: same root with Ø has overt agent, with -ch has implicit agent, with -j has no agent

theorem Coon2019.theme_persists_all_voices : Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.null = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.j = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.w = true ∧ Fragments.Chuj.rootTV_res.arity.hasInternalArg = true

Theme persistence across all four voice forms for √TV. The data shows √TV maintains its internal argument in active (Ø), passive (-ch), agentless passive (-j), and antipassive (-w). The fragment encodes this as a root property (arity), not a derived property — so it holds by construction.

theorem Coon2019.denotation_type_alignment : (toFragmentRoot Fragments.Chuj.CRootClass.tv).denotationType = some RootDenotationType.indivStatePred ∧ (toFragmentRoot Fragments.Chuj.CRootClass.itv).denotationType = some RootDenotationType.indivStatePred ∧ (toFragmentRoot Fragments.Chuj.CRootClass.pos).denotationType = some RootDenotationType.measureFn ∧ (toFragmentRoot Fragments.Chuj.CRootClass.nom).denotationType = some RootDenotationType.entityPred

The four root classes have distinct denotation types (@cite{coon-2019}, (3)). The fragment's denotationType field captures these: √TV/√ITV = indivStatePred ⟨e,⟨s,t⟩⟩, √POS = measureFn ⟨e,⟨s,d⟩⟩, √NOM = entityPred ⟨e,t⟩.

theorem Coon2019.tv_itv_same_type_different_arity : (toFragmentRoot Fragments.Chuj.CRootClass.tv).denotationType = (toFragmentRoot Fragments.Chuj.CRootClass.itv).denotationType ∧ (toFragmentRoot Fragments.Chuj.CRootClass.tv).arity ≠ (toFragmentRoot Fragments.Chuj.CRootClass.itv).arity

√TV and √ITV share semantic type (event predicate) but differ in arity. This is the formal content of the observation that both compose with an entity argument per @cite{davis-1997}, but only √TV projects a syntactic complement.

theorem Coon2019.w_verbalization_cross_class : Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.pos Fragments.Chuj.ChujVoiceSuffix.w = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.nom Fragments.Chuj.ChujVoiceSuffix.w = true ∧ Minimalist.buildDecomposition v_w positionalLower = [Minimalist.VerbHead.vDO, Minimalist.VerbHead.vBE] ∧ Minimalist.isActivity (Minimalist.buildDecomposition v_w activityLower) = true

The -w suffix cross-class generalization: -w verbalizes √POS and √NOM roots (data: both take -w), and the fragment predicts different event structures depending on the root's lower structure.