K'iche' Extraction Morphology Fragment

@cite{elkins-imanishi-coon-2026} @cite{henderson-2008} @cite{imanishi-2020} @cite{mondloch-2017} @cite{lopez-ixcoy-2022}

Theory-neutral data on the extraction particle wi in K'iche' (and more broadly K'ichean Mayan), contrasted with SJO Mam's =(y)a'.

The Phenomenon

When an oblique or PP undergoes Ā-movement in K'ichean languages, the particle wi appears after the verb in the position from which the phrase moved. Its distribution differs from Mam =(y)a' in several key respects:

1. Locus: wi appears at the extraction site (foot of the Ā-chain), while =(y)a' appears on the probe head (Voice⁰/Dir⁰).
2. Analysis: wi is copy spellout, while =(y)a' is an Agree reflex.
3. Reason obliques: wi does NOT appear with reason ('why') extraction; =(y)a' DOES.
4. Fronting Particle Generalization: wi occurs with phrasal (XP) movement but not head (X⁰) movement. This generalization does not hold for =(y)a', which is conditioned by clause size and oblique status, not movement type.

inductive Fragments.Kiche.ExtractedArgType : Type

Types of extracted arguments relevant for wi distribution.

• obliqueSpatial : ExtractedArgType
• obliqueTemporal : ExtractedArgType
• obliqueReason : ExtractedArgType
• obliqueInstrumental : ExtractedArgType
• subject : ExtractedArgType
• object : ExtractedArgType

instance Fragments.Kiche.instDecidableEqExtractedArgType : DecidableEq ExtractedArgType

Equations

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

instance Fragments.Kiche.instBEqExtractedArgType : BEq ExtractedArgType

Equations

• Fragments.Kiche.instBEqExtractedArgType = { beq := Fragments.Kiche.instBEqExtractedArgType.beq }

def Fragments.Kiche.instBEqExtractedArgType.beq : ExtractedArgType → ExtractedArgType → Bool

Equations

• Fragments.Kiche.instBEqExtractedArgType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Kiche.instReprExtractedArgType.repr : ExtractedArgType → Nat → Std.Format

Equations

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

instance Fragments.Kiche.instReprExtractedArgType : Repr ExtractedArgType

Equations

• Fragments.Kiche.instReprExtractedArgType = { reprPrec := Fragments.Kiche.instReprExtractedArgType.repr }

def Fragments.Kiche.ExtractedArgType.isOblique : ExtractedArgType → Bool

Is this argument type an oblique?

Equations

• Fragments.Kiche.ExtractedArgType.obliqueSpatial.isOblique = true
• Fragments.Kiche.ExtractedArgType.obliqueTemporal.isOblique = true
• Fragments.Kiche.ExtractedArgType.obliqueReason.isOblique = true
• Fragments.Kiche.ExtractedArgType.obliqueInstrumental.isOblique = true
• Fragments.Kiche.ExtractedArgType.subject.isOblique = false
• Fragments.Kiche.ExtractedArgType.object.isOblique = false

structure Fragments.Kiche.KicheExtractionDatum : Type

A K'iche' extraction data point: what is extracted and whether wi appears after the verb.

• label : String
• reference : String
• extractedType : ExtractedArgType
• wiLicensed : Bool

def Fragments.Kiche.instReprKicheExtractionDatum.repr : KicheExtractionDatum → Nat → Std.Format

Equations

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

instance Fragments.Kiche.instReprKicheExtractionDatum : Repr KicheExtractionDatum

Equations

• Fragments.Kiche.instReprKicheExtractionDatum = { reprPrec := Fragments.Kiche.instReprKicheExtractionDatum.repr }

def Fragments.Kiche.spatialOblExtraction : KicheExtractionDatum

Spatial oblique extraction: wi licensed. "Where did you buy it?" — wi appears at extraction site. @cite{romero-2012}; @cite{mondloch-2017}.

Equations

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

def Fragments.Kiche.instrumentalOblExtraction : KicheExtractionDatum

Instrumental oblique extraction: wi licensed. "With what did you hit it?" — wi at extraction site. @cite{mondloch-2017}.

Equations

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

def Fragments.Kiche.temporalOblExtraction : KicheExtractionDatum

Temporal oblique extraction: wi NOT licensed. "When did you buy it?" — no wi. Parallel to Mam: temporal obliques are exempt in both language groups. Elkins et al. §8.1.

Equations

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

def Fragments.Kiche.reasonOblExtraction : KicheExtractionDatum

Reason oblique extraction: wi NOT licensed. "Why did you buy it?" — no wi. KEY CONTRAST with Mam: SJO =(y)a' IS licensed with reason extraction. Elkins et al. §8.1.

Equations

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

def Fragments.Kiche.subjectExtraction : KicheExtractionDatum

Subject extraction: wi NOT licensed (Agent Focus instead). "Who bought it?" — AF morphology -Vk instead of wi. @cite{henderson-2008}; @cite{imanishi-2020}.

Equations

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

def Fragments.Kiche.objectExtraction : KicheExtractionDatum

Object extraction: wi NOT licensed. "What did you buy?" — no wi. @cite{romero-2012}.

Equations

• Fragments.Kiche.objectExtraction = { label := "Object extraction (no wi)", reference := "Romero 2012", extractedType := Fragments.Kiche.ExtractedArgType.object, wiLicensed := false }

def Fragments.Kiche.allData : List KicheExtractionDatum

All K'iche' extraction data points.

Equations

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

theorem Fragments.Kiche.wi_subset_of_obliques : (allData.all fun (d : KicheExtractionDatum) => d.wiLicensed == (d.extractedType == ExtractedArgType.obliqueSpatial || d.extractedType == ExtractedArgType.obliqueInstrumental)) = true

wi is licensed only with spatial and instrumental obliques — a proper subset of the oblique types that trigger Mam =(y)a'. Specifically, wi excludes temporal AND reason obliques, while =(y)a' excludes only temporal obliques.

theorem Fragments.Kiche.wi_not_core_args : subjectExtraction.wiLicensed = false ∧ objectExtraction.wiLicensed = false

wi does not appear with subject or object extraction.

theorem Fragments.Kiche.temporal_exempt : temporalOblExtraction.wiLicensed = false

Temporal exemption is shared across Mayan: neither wi (K'ichean) nor =(y)a' (Mam) appears with temporal oblique extraction.

def Fragments.Kiche.frontingParticleGeneralization : Bool

The Fronting Particle Generalization: wi occurs in clauses where phrasal (XP) movement has occurred, but NOT in clauses involving only head (X⁰) movement.

This generalization holds for K'ichean but NOT for Mam =(y)a': =(y)a' is conditioned by clause size (Voice projection) and oblique status, not by movement type (phrasal vs. head).

Elkins et al. §8.2 argue this difference follows from the locus: wi is copy spellout (sensitive to what moved), while =(y)a' is Agree on Voice (sensitive to what Voice probes for).

Equations

• Fragments.Kiche.frontingParticleGeneralization = true

def Fragments.Kiche.kicheanExtractionProfile : Interfaces.ExtractionProfile

K'ichean extraction profile: wi marks oblique extraction via copy spellout at the foot of the Ā-chain.

Equations

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

theorem Fragments.Kiche.kichean_marks_oblique : kicheanExtractionProfile.marks Interfaces.ExtractionTarget.oblique = true