K'iche' Agreement Fragment

Theory-neutral typological metadata for K'iche' (K'ichean Mayan) agreement morphology, following [Mon17] Lessons 4, 7–8, 9, 15. K'iche' has ergative-absolutive alignment realized through two verbal agreement paradigms: Set B (absolutive) cross-references intransitive S and transitive P and appears between the aspect marker and the root; Set A (ergative) cross-references transitive A, appears between the object marker and the root, and is identical to the possessive prefixes. Unlike its sister Kaqchikel, K'iche' has no construction-specific inverted alignment.

Main declarations

• Kiche.PhiFeatures: person/number/formality bundles, with HasPerson and HasNumber instances and the informal shorthand Kiche.phi.
• Kiche.setBMarker, Kiche.setAPreC, Kiche.setAPreV: the Set B (absolutive) and Set A (ergative, pre-consonantal / pre-vocalic) exponents.
• Kiche.ArgPosition.agreementSet, Kiche.ArgPosition.case: the agreement set and case each argument position triggers.
• Kiche.independentPronoun: the free personal pronouns.
• Kiche.setAExponent, Kiche.setBExponent: canonical φ-cell exponent tables for cross-Mayan consumption.

Implementation notes

The alignment is ergative-absolutive: Set B groups S and P (both trigger the same paradigm) while A triggers Set A. This contrasts with Mam, which is morphologically tripartite (S, A, P each distinct; [Sco23]). K'iche' has two 2nd-person formality levels; the formal forms (laal SG, alaq PL) are syntactically postverbal and pattern outside the prefix paradigm. K'iche' is HIGH-ABS (Set B pre-stem on Infl), and its case wiring reuses Mayan.ergCaseKiche (from Alignment.ergative); the canonical φ-cell exponent tables key on Agreement.Cell for cross-Mayan consumption. Extraction marking (AF and wi) lives in Kiche/Extraction.lean.

Person, number, and formality features

inductive 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 Kiche.instDecidableEqFormality : DecidableEq Formality

Equations

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

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

Equations

• Kiche.instReprFormality.repr Kiche.Formality.informal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.Formality.informal")).group prec✝
• Kiche.instReprFormality.repr Kiche.Formality.formal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.Formality.formal")).group prec✝

@[implicit_reducible]

instance Kiche.instReprFormality : Repr Formality

Equations

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

structure Kiche.PhiFeatures : Type

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

• person : Person
• number : Number
• formality : Formality

def 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 Kiche.instDecidableEqPhiFeatures : DecidableEq PhiFeatures

Equations

• Kiche.instDecidableEqPhiFeatures = Kiche.instDecidableEqPhiFeatures.decEq

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

Equations

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

@[implicit_reducible]

instance Kiche.instReprPhiFeatures : Repr PhiFeatures

Equations

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

@[implicit_reducible]

instance Kiche.instHasNumberPhiFeatures : HasNumber PhiFeatures

A K'iche' φ-bundle bears its number slot (HasNumber).

Equations

• Kiche.instHasNumberPhiFeatures = { numberOf := fun (φ : Kiche.PhiFeatures) => some φ.number }

@[implicit_reducible]

instance Kiche.instHasPersonPhiFeatures : HasPerson PhiFeatures

Equations

• Kiche.instHasPersonPhiFeatures = { personOf := fun (φ : Kiche.PhiFeatures) => some φ.person }

@[reducible, inline]

abbrev Kiche.phi (p : Person) (n : Number) : PhiFeatures

Shorthand for informal phi features.

Equations

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

Set B (absolutive) markers

def 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). [Mon17] Lessons 9, 15.

Equations

• Kiche.setBMarker { person := Person.first, number := Number.singular, formality := Kiche.Formality.informal } = "in-"
• Kiche.setBMarker { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = "at-"
• Kiche.setBMarker { person := Person.third, number := Number.singular, formality := Kiche.Formality.informal } = "∅"
• Kiche.setBMarker { person := Person.first, number := Number.plural, formality := Kiche.Formality.informal } = "oj-"
• Kiche.setBMarker { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = "ix-"
• Kiche.setBMarker { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = "ee-"
• Kiche.setBMarker { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = "la"
• Kiche.setBMarker { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = "alaq"
• Kiche.setBMarker { person := Person.first, number := number, formality := Kiche.Formality.informal } = "oj-"
• Kiche.setBMarker { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = "oj-"
• Kiche.setBMarker { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = "oj-"
• Kiche.setBMarker { person := Person.zero, number := number, formality := Kiche.Formality.informal } = "∅"
• Kiche.setBMarker { person := Person.second, number := number, formality := Kiche.Formality.informal } = "ix-"
• Kiche.setBMarker { person := Person.third, number := number, formality := Kiche.Formality.informal } = "ee-"
• Kiche.setBMarker { person := person, number := number, formality := Kiche.Formality.formal } = "Ø"

Set A (ergative) markers

def 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. [Mon17] Lessons 7, 15.

Equations

• Kiche.setAPreC { person := Person.first, number := Number.singular, formality := Kiche.Formality.informal } = "nu-/in-"
• Kiche.setAPreC { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = "a-"
• Kiche.setAPreC { person := Person.third, number := Number.singular, formality := Kiche.Formality.informal } = "u-"
• Kiche.setAPreC { person := Person.first, number := Number.plural, formality := Kiche.Formality.informal } = "qa-"
• Kiche.setAPreC { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = "i-"
• Kiche.setAPreC { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = "ki-"
• Kiche.setAPreC { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = "la"
• Kiche.setAPreC { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = "alaq"
• Kiche.setAPreC { person := Person.first, number := number, formality := Kiche.Formality.informal } = "qa-"
• Kiche.setAPreC { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = "qa-"
• Kiche.setAPreC { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = "qa-"
• Kiche.setAPreC { person := Person.zero, number := number, formality := Kiche.Formality.informal } = "∅"
• Kiche.setAPreC { person := Person.second, number := number, formality := Kiche.Formality.informal } = "i-"
• Kiche.setAPreC { person := Person.third, number := number, formality := Kiche.Formality.informal } = "ki-"
• Kiche.setAPreC { person := person, number := number, formality := Kiche.Formality.formal } = "Ø"

def Kiche.setAPreV : PhiFeatures → String

Set A (ergative) markers before vowel-initial roots. [Mon17] Lesson 8.

Equations

• Kiche.setAPreV { person := Person.first, number := Number.singular, formality := Kiche.Formality.informal } = "w-"
• Kiche.setAPreV { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = "aw-"
• Kiche.setAPreV { person := Person.third, number := Number.singular, formality := Kiche.Formality.informal } = "r-"
• Kiche.setAPreV { person := Person.first, number := Number.plural, formality := Kiche.Formality.informal } = "q-"
• Kiche.setAPreV { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = "iw-"
• Kiche.setAPreV { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = "k-"
• Kiche.setAPreV { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = "la"
• Kiche.setAPreV { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = "alaq"
• Kiche.setAPreV { person := Person.first, number := number, formality := Kiche.Formality.informal } = "q-"
• Kiche.setAPreV { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = "q-"
• Kiche.setAPreV { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = "q-"
• Kiche.setAPreV { person := Person.zero, number := number, formality := Kiche.Formality.informal } = "∅"
• Kiche.setAPreV { person := Person.second, number := number, formality := Kiche.Formality.informal } = "iw-"
• Kiche.setAPreV { person := Person.third, number := number, formality := Kiche.Formality.informal } = "k-"
• Kiche.setAPreV { person := person, number := number, formality := Kiche.Formality.formal } = "Ø"

Morphological positions

def 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. [Mon17] Lesson 9.

Equations

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

@[implicit_reducible]

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

Equations

• Kiche.instDecidableSetBIsPrefix φ = Kiche.instDecidableSetBIsPrefix._aux_1 φ

def Kiche.SetAIsPrefix (φ : PhiFeatures) : Prop

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

Equations

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

@[implicit_reducible]

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

Equations

• Kiche.instDecidableSetAIsPrefix φ = Kiche.instDecidableSetAIsPrefix._aux_1 φ

Argument positions and alignment

@[reducible, inline]

abbrev 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

• Kiche.ArgPosition = Features.Prominence.ArgumentRole

inductive Kiche.AgreementSet : Type

Which agreement set cross-references each argument position?

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

@[implicit_reducible]

instance Kiche.instDecidableEqAgreementSet : DecidableEq AgreementSet

Equations

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

@[implicit_reducible]

instance Kiche.instReprAgreementSet : Repr AgreementSet

Equations

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

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

Equations

• Kiche.instReprAgreementSet.repr Kiche.AgreementSet.setA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.AgreementSet.setA")).group prec✝
• Kiche.instReprAgreementSet.repr Kiche.AgreementSet.setB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.AgreementSet.setB")).group prec✝
• Kiche.instReprAgreementSet.repr Kiche.AgreementSet.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kiche.AgreementSet.none")).group prec✝

def 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

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

@[reducible, inline]

abbrev Kiche.ArgPosition.case : ArgPosition → Case

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

Equations

• Kiche.ArgPosition.case = Mayan.ergCaseKiche

Alignment theorems

theorem 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 Kiche.erg_abs_pattern : ArgPosition.case Features.Prominence.ArgumentRole.A ≠ ArgPosition.case Features.Prominence.ArgumentRole.P ∧ ArgPosition.case Features.Prominence.ArgumentRole.P = ArgPosition.case Features.Prominence.ArgumentRole.S

A receives ERG while P and S share a case (ABS) — the ergative partition, re-exported from Alignment.ergative_distinguishes_A.

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

Set B per-cell verification

theorem Kiche.setB_1sg : setBMarker (phi Person.first Number.singular) = "in-"

1SG absolutive: in-

theorem Kiche.setB_2sg : setBMarker (phi Person.second Number.singular) = "at-"

2SG absolutive: at-

theorem Kiche.setB_3sg : setBMarker (phi Person.third Number.singular) = "∅"

3SG absolutive: ∅ (null morpheme)

theorem Kiche.setB_1pl : setBMarker (phi Person.first Number.plural) = "oj-"

1PL absolutive: oj-

theorem Kiche.setB_2pl : setBMarker (phi Person.second Number.plural) = "ix-"

2PL absolutive: ix-

theorem Kiche.setB_3pl : setBMarker (phi Person.third Number.plural) = "ee-"

3PL absolutive: ee-

theorem Kiche.setB_2sg_form : setBMarker { person := Person.second, number := Number.singular, formality := Formality.formal } = "la"

2SG.FORM: la (postverbal)

theorem Kiche.setB_2pl_form : setBMarker { person := Person.second, number := Number.plural, formality := Formality.formal } = "alaq"

2PL.FORM: alaq (postverbal)

Set A per-cell verification

theorem Kiche.setA_1sg : setAPreC (phi Person.first Number.singular) = "nu-/in-"

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

theorem Kiche.setA_2sg : setAPreC (phi Person.second Number.singular) = "a-"

2SG ergative (preC): a-

theorem Kiche.setA_3sg : setAPreC (phi Person.third Number.singular) = "u-"

3SG ergative (preC): u-

theorem Kiche.setA_1pl : setAPreC (phi Person.first Number.plural) = "qa-"

1PL ergative (preC): qa-

theorem Kiche.setA_2pl : setAPreC (phi Person.second Number.plural) = "i-"

2PL ergative (preC): i-

theorem Kiche.setA_3pl : setAPreC (phi Person.third Number.plural) = "ki-"

3PL ergative (preC): ki-

theorem Kiche.setA_preV_1sg : setAPreV (phi Person.first Number.singular) = "w-"

1SG ergative (preV): w-

theorem Kiche.setA_preV_2sg : setAPreV (phi Person.second Number.singular) = "aw-"

2SG ergative (preV): aw-

theorem Kiche.setA_preV_3sg : setAPreV (phi Person.third Number.singular) = "r-"

3SG ergative (preV): r-

Possessives equal Set A

theorem Kiche.possessives_equal_setA : setAPreC (phi Person.first Number.plural) = "qa-" ∧ setAPreC (phi Person.second Number.singular) = "a-" ∧ setAPreC (phi Person.third Number.singular) = "u-" ∧ setAPreC (phi Person.third Number.plural) = "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. [Mon17] Lesson 15 explicitly notes this identity.

Formal markers are postverbal

theorem Kiche.setB_informal_prefix : SetBIsPrefix (phi Person.first Number.singular) ∧ SetBIsPrefix (phi Person.second Number.singular) ∧ SetBIsPrefix (phi Person.third Number.singular) ∧ SetBIsPrefix (phi Person.first Number.plural) ∧ SetBIsPrefix (phi Person.second Number.plural) ∧ SetBIsPrefix (phi Person.third Number.plural)

All informal Set B markers are prefixes.

theorem Kiche.setB_formal_postverbal : ¬SetBIsPrefix { person := Person.second, number := Number.singular, formality := Formality.formal } ∧ ¬SetBIsPrefix { person := Person.second, number := Number.plural, formality := Formality.formal }

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

Independent pronouns

def Kiche.independentPronoun : PhiFeatures → String

Independent (free) personal pronouns. These are used in nonverbal sentences and as emphatic/contrastive pronouns in verbal sentences. [Mon17] Lesson 4.

Equations

• Kiche.independentPronoun { person := Person.first, number := Number.singular, formality := Kiche.Formality.informal } = "in"
• Kiche.independentPronoun { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = "at"
• Kiche.independentPronoun { person := Person.third, number := Number.singular, formality := Kiche.Formality.informal } = "are'"
• Kiche.independentPronoun { person := Person.first, number := Number.plural, formality := Kiche.Formality.informal } = "oj"
• Kiche.independentPronoun { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = "ix"
• Kiche.independentPronoun { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = "a're'"
• Kiche.independentPronoun { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = "laal"
• Kiche.independentPronoun { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = "alaq"
• Kiche.independentPronoun { person := Person.first, number := number, formality := Kiche.Formality.informal } = "oj"
• Kiche.independentPronoun { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = "oj"
• Kiche.independentPronoun { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = "oj"
• Kiche.independentPronoun { person := Person.zero, number := number, formality := Kiche.Formality.informal } = "∅"
• Kiche.independentPronoun { person := Person.second, number := number, formality := Kiche.Formality.informal } = "ix"
• Kiche.independentPronoun { person := Person.third, number := number, formality := Kiche.Formality.informal } = "a're'"
• Kiche.independentPronoun { person := person, number := number, formality := Kiche.Formality.formal } = "are'"

theorem Kiche.pronoun_setB_correspondence : independentPronoun (phi Person.first Number.singular) = "in" ∧ independentPronoun (phi Person.second Number.singular) = "at" ∧ independentPronoun (phi Person.first Number.plural) = "oj" ∧ independentPronoun (phi Person.second Number.plural) = "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.

Cross-Mayan canonical wrappers

def Kiche.absPosition : Mayan.ABSPosition

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

Equations

• Kiche.absPosition = Mayan.ABSPosition.high

def Kiche.setALinearity : Mayan.MarkerLinearity

Set A linearity: prefixal ([Mon17] Lessons 7–8).

Equations

• Kiche.setALinearity = Mayan.MarkerLinearity.prefixal

def Kiche.setBLinearity : Mayan.MarkerLinearity

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

Equations

• Kiche.setBLinearity = Mayan.MarkerLinearity.prefixal

def Kiche.setAExponent : Mayan.ExponentTable

Canonical Set A exponent table (pre-consonantal allomorph; informal), keyed on the canonical φ-cell Agreement.Cell for cross-Mayan consumption.

Equations

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

def Kiche.setBExponent : Mayan.ExponentTable

Canonical Set B exponent table (informal) keyed on the canonical φ-cell Agreement.Cell.

Equations

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

theorem Kiche.p3sg_abs_null : Agreement.Paradigm.realize setBExponent (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = some "∅"

3rd person absolutive is null — invariant across the standard Mayan branches per [KN84] Table 8. Not pan-Mayan: see Mam exception via Mayan.isStandard.