Mam Voice System Fragment

@cite{elkins-torrence-brown-2026} @cite{scott-2023}

Minimalist infrastructure for the Mam verbal domain, connecting the language-specific clause sizes to the ClauseSpine and VoiceHead abstractions.

Variety note: Oblique extraction (=(y)a') data is from SJO (San Juan Ostuncalco) Mam via @cite{elkins-torrence-brown-2026}. Antipassive voice data draws on SJA (San Juan Atitán) Mam via @cite{scott-2023}. These are distinct varieties; shared infrastructure (clause spines, Voice heads) is parameterized where possible.

Key Claims

1. Mam transitive clauses project Voice⁰, which bears [uOblique].
2. Mam "aspectless" complements are VoiceP-sized — they lack aspect morphology but still project Voice.
3. Mam infinitival complements are VP-sized — they project only V, without Voice, Appl, or v.
4. The directional auxiliary (Dir⁰) is a Mam-specific head that also bears [uOblique] and can host =(y)a'. Dir is modeled as a light verb (V1 in the verbal template Voice > V1(Dir) > Appl > V2(root)) but is NOT added to Cat as it is not universal.

def Fragments.Mayan.Mam.mamVoice : Minimalism.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 Fragments.Mayan.Mam.mamTransitiveSpine : Minimalism.ClauseSpine

Mam transitive clause spine: full CP with Voice. Projects V, Appl, v, Voice, T, C. =(y)a' possible.

Equations

• Fragments.Mayan.Mam.mamTransitiveSpine = Minimalism.ClauseSpine.cP

def Fragments.Mayan.Mam.mamAspectlessSpine : Minimalism.ClauseSpine

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

Equations

• Fragments.Mayan.Mam.mamAspectlessSpine = Minimalism.ClauseSpine.voiceP

def Fragments.Mayan.Mam.mamInfinitivalSpine : Minimalism.ClauseSpine

Mam infinitival complement spine: VP-sized. Projects only V — no Voice, no Appl, no v. =(y)a' impossible because there is no Voice⁰ to bear [uOblique].

Equations

• Fragments.Mayan.Mam.mamInfinitivalSpine = Minimalism.ClauseSpine.bareVP

structure Fragments.Mayan.Mam.MamDirHead : Type

Mam directional auxiliary head (Dir⁰).

Dir is NOT a universal category — it is specific to Mayan languages. We model it as a language-specific type rather than adding to Cat (which would cascade to fValue, catFamily, epSemanticType, etc.).

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'. Both Voice and Dir independently Agree with an oblique passing through their specifier, yielding multiple =(y)a' along the movement path.

• cislocative : Bool

  Whether the directional is cislocative (toward speaker) or translocative (away from speaker)

• hasUOblique : Bool

  Whether this Dir head carries [uOblique], enabling Agree with passing obliques. Like Voice⁰, Dir⁰ can independently trigger =(y)a' spellout when oblique extraction passes through its domain.

def Fragments.Mayan.Mam.instDecidableEqMamDirHead.decEq (x✝ x✝¹ : MamDirHead) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Mayan.Mam.instDecidableEqMamDirHead : DecidableEq MamDirHead

Equations

• Fragments.Mayan.Mam.instDecidableEqMamDirHead = Fragments.Mayan.Mam.instDecidableEqMamDirHead.decEq

def Fragments.Mayan.Mam.instBEqMamDirHead.beq : MamDirHead → MamDirHead → Bool

Equations

• Fragments.Mayan.Mam.instBEqMamDirHead.beq { cislocative := a, hasUOblique := a_1 } { cislocative := b, hasUOblique := b_1 } = (a == b && a_1 == b_1)
• Fragments.Mayan.Mam.instBEqMamDirHead.beq x✝¹ x✝ = false

instance Fragments.Mayan.Mam.instBEqMamDirHead : BEq MamDirHead

Equations

• Fragments.Mayan.Mam.instBEqMamDirHead = { beq := Fragments.Mayan.Mam.instBEqMamDirHead.beq }

instance Fragments.Mayan.Mam.instReprMamDirHead : Repr MamDirHead

Equations

• Fragments.Mayan.Mam.instReprMamDirHead = { reprPrec := Fragments.Mayan.Mam.instReprMamDirHead.repr }

def Fragments.Mayan.Mam.instReprMamDirHead.repr : MamDirHead → ℕ → Std.Format

Equations

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

def Fragments.Mayan.Mam.MamDirHead.features (d : MamDirHead) : Minimalism.FeatureBundle

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

Equations

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

def Fragments.Mayan.Mam.dirCis : MamDirHead

Cislocative directional with [uOblique]: movement toward deictic center. Carries the same oblique probe as Voice⁰ (Elkins et al. §3.1, ex. 8).

Equations

• Fragments.Mayan.Mam.dirCis = { cislocative := true, hasUOblique := true }

def Fragments.Mayan.Mam.dirTrans : MamDirHead

Translocative directional with [uOblique]: movement away from deictic center.

Equations

• Fragments.Mayan.Mam.dirTrans = { cislocative := false, hasUOblique := true }

theorem Fragments.Mayan.Mam.dirCis_has_uOblique : dirCis.hasUOblique = true

Cislocative Dir carries [uOblique].

theorem Fragments.Mayan.Mam.dirTrans_has_uOblique : dirTrans.hasUOblique = true

Translocative Dir carries [uOblique].

theorem Fragments.Mayan.Mam.dir_features_match_voice : dirCis.features = mamVoice.features

Dir's probe features match Voice's: both carry [uOblique]. This ensures both heads can independently Agree with a passing oblique, yielding multiple =(y)a' along the movement path.

theorem Fragments.Mayan.Mam.mamTransitive_has_voice : mamTransitiveSpine.projects Minimalism.Cat.Voice = true

Mam transitive spine projects Voice.

theorem Fragments.Mayan.Mam.mamAspectless_has_voice : mamAspectlessSpine.projects Minimalism.Cat.Voice = true

Mam aspectless spine projects Voice.

theorem Fragments.Mayan.Mam.mamInfinitival_lacks_voice : mamInfinitivalSpine.projects Minimalism.Cat.Voice = false

Mam infinitival spine does NOT project Voice.

theorem Fragments.Mayan.Mam.mamVoice_has_uOblique : Minimalism.hasUnvaluedFeature mamVoice.features (Minimalism.FeatureVal.oblique false) = true

Mam Voice head carries [uOblique].

theorem Fragments.Mayan.Mam.mamVoice_is_phase : mamVoice.phaseHead = true

Mam Voice is a phase head.

theorem Fragments.Mayan.Mam.mamVoice_assigns_theta : mamVoice.assignsTheta = true

Mam Voice assigns a θ-role (agentive).

def Fragments.Mayan.Mam.eqYaVocab : Minimalism.VocabEntry

Vocabulary entry for =(y)a': maps [+oblique] on Voice⁰ to the exponent "=(y)a'". This is the Vocabulary Insertion rule in DM terms.

Equations

• Fragments.Mayan.Mam.eqYaVocab = { features := [Minimalism.GramFeature.valued (Minimalism.FeatureVal.oblique true)], exponent := "=(y)a'", context := some Minimalism.Cat.Voice }

def Fragments.Mayan.Mam.mamVoiceVocab : Minimalism.Vocabulary

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

Equations

• Fragments.Mayan.Mam.mamVoiceVocab = [Fragments.Mayan.Mam.eqYaVocab]

def Fragments.Mayan.Mam.mamPassiveVoice : Minimalism.VoiceHead

Mam passive Voice head: carries [uOblique] just like agentive Voice. The oblique probe is independent of Voice flavor — changing flavor from agentive to non-thematic does not remove [uOblique]. This is why =(y)a' co-occurs with passive -njtz (Elkins et al. §7.2).

Equations

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

theorem Fragments.Mayan.Mam.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. =(y)a' (conditioned by features) and -njtz (conditioned by flavor) are structurally independent.

def Fragments.Mayan.Mam.mamAntipassiveVoice : Minimalism.VoiceHead

Mam antipassive Voice head.

In antipassive constructions, the agent is still introduced by Voice but receives absolutive case (Set B marking) instead of ergative (Set A). The object is demoted to an oblique introduced by a relational noun. The verb bears the antipassive suffix -(a)n.

Antipassive Voice is NOT a phase head — the subject gets ABS, not ERG. This is the key structural difference from agentive Voice: the clause is syntactically intransitive despite having an agent.

In agent focus / ergative extraction contexts, the antipassive co-occurs with the suffix -ta (@cite{scott-2023}, §2.7.1.3).

Equations

• Fragments.Mayan.Mam.mamAntipassiveVoice = { flavor := Minimalism.VoiceFlavor.antipassive, hasD := true, phaseHead := false }

theorem Fragments.Mayan.Mam.mamAntipassive_assigns_theta : mamAntipassiveVoice.assignsTheta = true

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

theorem Fragments.Mayan.Mam.mamAntipassive_not_phase : mamAntipassiveVoice.phaseHead = false

Antipassive Voice is NOT a phase head.

theorem Fragments.Mayan.Mam.antipassive_vs_agentive : mamAntipassiveVoice.assignsTheta = mamVoice.assignsTheta ∧ mamAntipassiveVoice.phaseHead ≠ mamVoice.phaseHead

Antipassive and agentive Voice differ in phase-head status but both assign θ-roles. This captures the transitivity alternation: same agent, different case on the subject.

def Fragments.Mayan.Mam.mamVoiceSystem : Interfaces.VoiceSystemProfile

Mam voice system: two-way asymmetrical (agentive/passive).

Unlike Toba Batak's symmetrical pivot system, Mam's agentive voice is the basic form (phase head, overt agent) and passive is derived (non-phase, implicit agent). Voice does not determine pivot for extraction — instead, Voice carries [uOblique] which conditions extraction morphology (=(y)a').

Equations

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

theorem Fragments.Mayan.Mam.mam_voice_system_asymmetrical : mamVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.asymmetrical

theorem Fragments.Mayan.Mam.mam_voice_count : mamVoiceSystem.voiceCount = 3

theorem Fragments.Mayan.Mam.mam_not_simple_active_passive : mamVoiceSystem.isActivePassive = false

Mam is not a simple active/passive system — it also has antipassive.

theorem Fragments.Mayan.Mam.mam_no_oblique_pivots : mamVoiceSystem.distinguishesObliques = false