Chuj Root Classes

Root lexicon for Chuj (Q'anjob'alan, Mayan): the four Mayanist root classes and the root inventory of [Coo19] "Building verbs in Chuj: Consequences for the nature of roots."

Main declarations

• Chuj.RootClass: the four morphosyntactic root classes (√TV, √ITV, √POS, √NOM), identified by surface distribution.
• Chuj.ChujRoot: a root entry — form, gloss, and class label.
• Chuj.allRoots and the per-class lists tvRoots, itvRoots, posRoots, nomRoots, derived by filtering on the class label.

Implementation notes

The entry carries only the distributional class label; the theoretical coordinates ([Coo19]'s Classification values — semantic type, valency, transitive-Voice licensing) are a derived projection RootClass.toClassification in Studies/Coon2019.lean, following the derived-projection pattern of Studies/HaninkKoontzGarboden2025.lean.

inductive Chuj.RootClass : 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 [Coo19].

• tv : RootClass

  Transitive roots: form bare transitive stems.

• itv : RootClass

  Intransitive roots: take null v in intransitive stems.

• pos : RootClass

  Positional roots: require -w for verbalization.

• nom : RootClass

  Nominal roots: require -w for verbalization.

@[instance_reducible]

instance Chuj.instDecidableEqRootClass : DecidableEq RootClass

Equations

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

def Chuj.instReprRootClass.repr : RootClass → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Chuj.instReprRootClass : Repr RootClass

Equations

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

structure Chuj.ChujRoot : Type

A Chuj root entry from [Coo19]'s lexicon.

• form : String

  Chuj root form

• gloss : String

  English gloss

• class' : RootClass

  Morphosyntactic root class

@[instance_reducible]

instance Chuj.instReprChujRoot : Repr ChujRoot

Equations

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

def Chuj.instReprChujRoot.repr : ChujRoot → Nat → 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, class' := a_2 } { form := b, gloss := b_1, class' := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Chuj.instBEqChujRoot.beq x✝¹ x✝ = false

@[instance_reducible]

instance Chuj.instBEqChujRoot : BEq ChujRoot

Equations

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

@[instance_reducible]

instance Chuj.instDecidableEqChujRoot : DecidableEq ChujRoot

Equations

• Chuj.instDecidableEqChujRoot = Chuj.instDecidableEqChujRoot.decEq

def Chuj.instDecidableEqChujRoot.decEq (x✝ x✝¹ : ChujRoot) : Decidable (x✝ = x✝¹)

Equations

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

√TV roots (Table (5), p. 39)

def Chuj.xik : ChujRoot

Equations

• Chuj.xik = { form := "xik", gloss := "chop", class' := Chuj.RootClass.tv }

def Chuj.chonh : ChujRoot

Equations

• Chuj.chonh = { form := "chonh", gloss := "sell", class' := Chuj.RootClass.tv }

def Chuj.jax : ChujRoot

Equations

• Chuj.jax = { form := "jax", gloss := "grind", class' := Chuj.RootClass.tv }

def Chuj.chel : ChujRoot

Equations

• Chuj.chel = { form := "chel", gloss := "hug", class' := Chuj.RootClass.tv }

def Chuj.tek' : ChujRoot

Equations

• Chuj.tek' = { form := "tek'", gloss := "kick", class' := Chuj.RootClass.tv }

√TV roots from examples (not in Table (5))

def Chuj.mak' : ChujRoot

Equations

• Chuj.mak' = { form := "mak'", gloss := "hit", class' := Chuj.RootClass.tv }

def Chuj.il : ChujRoot

Equations

• Chuj.il = { form := "il", gloss := "see", class' := Chuj.RootClass.tv }

def Chuj.ch'ak : ChujRoot

Equations

• Chuj.ch'ak = { form := "ch'ak", gloss := "fell", class' := Chuj.RootClass.tv }

def Chuj.b'o' : ChujRoot

Equations

• Chuj.b'o' = { form := "b'o'", gloss := "make", class' := Chuj.RootClass.tv }

def Chuj.man : ChujRoot

Equations

• Chuj.man = { form := "man", gloss := "buy", class' := Chuj.RootClass.tv }

√ITV roots (Table (5), p. 39)

def Chuj.b'at : ChujRoot

Equations

• Chuj.b'at = { form := "b'at", gloss := "go", class' := Chuj.RootClass.itv }

def Chuj.way : ChujRoot

Equations

• Chuj.way = { form := "way", gloss := "sleep", class' := Chuj.RootClass.itv }

def Chuj.k'ey : ChujRoot

Equations

• Chuj.k'ey = { form := "k'ey", gloss := "ascend", class' := Chuj.RootClass.itv }

def Chuj.jaw : ChujRoot

Equations

• Chuj.jaw = { form := "jaw", gloss := "arrive", class' := Chuj.RootClass.itv }

def Chuj.ok' : ChujRoot

Equations

• Chuj.ok' = { form := "ok'", gloss := "cry", class' := Chuj.RootClass.itv }

√POS roots (Table (5), p. 39; Table (20), p. 47)

def Chuj.chot : ChujRoot

Equations

• Chuj.chot = { form := "chot", gloss := "crouched", class' := Chuj.RootClass.pos }

def Chuj.jenh : ChujRoot

Equations

• Chuj.jenh = { form := "jenh", gloss := "outstretched", class' := Chuj.RootClass.pos }

def Chuj.chek' : ChujRoot

Equations

• Chuj.chek' = { form := "chek'", gloss := "leaning", class' := Chuj.RootClass.pos }

def Chuj.lich' : ChujRoot

Equations

• Chuj.lich' = { form := "lich'", gloss := "extended", class' := Chuj.RootClass.pos }

def Chuj.b'ul : ChujRoot

Equations

• Chuj.b'ul = { form := "b'ul", gloss := "gathered", class' := Chuj.RootClass.pos }

def Chuj.kot : ChujRoot

Equations

• Chuj.kot = { form := "kot", gloss := "on four legs", class' := Chuj.RootClass.pos }

def Chuj.tel : ChujRoot

Equations

• Chuj.tel = { form := "tel", gloss := "lying down", class' := Chuj.RootClass.pos }

√NOM roots (Table (5), p. 39; Table (17), p. 46)

def Chuj.pat : ChujRoot

Equations

• Chuj.pat = { form := "pat", gloss := "house", class' := Chuj.RootClass.nom }

def Chuj.k'atzitz : ChujRoot

Equations

• Chuj.k'atzitz = { form := "k'atzitz", gloss := "wood", class' := Chuj.RootClass.nom }

def Chuj.ixim : ChujRoot

Equations

• Chuj.ixim = { form := "ixim", gloss := "corn", class' := Chuj.RootClass.nom }

def Chuj.winak : ChujRoot

Equations

• Chuj.winak = { form := "winak", gloss := "man", class' := Chuj.RootClass.nom }

def Chuj.chanhal : ChujRoot

Equations

• Chuj.chanhal = { form := "chanhal", gloss := "dance", class' := Chuj.RootClass.nom }

def Chuj.at'is : ChujRoot

Equations

• Chuj.at'is = { form := "at'is", gloss := "sneeze", class' := Chuj.RootClass.nom }

def Chuj.tz'ib' : ChujRoot

Equations

• Chuj.tz'ib' = { form := "tz'ib'", gloss := "writing", class' := Chuj.RootClass.nom }

Root lists

def Chuj.allRoots : List ChujRoot

The full root inventory.

Equations

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

def Chuj.tvRoots : List ChujRoot

All √TV roots.

Equations

• Chuj.tvRoots = List.filter (fun (x : Chuj.ChujRoot) => x.class' == Chuj.RootClass.tv) Chuj.allRoots

def Chuj.itvRoots : List ChujRoot

All √ITV roots.

Equations

• Chuj.itvRoots = List.filter (fun (x : Chuj.ChujRoot) => x.class' == Chuj.RootClass.itv) Chuj.allRoots

def Chuj.posRoots : List ChujRoot

All √POS roots.

Equations

• Chuj.posRoots = List.filter (fun (x : Chuj.ChujRoot) => x.class' == Chuj.RootClass.pos) Chuj.allRoots

def Chuj.nomRoots : List ChujRoot

All √NOM roots.

Equations

• Chuj.nomRoots = List.filter (fun (x : Chuj.ChujRoot) => x.class' == Chuj.RootClass.nom) Chuj.allRoots