Chuj Verb Building Fragment [Coo19]

[Dav97]

Theory-neutral fragment for Chuj (Q'anjob'alan, Mayan), encoding root classification, voice morphology, paradigm grammaticality, and lexical inventory from [Coo19] "Building verbs in Chuj: Consequences for the nature of roots."

Contents

1. Root classes (§§1–3): four abstract RootClassification types (√TV, √ITV, √POS, √NOM) with distributional CRootClass enum and bridge function.
2. Voice suffixes (§§4–5): ChujVoiceSuffix (Ø, -ch, -j, -w) with external argument status, thematic properties, and morphological forms.
3. Paradigm grammaticality (§6): which root×voice combinations are grammatical, and which roots form bare transitive stems.
4. -aj distribution (§7): existential closure suffix distribution across voice forms and antipassive subtypes.
5. Agent diagnostics (§8): agent-oriented adverb and by-phrase tests distinguishing -ch (implicit agent) from -j (no agent).
6. Voice system profile (§9): four-way asymmetrical voice system.
7. Root lexicon (§10): ChujRoot entries from Table (5) and additional examples in the paper.
8. Verification theorems (§11): paradigm, -aj, agent diagnostic, and root classification checks.

Modeling Notes

Root.Arity captures complement projection, not semantic type. Coon's semantic types (3) group {√TV, √ITV} together as ⟨e, ⟨s,t⟩⟩ — both compose with an entity argument per [Dav97]. But syntactically, only √TV projects a complement DP that persists across voice alternations; √ITV's entity argument becomes the subject. Our Root.Arity.selectsTheme captures the syntactic complement projection, giving {√TV} vs {√ITV, √POS, √NOM}. This matches the -aj diagnostic: -aj marks implicit arguments, and only √TV stems show -aj (the theme can be implicit), not √ITV.

def Chuj.rootTV_pc : RootClassification

√TV root (PC): selects theme, no entailed change-of-state. Semantic type ⟨e, ⟨s,t⟩⟩ ([Coo19], (3)). Examples: mak' "hit", tek' "kick".

Equations

• Chuj.rootTV_pc = { arity := Verb.Root.Arity.selectsTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.indivStatePred }

def Chuj.rootTV_res : RootClassification

√TV root (result): selects theme, entails change-of-state. Semantic type ⟨e, ⟨s,t⟩⟩ ([Coo19], (3)). Examples: jatz' "hit (breaking)", tzak' "wrap".

Equations

• Chuj.rootTV_res = { arity := Verb.Root.Arity.selectsTheme, changeType := RootType.result, denotationType := some RootDenotationType.indivStatePred }

def Chuj.rootITV : RootClassification

√ITV root: semantic type ⟨e, ⟨s,t⟩⟩ (same as √TV per [Dav97]), but does NOT project a complement — the entity argument becomes the subject. The class is morphologically defined: roots that appear with null v/Voice⁰ in intransitive stems (p. 40). Examples: way "sleep", ok' "cry", jaw "arrive", b'at "go".

Equations

• Chuj.rootITV = { arity := Verb.Root.Arity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.indivStatePred }

def Chuj.rootPOS : RootClassification

√POS root: positional/stative. Semantic type ⟨e, ⟨s,d⟩⟩ — a measure function, not a truth-value predicate. Examples: chot "sit", kot "on all fours", watz "lie face down".

Equations

• Chuj.rootPOS = { arity := Verb.Root.Arity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.measureFn }

def Chuj.rootNOM : RootClassification

√NOM root: nominal base. Semantic type ⟨e,t⟩ — entity predicate with no event argument ([Coo19], (3)). Examples: a' "water", ixim "corn", chanhal "dance".

Equations

• Chuj.rootNOM = { arity := Verb.Root.Arity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.entityPred }

theorem Chuj.four_way_classification : rootTV_res.arity = Verb.Root.Arity.selectsTheme ∧ rootTV_res.denotationType = some RootDenotationType.indivStatePred ∧ rootITV.arity = Verb.Root.Arity.noTheme ∧ rootITV.denotationType = some RootDenotationType.indivStatePred ∧ rootPOS.arity = Verb.Root.Arity.noTheme ∧ rootPOS.denotationType = some RootDenotationType.measureFn ∧ rootNOM.arity = Verb.Root.Arity.noTheme ∧ rootNOM.denotationType = some RootDenotationType.entityPred

Coon's four root classes are recovered as (arity × denotationType) pairs. √TV = selectsTheme + indivStatePred, √ITV = noTheme + indivStatePred, √POS = noTheme + measureFn, √NOM = noTheme + entityPred.

theorem Chuj.root_classes_pairwise_distinct : rootTV_res.arity ≠ rootITV.arity ∧ rootITV.denotationType ≠ rootPOS.denotationType ∧ rootITV.denotationType ≠ rootNOM.denotationType ∧ rootPOS.denotationType ≠ rootNOM.denotationType

The four root classes are pairwise distinguishable: no two share both arity and denotationType.

inductive Chuj.CRootClass : Type

The four morphosyntactic root classes in Chuj, identified by surface distribution (which suffixes they combine with, whether they form bare transitive stems). Labels follow Coon's notation.

• tv : CRootClass
• itv : CRootClass
• pos : CRootClass
• nom : CRootClass

@[implicit_reducible]

instance Chuj.instDecidableEqCRootClass : DecidableEq CRootClass

Equations

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

def Chuj.instReprCRootClass.repr : CRootClass → ℕ → Std.Format

Equations

• Chuj.instReprCRootClass.repr Chuj.CRootClass.tv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.CRootClass.tv")).group prec✝
• Chuj.instReprCRootClass.repr Chuj.CRootClass.itv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.CRootClass.itv")).group prec✝
• Chuj.instReprCRootClass.repr Chuj.CRootClass.pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.CRootClass.pos")).group prec✝
• Chuj.instReprCRootClass.repr Chuj.CRootClass.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.CRootClass.nom")).group prec✝

@[implicit_reducible]

instance Chuj.instReprCRootClass : Repr CRootClass

Equations

• Chuj.instReprCRootClass = { reprPrec := Chuj.instReprCRootClass.repr }

def Chuj.rootToClass (r : RootClassification) : CRootClass

Map an abstract RootClassification to the distributional CRootClass. The bridge is determined by (arity × denotationType).

Equations

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

theorem Chuj.rootToClass_correct : rootToClass rootTV_pc = CRootClass.tv ∧ rootToClass rootTV_res = CRootClass.tv ∧ rootToClass rootITV = CRootClass.itv ∧ rootToClass rootPOS = CRootClass.pos ∧ rootToClass rootNOM = CRootClass.nom

The bridge is correct for each abstract root definition.

inductive Chuj.ChujVoiceSuffix : Type

The four voice suffixes in Chuj (ex. (78), pp. 75–76).

• null : ChujVoiceSuffix
• ch : ChujVoiceSuffix
• j : ChujVoiceSuffix
• w : ChujVoiceSuffix

@[implicit_reducible]

instance Chuj.instDecidableEqChujVoiceSuffix : DecidableEq ChujVoiceSuffix

Equations

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

@[implicit_reducible]

instance Chuj.instReprChujVoiceSuffix : Repr ChujVoiceSuffix

Equations

• Chuj.instReprChujVoiceSuffix = { reprPrec := Chuj.instReprChujVoiceSuffix.repr }

def Chuj.instReprChujVoiceSuffix.repr : ChujVoiceSuffix → ℕ → Std.Format

Equations

• Chuj.instReprChujVoiceSuffix.repr Chuj.ChujVoiceSuffix.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ChujVoiceSuffix.null")).group prec✝
• Chuj.instReprChujVoiceSuffix.repr Chuj.ChujVoiceSuffix.ch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ChujVoiceSuffix.ch")).group prec✝
• Chuj.instReprChujVoiceSuffix.repr Chuj.ChujVoiceSuffix.j prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ChujVoiceSuffix.j")).group prec✝
• Chuj.instReprChujVoiceSuffix.repr Chuj.ChujVoiceSuffix.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ChujVoiceSuffix.w")).group prec✝

def Chuj.ChujVoiceSuffix.form : ChujVoiceSuffix → String

The morphological form of each suffix.

Equations

• Chuj.ChujVoiceSuffix.null.form = "Ø"
• Chuj.ChujVoiceSuffix.ch.form = "-ch"
• Chuj.ChujVoiceSuffix.j.form = "-j"
• Chuj.ChujVoiceSuffix.w.form = "-w"

inductive Chuj.ExtArgStatus : Type

Status of the external argument for each voice form.

• overt_erg : ExtArgStatus
• overt_abs : ExtArgStatus
• implicit : ExtArgStatus
• absent : ExtArgStatus

@[implicit_reducible]

instance Chuj.instDecidableEqExtArgStatus : DecidableEq ExtArgStatus

Equations

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

@[implicit_reducible]

instance Chuj.instReprExtArgStatus : Repr ExtArgStatus

Equations

• Chuj.instReprExtArgStatus = { reprPrec := Chuj.instReprExtArgStatus.repr }

def Chuj.instReprExtArgStatus.repr : ExtArgStatus → ℕ → Std.Format

Equations

• Chuj.instReprExtArgStatus.repr Chuj.ExtArgStatus.overt_erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ExtArgStatus.overt_erg")).group prec✝
• Chuj.instReprExtArgStatus.repr Chuj.ExtArgStatus.overt_abs prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ExtArgStatus.overt_abs")).group prec✝
• Chuj.instReprExtArgStatus.repr Chuj.ExtArgStatus.implicit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ExtArgStatus.implicit")).group prec✝
• Chuj.instReprExtArgStatus.repr Chuj.ExtArgStatus.absent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Chuj.ExtArgStatus.absent")).group prec✝

def Chuj.ChujVoiceSuffix.extArgStatus : ChujVoiceSuffix → ExtArgStatus

External argument status for each voice suffix (ex. (78)).

Equations

• Chuj.ChujVoiceSuffix.null.extArgStatus = Chuj.ExtArgStatus.overt_erg
• Chuj.ChujVoiceSuffix.ch.extArgStatus = Chuj.ExtArgStatus.implicit
• Chuj.ChujVoiceSuffix.j.extArgStatus = Chuj.ExtArgStatus.absent
• Chuj.ChujVoiceSuffix.w.extArgStatus = Chuj.ExtArgStatus.overt_abs

def Chuj.ChujVoiceSuffix.hasAgent : ChujVoiceSuffix → Bool

Whether the voice suffix assigns a thematic role to an external argument (observed via agent-oriented adverb diagnostics, §4.1–4.2).

Equations

• Chuj.ChujVoiceSuffix.null.hasAgent = true
• Chuj.ChujVoiceSuffix.ch.hasAgent = true
• Chuj.ChujVoiceSuffix.j.hasAgent = false
• Chuj.ChujVoiceSuffix.w.hasAgent = true

def Chuj.isGrammatical (rc : CRootClass) (vs : ChujVoiceSuffix) : Bool

Whether a root class can combine with a voice suffix to form a grammatical verb stem.

Based on the distributional facts in §§2–5:

• √TV: all four voices (Ø, -ch, -j, -w) — ex. (78)
• √ITV: null v only (§2.1, p. 40)
• √POS: -w only (§2.4, p. 43)
• √NOM: -w only (§3.1, p. 46)

Equations

• Chuj.isGrammatical Chuj.CRootClass.tv vs = true
• Chuj.isGrammatical Chuj.CRootClass.itv Chuj.ChujVoiceSuffix.null = true
• Chuj.isGrammatical Chuj.CRootClass.pos Chuj.ChujVoiceSuffix.w = true
• Chuj.isGrammatical Chuj.CRootClass.nom Chuj.ChujVoiceSuffix.w = true
• Chuj.isGrammatical rc vs = false

def Chuj.formsBareTransitive (rc : CRootClass) : Bool

√TV is the only class that forms bare transitive stems (§2.2, p. 41).

Equations

• Chuj.formsBareTransitive Chuj.CRootClass.tv = true
• Chuj.formsBareTransitive rc = false

inductive Chuj.AntipassiveType : Type

Whether -aj (existential closure) appears on a √TV stem in each voice form (ex. (78), pp. 75–76; §4.2, p. 72).

-aj marks the presence of an implicit argument:

• Ø: no implicit arg → no -aj
• -ch: implicit external arg → -aj on stem (§4.1.1, p. 68)
• -j: no external arg at all → no -aj
• -w (absolutive): implicit internal arg → -aj (ex. (55c), p. 65)
• -w (incorporation): overt bare NP internal arg → no -aj (ex. (54a), p. 64)

• absolutive : AntipassiveType
• incorporation : AntipassiveType

@[implicit_reducible]

instance Chuj.instDecidableEqAntipassiveType : DecidableEq AntipassiveType

Equations

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

@[implicit_reducible]

instance Chuj.instReprAntipassiveType : Repr AntipassiveType

Equations

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

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

Equations

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

def Chuj.ajOnPassive (vs : ChujVoiceSuffix) : Bool

-aj on √TV stems in passive/agentless contexts.

Equations

• Chuj.ajOnPassive Chuj.ChujVoiceSuffix.null = false
• Chuj.ajOnPassive Chuj.ChujVoiceSuffix.ch = true
• Chuj.ajOnPassive Chuj.ChujVoiceSuffix.j = false
• Chuj.ajOnPassive Chuj.ChujVoiceSuffix.w = false

def Chuj.ajOnAntipassive (apt : AntipassiveType) : Bool

-aj on √TV stems in antipassive (-w) contexts.

Equations

• Chuj.ajOnAntipassive Chuj.AntipassiveType.absolutive = true
• Chuj.ajOnAntipassive Chuj.AntipassiveType.incorporation = false

def Chuj.agentAdverbOK (vs : ChujVoiceSuffix) : Bool

Agent-oriented adverb test (§4.1.1–4.1.2). "on purpose" adverbs are grammatical with -chaj but not -j.

(63a) on purpose ... ix-ch'ak-chaj te' te'. 'The tree was felled on purpose.' ✓ (p. 68)

(67a) *on purpose ... ix-ch'ak-j-i te' te'. intended: 'The tree was felled on purpose.' ✗ (p. 70)

Equations

• Chuj.agentAdverbOK Chuj.ChujVoiceSuffix.null = true
• Chuj.agentAdverbOK Chuj.ChujVoiceSuffix.ch = true
• Chuj.agentAdverbOK Chuj.ChujVoiceSuffix.j = false
• Chuj.agentAdverbOK Chuj.ChujVoiceSuffix.w = true

def Chuj.byPhraseOK (vs : ChujVoiceSuffix) : Bool

By-phrase test (§4.1.1–4.1.2). Oblique agents ("yuj" DPs) are grammatical with -chaj but not -j.

(62) ... yuj ... 'by them' ✓ with -chaj (p. 68) (65–66) -uj phrases with -j are causal, not agentive (pp. 69–70)

Equations

• Chuj.byPhraseOK Chuj.ChujVoiceSuffix.null = false
• Chuj.byPhraseOK Chuj.ChujVoiceSuffix.ch = true
• Chuj.byPhraseOK Chuj.ChujVoiceSuffix.j = false
• Chuj.byPhraseOK Chuj.ChujVoiceSuffix.w = false

Chuj voice system

Four-way asymmetrical (Ø, -w, -ch, -j). Unlike pivot systems
(Toba Batak, Tagalog), Chuj voices don't promote arguments to a
privileged position. Instead, Voice controls whether an external
argument is overt, implicit, or absent. Each voice form is built
independently from root + v/Voice⁰: passive is not derived from
active. Non-pivot system; Voice controls EA status (Coon 2019). 

def Chuj.VoiceSystem.voices : List Voice.VoiceEntry

Equations

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

def Chuj.VoiceSystem.symmetry : Voice.VoiceSystemSymmetry

Equations

• Chuj.VoiceSystem.symmetry = Voice.VoiceSystemSymmetry.asymmetrical

theorem Chuj.chuj_voice_system_asymmetrical : VoiceSystem.symmetry = Voice.VoiceSystemSymmetry.asymmetrical

theorem Chuj.chuj_voice_count : Voice.voiceCount VoiceSystem.voices = 4

theorem Chuj.chuj_not_simple_active_passive : ¬Voice.isActivePassive VoiceSystem.voices

Chuj is NOT a simple active/passive: it has 4 voices, not 2.

theorem Chuj.chuj_no_oblique_pivots : ¬Voice.distinguishesObliques VoiceSystem.voices

structure Chuj.ChujRoot : Type

A Chuj root entry from the paper's lexicon.

• form : String

  Chuj root form

• gloss : String

  English gloss

• root : RootClassification

  Abstract root class

@[implicit_reducible]

instance Chuj.instReprChujRoot : Repr ChujRoot

Equations

• Chuj.instReprChujRoot = { reprPrec := Chuj.instReprChujRoot.repr }

def Chuj.instReprChujRoot.repr : ChujRoot → ℕ → Std.Format

Equations

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

def Chuj.instBEqChujRoot.beq : ChujRoot → ChujRoot → Bool

Equations

• Chuj.instBEqChujRoot.beq { form := a, gloss := a_1, root := a_2 } { form := b, gloss := b_1, root := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Chuj.instBEqChujRoot.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Chuj.instBEqChujRoot : BEq ChujRoot

Equations

• Chuj.instBEqChujRoot = { beq := Chuj.instBEqChujRoot.beq }

def Chuj.xik : ChujRoot

Equations

• Chuj.xik = { form := "xik", gloss := "chop", root := Chuj.rootTV_pc }

def Chuj.chonh : ChujRoot

Equations

• Chuj.chonh = { form := "chonh", gloss := "sell", root := Chuj.rootTV_pc }

def Chuj.jax : ChujRoot

Equations

• Chuj.jax = { form := "jax", gloss := "grind", root := Chuj.rootTV_pc }

def Chuj.chel : ChujRoot

Equations

• Chuj.chel = { form := "chel", gloss := "hug", root := Chuj.rootTV_pc }

def Chuj.tek' : ChujRoot

Equations

• Chuj.tek' = { form := "tek'", gloss := "kick", root := Chuj.rootTV_pc }

def Chuj.mak' : ChujRoot

Equations

• Chuj.mak' = { form := "mak'", gloss := "hit", root := Chuj.rootTV_pc }

def Chuj.il : ChujRoot

Equations

• Chuj.il = { form := "il", gloss := "see", root := Chuj.rootTV_pc }

def Chuj.ch'ak : ChujRoot

Equations

• Chuj.ch'ak = { form := "ch'ak", gloss := "fell", root := Chuj.rootTV_pc }

def Chuj.b'o' : ChujRoot

Equations

• Chuj.b'o' = { form := "b'o'", gloss := "make", root := Chuj.rootTV_pc }

def Chuj.man : ChujRoot

Equations

• Chuj.man = { form := "man", gloss := "buy", root := Chuj.rootTV_pc }

def Chuj.b'at : ChujRoot

Equations

• Chuj.b'at = { form := "b'at", gloss := "go", root := Chuj.rootITV }

def Chuj.way : ChujRoot

Equations

• Chuj.way = { form := "way", gloss := "sleep", root := Chuj.rootITV }

def Chuj.k'ey : ChujRoot

Equations

• Chuj.k'ey = { form := "k'ey", gloss := "ascend", root := Chuj.rootITV }

def Chuj.jaw : ChujRoot

Equations

• Chuj.jaw = { form := "jaw", gloss := "arrive", root := Chuj.rootITV }

def Chuj.ok' : ChujRoot

Equations

• Chuj.ok' = { form := "ok'", gloss := "cry", root := Chuj.rootITV }

def Chuj.chot : ChujRoot

Equations

• Chuj.chot = { form := "chot", gloss := "crouched", root := Chuj.rootPOS }

def Chuj.jenh : ChujRoot

Equations

• Chuj.jenh = { form := "jenh", gloss := "outstretched", root := Chuj.rootPOS }

def Chuj.lich' : ChujRoot

Equations

• Chuj.lich' = { form := "lich'", gloss := "leaning", root := Chuj.rootPOS }

def Chuj.b'ul : ChujRoot

Equations

• Chuj.b'ul = { form := "b'ul", gloss := "gathered", root := Chuj.rootPOS }

def Chuj.kot : ChujRoot

Equations

• Chuj.kot = { form := "kot", gloss := "on four legs", root := Chuj.rootPOS }

def Chuj.tel : ChujRoot

Equations

• Chuj.tel = { form := "tel", gloss := "lying down", root := Chuj.rootPOS }

def Chuj.pat : ChujRoot

Equations

• Chuj.pat = { form := "pat", gloss := "house", root := Chuj.rootNOM }

def Chuj.k'atzitz : ChujRoot

Equations

• Chuj.k'atzitz = { form := "k'atzitz", gloss := "wood", root := Chuj.rootNOM }

def Chuj.ixim : ChujRoot

Equations

• Chuj.ixim = { form := "ixim", gloss := "corn", root := Chuj.rootNOM }

def Chuj.winak : ChujRoot

Equations

• Chuj.winak = { form := "winak", gloss := "man", root := Chuj.rootNOM }

def Chuj.chanhal : ChujRoot

Equations

• Chuj.chanhal = { form := "chanhal", gloss := "dance", root := Chuj.rootNOM }

def Chuj.at'is : ChujRoot

Equations

• Chuj.at'is = { form := "at'is", gloss := "sneeze", root := Chuj.rootNOM }

def Chuj.tz'ib' : ChujRoot

Equations

• Chuj.tz'ib' = { form := "tz'ib'", gloss := "writing", root := Chuj.rootNOM }

def Chuj.tvRoots : List ChujRoot

All √TV roots from Table (5).

Equations

• Chuj.tvRoots = [Chuj.xik, Chuj.chonh, Chuj.jax, Chuj.chel, Chuj.tek']

def Chuj.itvRoots : List ChujRoot

All √ITV roots from Table (5).

Equations

• Chuj.itvRoots = [Chuj.b'at, Chuj.way, Chuj.k'ey, Chuj.jaw, Chuj.ok']

def Chuj.posRoots : List ChujRoot

All √POS roots from Table (5).

Equations

• Chuj.posRoots = [Chuj.chot, Chuj.jenh, Chuj.lich', Chuj.b'ul]

def Chuj.nomRoots : List ChujRoot

All √NOM roots from Table (5).

Equations

• Chuj.nomRoots = [Chuj.pat, Chuj.k'atzitz, Chuj.ixim, Chuj.winak, Chuj.chanhal]

theorem Chuj.tvRoots_selectTheme : (tvRoots.all fun (x : ChujRoot) => x.root.arity == Verb.Root.Arity.selectsTheme) = true

theorem Chuj.itvRoots_noTheme : (itvRoots.all fun (x : ChujRoot) => x.root.arity == Verb.Root.Arity.noTheme) = true

theorem Chuj.posRoots_measureFn : (posRoots.all fun (x : ChujRoot) => x.root.denotationType == some RootDenotationType.measureFn) = true

theorem Chuj.nomRoots_entityPred : (nomRoots.all fun (x : ChujRoot) => x.root.denotationType == some RootDenotationType.entityPred) = true

theorem Chuj.tvRoots_bridge : (tvRoots.all fun (r : ChujRoot) => rootToClass r.root == CRootClass.tv) = true

theorem Chuj.itvRoots_bridge : (itvRoots.all fun (r : ChujRoot) => rootToClass r.root == CRootClass.itv) = true

theorem Chuj.posRoots_bridge : (posRoots.all fun (r : ChujRoot) => rootToClass r.root == CRootClass.pos) = true

theorem Chuj.nomRoots_bridge : (nomRoots.all fun (r : ChujRoot) => rootToClass r.root == CRootClass.nom) = true

theorem Chuj.tv_all_voices : isGrammatical CRootClass.tv ChujVoiceSuffix.null = true ∧ isGrammatical CRootClass.tv ChujVoiceSuffix.ch = true ∧ isGrammatical CRootClass.tv ChujVoiceSuffix.j = true ∧ isGrammatical CRootClass.tv ChujVoiceSuffix.w = true

theorem Chuj.itv_only_null : isGrammatical CRootClass.itv ChujVoiceSuffix.null = true ∧ isGrammatical CRootClass.itv ChujVoiceSuffix.ch = false ∧ isGrammatical CRootClass.itv ChujVoiceSuffix.j = false ∧ isGrammatical CRootClass.itv ChujVoiceSuffix.w = false

theorem Chuj.pos_only_w : isGrammatical CRootClass.pos ChujVoiceSuffix.null = false ∧ isGrammatical CRootClass.pos ChujVoiceSuffix.ch = false ∧ isGrammatical CRootClass.pos ChujVoiceSuffix.j = false ∧ isGrammatical CRootClass.pos ChujVoiceSuffix.w = true

theorem Chuj.nom_only_w : isGrammatical CRootClass.nom ChujVoiceSuffix.null = false ∧ isGrammatical CRootClass.nom ChujVoiceSuffix.ch = false ∧ isGrammatical CRootClass.nom ChujVoiceSuffix.j = false ∧ isGrammatical CRootClass.nom ChujVoiceSuffix.w = true

theorem Chuj.only_tv_transitive : formsBareTransitive CRootClass.tv = true ∧ formsBareTransitive CRootClass.itv = false ∧ formsBareTransitive CRootClass.pos = false ∧ formsBareTransitive CRootClass.nom = false

theorem Chuj.ch_has_agent_j_does_not : ChujVoiceSuffix.ch.hasAgent = true ∧ ChujVoiceSuffix.j.hasAgent = false

theorem Chuj.agent_adverb_distinguishes : agentAdverbOK ChujVoiceSuffix.ch = true ∧ agentAdverbOK ChujVoiceSuffix.j = false

theorem Chuj.by_phrase_distinguishes : byPhraseOK ChujVoiceSuffix.ch = true ∧ byPhraseOK ChujVoiceSuffix.j = false

theorem Chuj.aj_tracks_implicit : ajOnPassive ChujVoiceSuffix.ch = true ∧ ajOnPassive ChujVoiceSuffix.j = false ∧ ajOnAntipassive AntipassiveType.absolutive = true ∧ ajOnAntipassive AntipassiveType.incorporation = false