Documentation

Linglib.Fragments.Mayan.Kaqchikel.Agreement

Kaqchikel Agreement Fragment @cite{preminger-2014} #

Theory-neutral typological metadata for Kaqchikel (K'ichean, Mayan) agreement morphology: paradigm exponents, person-number cells, argument positions, and the empirical AF agreement table.

The theory-laden apparatus that interprets this data — DM Vocabulary insertion, PersonGeometry feature decomposition, the omnivorous hierarchy, the AgreeOutcome inductive — lives in Phenomena/Agreement/Studies/Preminger2014.lean. Per the project Fragment-discipline rule (CLAUDE.md), fragments hold only consensus typological metadata; paper-specific apparatus is consumed in study files via projections.

The System #

Kaqchikel has two agreement paradigms on the verb:

Morpheme order on the verb (276): aspect - ABS - ERG - stem. Set B (ABS) precedes Set A (ERG).

PositionCaseAgreement
A (transitive agent)ERGSet A
P (transitive patient)ABSSet B
S (intransitive subj)ABSSet B

Unlike Mam, where Infl's φ-probe is blocked in transitives and the patient goes unagreed, Kaqchikel cross-references both transitive arguments (@cite{preminger-2014} Ch. 3 vs. @cite{scott-2023} for Mam).

Agent Focus Agreement (@cite{preminger-2014} §3.3, table 22) #

In AF constructions (clause-local agent extraction), the normal two-slot agreement collapses to a single marker drawn from the absolutive (Set B) paradigm. The empirical pattern: AF agreement is commutative (⟨1SG subj, 3SG obj⟩ = ⟨3SG subj, 1SG obj⟩ → in-) and a person restriction blocks combinations of two 1st/2nd-person arguments.

The empirical paradigm data sits here as afParadigm. The choice rule that predicts it is theory-laden — see Phenomena/Agreement/Studies/Preminger2014.lean for the two-probe relativized-probing derivation (after @cite{bejar-rezac-2003}, applied to Kichean per @cite{preminger-2014} §4.4). Earlier analyses (@cite{stiebels-2006} and others) framed the same surface pattern as a salience hierarchy [+participant] > [+plural] > default, an account @cite{preminger-2014} Ch. 7 explicitly argues against; the fragment deliberately avoids picking sides on that question.

source
def Fragments.Mayan.Kaqchikel.absPosition :
ABSPosition

Kaqchikel's absolutive morphemes appear in HIGH position (between aspect marker and the verb stem, pre-stem). Morpheme order: ASP-ABS-ERG-Stem (per ## The System table above).

Equations
Instances For
    source
    def Fragments.Mayan.Kaqchikel.setAExponent :
    PersonNumber → String

    Set A (ERG) markers: prefixes on Voice/v cross-referencing the transitive agent (@cite{preminger-2014} Ch. 3, table (29)). Parenthesized segments are dropped in certain phonological contexts; the grapheme j represents a voiceless velar fricative.

    Equations
    Instances For
      source
      def Fragments.Mayan.Kaqchikel.setBExponent :
      PersonNumber → String

      Set B (ABS) markers: preverbal markers on Infl/T cross-referencing the absolutive argument. The 3SG form (∅) is also the Elsewhere entry — the default when no more specific entry matches, as in the failure case of obligatory agreement (Ch. 5).

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Fragments.Mayan.Kaqchikel.ArgPosition :
        Type

        Argument positions in a Kaqchikel 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 (transitive agent), .P (transitive patient), .S (intransitive subject) directly.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Fragments.Mayan.Kaqchikel.ArgPosition.case :
          ArgPosition → Core.Case

          Perfective (ergative) case assignment for Kaqchikel. Definitionally equal to Fragments.Mayan.ergCaseKaqchikel, which derives from Alignment.ergative.assignCase in Theories/Syntax/Case/Alignment.lean — A → ERG, S/P → ABS.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Fragments.Mayan.Kaqchikel.ArgPosition.accCase :
            ArgPosition → Core.Case

            Non-perfective (PROG ajin) case assignment for Kaqchikel. Definitionally equal to Fragments.Mayan.accCaseKaqchikel, derived from Alignment.invertedErgative.assignCase. The construction-specific inverted pattern (S/A → ABS, P → ERG/GEN) documented by @cite{imanishi-2014} §3.3.1 and @cite{imanishi-2020}. Per @cite{imanishi-2014}: the Unaccusative Requirement on Nominalization passivizes the embedded clause; the object becomes the only Case-less DP and receives ERG/GEN from D as phase head; the subject is base-generated in matrix Spec-PredP (with ajin) and gets ABS from matrix Infl.

            Equations
            Instances For
              source
              def Fragments.Mayan.Kaqchikel.ArgPosition.IsPhiAgreed :
              ArgPosition → Prop

              Does this position participate in φ-Agree? In Kaqchikel, ALL core argument positions trigger agreement: agent via Set A on Voice/v, patient and intranS via Set B on Infl/T. This contrasts with Mam, where the patient is NOT agreed with (Infl's probe is blocked by VoiceP; @cite{scott-2023}). Ditransitive R/T default to participating (Kaqchikel ditransitive agreement not modeled in this fragment).

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Fragments.Mayan.Kaqchikel.instDecidablePredArgPositionIsPhiAgreed :
                DecidablePred ArgPosition.IsPhiAgreed
                Equations
                source
                def Fragments.Mayan.Kaqchikel.kaqArgPositions :
                List ArgPosition

                The three monotransitive argument positions (omits ditransitive R/T).

                Equations
                Instances For
                  source
                  structure Fragments.Mayan.Kaqchikel.AFAgreementDatum :
                  Type

                  An AF agreement datum: subject φ, object φ, and the resulting single agreement marker (or none for person-restriction violations).

                  Instances For
                    source
                    @[implicit_reducible]
                    instance Fragments.Mayan.Kaqchikel.instReprAFAgreementDatum :
                    Repr AFAgreementDatum
                    Equations
                    source
                    def Fragments.Mayan.Kaqchikel.instReprAFAgreementDatum.repr :
                    AFAgreementDatum → ℕ → Std.Format
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Fragments.Mayan.Kaqchikel.afParadigm :
                      List AFAgreementDatum

                      The empirical AF agreement paradigm (@cite{preminger-2014} table (22)). Each row records the observed agreement marker for a given subject-object combination in clause-local agent extraction.

                      The first 11 rows reproduce the paper's table exactly. Rows 12–15 demonstrate commutativity (§3.2, fn. a): the table uses set notation {φ₁, φ₂}, so swapping subj/obj yields the same marker. Rows 16–17 test person restriction violations ((25)).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Fragments.Mayan.Kaqchikel.VerbForm.agreementSlots :
                        VerbForm → ℕ

                        Number of agreement slots for each verb form. Transitive: two slots (Set A + Set B). AF: one slot (single omnivorous marker from the ABS paradigm).

                        Equations
                        Instances For
                          source
                          theorem Fragments.Mayan.Kaqchikel.A_case :
                          ArgPosition.case Features.Prominence.ArgumentRole.A = UD.Case.erg

                          Agent gets ERG (from Voice).

                          source
                          theorem Fragments.Mayan.Kaqchikel.P_case :
                          ArgPosition.case Features.Prominence.ArgumentRole.P = UD.Case.abs

                          Patient gets ABS (from Infl).

                          source
                          theorem Fragments.Mayan.Kaqchikel.S_case :
                          ArgPosition.case Features.Prominence.ArgumentRole.S = UD.Case.abs

                          Intransitive S gets ABS (from Infl).

                          source
                          theorem Fragments.Mayan.Kaqchikel.erg_abs_alignment :
                          ArgPosition.case Features.Prominence.ArgumentRole.A ≠ ArgPosition.case Features.Prominence.ArgumentRole.P ∧ ArgPosition.case Features.Prominence.ArgumentRole.P = ArgPosition.case Features.Prominence.ArgumentRole.S

                          Ergative-absolutive alignment: the agent is distinguished (ERG) while patient and intranS share a case value (ABS).

                          source
                          theorem Fragments.Mayan.Kaqchikel.acc_alignment :
                          ArgPosition.accCase Features.Prominence.ArgumentRole.A = ArgPosition.accCase Features.Prominence.ArgumentRole.S ∧ ArgPosition.accCase Features.Prominence.ArgumentRole.A ≠ ArgPosition.accCase Features.Prominence.ArgumentRole.P

                          Accusative alignment in non-perfective: S/A pattern together (ABS), O is distinct (GEN). Mirror image of Chol/Q'anjob'al.

                          source
                          theorem Fragments.Mayan.Kaqchikel.all_positions_agreed (p : ArgPosition) :
                          p ∈ kaqArgPositions → p.IsPhiAgreed

                          All three argument positions trigger φ-agreement.

                          source
                          theorem Fragments.Mayan.Kaqchikel.af_single_slot :
                          VerbForm.agentFocus.agreementSlots = 1

                          AF has a single agreement slot (one marker from the ABS paradigm).

                          source
                          theorem Fragments.Mayan.Kaqchikel.trans_dual_slots :
                          VerbForm.transitive.agreementSlots = 2

                          Transitive has dual agreement slots (Set A + Set B).

                          source
                          theorem Fragments.Mayan.Kaqchikel.af_no_ergative :
                          VerbForm.agentFocus.hasSetA = false ∧ VerbForm.agentFocus.agreementSlots = 1

                          AF loses ergative (Set A) agreement: the single AF marker is drawn from the absolutive paradigm, not the ergative. Cross-references VerbForm.hasSetA from AgentFocus.lean.

                          source
                          theorem Fragments.Mayan.Kaqchikel.trans_has_ergative :
                          VerbForm.transitive.hasSetA = true ∧ VerbForm.transitive.agreementSlots = 2

                          Transitive retains ergative (Set A) agreement.

                          source
                          def Fragments.Mayan.Kaqchikel.caseInventory :
                          Finset Core.Case

                          Kaqchikel case inventory, derived from argument position case values.

                          Equations
                          Instances For
                            source
                            theorem Fragments.Mayan.Kaqchikel.inventory_covers_positions (p : ArgPosition) :
                            p ∈ kaqArgPositions → p.case ∈ caseInventory

                            The inventory covers all argument positions: every position's case is in the inventory.