Coon, Mateo Pedro & Preminger (2014) @cite{coon-mateo-pedro-preminger-2014}

The role of Case in A-bar extraction asymmetries: Evidence from Mayan. Linguistic Variation 14(2), 179–242.

Core Claim

Syntactic ergativity — the ban on A-bar extracting transitive subjects in languages like Q'anjob'al — is not about properties of the ergative NP. It is a locality problem in case assignment to the absolutive object.

In HIGH-ABS languages (ABS=NOM), Infl⁰ assigns absolutive case. The transitive object must raise out of vP to receive this case, passing through the single escape hatch at the vP phase edge — trapping the subject. In LOW-ABS languages (ABS=DEF), v⁰ assigns absolutive locally within vP. The escape hatch is free and the subject extracts without issue.

The Agent Focus Construction

Q'anjob'al's AF morpheme -on is analyzed as a marked variant of Voice⁰ that assigns structural case to the internal argument (the transitive object). When Voice⁰_AF assigns case, Infl⁰ is freed to assign case to the subject. With the escape hatch unoccupied, the subject can extract. The intransitive status suffix -i surfaces because AF Voice is non-phasal (intransitive v⁰).

The Crazy Antipassive

The same -on morpheme appears in Q'anjob'al non-finite embedded transitives — environments where Infl⁰ is absent and thus cannot assign case to objects. The -on provides the needed case source, further supporting its role as a case-assigner.

Three Factors for Syntactic Ergativity in Q'anjob'al

1. Transitive vP is phasal (constitutes a locality domain)
2. The transitive subject is generated below vP (in Spec,VoiceP)
3. There is only a single specifier available for extraction out of vP

inductive Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase : Type

Abstract case features assigned by functional heads. Following @cite{legate-2008}, "absolutive" is not an abstract case but a descriptive cover term for the morphological form shared by transitive objects and intransitive subjects. The actual abstract cases are:

• NOM: assigned by Infl⁰ (to intransitive subjects universally, and to transitive objects in ABS=NOM languages)
• ACC: assigned by v⁰ (to transitive objects in ABS=DEF languages)
• ERG: assigned by v⁰ (to transitive subjects universally)

• nom : AbstractCase
• acc : AbstractCase
• erg : AbstractCase

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqAbstractCase : DecidableEq AbstractCase

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqAbstractCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqAbstractCase.beq : AbstractCase → AbstractCase → Bool

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqAbstractCase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqAbstractCase : BEq AbstractCase

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqAbstractCase = { beq := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqAbstractCase.beq }

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprAbstractCase : Repr AbstractCase

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprAbstractCase = { reprPrec := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprAbstractCase.repr }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprAbstractCase.repr : AbstractCase → ℕ → Std.Format

Equations

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

inductive Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.FunctionalHead : Type

Which functional head assigns each abstract case.

• infl : FunctionalHead
• v : FunctionalHead

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqFunctionalHead : DecidableEq FunctionalHead

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqFunctionalHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqFunctionalHead.beq : FunctionalHead → FunctionalHead → Bool

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqFunctionalHead.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqFunctionalHead : BEq FunctionalHead

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqFunctionalHead = { beq := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqFunctionalHead.beq }

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprFunctionalHead : Repr FunctionalHead

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprFunctionalHead = { reprPrec := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprFunctionalHead.repr }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprFunctionalHead.repr : FunctionalHead → ℕ → Std.Format

Equations

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

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.assigner : AbstractCase → FunctionalHead

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.nom.assigner = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.FunctionalHead.infl
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.acc.assigner = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.FunctionalHead.v
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.erg.assigner = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.FunctionalHead.v

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.erg_from_v : AbstractCase.erg.assigner = FunctionalHead.v

ERG is always from v⁰, NOM is always from Infl⁰.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.nom_from_infl : AbstractCase.nom.assigner = FunctionalHead.infl

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectAbstractCase : Fragments.Mayan.CaseLocus → AbstractCase

The abstract case assigned to the transitive object depends on the case locus parameter.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectAbstractCase Fragments.Mayan.CaseLocus.absNom = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.nom
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectAbstractCase Fragments.Mayan.CaseLocus.absDef = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.acc

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.subjectAbstractCase (_locus : Fragments.Mayan.CaseLocus) : AbstractCase

Transitive subjects always receive ERG from v⁰, regardless of case locus. This uniformity is the paper's key insight: the variation is in how objects are licensed, not subjects.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.subjectAbstractCase _locus = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.erg

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.subject_case_uniform (l1 l2 : Fragments.Mayan.CaseLocus) : subjectAbstractCase l1 = subjectAbstractCase l2

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectMustExitVP (locus : Fragments.Mayan.CaseLocus) : Bool

Does the object need to move out of vP for case? The object must escape the vP phase domain to reach Infl⁰ iff case is assigned by Infl⁰.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectMustExitVP Fragments.Mayan.CaseLocus.absNom = true
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectMustExitVP Fragments.Mayan.CaseLocus.absDef = false

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectCaseIsExternal (locus : Fragments.Mayan.CaseLocus) : Bool

The object case assigner determines whether the object is licensed inside or outside vP.

Equations

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

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.subjectTrapped (locus : Fragments.Mayan.CaseLocus) (transitive : Bool) : Bool

When the transitive object exits vP through the phase edge (Spec,vP), it occupies the single escape hatch. The subject, base-generated in Spec,VoiceP (below the vP phase boundary), cannot exit the phase domain because the escape hatch is occupied.

This is the paper's core contribution: the ban on extracting transitive subjects follows from a locality problem in how case is assigned to objects, not from any property of the ergative subject itself.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.subjectTrapped locus transitive = (transitive && Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectMustExitVP locus)

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.hasSyntacticErgativity (locus : Fragments.Mayan.CaseLocus) : Bool

Syntactic ergativity: the ban on A-bar extraction of transitive subjects. Predicted to occur iff the language is ABS=NOM (HIGH-ABS).

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.hasSyntacticErgativity locus = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.subjectTrapped locus true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.absNom_has_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absNom = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.absDef_no_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absDef = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.intransitive_subject_never_trapped (locus : Fragments.Mayan.CaseLocus) : subjectTrapped locus false = false

Intransitive subjects are NEVER trapped, regardless of case locus: there is no transitive object to occupy the escape hatch. This correctly predicts that intransitive subjects extract freely in both HIGH-ABS and LOW-ABS languages.

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.voiceAF : Minimalism.VoiceHead

Agent Focus Voice: a marked variant of Voice⁰ that assigns structural case to the internal argument (the transitive object).

Following @cite{ordonez-1995} on Popti', -on assigns case to the object. Unlike regular transitive Voice, AF Voice is NOT a phase head: its v⁰ is the intransitive variety (non-phasal), explaining why the intransitive status suffix -i surfaces rather than transitive -V'.

AF is a "last-resort" strategy, akin to English of-insertion: the marked variant of Voice⁰ is merged only when the normal derivation (with regular transitive Voice) would crash — i.e., when the subject must be A-bar extracted.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.voiceAF = { flavor := Minimalism.VoiceFlavor.agentive, hasD := true, phaseHead := false, checksCase := true }

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_assigns_case : voiceAF.checksCase = true

AF Voice assigns case to the object.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_not_phase : voiceAF.phaseHead = false

AF Voice is NOT a phase head (intransitive v⁰).

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_introduces_agent : voiceAF.assignsTheta = true

AF Voice still introduces an external argument (the agent).

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.afCircumventsTrapping : Bool

AF Voice circumvents the trapping mechanism because it assigns case to the object (so the object need not move to Spec,vP) AND because AF's v⁰ is non-phasal (so vP is not a locality domain). Either property alone would free the subject, but both hold simultaneously for AF Voice.

Equations

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

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_frees_subject : afCircumventsTrapping = true

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.caseAloneFreesExtraction (v : Minimalism.VoiceHead) : Bool

The case-assignment property alone is what frees extraction: when Voice checks case, the object receives case inside vP and need not move to the escape hatch. This is the paper's primary explanation for why AF circumvents the extraction ban.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.caseAloneFreesExtraction v = v.checksCase

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_case_frees : caseAloneFreesExtraction voiceAF = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_morphology_from_phase : voiceAF.phaseHead = false

The non-phasal status explains AF's morphology (intransitive status suffix -i) rather than the extraction facts. Since AF's v⁰ is intransitive, no ergative case is assigned to the subject.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.regular_voice_traps : Minimalism.voiceAgent.phaseHead = true ∧ Minimalism.voiceAgent.checksCase = false

Contrast with regular transitive Voice: phasal, does NOT check case.

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectLicensedInNonFinite (locus : Fragments.Mayan.CaseLocus) : Bool

In non-finite embedded clauses, Infl⁰ is absent (no aspect marking). This makes predictions depending on the case locus:

• ABS=NOM: transitive objects cannot be licensed (Infl⁰ absent). They require -on ("Crazy Antipassive") or detransitivization.
• ABS=DEF: transitive objects are licensed by v⁰ (present even without Infl⁰). They are fine in non-finite clauses.

Intransitive subjects lose absolutive case in BOTH types (Infl⁰ assigns NOM to intransitive subjects universally in Mayan).

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absNom = false
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absDef = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.absNom_objects_unlicensed_nonfinite : objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absNom = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.absDef_objects_licensed_nonfinite : objectLicensedInNonFinite Fragments.Mayan.CaseLocus.absDef = true

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.intranSLicensedInNonFinite (_locus : Fragments.Mayan.CaseLocus) : Bool

Intransitive subjects are unlicensed in non-finite clauses regardless of case locus, because Infl⁰ (the universal NOM assigner for intransitive S) is absent.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.intranSLicensedInNonFinite _locus = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.intranS_unlicensed_nonfinite (locus : Fragments.Mayan.CaseLocus) : intranSLicensedInNonFinite locus = false

inductive Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ObjectType : Type

Some objects do not require structural case: reflexive objects, extended reflexive objects, and bare (determinerless) NPs. These are licensed by pseudo-incorporation into the verb stem (§5.2).

Extended reflexives (possessor bound by subject, e.g., s-na? '3ERG-house') are formally identical to reflexives — the possessed nominal has lost its independent referential meaning.

Prediction: AF is impossible with caseless objects. Since AF exists precisely to assign case to the object, it is vacuous (and thus blocked as last-resort) when the object needs no case.

• fullDP : ObjectType
• reflexive : ObjectType
• extendedReflexive : ObjectType
• bareNP : ObjectType

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqObjectType : DecidableEq ObjectType

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqObjectType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqObjectType : BEq ObjectType

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqObjectType = { beq := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqObjectType.beq }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqObjectType.beq : ObjectType → ObjectType → Bool

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqObjectType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprObjectType.repr : ObjectType → ℕ → Std.Format

Equations

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

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprObjectType : Repr ObjectType

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprObjectType = { reprPrec := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprObjectType.repr }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ObjectType.needsCase : ObjectType → Bool

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ObjectType.fullDP.needsCase = true
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ObjectType.reflexive.needsCase = false
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ObjectType.extendedReflexive.needsCase = false
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ObjectType.bareNP.needsCase = false

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.afAvailable (obj : ObjectType) : Bool

AF is available iff the object needs case.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.afAvailable obj = obj.needsCase

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_available_fullDP : afAvailable ObjectType.fullDP = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_unavailable_reflexive : afAvailable ObjectType.reflexive = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_unavailable_extReflexive : afAvailable ObjectType.extendedReflexive = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_unavailable_bareNP : afAvailable ObjectType.bareNP = false

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.caselessObjectFreesSubject (obj : ObjectType) : Bool

When the object is caseless, regular transitive Voice is used even for agent extraction: the object remains inside vP (no case-driven movement) and does not block the escape hatch. The subject is NOT trapped.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.caselessObjectFreesSubject obj = !obj.needsCase

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.reflexive_frees_subject : caselessObjectFreesSubject ObjectType.reflexive = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobal_has_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absNom = true

Q'anjob'al is a HIGH-ABS language with syntactic ergativity.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.chol_no_syntactic_ergativity : hasSyntacticErgativity Fragments.Mayan.CaseLocus.absDef = false

Chol is a LOW-ABS language without syntactic ergativity.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobal_erg_alignment : Fragments.Mayan.Qanjobal.ArgPosition.agent.ergCase = Minimalism.CaseVal.erg ∧ Fragments.Mayan.Qanjobal.ArgPosition.patient.ergCase = Minimalism.CaseVal.abs

Q'anjob'al's ergative alignment matches the standard pattern: transitive agent = ERG, transitive object = ABS.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.chol_erg_alignment : Fragments.Mayan.Chol.ArgPosition.agent.ergCase = Minimalism.CaseVal.erg ∧ Fragments.Mayan.Chol.ArgPosition.patient.ergCase = Minimalism.CaseVal.abs

Chol's ergative alignment matches the same standard pattern.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.shared_morphology_different_syntax : Fragments.Mayan.Qanjobal.ArgPosition.agent.ergCase = Fragments.Mayan.Chol.ArgPosition.agent.ergCase ∧ hasSyntacticErgativity Fragments.Mayan.CaseLocus.absNom ≠ hasSyntacticErgativity Fragments.Mayan.CaseLocus.absDef

Despite sharing ergative morphology, Q'anjob'al and Chol differ in whether agent extraction is banned. The difference traces to their distinct case loci, not to properties of the ergative NP.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobal_high_abs : Fragments.Mayan.Qanjobal.absPosition = Fragments.Mayan.ABSPosition.high

Fragment-grounded ABSPosition: Q'anjob'al is HIGH-ABS.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.chol_low_abs : Fragments.Mayan.Chol.absPosition = Fragments.Mayan.ABSPosition.low

Fragment-grounded ABSPosition: Chol is LOW-ABS.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.fragments_ground_tada : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.Qanjobal.absPosition) = true ∧ hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.Chol.absPosition) = false

The fragment ABSPosition values derive the correct syntactic ergativity predictions: Q'anjob'al has it, Chol does not. This grounds Tada's Generalization in fragment data rather than hard-coded table entries.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobal_extraction_consistent : Fragments.Mayan.Qanjobal.ExtractionTarget.agent.extractable = false

Q'anjob'al's extraction data is consistent with the prediction: agent extraction is banned in regular transitives.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.chol_extraction_consistent : Fragments.Mayan.Chol.ExtractionTarget.agent.extractable = true

Chol's extraction data is consistent: agent extracts freely.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobal_af_itv : Fragments.Mayan.Qanjobal.agentFocusForm.statusSuffix = Fragments.Mayan.Qanjobal.StatusSuffix.itv

Q'anjob'al's AF form carries the intransitive status suffix, matching the prediction that AF Voice is non-phasal (intransitive v⁰).

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.crazy_ap_unified : Fragments.Mayan.Qanjobal.crazyAntipassiveForm = Fragments.Mayan.Qanjobal.agentFocusForm

The Crazy Antipassive form is identical to AF: same -on morpheme, same intransitive status suffix. Supports the unified analysis of -on as a case-assigner in environments where case is otherwise unavailable.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.chol_nonfinite_predictions : Fragments.Mayan.Chol.absObjectInNonFinite = true ∧ Fragments.Mayan.Chol.absIntranSInNonFinite = false

Non-finite absolutive asymmetry in Chol: objects are available (v⁰ assigns case) but intransitive subjects are not (Infl⁰ absent). Follows from LOW-ABS: v⁰ handles objects, Infl⁰ handles intransitives.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.tada_derived_high : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.high) = true

Tada's Generalization is now DERIVED from the case-assignment analysis rather than merely stated as a correlation. The observable parameter ABSPosition maps to CaseLocus, which determines whether syntactic ergativity arises.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.tada_derived_low : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus Fragments.Mayan.ABSPosition.low) = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.tada_from_case_theory (pos : ABSPosition) : hasSyntacticErgativity (Fragments.Mayan.toCaseLocus pos) = (pos == Fragments.Mayan.ABSPosition.high)

The morphological observation (ABSPosition) and the syntactic observation (extraction asymmetry) are connected through the case-assignment locus: for both values of the parameter, the predicted syntactic ergativity matches what Tada's table reports for the non-outlier languages.

structure Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.SyntacticErgativityFactors : Type

The three factors that combine to produce the ban on extracting transitive subjects in Q'anjob'al. All three are necessary; removing any one would free the subject.

• vPIsPhasal : Bool

  I. Transitive vP is phasal (locality domain).

• subjectBelowVP : Bool

  II. The transitive subject is generated below vP.

• singleEscapeHatch : Bool

  III. Only a single specifier available for extraction out of vP.

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqSyntacticErgativityFactors : DecidableEq SyntacticErgativityFactors

Equations

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

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqSyntacticErgativityFactors.decEq (x✝ x✝¹ : SyntacticErgativityFactors) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqSyntacticErgativityFactors : BEq SyntacticErgativityFactors

Equations

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

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqSyntacticErgativityFactors.beq : SyntacticErgativityFactors → SyntacticErgativityFactors → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqSyntacticErgativityFactors.beq x✝¹ x✝ = false

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprSyntacticErgativityFactors.repr : SyntacticErgativityFactors → ℕ → Std.Format

Equations

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

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprSyntacticErgativityFactors : Repr SyntacticErgativityFactors

Equations

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

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.SyntacticErgativityFactors.producesTrapping (f : SyntacticErgativityFactors) : Bool

Equations

• f.producesTrapping = (f.vPIsPhasal && f.subjectBelowVP && f.singleEscapeHatch)

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobalFactors : SyntacticErgativityFactors

Q'anjob'al instantiates all three factors.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobalFactors = { vPIsPhasal := true, subjectBelowVP := true, singleEscapeHatch := true }

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobal_all_three : qanjobalFactors.producesTrapping = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.factor1_necessary : (have __src := qanjobalFactors; { vPIsPhasal := false, subjectBelowVP := __src.subjectBelowVP, singleEscapeHatch := __src.singleEscapeHatch }).producesTrapping = false

Removing any single factor would free the subject.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.factor2_necessary : (have __src := qanjobalFactors; { vPIsPhasal := __src.vPIsPhasal, subjectBelowVP := false, singleEscapeHatch := __src.singleEscapeHatch }).producesTrapping = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.factor3_necessary : (have __src := qanjobalFactors; { vPIsPhasal := __src.vPIsPhasal, subjectBelowVP := __src.subjectBelowVP, singleEscapeHatch := false }).producesTrapping = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.voice_phase_is_factor1 : Minimalism.voiceAgent.phaseHead = true

Agentive Voice is a phase head — this is factor I.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_removes_factor1 : voiceAF.phaseHead = false

AF removes factor I: AF Voice is not phasal. With a non-phasal vP, there is no locality boundary trapping the subject.

structure Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.ErgativityTypology : Type

The paper's table (10): morphological ergativity and syntactic ergativity are logically independent. Morphological ergativity is shared by all Mayan languages; syntactic ergativity (the extraction ban) arises only in ABS=NOM (HIGH-ABS) languages.

	+morph.erg	-morph.erg
+syntactic ergativity	Q'anjob'al	unattested
-syntactic ergativity	Chol	English

The [-morph,+syn] cell is predicted unattested: syntactic ergativity requires Infl⁰ to assign case to the object, which only arises in morphologically ergative systems.

• morphErg : Bool
• synErg : Bool

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology.decEq (x✝ x✝¹ : ErgativityTypology) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology : DecidableEq ErgativityTypology

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology = Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqErgativityTypology.decEq

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqErgativityTypology : BEq ErgativityTypology

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqErgativityTypology = { beq := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqErgativityTypology.beq }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqErgativityTypology.beq : ErgativityTypology → ErgativityTypology → Bool

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqErgativityTypology.beq { morphErg := a, synErg := a_1 } { morphErg := b, synErg := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqErgativityTypology.beq x✝¹ x✝ = false

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprErgativityTypology : Repr ErgativityTypology

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprErgativityTypology = { reprPrec := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprErgativityTypology.repr }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprErgativityTypology.repr : ErgativityTypology → ℕ → Std.Format

Equations

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

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobalTypology : ErgativityTypology

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.qanjobalTypology = { morphErg := true, synErg := true }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.cholTypology : ErgativityTypology

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.cholTypology = { morphErg := true, synErg := false }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.englishTypology : ErgativityTypology

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.englishTypology = { morphErg := false, synErg := false }

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.morph_erg_necessary_not_sufficient : qanjobalTypology.morphErg = cholTypology.morphErg ∧ qanjobalTypology.synErg ≠ cholTypology.synErg

Morphological ergativity is necessary but not sufficient for syntactic ergativity. Q'anjob'al and Chol are both morphologically ergative but differ in syntactic ergativity.

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.predictedUnattested (t : ErgativityTypology) : Bool

The [-morph.erg, +syn.erg] cell is predicted unattested: syntactic ergativity requires HIGH-ABS (Infl⁰ licensing objects), which entails morphological ergativity.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.predictedUnattested t = (!t.morphErg && t.synErg)

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.unattested_cell : predictedUnattested { morphErg := false, synErg := true } = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.attested_cells : predictedUnattested qanjobalTypology = false ∧ predictedUnattested cholTypology = false ∧ predictedUnattested englishTypology = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_person_restriction : Fragments.Mayan.Qanjobal.PersonRestriction.third.requiresAF = true ∧ Fragments.Mayan.Qanjobal.PersonRestriction.first.requiresAF = false

AF is restricted to 3rd person agents in Q'anjob'al (§5.1, ex. 72). The fragment's PersonRestriction captures this. The theoretical explanation: 1st/2nd person pronouns may be base-generated in Spec,CP (following Baker 2008), so they never need to extract through the vP phase edge — the trapping problem does not arise for them.

The Crazy Antipassive, by contrast, is NOT person-restricted: it applies in ALL non-finite embedded transitives regardless of the person of the subject, because the trigger there is the absence of Infl⁰ (not extraction through a phase edge).

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.crazy_ap_no_person_restriction : Fragments.Mayan.Qanjobal.PersonRestriction.first.requiresCrazyAP = true ∧ Fragments.Mayan.Qanjobal.PersonRestriction.third.requiresCrazyAP = true

inductive Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement : Type

The paper's §5.3 prediction: in HIGH-ABS languages, not only subjects but NOTHING generated inside a transitive vP (besides the object itself) should be able to escape. The object's movement to Spec,vP for case renders the single escape hatch occupied — trapping everything inside the phase domain.

This distinguishes the case-based account from ergative-property accounts: the latter predict only subjects are banned; the former predicts a general vP-internal extraction restriction.

• subject : VPInternalElement
• lowAdverb : VPInternalElement
• secondObject : VPInternalElement

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqVPInternalElement : DecidableEq VPInternalElement

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instDecidableEqVPInternalElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqVPInternalElement : BEq VPInternalElement

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqVPInternalElement = { beq := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqVPInternalElement.beq }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqVPInternalElement.beq : VPInternalElement → VPInternalElement → Bool

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instBEqVPInternalElement.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprVPInternalElement.repr : VPInternalElement → ℕ → Std.Format

Equations

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

instance Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprVPInternalElement : Repr VPInternalElement

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprVPInternalElement = { reprPrec := Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.instReprVPInternalElement.repr }

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.canEscapeHighABS : VPInternalElement → Bool

Can this vP-internal element escape a transitive vP in a HIGH-ABS language? None can — the escape hatch is occupied by the object.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.subject.canEscapeHighABS = false
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.lowAdverb.canEscapeHighABS = false
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.secondObject.canEscapeHighABS = false

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.canEscapeLowABS : VPInternalElement → Bool

In a LOW-ABS language, the escape hatch is free.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.subject.canEscapeLowABS = true
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.lowAdverb.canEscapeLowABS = true
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.VPInternalElement.secondObject.canEscapeLowABS = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.vp_internal_ban_high_abs : VPInternalElement.subject.canEscapeHighABS = false ∧ VPInternalElement.lowAdverb.canEscapeHighABS = false ∧ VPInternalElement.secondObject.canEscapeHighABS = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.vp_internal_free_low_abs : VPInternalElement.subject.canEscapeLowABS = true ∧ VPInternalElement.lowAdverb.canEscapeLowABS = true ∧ VPInternalElement.secondObject.canEscapeLowABS = true

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.hasDoubleObjectConstruction (locus : Fragments.Mayan.CaseLocus) : Bool

Double-object constructions are systematically absent in HIGH-ABS languages (Q'anjob'al, Kaqchikel) but present in LOW-ABS Chol (via applicative). This is consistent with the general vP-internal ban.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absNom = false
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absDef = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.doc_absent_high_abs : hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absNom = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.doc_present_low_abs : hasDoubleObjectConstruction Fragments.Mayan.CaseLocus.absDef = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.reflexive_end_to_end : ObjectType.reflexive.needsCase = false ∧ afAvailable ObjectType.reflexive = false ∧ caselessObjectFreesSubject ObjectType.reflexive = true

End-to-end argumentation chain for reflexive objects (§5.2):

1. Reflexive objects are caseless (pseudo-incorporated)
2. AF exists to assign case → AF is vacuous with caseless objects
3. With no case-driven movement, the object stays in situ
4. The escape hatch is unoccupied
5. The subject is free to extract using regular transitive Voice
6. Therefore: reflexive + agent extraction = regular transitive form

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.extReflexive_end_to_end : ObjectType.extendedReflexive.needsCase = false ∧ afAvailable ObjectType.extendedReflexive = false ∧ caselessObjectFreesSubject ObjectType.extendedReflexive = true

Extended reflexives (possessor bound by subject) pattern with reflexives: caseless, AF impossible, subject extracts freely. Examples (75a)–(76a) of @cite{coon-mateo-pedro-preminger-2014}.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.fullDP_end_to_end : ObjectType.fullDP.needsCase = true ∧ afAvailable ObjectType.fullDP = true ∧ caselessObjectFreesSubject ObjectType.fullDP = false

Contrast: full DP object requires case → AF needed → AF available.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.voice_phase_bridge : Minimalism.voiceAgent.phaseHead = true ∧ voiceAF.phaseHead = false ∧ Minimalism.voicePassive.phaseHead = false ∧ Minimalism.voiceAnticausative.phaseHead = false

The trapping mechanism is grounded in Phase theory: regular transitive Voice is a phase head (v*), so vP constitutes a locality domain under the PIC. AF Voice is NOT a phase head, so it does not create a phase boundary — the complement remains accessible.

This connects the Boolean phaseHead on VoiceHead to the Phase module's isPhaseHead.

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.voiceTrapsSubject (v : Minimalism.VoiceHead) (locus : Fragments.Mayan.CaseLocus) : Bool

Phase headedness partitions Voice into {trapping, non-trapping}: a Voice head traps the subject iff it is a phase head AND does not itself check case (freeing Infl⁰ to do so).

Equations

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

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.agent_voice_traps_absNom : voiceTrapsSubject Minimalism.voiceAgent Fragments.Mayan.CaseLocus.absNom = true

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.agent_voice_free_absDef : voiceTrapsSubject Minimalism.voiceAgent Fragments.Mayan.CaseLocus.absDef = false

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_voice_never_traps (locus : Fragments.Mayan.CaseLocus) : voiceTrapsSubject voiceAF locus = false

def Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.toCaseVal : AbstractCase → Minimalism.CaseVal

The paper's AbstractCase maps to the framework's CaseVal.

Equations

• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.nom.toCaseVal = Minimalism.CaseVal.nom
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.acc.toCaseVal = Minimalism.CaseVal.acc
• Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.AbstractCase.erg.toCaseVal = Minimalism.CaseVal.erg

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.caseVal_bridge_object (locus : Fragments.Mayan.CaseLocus) : (objectAbstractCase locus).toCaseVal = match locus with | Fragments.Mayan.CaseLocus.absNom => Minimalism.CaseVal.nom | Fragments.Mayan.CaseLocus.absDef => Minimalism.CaseVal.acc

The mapping preserves the assigner structure: ERG comes from v⁰, NOM comes from Infl⁰, and the object case depends on the parameter.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.caseVal_bridge_subject (locus : Fragments.Mayan.CaseLocus) : (subjectAbstractCase locus).toCaseVal = Minimalism.CaseVal.erg

Different Mayan languages circumvent syntactic ergativity through different mechanisms (@cite{coon-mateo-pedro-preminger-2014}, §4.2, §5). Q'anjob'al uses case assignment: Voice_AF assigns case to the object, freeing the escape hatch. Kaqchikel uses an anti-locality repair: AF structure avoids the too-local Spec,TP → Spec,CP movement step (SSAL), at the cost of losing Set A agreement (@cite{erlewine-2016}).

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.af_mechanism_contrast : voiceAF.checksCase = true ∧ Fragments.Mayan.Kaqchikel.kaqVoice.checksCase = false

Q'anjob'al AF Voice checks case; Kaqchikel's regular Voice does NOT. This is the core parametric difference: Q'anjob'al's AF is a case-assigning repair, while Kaqchikel's AF is a locality repair.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.shared_phase_problem : Minimalism.voiceAgent.phaseHead = true ∧ Fragments.Mayan.Kaqchikel.kaqVoice.phaseHead = true

Both languages share the underlying problem: agentive Voice is a phase head, creating a locality boundary that traps the subject.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.both_have_extraction_asymmetries : Fragments.Mayan.Qanjobal.absPosition = Fragments.Mayan.ABSPosition.high ∧ Fragments.Mayan.Qanjobal.ExtractionTarget.agent.extractable = false ∧ Fragments.Mayan.Kaqchikel.kaqAFType = Fragments.Mayan.Kaqchikel.MayanAFType.afLanguage

Both Q'anjob'al and Kaqchikel are HIGH-ABS languages with extraction asymmetries: agent extraction is blocked without AF in both.

theorem Phenomena.Ergativity.Studies.CoonMateoPedroPreminger2014.both_af_lose_setA : Fragments.Mayan.Qanjobal.agentFocusForm.hasSetA = false ∧ Fragments.Mayan.Kaqchikel.VerbForm.agentFocus.hasSetA = false

Kaqchikel AF loses Set A agreement (the agent never enters Spec,TP). Q'anjob'al AF also loses Set A agreement. Same surface morphological effect, different underlying mechanism.