Kaqchikel Agent Focus Fragment @cite{erlewine-2016}

Theory-neutral typological data for Agent Focus (AF) in Kaqchikel (K'ichean, Mayan): verb-form types, the empirical extraction profile, and the typological AF/extraction-gap classification.

The theory-laden apparatus that interprets this data lives in study files per the project Fragment-discipline rule (CLAUDE.md):

• OT competing-derivations + SSAL/XRef constraints + ranking → Phenomena/FillerGap/Studies/Erlewine2016.lean
• Minimalist Voice/ClauseSpine for Kaqchikel → Phenomena/Ergativity/Studies/CoonMateoPedroPreminger2014.lean

The Paradigm

Extracted arg	Verb form	Agreement
None (declarative)	Transitive	Set A + Set B
Patient/Abs	Transitive	Set A + Set B
Agent/Erg (local)	AF (-Vn)	Set B only
Agent/Erg (long)	Transitive	Set A + Set B

AF is obligatory for clause-local agent extraction and ungrammatical for patient extraction or long-distance agent extraction — it is not a free alternation but a locality-sensitive, structurally conditioned repair. The structural analysis (SSAL ≫ XRef OT competition) lives in the Erlewine2016 study file.

inductive Fragments.Mayan.Kaqchikel.VerbForm : Type

Verbal morphology in a Kaqchikel clause: either the normal transitive form (with Set A ergative agreement) or Agent Focus (with -Vn and no Set A).

• transitive : VerbForm

  Normal transitive: Set A (erg) + Set B (abs) agreement.

• agentFocus : VerbForm

  Agent Focus: suffix -Vn, Set B only, no Set A (erg).

@[implicit_reducible]

instance Fragments.Mayan.Kaqchikel.instDecidableEqVerbForm : DecidableEq VerbForm

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kaqchikel.instReprVerbForm : Repr VerbForm

Equations

• Fragments.Mayan.Kaqchikel.instReprVerbForm = { reprPrec := Fragments.Mayan.Kaqchikel.instReprVerbForm.repr }

def Fragments.Mayan.Kaqchikel.instReprVerbForm.repr : VerbForm → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kaqchikel.VerbForm.hasSetA : VerbForm → Bool

Does this verb form bear ergative (Set A) agreement?

Equations

• Fragments.Mayan.Kaqchikel.VerbForm.transitive.hasSetA = true
• Fragments.Mayan.Kaqchikel.VerbForm.agentFocus.hasSetA = false

def Fragments.Mayan.Kaqchikel.VerbForm.hasAFSuffix : VerbForm → Bool

Does this verb form bear the AF suffix -Vn?

Equations

• Fragments.Mayan.Kaqchikel.VerbForm.transitive.hasAFSuffix = false
• Fragments.Mayan.Kaqchikel.VerbForm.agentFocus.hasAFSuffix = true

structure Fragments.Mayan.Kaqchikel.ExtractionDatum : Type

An extraction datum: which argument is extracted and which verb form surfaces.

• extracted : Typology.ArgumentRole
• verbForm : VerbForm
• judgment : Typology.ExtractionMarkingStrategy

def Fragments.Mayan.Kaqchikel.instReprExtractionDatum.repr : ExtractionDatum → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kaqchikel.instReprExtractionDatum : Repr ExtractionDatum

Equations

• Fragments.Mayan.Kaqchikel.instReprExtractionDatum = { reprPrec := Fragments.Mayan.Kaqchikel.instReprExtractionDatum.repr }

def Fragments.Mayan.Kaqchikel.agentExtractionAF : ExtractionDatum

Agent extraction (clause-local) requires AF.

Equations

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

def Fragments.Mayan.Kaqchikel.agentExtractionTrans : ExtractionDatum

Agent extraction with normal transitive (clause-local) is ungrammatical.

Equations

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

def Fragments.Mayan.Kaqchikel.patientExtractionTrans : ExtractionDatum

Patient extraction uses normal transitive.

Equations

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

def Fragments.Mayan.Kaqchikel.longDistanceAgentExtraction : ExtractionDatum

Long-distance agent extraction uses normal transitive, NOT AF. When the agent extracts from an embedded clause, it passes through intermediate Spec,CP positions via successive-cyclic movement. Each step crosses enough structure to satisfy SSAL — the too-local Spec,TP → Spec,CP step within the embedded clause is avoided.

This is the key evidence that AF is triggered by locality of movement, not simply by agent extraction (@cite{erlewine-2016} §2.3, examples 21–22).

Equations

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

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

Kaqchikel's extraction morphology profile: agent focus alternation. Canonical name extractionProfile (uniform with Chol, Q'anjob'al).

Equations

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

inductive Fragments.Mayan.Kaqchikel.MayanAFType : Type

Mayan languages vary in whether AF is available, depending on the ranking of SSAL vs XRef. This produces a two-way typological split:

• AF languages: SSAL >> XRef. Anti-locality violation is repaired by switching to AF morphology. E.g., Kaqchikel, Q'anjob'al.
• Extraction-gap languages: XRef >> SSAL. No AF repair available; clause-local agent extraction is simply ungrammatical. E.g., Chol.

Both types share the same underlying problem (SSAL blocks clause-local agent extraction); they differ only in whether the grammar provides a repair strategy.

• afLanguage : MayanAFType

  SSAL >> XRef: AF available as repair for anti-locality.

• extractionGap : MayanAFType

  XRef >> SSAL: no repair; extraction gap.

@[implicit_reducible]

instance Fragments.Mayan.Kaqchikel.instDecidableEqMayanAFType : DecidableEq MayanAFType

Equations

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

@[implicit_reducible]

instance Fragments.Mayan.Kaqchikel.instReprMayanAFType : Repr MayanAFType

Equations

• Fragments.Mayan.Kaqchikel.instReprMayanAFType = { reprPrec := Fragments.Mayan.Kaqchikel.instReprMayanAFType.repr }

def Fragments.Mayan.Kaqchikel.instReprMayanAFType.repr : MayanAFType → Nat → Std.Format

Equations

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

def Fragments.Mayan.Kaqchikel.kaqAFType : MayanAFType

Kaqchikel is an AF language (SSAL >> XRef).

Equations

• Fragments.Mayan.Kaqchikel.kaqAFType = Fragments.Mayan.Kaqchikel.MayanAFType.afLanguage

theorem Fragments.Mayan.Kaqchikel.af_no_set_a : VerbForm.agentFocus.hasSetA = false

AF does not bear Set A (ergative) agreement.

theorem Fragments.Mayan.Kaqchikel.trans_has_set_a : VerbForm.transitive.hasSetA = true

Normal transitive does bear Set A agreement.

theorem Fragments.Mayan.Kaqchikel.af_has_suffix : VerbForm.agentFocus.hasAFSuffix = true

AF bears the -Vn suffix.

def Fragments.Mayan.Kaqchikel.kaqVoiceSystem : Interfaces.VoiceSystemProfile

Kaqchikel voice system: two-way asymmetrical (transitive/AF).

Not a true pivot system — AF is a locality-sensitive repair for clause-local agent extraction, not a symmetric voice alternation. Transitive is the basic form; AF is derived (triggered by SSAL).

Equations

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

theorem Fragments.Mayan.Kaqchikel.kaq_voice_system_asymmetrical : kaqVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.asymmetrical

theorem Fragments.Mayan.Kaqchikel.kaq_voice_count : kaqVoiceSystem.voiceCount = 2

theorem Fragments.Mayan.Kaqchikel.kaq_both_promote_agent : (kaqVoiceSystem.voices.all fun (x : Interfaces.VoiceEntry) => x.promotes == Interfaces.PivotTarget.agent) = true

Both Kaqchikel voices promote agent — AF is not a patient-promoting voice but an alternative agent-extracting structure.

theorem Fragments.Mayan.Kaqchikel.kaq_not_active_passive : ¬kaqVoiceSystem.isActivePassive

Kaqchikel is NOT an active/passive system: it lacks a patient-promoting voice.