Oblique Extraction in Mayan

@cite{elkins-torrence-brown-2026} @cite{mendes-ranero-2021} @cite{imanishi-2020}

Part I: Cross-Linguistic Comparison

Cross-linguistic comparison of extraction morphology in two Mayan language groups: SJO Mam (=(y)a') and K'ichean (wi). Both mark oblique extraction with a dedicated morpheme, but the underlying mechanisms and distributional properties differ.

Shared Properties

• Both mark oblique extraction (spatial, instrumental)
• Both exempt temporal obliques ('when')
• Neither marks subject extraction (Agent Focus instead)
• Neither marks object extraction

Parametric Differences

Property	Mam =(y)a'	K'ichean wi
Locus	On probe (Voice⁰)	At extraction site
Mechanism	Agree reflex	Copy spellout
Reason obliques ('why')	=(y)a' ✓	wi ✗
FPG (matrix wi ↔ embedded comp)	Does not hold	Holds
Conditioned by clause size	Yes (Voice project.)	No
Multiple spellout in LD	Yes (per Voice/Dir)	Unclear

Part II: Minimalist Analysis

Connects three Minimalist abstractions — ClauseSpine, Agree/feature-valuation, and Spellout — to the empirical data on =(y)a' distribution in SJO Mam.

1. Voice⁰ (and Dir⁰) in Mam carry [uOblique] (an unvalued probe feature).
2. When an oblique DP undergoes successive-cyclic Ā-movement through Spec,VoiceP, Agree values [uOblique] as [+oblique] on Voice⁰.
3. At Spellout (PF), [+oblique] on Voice⁰ is realized as =(y)a'.
4. In infinitival complements, Voice is not projected (VP-sized), so there is no [uOblique] probe — =(y)a' cannot appear.
5. In long-distance extraction, each Voice⁰/Dir⁰ along the movement path independently Agrees, yielding multiple =(y)a' (one per Voice/Dir).

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.both_mark_oblique : Fragments.Mayan.Mam.mamExtractionProfile.strategy = Typology.ExtractionMarkingStrategy.dedicatedMorpheme ∧ Fragments.Mayan.Kiche.kicheanExtractionProfile.strategy = Typology.ExtractionMarkingStrategy.dedicatedMorpheme

Both Mam and K'ichean use dedicated morphemes for oblique extraction.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.both_exempt_temporal : (Fragments.Mayan.Mam.temporalOblExtraction.isTemporal = true ∧ Fragments.Mayan.Mam.temporalOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked) ∧ Fragments.Mayan.Kiche.temporalOblExtraction.wiLicensed = false

Both exempt temporal obliques from extraction marking.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.neither_marks_subject : Fragments.Mayan.Mam.transSubjExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Kiche.subjectExtraction.wiLicensed = false

Neither marks subject extraction (Agent Focus instead).

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.neither_marks_object : Fragments.Mayan.Mam.transObjExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Kiche.objectExtraction.wiLicensed = false

Neither marks object extraction.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.reason_oblique_contrast : Fragments.Mayan.Mam.transOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Kiche.reasonOblExtraction.wiLicensed = false

KEY CONTRAST — Reason obliques ('why'): Mam =(y)a' IS licensed with reason extraction; K'ichean wi is NOT.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.clause_size_sensitivity : Fragments.Mayan.Mam.MamClauseType.fullCP.projectsVoice = true ∧ Fragments.Mayan.Mam.MamClauseType.aspectless.projectsVoice = true ∧ Fragments.Mayan.Mam.MamClauseType.infinitival.projectsVoice = false

Mam =(y)a' is conditioned by clause size (Voice must project); K'ichean wi is conditioned by complementizer presence (FPG).

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.kichean_fpg_holds : (Fragments.Mayan.Kiche.ldData.all fun (d : Fragments.Mayan.Kiche.KicheLongDistanceDatum) => d.embeddedType.hasComp == d.wiOnMatrix) = true

The FPG holds for K'ichean: matrix wi tracks overt complementizer.

inductive Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism : Type

Genuinely different mechanisms producing superficially similar patterns.

• agreeReflex : ExtractionMorphologyMechanism
• copySpellout : ExtractionMorphologyMechanism

@[implicit_reducible]

instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqExtractionMorphologyMechanism : DecidableEq ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqExtractionMorphologyMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism.repr : ExtractionMorphologyMechanism → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprExtractionMorphologyMechanism : Repr ExtractionMorphologyMechanism

Equations

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

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamMechanism : ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamMechanism = Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism.agreeReflex

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.kicheanMechanism : ExtractionMorphologyMechanism

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.kicheanMechanism = Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.ExtractionMorphologyMechanism.copySpellout

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.different_mechanisms : mamMechanism ≠ kicheanMechanism

Mam Voice substrate (Minimalist)

This subsection houses the Minimalist VoiceHead, ClauseSpine, and MamDirHead definitions for Mam, formerly in Linglib/Fragments/Mayan/Mam/VoiceSystem.lean. Per CLAUDE.md "Per-language paper-specific apparatus lives in Studies, not Fragments," these belong with the paper that anchors them (@cite{elkins-torrence-brown-2026} for the =(y)a' analysis; @cite{scott-2023} for the antipassive). The Fragment file retains only the theory-neutral mamVoiceSystem : VoiceSystemProfile.

Phenomena/Agreement/Studies/Scott2023.lean consumes mamVoice and eqYaVocab from this file via cross-Studies import.

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamVoice : Minimalist.VoiceHead

Mam agentive Voice head with [uOblique] probe.

In Mam, Voice⁰ probes for an oblique feature on a passing Ā-moved constituent. When an oblique DP moves through Spec,VoiceP, Agree values [uOblique] as [+oblique], which is then spelled out as =(y)a' at PF.

Equations

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

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamTransitiveSpine : Minimalist.ClauseSpine

Mam transitive clause spine: full CP with Voice.

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamTransitiveSpine = Minimalist.ClauseSpine.cP

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAspectlessSpine : Minimalist.ClauseSpine

Mam aspectless complement spine: VoiceP-sized. Still has Voice → =(y)a' possible.

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAspectlessSpine = Minimalist.ClauseSpine.voiceP

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamInfinitivalSpine : Minimalist.ClauseSpine

Mam infinitival complement spine: VP-sized. No Voice → =(y)a' impossible.

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamInfinitivalSpine = Minimalist.ClauseSpine.bareVP

structure Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.MamDirHead : Type

Mam directional auxiliary head (Dir⁰).

Dir is NOT a universal category — it is specific to Mayan languages. Modeled as a language-specific type rather than added to Cat. In Elkins et al.'s analysis, Dir⁰ occupies V1 position in the verbal template (Voice > V1(Dir) > Appl > V2(root)). Like Voice⁰, Dir⁰ bears [uOblique] and can host =(y)a'.

• cislocative : Bool

  Cislocative (toward speaker) vs translocative (away).

• hasUOblique : Bool

  Whether this Dir head carries [uOblique].

@[implicit_reducible]

instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqMamDirHead : DecidableEq MamDirHead

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqMamDirHead = Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqMamDirHead.decEq

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instDecidableEqMamDirHead.decEq (x✝ x✝¹ : MamDirHead) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprMamDirHead.repr : MamDirHead → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprMamDirHead : Repr MamDirHead

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprMamDirHead = { reprPrec := Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.instReprMamDirHead.repr }

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.MamDirHead.features (d : MamDirHead) : Minimalist.FeatureBundle

Dir⁰'s probe features when it carries [uOblique].

Equations

• d.features = if d.hasUOblique = true then [Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.oblique false)] else []

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dirCis : MamDirHead

Cislocative directional with [uOblique].

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dirCis = { cislocative := true, hasUOblique := true }

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dirTrans : MamDirHead

Translocative directional with [uOblique].

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dirTrans = { cislocative := false, hasUOblique := true }

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.eqYaVocab : Minimalist.VocabEntry

Vocabulary entry for =(y)a': maps [+oblique] on Voice⁰ to "=(y)a'".

Equations

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

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamVoiceVocab : Minimalist.Vocabulary

The Mam Voice vocabulary: just the =(y)a' entry.

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamVoiceVocab = [Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.eqYaVocab]

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamPassiveVoice : Minimalist.VoiceHead

Mam passive Voice head: carries [uOblique] just like agentive Voice. @cite{elkins-torrence-brown-2026} §7.2: =(y)a' co-occurs with passive -njtz.

Equations

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

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAntipassiveVoice : Minimalist.VoiceHead

Mam antipassive Voice head (@cite{scott-2023} §2.5.4.1). Subject gets ABS not ERG; not a phase head.

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAntipassiveVoice = { flavor := Minimalist.VoiceFlavor.antipassive, hasD := true }

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamVoice_has_uOblique : Minimalist.hasUnvaluedFeature mamVoice.features (Minimalist.FeatureVal.oblique false) = true

Mam Voice head carries [uOblique].

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamVoice_is_phase : mamVoice.IsPhasal

Mam Voice is a phase head.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamVoice_assigns_theta : mamVoice.AssignsTheta

Mam Voice assigns a θ-role (agentive).

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamTransitive_has_voice : mamTransitiveSpine.projects Minimalist.Cat.Voice = true

Mam transitive spine projects Voice.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAspectless_has_voice : mamAspectlessSpine.projects Minimalist.Cat.Voice = true

Mam aspectless spine projects Voice.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamInfinitival_lacks_voice : mamInfinitivalSpine.projects Minimalist.Cat.Voice = false

Mam infinitival spine does NOT project Voice.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dirCis_has_uOblique : dirCis.hasUOblique = true

Cislocative Dir carries [uOblique].

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dirTrans_has_uOblique : dirTrans.hasUOblique = true

Translocative Dir carries [uOblique].

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dir_features_match_voice : dirCis.features = mamVoice.features

Dir's probe features match Voice's.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.passive_voice_same_features : mamPassiveVoice.features = mamVoice.features ∧ mamPassiveVoice.flavor ≠ mamVoice.flavor

Passive and agentive Voice differ in flavor but share the same oblique probe features.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAntipassive_assigns_theta : mamAntipassiveVoice.AssignsTheta

Antipassive Voice assigns a θ-role (the agent is present).

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAntipassive_not_phase : ¬mamAntipassiveVoice.IsPhasal

Antipassive Voice is NOT a phase head.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.antipassive_vs_agentive : (mamAntipassiveVoice.AssignsTheta ↔ mamVoice.AssignsTheta) ∧ (mamAntipassiveVoice.IsPhasal ↔ ¬mamVoice.IsPhasal)

Antipassive and agentive Voice differ in phase-head status but both assign θ-roles.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spellout_oblique_voice : Minimalist.spellout mamVoiceVocab [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] (some Minimalist.Cat.Voice) = some "=(y)a'"

Valued [+oblique] on Voice spells out as =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spellout_no_oblique : Minimalist.spellout mamVoiceVocab [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique false)] (some Minimalist.Cat.Voice) = none

Without [+oblique], Voice has no exponent from this vocabulary.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spellout_oblique_wrong_context : Minimalist.spellout mamVoiceVocab [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] (some Minimalist.Cat.T) = none

[+oblique] on a non-Voice head does not yield =(y)a' (context restriction blocks insertion).

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.predictEqYa (spine : Minimalist.ClauseSpine) (obliqueExtracted : Bool) (isTemporal : Bool := false) : Fragments.Mayan.Mam.MamExtractionJudgment

Predict whether =(y)a' is licensed from a clause spine and extraction type.

Equations

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

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_trans_obl : mamTransitiveSpine.projects Minimalist.Cat.Voice = true ∧ predictEqYa mamTransitiveSpine true = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.transOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

Transitive clause + oblique extraction → =(y)a' licensed.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_trans_subj : predictEqYa mamTransitiveSpine false = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Mam.transSubjExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked

Transitive + subject extraction → no =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_trans_obj : predictEqYa mamTransitiveSpine false = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Mam.transObjExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked

Transitive + object extraction → no =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_passive_obl : mamTransitiveSpine.projects Minimalist.Cat.Voice = true ∧ predictEqYa mamTransitiveSpine true = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.passiveOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

Passive + oblique → =(y)a' licensed.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_temporal_obl : predictEqYa mamTransitiveSpine true true = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Mam.temporalOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked

Temporal oblique + full clause → =(y)a' BLOCKED.

def Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spineOf : Fragments.Mayan.Mam.MamClauseType → Minimalist.ClauseSpine

Map MamClauseType to the corresponding ClauseSpine.

Equations

• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spineOf Fragments.Mayan.Mam.MamClauseType.fullCP = Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamTransitiveSpine
• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spineOf Fragments.Mayan.Mam.MamClauseType.aspectless = Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamAspectlessSpine
• Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.spineOf Fragments.Mayan.Mam.MamClauseType.infinitival = Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.mamInfinitivalSpine

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_ld_fullCP : (spineOf Fragments.Mayan.Mam.ldFullCP.embeddedClauseType).projects Minimalist.Cat.Voice = true ∧ Fragments.Mayan.Mam.ldFullCP.matrixJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.ldFullCP.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

LD from full CP → =(y)a' licensed on both predicates.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_ld_aspectless : (spineOf Fragments.Mayan.Mam.ldAspectless.embeddedClauseType).projects Minimalist.Cat.Voice = true ∧ Fragments.Mayan.Mam.ldAspectless.matrixJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.ldAspectless.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

LD from aspectless → =(y)a' licensed on both.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_ld_infinitival : (spineOf Fragments.Mayan.Mam.ldInfinitival.embeddedClauseType).projects Minimalist.Cat.Voice = false ∧ Fragments.Mayan.Mam.ldInfinitival.matrixJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.ldInfinitival.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked

LD from infinitival → =(y)a' on matrix only.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.bridge_ld_eq : Fragments.Mayan.Mam.ldEmbeddedQuestion.matrixJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Mam.ldEmbeddedQuestion.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

EQ → =(y)a' on embedded only.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.all_mono_predictions_match : (Fragments.Mayan.Mam.monoData.all fun (d : Fragments.Mayan.Mam.MamExtractionDatum) => predictEqYa (spineOf d.clauseType) d.obliqueExtracted d.isTemporal == d.judgment) = true

All monoclausal predictions match.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.all_ld_embedded_predictions_match : (Fragments.Mayan.Mam.ldData.all fun (d : Fragments.Mayan.Mam.MamLongDistanceDatum) => d.embeddedClauseType.projectsVoice == (d.embeddedJudgment == Fragments.Mayan.Mam.MamExtractionJudgment.licensed)) = true

All LD embedded predictions match.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.eqya_not_resumptive : Fragments.Mayan.Mam.eqyaIslandSensitive = true

Against resumptive-pronoun analysis: =(y)a' is island-sensitive.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.eqya_not_agent_focus : mamPassiveVoice.features = mamVoice.features ∧ mamPassiveVoice.flavor ≠ mamVoice.flavor ∧ Fragments.Mayan.Mam.passiveOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.transSubjExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked ∧ Fragments.Mayan.Mam.transOblExtraction.judgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed

Against Agent Focus analysis: =(y)a' co-occurs with passive voice.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.eqya_not_copy_spellout : (spineOf Fragments.Mayan.Mam.MamClauseType.aspectless).projects Minimalist.Cat.Voice = true ∧ (spineOf Fragments.Mayan.Mam.MamClauseType.infinitival).projects Minimalist.Cat.Voice = false ∧ Fragments.Mayan.Mam.ldAspectless.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.licensed ∧ Fragments.Mayan.Mam.ldInfinitival.embeddedJudgment = Fragments.Mayan.Mam.MamExtractionJudgment.blocked

Against copy spellout: =(y)a' disappears when Voice is absent.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.clauseSpine_finer_than_complementSize : mamAspectlessSpine.projects Minimalist.Cat.Voice = true ∧ mamInfinitivalSpine.projects Minimalist.Cat.Voice = false

ClauseSpine is finer than ComplementSize: it can distinguish infinitival (VP) from aspectless (VoiceP).

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dir_probe_matches_voice : dirCis.features = mamVoice.features

Dir⁰ also carries [uOblique].

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.dir_spellout_eqya : Minimalist.spellout mamVoiceVocab [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] (some Minimalist.Cat.Voice) = some "=(y)a'"

Dir⁰ with valued [+oblique] also spells out as =(y)a'.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.derivation_tree_size : Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.cp✝.nodeCount = 6

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voice_has_uOblique : Minimalist.hasUnvaluedFeature mamVoice.features (Minimalist.FeatureVal.oblique false) = true

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voice_agree_values_oblique : Minimalist.applyAgree mamVoice.features Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.oblique_goal_features✝ (Minimalist.FeatureVal.oblique false) = some [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)]

Agree at Voice: [uOblique] valued by oblique DP's [+oblique].

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voice_spellout_eqya : Minimalist.spellout mamVoiceVocab [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] (some Minimalist.Cat.Voice) = some "=(y)a'"

Spellout: valued [+oblique] on Voice maps to "=(y)a'".

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.full_derivation_pipeline : ((Minimalist.applyAgree mamVoice.features Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.oblique_goal_features✝ (Minimalist.FeatureVal.oblique false)).bind fun (fb : Minimalist.FeatureBundle) => Minimalist.spellout mamVoiceVocab fb (some Minimalist.Cat.Voice)) = some "=(y)a'"

Full derivation pipeline: Agree then Spellout → "=(y)a'".

Voice⁰ in Mam carries two independent probes:

1. φ-probe [uPerson, uNumber] (analyzed by @cite{scott-2023}): Agrees with agent in Spec,VoiceP, yielding Set A morphology.
2. Oblique probe [uOblique] (analyzed by @cite{elkins-torrence-brown-2026}, this file): Agrees with a passing Ā-moved oblique, yielding =(y)a' on Voice⁰.

Both are instances of the same abstract Agree operation: probe searches c-command domain, finds closest matching goal, copies features, and the valued features are spelled out by Vocabulary Insertion. They differ only in which features they probe for and what vocabulary entries match.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.both_probes_unvalued : List.all Scott2023.voiceProbe Minimalist.GramFeature.isUnvalued = true ∧ List.all Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voiceOblProbe✝ Minimalist.GramFeature.isUnvalued = true

Both Voice probes are unvalued features.

theorem Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.phi_and_oblique_agree_parallel : ((Minimalist.applyAgree Scott2023.voiceProbe Scott2023.dp3sg (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Features.Prominence.PersonLevel.third))).bind fun (fb : Minimalist.FeatureBundle) => Minimalist.applyAgree fb Scott2023.dp3sg (Minimalist.FeatureVal.phi (Minimalist.PhiFeature.number Number.sg))) = some Scott2023.voiceFullyAgreed ∧ Minimalist.spellout Scott2023.setAVocab Scott2023.voiceFullyAgreed (some Minimalist.Cat.v) = some "t-" ∧ Minimalist.applyAgree Phenomena.FillerGap.Studies.ElkinsTorrenceBrown2026.voiceOblProbe✝ [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] (Minimalist.FeatureVal.oblique false) = some [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] ∧ Minimalist.spellout [eqYaVocab] [Minimalist.GramFeature.valued (Minimalist.FeatureVal.oblique true)] (some Minimalist.Cat.Voice) = some "=(y)a'"

φ-Agree (Scott 2023) and oblique-Agree (this paper) are parallel instances of the same operation, differing only in which features are probed and which vocabulary entries match.