Mam Extraction Morphology Fragment @cite{elkins-imanishi-coon-2026}

Theory-neutral data on extraction morphology in San Juan Ostuncalco (SJO) Mam, a Mayan language spoken in the Western Highlands of Guatemala.

The Phenomenon

When an oblique argument undergoes Ā-movement (wh-movement, focus fronting, relativization) in Mam, the optional enclitic =(y)a' may appear on the verbal complex — specifically on Voice⁰ or Dir⁰ (directional auxiliary). Its distribution is conditioned by two factors:

1. Clause size: =(y)a' is licensed only in clauses that project Voice⁰. In infinitival complements (VP-sized, lacking Voice), =(y)a' is impossible even when an oblique has extracted (Elkins et al. §6).

2. Extraction target: =(y)a' marks specifically oblique extraction. Subject extraction triggers Agent Focus (-a), not =(y)a'. Object extraction triggers neither (§3.1). Temporal obliques ('when') also do not trigger =(y)a' (§8.1).

Key Empirical Finding: Multiple Spellout

In long-distance extraction through full CPs and aspectless clauses, =(y)a' can appear on BOTH the matrix and embedded predicates — one per Voice/Dir head along the successive-cyclic movement path (Table 4, §6.2).

Data Sources

All data from @cite{elkins-imanishi-coon-2026}, "Wh-movement and oblique extraction in SJO Mam". Examples cited by section/example number.

inductive Fragments.Mam.MamClauseType : Type

The three clause sizes relevant for =(y)a' distribution in Mam. These correspond to different structural sizes of the verbal domain (@cite{elkins-imanishi-coon-2026} §6.1, following @cite{coon-2019} and @cite{elkins-imanishi-coon-2026}):

• fullCP: Full finite clause with aspect — projects Voice
• aspectless: VoiceP-sized complement (no aspect) — projects Voice
• infinitival: VP-sized complement — does NOT project Voice

• fullCP : MamClauseType

  Full finite clause with aspect marking. Projects the full verbal spine including Voice. =(y)a' licensed on oblique extraction.

• aspectless : MamClauseType

  VoiceP-sized complement: lacks aspect but projects Voice. =(y)a' licensed on oblique extraction (Elkins et al. §6.1, following @cite{elkins-imanishi-coon-2026}).

• infinitival : MamClauseType

  VP-sized infinitival complement: no Voice projected. =(y)a' impossible — no Voice⁰ to host [oblique] (Elkins et al. §6.1).

instance Fragments.Mam.instDecidableEqMamClauseType : DecidableEq MamClauseType

Equations

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

def Fragments.Mam.instBEqMamClauseType.beq : MamClauseType → MamClauseType → Bool

Equations

• Fragments.Mam.instBEqMamClauseType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mam.instBEqMamClauseType : BEq MamClauseType

Equations

• Fragments.Mam.instBEqMamClauseType = { beq := Fragments.Mam.instBEqMamClauseType.beq }

def Fragments.Mam.instReprMamClauseType.repr : MamClauseType → Nat → Std.Format

Equations

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

instance Fragments.Mam.instReprMamClauseType : Repr MamClauseType

Equations

• Fragments.Mam.instReprMamClauseType = { reprPrec := Fragments.Mam.instReprMamClauseType.repr }

def Fragments.Mam.MamClauseType.projectsVoice : MamClauseType → Bool

Does this clause type project Voice?

Equations

• Fragments.Mam.MamClauseType.fullCP.projectsVoice = true
• Fragments.Mam.MamClauseType.aspectless.projectsVoice = true
• Fragments.Mam.MamClauseType.infinitival.projectsVoice = false

inductive Fragments.Mam.MamExtractionJudgment : Type

Judgment on the status of =(y)a' in a given configuration. Note: =(y)a' is an optional enclitic. licensed means =(y)a' may grammatically appear; blocked means it may not. The optionality of =(y)a' when licensed is orthogonal to its distributional constraints.

• licensed : MamExtractionJudgment

  =(y)a' is licensed (may appear) in this configuration

• blocked : MamExtractionJudgment

  =(y)a' is blocked (may not appear) in this configuration

instance Fragments.Mam.instDecidableEqMamExtractionJudgment : DecidableEq MamExtractionJudgment

Equations

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

def Fragments.Mam.instBEqMamExtractionJudgment.beq : MamExtractionJudgment → MamExtractionJudgment → Bool

Equations

• Fragments.Mam.instBEqMamExtractionJudgment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Mam.instBEqMamExtractionJudgment : BEq MamExtractionJudgment

Equations

• Fragments.Mam.instBEqMamExtractionJudgment = { beq := Fragments.Mam.instBEqMamExtractionJudgment.beq }

instance Fragments.Mam.instReprMamExtractionJudgment : Repr MamExtractionJudgment

Equations

• Fragments.Mam.instReprMamExtractionJudgment = { reprPrec := Fragments.Mam.instReprMamExtractionJudgment.repr }

def Fragments.Mam.instReprMamExtractionJudgment.repr : MamExtractionJudgment → Nat → Std.Format

Equations

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

structure Fragments.Mam.MamExtractionDatum : Type

A monoclausal extraction data point: a clause type, what is extracted, and whether =(y)a' is licensed.

• label : String

  Descriptive label

• reference : String

  Section/example reference in @cite{elkins-imanishi-coon-2026}

• clauseType : MamClauseType

  Type of clause

• obliqueExtracted : Bool

  Is an oblique being extracted?

• isTemporal : Bool

  Is the extracted oblique temporal ('when')? Temporal obliques do not trigger =(y)a' even when they are genuinely oblique and genuinely extracted (§8.1, ex. 56). This is currently unexplained — the paper notes it as an open question: "we leave an account of this for future work" (§8.1). We encode the exemption honestly rather than hiding it by setting obliqueExtracted := false for temporals.

• judgment : MamExtractionJudgment

  Judgment on =(y)a'

def Fragments.Mam.instReprMamExtractionDatum.repr : MamExtractionDatum → Nat → Std.Format

Equations

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

instance Fragments.Mam.instReprMamExtractionDatum : Repr MamExtractionDatum

Equations

• Fragments.Mam.instReprMamExtractionDatum = { reprPrec := Fragments.Mam.instReprMamExtractionDatum.repr }

def Fragments.Mam.transOblExtraction : MamExtractionDatum

Transitive clause, oblique extraction: =(y)a' licensed. "Where did the man buy the tortillas?" — =(y)a' on Dir⁰. Elkins et al. §3.1, ex. (8).

Equations

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

def Fragments.Mam.transSubjExtraction : MamExtractionDatum

Transitive clause, subject extraction: =(y)a' blocked. "Who bought the tortillas?" — Agent Focus (-a) instead, no =(y)a'. Elkins et al. §3.1, ex. (6).

Equations

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

def Fragments.Mam.transObjExtraction : MamExtractionDatum

Transitive clause, object extraction: =(y)a' blocked. "What did the man buy?" — no =(y)a'. Elkins et al. §3.1, ex. (7).

Equations

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

def Fragments.Mam.passiveOblExtraction : MamExtractionDatum

Passive clause, oblique extraction: =(y)a' licensed. "Where were the tortillas bought?" — =(y)a' appears even without agent. Elkins et al. §4.1, ex. (17)–(18).

Equations

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

def Fragments.Mam.temporalOblExtraction : MamExtractionDatum

Temporal oblique extraction: =(y)a' BLOCKED. "When" (b'iix taq) does not trigger =(y)a', unlike spatial and other obliques. Elkins et al. §8.1, ex. (56).

Note: temporal obliques ARE obliques and ARE extracted — we encode this honestly with obliqueExtracted := true, isTemporal := true rather than pretending they're not obliques. The exemption is unexplained; the paper notes: "we leave an account of this for future work" (§8.1).

Equations

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

def Fragments.Mam.monoData : List MamExtractionDatum

All monoclausal extraction data points.

Equations

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

structure Fragments.Mam.MamLongDistanceDatum : Type

A long-distance extraction data point: tracks =(y)a' status on both the matrix and embedded predicates independently. This captures the paper's central empirical finding (Table 4, §6.2): =(y)a' can appear on BOTH predicates along the successive-cyclic movement path.

• label : String

  Descriptive label

• reference : String

  Section/example reference

• embeddedClauseType : MamClauseType

  Type of embedded clause

• matrixJudgment : MamExtractionJudgment

  =(y)a' status on the matrix predicate

• embeddedJudgment : MamExtractionJudgment

  =(y)a' status on the embedded predicate

def Fragments.Mam.instReprMamLongDistanceDatum.repr : MamLongDistanceDatum → Nat → Std.Format

Equations

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

instance Fragments.Mam.instReprMamLongDistanceDatum : Repr MamLongDistanceDatum

Equations

• Fragments.Mam.instReprMamLongDistanceDatum = { reprPrec := Fragments.Mam.instReprMamLongDistanceDatum.repr }

def Fragments.Mam.ldFullCP : MamLongDistanceDatum

Long-distance extraction from full CP: =(y)a' licensed on BOTH matrix and embedded predicates. Table 4, Row 1; §6.2, ex. (39)–(40).

Equations

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

def Fragments.Mam.ldAspectless : MamLongDistanceDatum

Long-distance extraction from aspectless clause: =(y)a' licensed on BOTH. Table 4, Row 2; §6.2.

Equations

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

def Fragments.Mam.ldInfinitival : MamLongDistanceDatum

Long-distance extraction from infinitival: =(y)a' licensed on matrix but BLOCKED on embedded. Table 4, Row 3; §6.2, ex. (45)–(46).

Equations

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

def Fragments.Mam.ldEmbeddedQuestion : MamLongDistanceDatum

Embedded question (1-step extraction): =(y)a' BLOCKED on matrix, licensed on embedded. Table 4, Row 4; §4.2, ex. (25)–(26).

Equations

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

def Fragments.Mam.ldData : List MamLongDistanceDatum

All long-distance extraction data points (Table 4).

Equations

• Fragments.Mam.ldData = [Fragments.Mam.ldFullCP, Fragments.Mam.ldAspectless, Fragments.Mam.ldInfinitival, Fragments.Mam.ldEmbeddedQuestion]

theorem Fragments.Mam.trans_obl_licensed : transOblExtraction.judgment = MamExtractionJudgment.licensed

theorem Fragments.Mam.trans_subj_blocked : transSubjExtraction.judgment = MamExtractionJudgment.blocked

theorem Fragments.Mam.trans_obj_blocked : transObjExtraction.judgment = MamExtractionJudgment.blocked

theorem Fragments.Mam.passive_obl_licensed : passiveOblExtraction.judgment = MamExtractionJudgment.licensed

theorem Fragments.Mam.temporal_obl_blocked : temporalOblExtraction.judgment = MamExtractionJudgment.blocked

theorem Fragments.Mam.eqya_iff_voice_and_oblique : (monoData.all fun (d : MamExtractionDatum) => (d.clauseType.projectsVoice && d.obliqueExtracted && !d.isTemporal) == (d.judgment == MamExtractionJudgment.licensed)) = true

Core generalization (monoclausal): =(y)a' is licensed iff the clause projects Voice AND a non-temporal oblique is extracted.

The !d.isTemporal conjunct is a stipulation — the paper does not explain why temporal obliques are exempt (§8.1). It is separated out as a distinct condition rather than hidden in obliqueExtracted.

theorem Fragments.Mam.ld_embedded_tracks_voice : (ldData.all fun (d : MamLongDistanceDatum) => d.embeddedClauseType.projectsVoice == (d.embeddedJudgment == MamExtractionJudgment.licensed)) = true

Multiple spellout: in long-distance extraction, =(y)a' is licensed on each predicate whose clause projects Voice. Matrix clause always projects Voice (it's a full CP).

theorem Fragments.Mam.eqya_tracks_oblique_not_extraction : transSubjExtraction.clauseType = transOblExtraction.clauseType ∧ transObjExtraction.clauseType = transOblExtraction.clauseType ∧ transSubjExtraction.judgment = MamExtractionJudgment.blocked ∧ transObjExtraction.judgment = MamExtractionJudgment.blocked ∧ transOblExtraction.judgment = MamExtractionJudgment.licensed

=(y)a' tracks oblique, not extraction in general: subject and object extraction in the same clause size do not trigger =(y)a'.

theorem Fragments.Mam.temporal_is_oblique_but_exempt : temporalOblExtraction.obliqueExtracted = true ∧ temporalOblExtraction.isTemporal = true ∧ temporalOblExtraction.judgment = MamExtractionJudgment.blocked

Temporal obliques are genuine obliques that undergo genuine extraction, but are exempt from =(y)a' marking. This is an open question.

structure Fragments.Mam.MovementReflex : Type

A morphological reflex of syntactic Ā-movement inherits movement's locality properties. Since Ā-movement is phase-bounded (Phase Impenetrability Condition; Phase.lean), any morpheme that requires movement through a probe's specifier is island-sensitive.

This replaces a stipulated Bool with a derivation from two independent properties:

1. The morpheme requires Ā-movement (established by the Agree analysis)
2. Movement is phase-bounded (from PIC)

References:

• @cite{chomsky-2000} on PIC
• @cite{elkins-imanishi-coon-2026} §7.1 on =(y)a' island sensitivity

• requiresMovement : Bool

  The morpheme is a spellout of features valued via Agree with a constituent that has undergone Ā-movement through the probe's specifier. Established by the Agree analysis in §5.

• movementPhaseBounded : Bool

  Movement is bounded by phases (PIC; Phase.lean). Islands are configurations where the phase edge is unavailable, blocking successive-cyclic movement.

def Fragments.Mam.instDecidableEqMovementReflex.decEq (x✝ x✝¹ : MovementReflex) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Mam.instDecidableEqMovementReflex : DecidableEq MovementReflex

Equations

• Fragments.Mam.instDecidableEqMovementReflex = Fragments.Mam.instDecidableEqMovementReflex.decEq

instance Fragments.Mam.instBEqMovementReflex : BEq MovementReflex

Equations

• Fragments.Mam.instBEqMovementReflex = { beq := Fragments.Mam.instBEqMovementReflex.beq }

def Fragments.Mam.instBEqMovementReflex.beq : MovementReflex → MovementReflex → Bool

Equations

• Fragments.Mam.instBEqMovementReflex.beq { requiresMovement := a, movementPhaseBounded := a_1 } { requiresMovement := b, movementPhaseBounded := b_1 } = (a == b && a_1 == b_1)
• Fragments.Mam.instBEqMovementReflex.beq x✝¹ x✝ = false

instance Fragments.Mam.instReprMovementReflex : Repr MovementReflex

Equations

• Fragments.Mam.instReprMovementReflex = { reprPrec := Fragments.Mam.instReprMovementReflex.repr }

def Fragments.Mam.instReprMovementReflex.repr : MovementReflex → Nat → Std.Format

Equations

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

def Fragments.Mam.MovementReflex.islandSensitive (mr : MovementReflex) : Bool

Island sensitivity is derived: a movement reflex is island-sensitive iff the morpheme requires movement AND movement is phase-bounded. No movement → no Agree → no spellout.

Equations

• mr.islandSensitive = (mr.requiresMovement && mr.movementPhaseBounded)

def Fragments.Mam.eqyaMovementReflex : MovementReflex

=(y)a' is a movement reflex: it requires Ā-movement of the oblique through Spec,VoiceP (so Voice can Agree [uOblique]), and movement is phase-bounded (PIC).

Equations

• Fragments.Mam.eqyaMovementReflex = { requiresMovement := true, movementPhaseBounded := true }

def Fragments.Mam.eqyaIslandSensitive : Bool

Island sensitivity of =(y)a' follows from its being a movement reflex. Derived from requiresMovement ∧ movementPhaseBounded, not stipulated.

Equations

• Fragments.Mam.eqyaIslandSensitive = Fragments.Mam.eqyaMovementReflex.islandSensitive

theorem Fragments.Mam.eqya_island_sensitive_derived : eqyaMovementReflex.islandSensitive = true

Proof that the derivation yields island sensitivity.

theorem Fragments.Mam.passive_oblique_cooccurrence : passiveOblExtraction.judgment = MamExtractionJudgment.licensed

=(y)a' co-occurs with passive voice morphology (-njtz). This is encoded as empirical data: passiveOblExtraction.judgment =.licensed. The co-occurrence is derivable from VoiceHead field independence: passive -njtz is conditioned by VoiceFlavor, while =(y)a' is conditioned by features ([+oblique]). These are independent fields in VoiceHead, so changing the flavor does not affect the features. See MinimalismOblExtraction.eqya_not_agent_focus for the structural derivation. Elkins et al. §7.2, ex. (53)–(54).

def Fragments.Mam.mamExtractionProfile : Interfaces.ExtractionProfile

Mam extraction profile: dedicated morpheme strategy, marks oblique only. Excludes temporal obliques (§8.1).

Equations

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

theorem Fragments.Mam.mam_marks_oblique : mamExtractionProfile.marks Interfaces.ExtractionTarget.oblique = true

theorem Fragments.Mam.mam_no_mark_subject : mamExtractionProfile.marks Interfaces.ExtractionTarget.subject = false