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

@[instance_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✝

@[instance_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.

@[instance_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.

@[instance_reducible]

instance Kiche.instReprPhiFeatures : Repr PhiFeatures

Equations

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

@[instance_reducible]

instance Kiche.instHasNumberPhiFeatures : HasNumber PhiFeatures

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

Equations

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

@[instance_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 → List Morphology.Morph

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 } = [Morphology.Morph.pref "in"]
• Kiche.setBMarker { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "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 } = [Morphology.Morph.pref "oj"]
• Kiche.setBMarker { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "ix"]
• Kiche.setBMarker { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "ee"]
• Kiche.setBMarker { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = [Morphology.Morph.free "la"]
• Kiche.setBMarker { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = [Morphology.Morph.free "alaq"]
• Kiche.setBMarker { person := Person.first, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "oj"]
• Kiche.setBMarker { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "oj"]
• Kiche.setBMarker { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "oj"]
• Kiche.setBMarker { person := Person.zero, number := number, formality := Kiche.Formality.informal } = []
• Kiche.setBMarker { person := Person.second, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "ix"]
• Kiche.setBMarker { person := Person.third, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "ee"]
• Kiche.setBMarker { person := person, number := number, formality := Kiche.Formality.formal } = []

Set A (ergative) markers

def Kiche.setAPreC : PhiFeatures → List Morphology.Morph

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 } = [Morphology.Morph.pref "nu"]
• Kiche.setAPreC { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "a"]
• Kiche.setAPreC { person := Person.third, number := Number.singular, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "u"]
• Kiche.setAPreC { person := Person.first, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "qa"]
• Kiche.setAPreC { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "i"]
• Kiche.setAPreC { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "ki"]
• Kiche.setAPreC { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = [Morphology.Morph.free "la"]
• Kiche.setAPreC { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = [Morphology.Morph.free "alaq"]
• Kiche.setAPreC { person := Person.first, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "qa"]
• Kiche.setAPreC { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "qa"]
• Kiche.setAPreC { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "qa"]
• Kiche.setAPreC { person := Person.zero, number := number, formality := Kiche.Formality.informal } = []
• Kiche.setAPreC { person := Person.second, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "i"]
• Kiche.setAPreC { person := Person.third, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "ki"]
• Kiche.setAPreC { person := person, number := number, formality := Kiche.Formality.formal } = []

def Kiche.setAPreV : PhiFeatures → List Morphology.Morph

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

Equations

• Kiche.setAPreV { person := Person.first, number := Number.singular, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "w"]
• Kiche.setAPreV { person := Person.second, number := Number.singular, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "aw"]
• Kiche.setAPreV { person := Person.third, number := Number.singular, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "r"]
• Kiche.setAPreV { person := Person.first, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "q"]
• Kiche.setAPreV { person := Person.second, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "iw"]
• Kiche.setAPreV { person := Person.third, number := Number.plural, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "k"]
• Kiche.setAPreV { person := Person.second, number := Number.singular, formality := Kiche.Formality.formal } = [Morphology.Morph.free "la"]
• Kiche.setAPreV { person := Person.second, number := Number.plural, formality := Kiche.Formality.formal } = [Morphology.Morph.free "alaq"]
• Kiche.setAPreV { person := Person.first, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "q"]
• Kiche.setAPreV { person := Person.firstInclusive, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "q"]
• Kiche.setAPreV { person := Person.firstExclusive, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "q"]
• Kiche.setAPreV { person := Person.zero, number := number, formality := Kiche.Formality.informal } = []
• Kiche.setAPreV { person := Person.second, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "iw"]
• Kiche.setAPreV { person := Person.third, number := number, formality := Kiche.Formality.informal } = [Morphology.Morph.pref "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)

@[instance_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)

@[instance_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

@[instance_reducible]

instance Kiche.instDecidableEqAgreementSet : DecidableEq AgreementSet

Equations

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

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✝

@[instance_reducible]

instance Kiche.instReprAgreementSet : Repr AgreementSet

Equations

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

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) = [Morphology.Morph.pref "in"]

1SG absolutive: in-

theorem Kiche.setB_2sg : setBMarker (phi Person.second Number.singular) = [Morphology.Morph.pref "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) = [Morphology.Morph.pref "oj"]

1PL absolutive: oj-

theorem Kiche.setB_2pl : setBMarker (phi Person.second Number.plural) = [Morphology.Morph.pref "ix"]

2PL absolutive: ix-

theorem Kiche.setB_3pl : setBMarker (phi Person.third Number.plural) = [Morphology.Morph.pref "ee"]

3PL absolutive: ee-

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

2SG.FORM: la (postverbal)

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

2PL.FORM: alaq (postverbal)

Set A per-cell verification

theorem Kiche.setA_1sg : setAPreC (phi Person.first Number.singular) = [Morphology.Morph.pref "nu"]

1SG ergative (preC): nu- (possessive citation form; in- as transitive subject per [Mon17] Lesson 15 — both pre-consonantal, with w- pre-vocalic for both constructions)

theorem Kiche.setA_2sg : setAPreC (phi Person.second Number.singular) = [Morphology.Morph.pref "a"]

2SG ergative (preC): a-

theorem Kiche.setA_3sg : setAPreC (phi Person.third Number.singular) = [Morphology.Morph.pref "u"]

3SG ergative (preC): u-

theorem Kiche.setA_1pl : setAPreC (phi Person.first Number.plural) = [Morphology.Morph.pref "qa"]

1PL ergative (preC): qa-

theorem Kiche.setA_2pl : setAPreC (phi Person.second Number.plural) = [Morphology.Morph.pref "i"]

2PL ergative (preC): i-

theorem Kiche.setA_3pl : setAPreC (phi Person.third Number.plural) = [Morphology.Morph.pref "ki"]

3PL ergative (preC): ki-

theorem Kiche.setA_preV_1sg : setAPreV (phi Person.first Number.singular) = [Morphology.Morph.pref "w"]

1SG ergative (preV): w-

theorem Kiche.setA_preV_2sg : setAPreV (phi Person.second Number.singular) = [Morphology.Morph.pref "aw"]

2SG ergative (preV): aw-

theorem Kiche.setA_preV_3sg : setAPreV (phi Person.third Number.singular) = [Morphology.Morph.pref "r"]

3SG ergative (preV): r-

Possessives equal Set A

theorem Kiche.possessives_equal_setA : setAPreC (phi Person.first Number.plural) = [Morphology.Morph.pref "qa"] ∧ setAPreC (phi Person.second Number.singular) = [Morphology.Morph.pref "a"] ∧ setAPreC (phi Person.third Number.singular) = [Morphology.Morph.pref "u"] ∧ setAPreC (phi Person.third Number.plural) = [Morphology.Morph.pref "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 : Phonology.Segment.Class → Mayan.ExponentTable

Canonical Set A exponent table (informal) by following-segment environment, 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.

Formality-forgetting hom to canonical cells

def Kiche.PhiFeatures.toCell (φ : PhiFeatures) : Option Agreement.Cell

The formality-forgetting hom from K'iche' φ-bundles to the canonical Agreement.Cell: an informal bundle maps to its person/number cell (person via Person.toUD, number via Number.toUD); the two formal 2nd-person forms are postverbal, outside the prefix paradigm the Cell-keyed tables record, so they forget to none.

Equations

• φ.toCell = match φ.formality with | Kiche.Formality.formal => none | Kiche.Formality.informal => some { person := some φ.person.toUD, number := φ.number.toUD }

theorem Kiche.toCell_formal (p : Person) (n : Number) : { person := p, number := n, formality := Formality.formal }.toCell = none

Formal cells lie outside the prefix paradigm and forget to none.

theorem Kiche.setBExponent_agrees_informal : (phi Person.first Number.singular).toCell.bind (Agreement.Paradigm.realize setBExponent) = some (setBMarker (phi Person.first Number.singular)) ∧ (phi Person.second Number.singular).toCell.bind (Agreement.Paradigm.realize setBExponent) = some (setBMarker (phi Person.second Number.singular)) ∧ (phi Person.third Number.singular).toCell.bind (Agreement.Paradigm.realize setBExponent) = some (setBMarker (phi Person.third Number.singular)) ∧ (phi Person.first Number.plural).toCell.bind (Agreement.Paradigm.realize setBExponent) = some (setBMarker (phi Person.first Number.plural)) ∧ (phi Person.second Number.plural).toCell.bind (Agreement.Paradigm.realize setBExponent) = some (setBMarker (phi Person.second Number.plural)) ∧ (phi Person.third Number.plural).toCell.bind (Agreement.Paradigm.realize setBExponent) = some (setBMarker (phi Person.third Number.plural))

On the six basic informal cells the hom lands on the very cell the canonical Set B table keys, and the two tables agree: looking φ.toCell up in setBExponent returns the direct exponent setBMarker φ.

theorem Kiche.setAExponent_agrees_informal : (phi Person.first Number.singular).toCell.bind (Agreement.Paradigm.realize (setAExponent Phonology.Segment.Class.consonant)) = some (setAPreC (phi Person.first Number.singular)) ∧ (phi Person.second Number.singular).toCell.bind (Agreement.Paradigm.realize (setAExponent Phonology.Segment.Class.consonant)) = some (setAPreC (phi Person.second Number.singular)) ∧ (phi Person.third Number.plural).toCell.bind (Agreement.Paradigm.realize (setAExponent Phonology.Segment.Class.consonant)) = some (setAPreC (phi Person.third Number.plural)) ∧ (phi Person.first Number.singular).toCell.bind (Agreement.Paradigm.realize (setAExponent Phonology.Segment.Class.vowel)) = some (setAPreV (phi Person.first Number.singular)) ∧ (phi Person.second Number.singular).toCell.bind (Agreement.Paradigm.realize (setAExponent Phonology.Segment.Class.vowel)) = some (setAPreV (phi Person.second Number.singular)) ∧ (phi Person.third Number.plural).toCell.bind (Agreement.Paradigm.realize (setAExponent Phonology.Segment.Class.vowel)) = some (setAPreV (phi Person.third Number.plural))

The same agreement holds for Set A in both following-segment environments: φ.toCell in setAExponent env returns setAPreC φ (pre-consonant) or setAPreV φ (pre-vowel).