Chuj Verb Building Fragment @cite{coon-2019}

@cite{davis-1997}

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

Contents

1. Root classes (§§1–3): four abstract Root 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

RootArity 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 @cite{davis-1997}. But syntactically, only √TV projects a complement DP that persists across voice alternations; √ITV's entity argument becomes the subject. Our RootArity.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 Fragments.Chuj.rootTV_pc : Root

√TV root (PC): selects theme, no entailed change-of-state. Semantic type ⟨e, ⟨s,t⟩⟩ (@cite{coon-2019}, (3)). Examples: mak' "hit", tek' "kick".

Equations

• Fragments.Chuj.rootTV_pc = { arity := RootArity.selectsTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.eventPred }

def Fragments.Chuj.rootTV_res : Root

√TV root (result): selects theme, entails change-of-state. Semantic type ⟨e, ⟨s,t⟩⟩ (@cite{coon-2019}, (3)). Examples: jatz' "hit (breaking)", tzak' "wrap".

Equations

• Fragments.Chuj.rootTV_res = { arity := RootArity.selectsTheme, changeType := RootType.result, denotationType := some RootDenotationType.eventPred }

def Fragments.Chuj.rootITV : Root

√ITV root: semantic type ⟨e, ⟨s,t⟩⟩ (same as √TV per @cite{davis-1997}), 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

• Fragments.Chuj.rootITV = { arity := RootArity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.eventPred }

def Fragments.Chuj.rootPOS : Root

√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

• Fragments.Chuj.rootPOS = { arity := RootArity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.measureFn }

def Fragments.Chuj.rootNOM : Root

√NOM root: nominal base. Semantic type ⟨e,t⟩ — entity predicate with no event argument (@cite{coon-2019}, (3)). Examples: a' "water", ixim "corn", chanhal "dance".

Equations

• Fragments.Chuj.rootNOM = { arity := RootArity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.entityPred }

theorem Fragments.Chuj.four_way_classification : rootTV_res.arity = RootArity.selectsTheme ∧ rootTV_res.denotationType = some RootDenotationType.eventPred ∧ rootITV.arity = RootArity.noTheme ∧ rootITV.denotationType = some RootDenotationType.eventPred ∧ rootPOS.arity = RootArity.noTheme ∧ rootPOS.denotationType = some RootDenotationType.measureFn ∧ rootNOM.arity = RootArity.noTheme ∧ rootNOM.denotationType = some RootDenotationType.entityPred

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

theorem Fragments.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 Fragments.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

instance Fragments.Chuj.instDecidableEqCRootClass : DecidableEq CRootClass

Equations

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

instance Fragments.Chuj.instBEqCRootClass : BEq CRootClass

Equations

• Fragments.Chuj.instBEqCRootClass = { beq := Fragments.Chuj.instBEqCRootClass.beq }

def Fragments.Chuj.instBEqCRootClass.beq : CRootClass → CRootClass → Bool

Equations

• Fragments.Chuj.instBEqCRootClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Chuj.instReprCRootClass : Repr CRootClass

Equations

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

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

Equations

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

def Fragments.Chuj.rootToClass (r : Root) : CRootClass

Map an abstract Root 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 Fragments.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 Fragments.Chuj.ChujVoiceSuffix : Type

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

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

instance Fragments.Chuj.instDecidableEqChujVoiceSuffix : DecidableEq ChujVoiceSuffix

Equations

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

def Fragments.Chuj.instBEqChujVoiceSuffix.beq : ChujVoiceSuffix → ChujVoiceSuffix → Bool

Equations

• Fragments.Chuj.instBEqChujVoiceSuffix.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Chuj.instBEqChujVoiceSuffix : BEq ChujVoiceSuffix

Equations

• Fragments.Chuj.instBEqChujVoiceSuffix = { beq := Fragments.Chuj.instBEqChujVoiceSuffix.beq }

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

Equations

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

instance Fragments.Chuj.instReprChujVoiceSuffix : Repr ChujVoiceSuffix

Equations

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

def Fragments.Chuj.ChujVoiceSuffix.form : ChujVoiceSuffix → String

The morphological form of each suffix.

Equations

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

inductive Fragments.Chuj.ExtArgStatus : Type

Status of the external argument for each voice form.

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

instance Fragments.Chuj.instDecidableEqExtArgStatus : DecidableEq ExtArgStatus

Equations

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

def Fragments.Chuj.instBEqExtArgStatus.beq : ExtArgStatus → ExtArgStatus → Bool

Equations

• Fragments.Chuj.instBEqExtArgStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Chuj.instBEqExtArgStatus : BEq ExtArgStatus

Equations

• Fragments.Chuj.instBEqExtArgStatus = { beq := Fragments.Chuj.instBEqExtArgStatus.beq }

instance Fragments.Chuj.instReprExtArgStatus : Repr ExtArgStatus

Equations

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

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

Equations

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

def Fragments.Chuj.ChujVoiceSuffix.extArgStatus : ChujVoiceSuffix → ExtArgStatus

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

Equations

• 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
• Fragments.Chuj.ChujVoiceSuffix.w.extArgStatus = Fragments.Chuj.ExtArgStatus.overt_abs

def Fragments.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

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

def Fragments.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

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

def Fragments.Chuj.formsBareTransitive (rc : CRootClass) : Bool

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

Equations

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

inductive Fragments.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

instance Fragments.Chuj.instDecidableEqAntipassiveType : DecidableEq AntipassiveType

Equations

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

def Fragments.Chuj.instBEqAntipassiveType.beq : AntipassiveType → AntipassiveType → Bool

Equations

• Fragments.Chuj.instBEqAntipassiveType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Chuj.instBEqAntipassiveType : BEq AntipassiveType

Equations

• Fragments.Chuj.instBEqAntipassiveType = { beq := Fragments.Chuj.instBEqAntipassiveType.beq }

instance Fragments.Chuj.instReprAntipassiveType : Repr AntipassiveType

Equations

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

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

Equations

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

def Fragments.Chuj.ajOnPassive (vs : ChujVoiceSuffix) : Bool

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

Equations

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

def Fragments.Chuj.ajOnAntipassive (apt : AntipassiveType) : Bool

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

Equations

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

def Fragments.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

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

def Fragments.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

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

def Fragments.Chuj.chujVoiceSystem : Interfaces.VoiceSystemProfile

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.

Equations

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

theorem Fragments.Chuj.chuj_voice_system_asymmetrical : chujVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.asymmetrical

theorem Fragments.Chuj.chuj_voice_count : chujVoiceSystem.voiceCount = 4

theorem Fragments.Chuj.chuj_not_simple_active_passive : chujVoiceSystem.isActivePassive = false

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

theorem Fragments.Chuj.chuj_no_oblique_pivots : chujVoiceSystem.distinguishesObliques = false

structure Fragments.Chuj.ChujRoot : Type

A Chuj root entry from the paper's lexicon.

• form : String

  Chuj root form

• gloss : String

  English gloss

• root : Root

  Abstract root class

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

Equations

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

instance Fragments.Chuj.instReprChujRoot : Repr ChujRoot

Equations

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

instance Fragments.Chuj.instBEqChujRoot : BEq ChujRoot

Equations

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

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

Equations

• Fragments.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))
• Fragments.Chuj.instBEqChujRoot.beq x✝¹ x✝ = false

def Fragments.Chuj.xik : ChujRoot

Equations

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

def Fragments.Chuj.chonh : ChujRoot

Equations

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

def Fragments.Chuj.jax : ChujRoot

Equations

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

def Fragments.Chuj.chel : ChujRoot

Equations

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

def Fragments.Chuj.tek' : ChujRoot

Equations

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

def Fragments.Chuj.mak' : ChujRoot

Equations

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

def Fragments.Chuj.il : ChujRoot

Equations

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

def Fragments.Chuj.ch'ak : ChujRoot

Equations

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

def Fragments.Chuj.b'o' : ChujRoot

Equations

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

def Fragments.Chuj.man : ChujRoot

Equations

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

def Fragments.Chuj.b'at : ChujRoot

Equations

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

def Fragments.Chuj.way : ChujRoot

Equations

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

def Fragments.Chuj.k'ey : ChujRoot

Equations

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

def Fragments.Chuj.jaw : ChujRoot

Equations

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

def Fragments.Chuj.ok' : ChujRoot

Equations

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

def Fragments.Chuj.chot : ChujRoot

Equations

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

def Fragments.Chuj.jenh : ChujRoot

Equations

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

def Fragments.Chuj.lich' : ChujRoot

Equations

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

def Fragments.Chuj.b'ul : ChujRoot

Equations

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

def Fragments.Chuj.kot : ChujRoot

Equations

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

def Fragments.Chuj.tel : ChujRoot

Equations

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

def Fragments.Chuj.pat : ChujRoot

Equations

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

def Fragments.Chuj.k'atzitz : ChujRoot

Equations

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

def Fragments.Chuj.ixim : ChujRoot

Equations

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

def Fragments.Chuj.winak : ChujRoot

Equations

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

def Fragments.Chuj.chanhal : ChujRoot

Equations

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

def Fragments.Chuj.at'is : ChujRoot

Equations

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

def Fragments.Chuj.tz'ib' : ChujRoot

Equations

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

def Fragments.Chuj.tvRoots : List ChujRoot

All √TV roots from Table (5).

Equations

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

def Fragments.Chuj.itvRoots : List ChujRoot

All √ITV roots from Table (5).

Equations

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

def Fragments.Chuj.posRoots : List ChujRoot

All √POS roots from Table (5).

Equations

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

def Fragments.Chuj.nomRoots : List ChujRoot

All √NOM roots from Table (5).

Equations

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

theorem Fragments.Chuj.tvRoots_selectTheme : (tvRoots.all fun (x : ChujRoot) => x.root.arity == RootArity.selectsTheme) = true

theorem Fragments.Chuj.itvRoots_noTheme : (itvRoots.all fun (x : ChujRoot) => x.root.arity == RootArity.noTheme) = true

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

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

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

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

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

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

theorem Fragments.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 Fragments.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 Fragments.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 Fragments.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 Fragments.Chuj.only_tv_transitive : formsBareTransitive CRootClass.tv = true ∧ formsBareTransitive CRootClass.itv = false ∧ formsBareTransitive CRootClass.pos = false ∧ formsBareTransitive CRootClass.nom = false

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

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

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

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