K'iche' Agreement Fragment @cite{mondloch-2017}

Theory-neutral typological metadata for K'iche' (K'ichean Mayan) agreement morphology, following @cite{mondloch-2017} Lessons 4, 7–8, 9, 15. K'iche' is uniformly ergative-absolutive (Set B = ABS, Set A = ERG); unlike its sister Kaqchikel it has no construction-specific inverted alignment.

The System

K'iche' has an ergative-absolutive alignment system realized through two agreement paradigms on the verb:

• Set B (ABS): absolutive markers that cross-reference the sole argument of intransitives (S) and the object of transitives (P). These appear between the aspect marker and the verb root.
• Set A (ERG): ergative markers that cross-reference the subject of transitives (A). These appear between the object marker and the root. Set A markers are identical to the possessive pronouns used before consonant-initial nouns (Lesson 7).

Paradigms

Set B (Absolutive) — Lesson 9

Person	Singular	Plural
1	in-	oj-
2	at-	ix-
3	Ø-	ee-
2.FORM	la (postverbal)	alaq (postverbal)

Set A (Ergative, preconsonantal) — Lessons 7, 15

Person	Singular	Plural
1	nu‑ / in‑	qa-
2	a-	i-
3	u-	ki-
2.FORM	la (postverbal)	alaq (postverbal)

Set A (Ergative, prevocalic) — Lesson 8

Person	Singular	Plural
1	w-	q-
2	aw-	iw-
3	r-	k-
2.FORM	la (postverbal)	alaq (postverbal)

Alignment

The alignment is ergative-absolutive: Set B groups S and P together (both trigger the same paradigm), while A triggers a distinct paradigm (Set A). This contrasts with Mam, which shows morphologically tripartite alignment (S, A, and P each trigger distinct patterns; @cite{scott-2023}).

Formal address

K'iche' has two levels of formality for 2nd person: informal and formal. The formal forms (laal SG, alaq PL) are syntactically postverbal and do not participate in the prefix paradigm.

inductive Fragments.Mayan.Kiche.Formality : Type

Formality level for 2nd person. K'iche'-specific: the formal forms (laal SG, alaq PL) are postverbal and pattern outside the prefix paradigm.

• informal : Formality
• formal : Formality

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instDecidableEqFormality : DecidableEq Formality

Equations

• Fragments.Mayan.Kiche.instDecidableEqFormality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mayan.Kiche.instReprFormality.repr : Formality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instReprFormality : Repr Formality

Equations

• Fragments.Mayan.Kiche.instReprFormality = { reprPrec := Fragments.Mayan.Kiche.instReprFormality.repr }

structure Fragments.Mayan.Kiche.PhiFeatures : Type

A person/number/formality specification. Uses canonical Features.Prominence.PersonLevel for cross-language compatibility; Formality is K'iche'-specific.

• person : Features.Prominence.PersonLevel
• number : Number
• formality : Formality

def Fragments.Mayan.Kiche.instDecidableEqPhiFeatures.decEq (x✝ x✝¹ : PhiFeatures) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instDecidableEqPhiFeatures : DecidableEq PhiFeatures

Equations

• Fragments.Mayan.Kiche.instDecidableEqPhiFeatures = Fragments.Mayan.Kiche.instDecidableEqPhiFeatures.decEq

def Fragments.Mayan.Kiche.instReprPhiFeatures.repr : PhiFeatures → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instReprPhiFeatures : Repr PhiFeatures

Equations

• Fragments.Mayan.Kiche.instReprPhiFeatures = { reprPrec := Fragments.Mayan.Kiche.instReprPhiFeatures.repr }

@[reducible, inline]

abbrev Fragments.Mayan.Kiche.phi (p : Features.Prominence.PersonLevel) (n : Number) : PhiFeatures

Shorthand for informal phi features.

Equations

• Fragments.Mayan.Kiche.phi p n = { person := p, number := n, formality := Fragments.Mayan.Kiche.Formality.informal }

def Fragments.Mayan.Kiche.setBMarker : PhiFeatures → String

Set B (absolutive) agreement markers. These are verbal prefixes (or postverbal particles for formal forms) that cross-reference S (intransitive subject) and P (transitive object). @cite{mondloch-2017} Lessons 9, 15.

Equations

• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "in-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "at-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "∅"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ee-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "la"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix-"
• Fragments.Mayan.Kiche.setBMarker { person := Features.Prominence.PersonLevel.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ee-"
• Fragments.Mayan.Kiche.setBMarker { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "Ø"

def Fragments.Mayan.Kiche.setAPreC : PhiFeatures → String

Set A (ergative) markers before consonant-initial roots. These cross-reference A (transitive subject) and are identical to possessive pronouns before consonant-initial nouns. @cite{mondloch-2017} Lessons 7, 15.

Equations

• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "nu-/in-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "a-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "u-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "qa-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "i-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ki-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "la"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "qa-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "i-"
• Fragments.Mayan.Kiche.setAPreC { person := Features.Prominence.PersonLevel.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ki-"
• Fragments.Mayan.Kiche.setAPreC { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "Ø"

def Fragments.Mayan.Kiche.setAPreV : PhiFeatures → String

Set A (ergative) markers before vowel-initial roots. @cite{mondloch-2017} Lesson 8.

Equations

• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "w-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "aw-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "r-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "q-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "iw-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "k-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "la"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "q-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "iw-"
• Fragments.Mayan.Kiche.setAPreV { person := Features.Prominence.PersonLevel.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "k-"
• Fragments.Mayan.Kiche.setAPreV { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "Ø"

def Fragments.Mayan.Kiche.SetBIsPrefix (φ : PhiFeatures) : Prop

Is a Set B marker a prefix (appearing before the root) or a postverbal particle? Formal forms are postverbal; all others are prefixes. @cite{mondloch-2017} Lesson 9.

Equations

• Fragments.Mayan.Kiche.SetBIsPrefix φ = (φ.formality = Fragments.Mayan.Kiche.Formality.informal)

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instDecidableSetBIsPrefix (φ : PhiFeatures) : Decidable (SetBIsPrefix φ)

Equations

• Fragments.Mayan.Kiche.instDecidableSetBIsPrefix φ = Fragments.Mayan.Kiche.instDecidableSetBIsPrefix._aux_1 φ

def Fragments.Mayan.Kiche.SetAIsPrefix (φ : PhiFeatures) : Prop

Is a Set A marker a prefix or postverbal? Same distribution as Set B: formal forms are postverbal.

Equations

• Fragments.Mayan.Kiche.SetAIsPrefix φ = (φ.formality = Fragments.Mayan.Kiche.Formality.informal)

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instDecidableSetAIsPrefix (φ : PhiFeatures) : Decidable (SetAIsPrefix φ)

Equations

• Fragments.Mayan.Kiche.instDecidableSetAIsPrefix φ = Fragments.Mayan.Kiche.instDecidableSetAIsPrefix._aux_1 φ

@[reducible, inline]

abbrev Fragments.Mayan.Kiche.ArgPosition : Type

Argument positions in a K'iche' clause. Aliased to the canonical Features.Prominence.ArgumentRole (S/A/P/R/T) so cross-Mayan and cross-framework code shares one inventory. Use the canonical constructor names .A / .P / .S directly.

Equations

• Fragments.Mayan.Kiche.ArgPosition = Features.Prominence.ArgumentRole

inductive Fragments.Mayan.Kiche.AgreementSet : Type

Which agreement set cross-references each argument position?

• setA : AgreementSet
• setB : AgreementSet
• none : AgreementSet

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instDecidableEqAgreementSet : DecidableEq AgreementSet

Equations

• Fragments.Mayan.Kiche.instDecidableEqAgreementSet x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Mayan.Kiche.instReprAgreementSet.repr : AgreementSet → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kiche.instReprAgreementSet : Repr AgreementSet

Equations

• Fragments.Mayan.Kiche.instReprAgreementSet = { reprPrec := Fragments.Mayan.Kiche.instReprAgreementSet.repr }

def Fragments.Mayan.Kiche.ArgPosition.agreementSet : ArgPosition → AgreementSet

The agreement set triggered by each argument position. S and P both trigger Set B (= absolutive grouping). A triggers Set A (= ergative). Ditransitive R/T default to .none (not modeled in this fragment).

Equations

• Fragments.Mayan.Kiche.ArgPosition.agreementSet Features.Prominence.ArgumentRole.A = Fragments.Mayan.Kiche.AgreementSet.setA
• Fragments.Mayan.Kiche.ArgPosition.agreementSet Features.Prominence.ArgumentRole.P = Fragments.Mayan.Kiche.AgreementSet.setB
• Fragments.Mayan.Kiche.ArgPosition.agreementSet Features.Prominence.ArgumentRole.S = Fragments.Mayan.Kiche.AgreementSet.setB
• Fragments.Mayan.Kiche.ArgPosition.agreementSet Features.Prominence.ArgumentRole.R = Fragments.Mayan.Kiche.AgreementSet.none
• Fragments.Mayan.Kiche.ArgPosition.agreementSet Features.Prominence.ArgumentRole.T = Fragments.Mayan.Kiche.AgreementSet.none

@[reducible, inline]

abbrev Fragments.Mayan.Kiche.ArgPosition.case : ArgPosition → Core.Case

The case associated with each argument position. Definitionally equal to Fragments.Mayan.ergCaseKiche, which derives from Alignment.ergative.assignCase in Theories/Syntax/Case/Alignment.lean.

Equations

• Fragments.Mayan.Kiche.ArgPosition.case = Fragments.Mayan.ergCaseKiche

theorem Fragments.Mayan.Kiche.ergative_absolutive_alignment : ArgPosition.agreementSet Features.Prominence.ArgumentRole.S = ArgPosition.agreementSet Features.Prominence.ArgumentRole.P ∧ ArgPosition.agreementSet Features.Prominence.ArgumentRole.A ≠ ArgPosition.agreementSet Features.Prominence.ArgumentRole.P

K'iche' groups S and P together (both trigger Set B): ergative-absolutive alignment.

theorem Fragments.Mayan.Kiche.erg_abs_pattern : ArgPosition.case Features.Prominence.ArgumentRole.S = ArgPosition.case Features.Prominence.ArgumentRole.P ∧ ArgPosition.case Features.Prominence.ArgumentRole.A ≠ ArgPosition.case Features.Prominence.ArgumentRole.S

S and P receive the same case (ABS); A receives ERG.

theorem Fragments.Mayan.Kiche.kiche_not_tripartite : ArgPosition.case Features.Prominence.ArgumentRole.S = ArgPosition.case Features.Prominence.ArgumentRole.P

K'iche' alignment contrast with Mam: K'iche' is ergative-absolutive (S = P ≠ A), while Mam is tripartite (S ≠ A ≠ P, all three receive distinct cases). In K'iche', both P and S trigger Set B; in Mam, P triggers no agreement at all.

theorem Fragments.Mayan.Kiche.setB_1sg : setBMarker (phi Features.Prominence.PersonLevel.first UD.Number.Sing) = "in-"

1SG absolutive: in-

theorem Fragments.Mayan.Kiche.setB_2sg : setBMarker (phi Features.Prominence.PersonLevel.second UD.Number.Sing) = "at-"

2SG absolutive: at-

theorem Fragments.Mayan.Kiche.setB_3sg : setBMarker (phi Features.Prominence.PersonLevel.third UD.Number.Sing) = "∅"

3SG absolutive: ∅ (null morpheme)

theorem Fragments.Mayan.Kiche.setB_1pl : setBMarker (phi Features.Prominence.PersonLevel.first UD.Number.Plur) = "oj-"

1PL absolutive: oj-

theorem Fragments.Mayan.Kiche.setB_2pl : setBMarker (phi Features.Prominence.PersonLevel.second UD.Number.Plur) = "ix-"

2PL absolutive: ix-

theorem Fragments.Mayan.Kiche.setB_3pl : setBMarker (phi Features.Prominence.PersonLevel.third UD.Number.Plur) = "ee-"

3PL absolutive: ee-

theorem Fragments.Mayan.Kiche.setB_2sg_form : setBMarker { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Formality.formal } = "la"

2SG.FORM: la (postverbal)

theorem Fragments.Mayan.Kiche.setB_2pl_form : setBMarker { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Formality.formal } = "alaq"

2PL.FORM: alaq (postverbal)

theorem Fragments.Mayan.Kiche.setA_1sg : setAPreC (phi Features.Prominence.PersonLevel.first UD.Number.Sing) = "nu-/in-"

1SG ergative (preC): nu‑ or in‑

theorem Fragments.Mayan.Kiche.setA_2sg : setAPreC (phi Features.Prominence.PersonLevel.second UD.Number.Sing) = "a-"

2SG ergative (preC): a-

theorem Fragments.Mayan.Kiche.setA_3sg : setAPreC (phi Features.Prominence.PersonLevel.third UD.Number.Sing) = "u-"

3SG ergative (preC): u-

theorem Fragments.Mayan.Kiche.setA_1pl : setAPreC (phi Features.Prominence.PersonLevel.first UD.Number.Plur) = "qa-"

1PL ergative (preC): qa-

theorem Fragments.Mayan.Kiche.setA_2pl : setAPreC (phi Features.Prominence.PersonLevel.second UD.Number.Plur) = "i-"

2PL ergative (preC): i-

theorem Fragments.Mayan.Kiche.setA_3pl : setAPreC (phi Features.Prominence.PersonLevel.third UD.Number.Plur) = "ki-"

3PL ergative (preC): ki-

theorem Fragments.Mayan.Kiche.setA_preV_1sg : setAPreV (phi Features.Prominence.PersonLevel.first UD.Number.Sing) = "w-"

1SG ergative (preV): w-

theorem Fragments.Mayan.Kiche.setA_preV_2sg : setAPreV (phi Features.Prominence.PersonLevel.second UD.Number.Sing) = "aw-"

2SG ergative (preV): aw-

theorem Fragments.Mayan.Kiche.setA_preV_3sg : setAPreV (phi Features.Prominence.PersonLevel.third UD.Number.Sing) = "r-"

3SG ergative (preV): r-

theorem Fragments.Mayan.Kiche.possessives_equal_setA : setAPreC (phi Features.Prominence.PersonLevel.first UD.Number.Plur) = "qa-" ∧ setAPreC (phi Features.Prominence.PersonLevel.second UD.Number.Sing) = "a-" ∧ setAPreC (phi Features.Prominence.PersonLevel.third UD.Number.Sing) = "u-" ∧ setAPreC (phi Features.Prominence.PersonLevel.third UD.Number.Plur) = "ki-"

Set A markers are identical to possessive pronouns: the transitive subject markers (Lesson 15) are the same forms as the possessive prefixes (Lessons 7–8). This is a hallmark of ergative-absolutive languages, where ERG agreement and possession share the same morphological paradigm. @cite{mondloch-2017} Lesson 15 explicitly notes this identity.

theorem Fragments.Mayan.Kiche.setB_informal_prefix : SetBIsPrefix (phi Features.Prominence.PersonLevel.first UD.Number.Sing) ∧ SetBIsPrefix (phi Features.Prominence.PersonLevel.second UD.Number.Sing) ∧ SetBIsPrefix (phi Features.Prominence.PersonLevel.third UD.Number.Sing) ∧ SetBIsPrefix (phi Features.Prominence.PersonLevel.first UD.Number.Plur) ∧ SetBIsPrefix (phi Features.Prominence.PersonLevel.second UD.Number.Plur) ∧ SetBIsPrefix (phi Features.Prominence.PersonLevel.third UD.Number.Plur)

All informal Set B markers are prefixes.

theorem Fragments.Mayan.Kiche.setB_formal_postverbal : ¬SetBIsPrefix { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Formality.formal } ∧ ¬SetBIsPrefix { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Formality.formal }

Formal Set B markers are NOT prefixes (they're postverbal).

def Fragments.Mayan.Kiche.independentPronoun : PhiFeatures → String

Independent (free) personal pronouns. These are used in nonverbal sentences and as emphatic/contrastive pronouns in verbal sentences. @cite{mondloch-2017} Lesson 4.

Equations

• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.first, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "in"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "at"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.third, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.informal } = "are'"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.first, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.third, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.informal } = "a're'"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.second, number := UD.Number.Sing, formality := Fragments.Mayan.Kiche.Formality.formal } = "laal"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.second, number := UD.Number.Plur, formality := Fragments.Mayan.Kiche.Formality.formal } = "alaq"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.first, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "oj"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.second, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "ix"
• Fragments.Mayan.Kiche.independentPronoun { person := Features.Prominence.PersonLevel.third, number := number, formality := Fragments.Mayan.Kiche.Formality.informal } = "a're'"
• Fragments.Mayan.Kiche.independentPronoun { person := person, number := number, formality := Fragments.Mayan.Kiche.Formality.formal } = "are'"

theorem Fragments.Mayan.Kiche.pronoun_setB_correspondence : independentPronoun (phi Features.Prominence.PersonLevel.first UD.Number.Sing) = "in" ∧ independentPronoun (phi Features.Prominence.PersonLevel.second UD.Number.Sing) = "at" ∧ independentPronoun (phi Features.Prominence.PersonLevel.first UD.Number.Plur) = "oj" ∧ independentPronoun (phi Features.Prominence.PersonLevel.second UD.Number.Plur) = "ix"

Independent pronouns correspond to Set B (absolutive) markers in form: 1SG in = Set B in-, 2SG at = Set B at-, etc. This is expected for an ergative language where the independent pronouns pattern with absolutive agreement.

def Fragments.Mayan.Kiche.absPosition : ABSPosition

K'iche' is HIGH-ABS: Set B markers appear pre-stem on Infl.

Equations

• Fragments.Mayan.Kiche.absPosition = Fragments.Mayan.ABSPosition.high

def Fragments.Mayan.Kiche.setALinearity : MarkerLinearity

Set A linearity: prefixal (per Mondloch Lessons 7-8).

Equations

• Fragments.Mayan.Kiche.setALinearity = Fragments.Mayan.MarkerLinearity.prefixal

def Fragments.Mayan.Kiche.setBLinearity : MarkerLinearity

Set B linearity: prefixal (HIGH-ABS K'ichean morphology).

Equations

• Fragments.Mayan.Kiche.setBLinearity = Fragments.Mayan.MarkerLinearity.prefixal

def Fragments.Mayan.Kiche.setAExponent : PersonNumber → String

Canonical Set A exponent table (pre-consonantal allomorph; informal), keyed on Mayan.PersonNumber for cross-Mayan consumption.

Equations

• Fragments.Mayan.Kiche.setAExponent Fragments.Mayan.PersonNumber.p1sg = Fragments.Mayan.Kiche.setAPreC (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.first UD.Number.Sing)
• Fragments.Mayan.Kiche.setAExponent Fragments.Mayan.PersonNumber.p2sg = Fragments.Mayan.Kiche.setAPreC (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.second UD.Number.Sing)
• Fragments.Mayan.Kiche.setAExponent Fragments.Mayan.PersonNumber.p3sg = Fragments.Mayan.Kiche.setAPreC (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.third UD.Number.Sing)
• Fragments.Mayan.Kiche.setAExponent Fragments.Mayan.PersonNumber.p1pl = Fragments.Mayan.Kiche.setAPreC (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.first UD.Number.Plur)
• Fragments.Mayan.Kiche.setAExponent Fragments.Mayan.PersonNumber.p2pl = Fragments.Mayan.Kiche.setAPreC (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.second UD.Number.Plur)
• Fragments.Mayan.Kiche.setAExponent Fragments.Mayan.PersonNumber.p3pl = Fragments.Mayan.Kiche.setAPreC (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.third UD.Number.Plur)

def Fragments.Mayan.Kiche.setBExponent : PersonNumber → String

Canonical Set B exponent table (informal) keyed on Mayan.PersonNumber.

Equations

• Fragments.Mayan.Kiche.setBExponent Fragments.Mayan.PersonNumber.p1sg = Fragments.Mayan.Kiche.setBMarker (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.first UD.Number.Sing)
• Fragments.Mayan.Kiche.setBExponent Fragments.Mayan.PersonNumber.p2sg = Fragments.Mayan.Kiche.setBMarker (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.second UD.Number.Sing)
• Fragments.Mayan.Kiche.setBExponent Fragments.Mayan.PersonNumber.p3sg = Fragments.Mayan.Kiche.setBMarker (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.third UD.Number.Sing)
• Fragments.Mayan.Kiche.setBExponent Fragments.Mayan.PersonNumber.p1pl = Fragments.Mayan.Kiche.setBMarker (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.first UD.Number.Plur)
• Fragments.Mayan.Kiche.setBExponent Fragments.Mayan.PersonNumber.p2pl = Fragments.Mayan.Kiche.setBMarker (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.second UD.Number.Plur)
• Fragments.Mayan.Kiche.setBExponent Fragments.Mayan.PersonNumber.p3pl = Fragments.Mayan.Kiche.setBMarker (Fragments.Mayan.Kiche.phi Features.Prominence.PersonLevel.third UD.Number.Plur)

theorem Fragments.Mayan.Kiche.p3sg_abs_null : setBExponent PersonNumber.p3sg = "∅"

3rd person absolutive is null — invariant across the standard Mayan branches per @cite{kaufman-norman-1984} Table 8. Not pan-Mayan: see Mam exception via MayanLang.isStandard.

def Fragments.Mayan.Kiche.extractionProfile : Typology.ExtractionProfile

K'iche''s extraction profile: Agent-Focus Antipassive is productive (@cite{mondloch-2017} Lesson 22, with parallel coverage at Lessons 30 + 33 for radical TV and perfect aspect). The voice marker is -n (shared morphologically with the Absolutive Antipassive of Lesson 21; the AF vs absolutive-antipassive alternation is syntactic — both arguments overt for AF, object suppressed for absolutive antipassive — not morphological). HIGH-ABS K'ichean, structurally analogous to Kaqchikel.

Equations

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