@cite{marantz-1991} — Case and Licensing

@cite{marantz-1991}

Two central claims:

1. Abstract Case ≠ morphological case. NPs are licensed by projection and the EPP, not by Case theory. Morphological case is post-syntactic, inserted at Morphological Structure.

2. Burzio's generalization decomposes into the EPP (sentences need subjects) and the Ergative generalization (no ERG/ACC on non-thematic/derived subjects). The latter concerns morphological case realization, not abstract licensing.

Case Realization Hierarchy

Morphological case obeys a disjunctive hierarchy:

lexically governed > dependent (ACC/ERG) > unmarked > default

This is formalized in DependentCase.lean as CaseSource (lexical > dependent > unmarked). @cite{marantz-1991}'s fourth level, default case (absolute last resort when no other principle applies), is not modeled separately; it is conceptually distinct from unmarked (which is environment-sensitive — e.g., GEN inside NPs, NOM inside IPs) but our current grammar never needs to distinguish them. @cite{baker-2015} later developed the hierarchy into a full cross-linguistic algorithm.

Dependent Case

ACC and ERG are dependent cases — assigned relationally:

• ACC: dependent case assigned to the lower of two caseless NPs
• ERG: dependent case assigned to the higher of two caseless NPs
• The two NPs must be distinct (not in the same chain); this is implicit in our list representation where each NPInDomain is a distinct structural position.

Georgian Split Ergativity

Present series INFL selects accusative alignment → surface NOM-DAT pattern (where DAT is the spell-out of abstract dependent ACC). Aorist series INFL selects ergative alignment → surface ERG-NOM pattern (where NOM is the spell-out of abstract unmarked ABS). Crucially, agreement direction is independent of case direction — the split in case morphology across tense series does NOT correlate with any split in agreement (which always targets the same positions).

Evidential series (DAT-NOM "inversion") is not derived from the dependent case algorithm; it reflects a morphological property of evidential INFL. The algorithm covers present and aorist only.

Abstract Case vs Morphological Case

The dependent case algorithm produces abstract case values (CaseVal). These map to morphological surface forms (Core.Case) via language-specific spell-out at Morphological Structure. In Georgian: abstract ACC → morphological DAT (dative and accusative case have fallen together), abstract ABS → morphological NOM (unmarked surface form).

Case Hierarchy ↔ Agreement Hierarchy

The case realization hierarchy (lexical > dependent > unmarked) parallels the Moravcsik agreement accessibility hierarchy formalized in CaseDiscrimination.lean. Both rank case types identically; the former determines case assignment priority, the latter determines agreement visibility. The bridge sourceToAccessibility connects the two.

def Phenomena.Case.Studies.Marantz1991.alignmentToLangType : Core.AlignmentFamily → Minimalism.CaseLanguageType

Map alignment family to dependent case language type. Bridges the typological description (Core.SplitErgativity) to the case algorithm (DependentCase).

Equations

• Phenomena.Case.Studies.Marantz1991.alignmentToLangType Core.AlignmentFamily.accusative = Minimalism.CaseLanguageType.accusative
• Phenomena.Case.Studies.Marantz1991.alignmentToLangType Core.AlignmentFamily.ergative = Minimalism.CaseLanguageType.ergative

def Phenomena.Case.Studies.Marantz1991.georgianLangType (ts : Fragments.Georgian.Agreement.TenseSeries) : Minimalism.CaseLanguageType

Georgian language type for a given tense series.

Equations

• Phenomena.Case.Studies.Marantz1991.georgianLangType ts = Phenomena.Case.Studies.Marantz1991.alignmentToLangType (Fragments.Georgian.Agreement.georgianSplit.alignment ts)

theorem Phenomena.Case.Studies.Marantz1991.present_is_accusative : georgianLangType Fragments.Georgian.Agreement.TenseSeries.present = Minimalism.CaseLanguageType.accusative

theorem Phenomena.Case.Studies.Marantz1991.aorist_is_ergative : georgianLangType Fragments.Georgian.Agreement.TenseSeries.aorist = Minimalism.CaseLanguageType.ergative

def Phenomena.Case.Studies.Marantz1991.georgianNPs : Fragments.Georgian.Agreement.VerbClass → List Minimalism.NPInDomain

NP configuration for each Georgian verb class (present/aorist).

• Class 1 (transitive): 2 NPs (subject + object), both structural
• Class 2 (unaccusative): 1 NP (sole argument, raised to Spec-TP)
• Class 3 (unergative): 2 positions — subject + empty object. @cite{marantz-1991}: Georgian counts an unfilled object position as a distinct position for dependent case, explaining why unergatives get ERG despite being intransitive.
• Class 4 (psych): 2 NPs — DAT subject (lexical/quirky) + NOM object

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Case.Studies.Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class1 = [{ label := "subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]
• Phenomena.Case.Studies.Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class2 = [{ label := "subj", lexicalCase := none }]
• Phenomena.Case.Studies.Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class3 = [{ label := "subj", lexicalCase := none }, { label := "empty", lexicalCase := none }]

def Phenomena.Case.Studies.Marantz1991.georgianCaseResult (vc : Fragments.Georgian.Agreement.VerbClass) (ts : Fragments.Georgian.Agreement.TenseSeries) : List Minimalism.CasedNP

Run the dependent case algorithm for a Georgian verb class in a given tense series.

Equations

• Phenomena.Case.Studies.Marantz1991.georgianCaseResult vc ts = Minimalism.assignCases (Phenomena.Case.Studies.Marantz1991.georgianLangType ts) (Phenomena.Case.Studies.Marantz1991.georgianNPs vc)

def Phenomena.Case.Studies.Marantz1991.georgianSpellout : Minimalism.CaseVal → Core.Case

Georgian-specific mapping from abstract case (algorithm output) to surface morphological case. This is the language-specific spell-out at Morphological Structure — the locus of @cite{marantz-1991}'s abstract/morphological case distinction.

• Abstract ACC → morphological DAT (dative and accusative morphological case have fallen together in Georgian into what is called "the dative case" — @cite{marantz-1991} p. 12)
• Abstract ABS → morphological NOM (unmarked surface form)
• Abstract ERG → morphological ERG

Equations

• Phenomena.Case.Studies.Marantz1991.georgianSpellout Minimalism.CaseVal.nom = Core.Case.nom
• Phenomena.Case.Studies.Marantz1991.georgianSpellout Minimalism.CaseVal.acc = Core.Case.dat
• Phenomena.Case.Studies.Marantz1991.georgianSpellout Minimalism.CaseVal.erg = Core.Case.erg
• Phenomena.Case.Studies.Marantz1991.georgianSpellout Minimalism.CaseVal.abs = Core.Case.nom
• Phenomena.Case.Studies.Marantz1991.georgianSpellout x✝ = x✝.toCase

theorem Phenomena.Case.Studies.Marantz1991.acc_surfaces_as_dat : georgianSpellout Minimalism.CaseVal.acc = Core.Case.dat

theorem Phenomena.Case.Studies.Marantz1991.abs_surfaces_as_nom : georgianSpellout Minimalism.CaseVal.abs = Core.Case.nom

The dependent case algorithm + Georgian spell-out produces exactly the surface case frames recorded in Fragments.Georgian.Agreement. This is the core empirical validation: the algorithm derives all 8 verb-class × tense combinations for subjects.

theorem Phenomena.Case.Studies.Marantz1991.subject_derivation_matches_fragment : ([Fragments.Georgian.Agreement.VerbClass.class1, Fragments.Georgian.Agreement.VerbClass.class2, Fragments.Georgian.Agreement.VerbClass.class3, Fragments.Georgian.Agreement.VerbClass.class4].all fun (vc : Fragments.Georgian.Agreement.VerbClass) => [Fragments.Georgian.Agreement.TenseSeries.present, Fragments.Georgian.Agreement.TenseSeries.aorist].all fun (ts : Fragments.Georgian.Agreement.TenseSeries) => georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝ "subj" (georgianCaseResult vc ts)) == Fragments.Georgian.Agreement.verbClassSubjectCase vc ts) = true

All subject cases derived from the algorithm match the fragment data.

theorem Phenomena.Case.Studies.Marantz1991.object_derivation_matches : georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.present)) = Core.Case.dat ∧ georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝¹ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist)) = Core.Case.nom ∧ georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝² "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.present)) = Core.Case.nom ∧ georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝³ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.aorist)) = Core.Case.nom

Object cases for transitive classes also match.

@cite{marantz-1991}'s Ergative generalization: ergative case may appear on the subject of an intransitive clause, but not on a derived subject.

Under dependent case, this follows from the NP count: ERG requires
a lower caseless NP as competitor. A derived (raised) unaccusative
subject has no such competitor — the sole NP gets unmarked case.
An unergative subject, by contrast, c-commands an (empty) object
position that Georgian counts as a competitor. 

theorem Phenomena.Case.Studies.Marantz1991.class1_aorist_erg : georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist)) = Core.Case.erg

Class 1 aorist: transitive subject gets ERG.

theorem Phenomena.Case.Studies.Marantz1991.class2_aorist_no_erg : georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class2 Fragments.Georgian.Agreement.TenseSeries.aorist)) = Core.Case.nom

Class 2 aorist: unaccusative subject does NOT get ERG.

theorem Phenomena.Case.Studies.Marantz1991.class3_aorist_erg : georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class3 Fragments.Georgian.Agreement.TenseSeries.aorist)) = Core.Case.erg

Class 3 aorist: unergative subject DOES get ERG (empty object position serves as competitor).

theorem Phenomena.Case.Studies.Marantz1991.class4_lexical_dat : Phenomena.Case.Studies.Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.aorist) = Minimalism.CaseVal.dat ∧ Minimalism.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.aorist) = some Minimalism.CaseSource.lexical

Class 4: quirky DAT takes priority (lexical > dependent).

theorem Phenomena.Case.Studies.Marantz1991.ergative_requires_competitor : Minimalism.getSourceOf "sole" (Minimalism.assignCases Minimalism.CaseLanguageType.ergative [{ label := "sole", lexicalCase := none }]) = some Minimalism.CaseSource.unmarked ∧ Minimalism.getSourceOf "higher" (Minimalism.assignCases Minimalism.CaseLanguageType.ergative [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]) = some Minimalism.CaseSource.dependent

The Ergative generalization follows from NP count: 1 NP (unaccusative) → no ERG; ≥2 positions → ERG possible.

@cite{marantz-1991}'s key insight: Burzio's generalization ("non-thematic subject → no accusative object") splits into:

1. **EPP**: sentences require subjects (projection + EPP suffice)
2. **Dependent case**: ACC requires a *distinct* higher caseless NP
   as competitor

When Voice is non-thematic (unaccusative), no external argument is
introduced. The sole internal argument raises to Spec-TP. Only one
NP exists in the domain → no case competitor → no dependent ACC.

Marantz's counterexamples — adversity passives and "strike" verbs —
have non-thematic subjects AND accusative objects. Under dependent
case, this is predicted: the subject and object occupy *distinct*
structural positions, so the ACC condition IS met. 

theorem Phenomena.Case.Studies.Marantz1991.burzio_unaccusative_no_acc : Minimalism.getCaseOf "theme" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative [{ label := "theme", lexicalCase := none }]) = some Minimalism.CaseVal.nom ∧ Minimalism.getSourceOf "theme" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative [{ label := "theme", lexicalCase := none }]) = some Minimalism.CaseSource.unmarked

Unaccusative: sole NP, no ACC. The "Burzio effect."

theorem Phenomena.Case.Studies.Marantz1991.burzio_transitive_has_acc : Minimalism.getCaseOf "theme" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative [{ label := "agent", lexicalCase := none }, { label := "theme", lexicalCase := none }]) = some Minimalism.CaseVal.acc

Transitive: external argument provides the case competitor → ACC.

theorem Phenomena.Case.Studies.Marantz1991.nonthematic_subject_with_acc : Minimalism.getCaseOf "obj" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative [{ label := "derived_subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]) = some Minimalism.CaseVal.acc

Marantz's counterexample: non-thematic subject with ACC object. Two NPs in distinct chains → dependent case applies despite non-thematic subject. Refutes Burzio's abstract-Case version.

def Phenomena.Case.Studies.Marantz1991.npCount (voice : Minimalism.VoiceHead) (internalArgs : ℕ) : ℕ

Voice determines NP count: θ-assigning Voice adds an external argument. This bridges Voice theory to the configural case algorithm.

Equations

• Phenomena.Case.Studies.Marantz1991.npCount voice internalArgs = if voice.assignsTheta = true then 1 + internalArgs else internalArgs

theorem Phenomena.Case.Studies.Marantz1991.agentive_two_nps : npCount Minimalism.voiceAgent 1 = 2

theorem Phenomena.Case.Studies.Marantz1991.anticausative_one_np : npCount Minimalism.voiceAnticausative 1 = 1

Hindi has aspect-conditioned split ergativity: perfective triggers ERG on the transitive agent (-ne), imperfective has NOM-ACC. The dependent case algorithm derives both patterns from the same mechanism with different CaseLanguageType settings.

@cite{marantz-1991}: Hindi ERG is prohibited on unaccusative subjects
(*siitta (\*ne) aayii* 'Sita arrived'), optional on unergatives, and
obligatory on transitives. The unaccusative prohibition follows from
dependent case: a sole argument has no competitor. 

def Phenomena.Case.Studies.Marantz1991.hindiTransitive (aspect : Core.Aspect) : List Minimalism.CasedNP

Equations

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

theorem Phenomena.Case.Studies.Marantz1991.hindi_perfective_erg : Minimalism.getCaseOf "agent" (hindiTransitive Core.Aspect.perfective) = some Minimalism.CaseVal.erg ∧ Minimalism.getCaseOf "theme" (hindiTransitive Core.Aspect.perfective) = some Minimalism.CaseVal.abs

theorem Phenomena.Case.Studies.Marantz1991.hindi_imperfective_nom_acc : Minimalism.getCaseOf "agent" (hindiTransitive Core.Aspect.imperfective) = some Minimalism.CaseVal.nom ∧ Minimalism.getCaseOf "theme" (hindiTransitive Core.Aspect.imperfective) = some Minimalism.CaseVal.acc

theorem Phenomena.Case.Studies.Marantz1991.hindi_split_is_algorithmic : hindiTransitive Core.Aspect.perfective ≠ hindiTransitive Core.Aspect.imperfective

The split is derived from the same algorithm, not stipulated.

theorem Phenomena.Case.Studies.Marantz1991.hindi_perfective_unaccusative_no_erg : have result := Minimalism.assignCases (alignmentToLangType (Core.hindiSplit.alignment Core.Aspect.perfective)) [{ label := "theme", lexicalCase := none }]; Minimalism.getCaseOf "theme" result = some Minimalism.CaseVal.abs ∧ Minimalism.getSourceOf "theme" result = some Minimalism.CaseSource.unmarked

Hindi perfective unaccusative: sole NP, no ERG. Derives siitta (*ne) aayii — ERG is prohibited on unaccusatives because there is no caseless competitor for dependent case.

theorem Phenomena.Case.Studies.Marantz1991.hindi_perfective_unergative_with_phantom : have result := Minimalism.assignCases (alignmentToLangType (Core.hindiSplit.alignment Core.Aspect.perfective)) [{ label := "subj", lexicalCase := none }, { label := "empty", lexicalCase := none }]; Minimalism.getCaseOf "subj" result = some Minimalism.CaseVal.erg

Hindi unergative in the perfective: the unfilled object position may or may not count as a competitor, yielding optional ERG. With a phantom position (Georgian-style), ERG appears.

theorem Phenomena.Case.Studies.Marantz1991.hindi_perfective_unergative_without_phantom : have result := Minimalism.assignCases (alignmentToLangType (Core.hindiSplit.alignment Core.Aspect.perfective)) [{ label := "subj", lexicalCase := none }]; Minimalism.getCaseOf "subj" result = some Minimalism.CaseVal.abs ∧ Minimalism.getSourceOf "subj" result = some Minimalism.CaseSource.unmarked

Without a phantom position, the unergative subject gets unmarked ABS (= no ERG). This models the optionality as a parameter: does the language count unfilled positions for dependent case?

theorem Phenomena.Case.Studies.Marantz1991.phantom_np_parameter : georgianSpellout (Phenomena.Case.Studies.Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class3 Fragments.Georgian.Agreement.TenseSeries.aorist)) = Core.Case.erg ∧ Minimalism.getCaseOf "subj" (Minimalism.assignCases Minimalism.CaseLanguageType.ergative [{ label := "subj", lexicalCase := none }]) = some Minimalism.CaseVal.abs

Cross-linguistic contrast: Georgian obligatorily counts unfilled positions (Class 3 always gets ERG), while Hindi optionally does (unergative ERG is optional). Both patterns are derived from the same algorithm — the only parameter is whether a phantom NP is included in the domain.

Georgian demonstrates all three levels of @cite{marantz-1991}'s case realization hierarchy within a single language:

| Level     | `CaseSource` | Georgian example |
|-----------|-------------|------------------|
| Lexical   | `.lexical`  | Class 4 DAT (quirky) |
| Dependent | `.dependent`| Class 1 aorist ERG, present ACC |
| Unmarked  | `.unmarked` | Class 2 NOM, Class 1 present NOM | 

theorem Phenomena.Case.Studies.Marantz1991.all_three_sources_attested : Minimalism.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.present) = some Minimalism.CaseSource.lexical ∧ Minimalism.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist) = some Minimalism.CaseSource.dependent ∧ Minimalism.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class2 Fragments.Georgian.Agreement.TenseSeries.aorist) = some Minimalism.CaseSource.unmarked

theorem Phenomena.Case.Studies.Marantz1991.lexical_bleeds_dependent_georgian : Minimalism.getSourceOf "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.present) = some Minimalism.CaseSource.unmarked ∧ Minimalism.getSourceOf "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.present) = some Minimalism.CaseSource.dependent

Lexical case bleeds dependent case: Class 4's DAT subject prevents ACC on the object (no caseless competitor above it).

@cite{marantz-1991}'s case realization hierarchy (lexical > dependent > unmarked) parallels the Moravcsik agreement accessibility hierarchy (@cite{preminger-2014}, formalized in CaseDiscrimination.lean). Both rank case types identically — the same hierarchy governs which case "wins" in realization and which DPs are visible to agreement probes.

The bridge `sourceToAccessibility` connects the two domains. 

def Phenomena.Case.Studies.Marantz1991.sourceToAccessibility : Minimalism.CaseSource → Minimalism.CaseAccessibility

Map case assignment source to agreement accessibility level. The hierarchies are isomorphic: lexical→lexical, dependent→dependent, unmarked→unmarked.

Equations

• Phenomena.Case.Studies.Marantz1991.sourceToAccessibility Minimalism.CaseSource.lexical = Minimalism.CaseAccessibility.lexical
• Phenomena.Case.Studies.Marantz1991.sourceToAccessibility Minimalism.CaseSource.dependent = Minimalism.CaseAccessibility.dependent
• Phenomena.Case.Studies.Marantz1991.sourceToAccessibility Minimalism.CaseSource.unmarked = Minimalism.CaseAccessibility.unmarked

theorem Phenomena.Case.Studies.Marantz1991.accessibility_preserves_rank (s : Minimalism.CaseSource) : (sourceToAccessibility s).rank = match s with | Minimalism.CaseSource.lexical => 0 | Minimalism.CaseSource.dependent => 1 | Minimalism.CaseSource.unmarked => 2

The mapping preserves the rank ordering.

theorem Phenomena.Case.Studies.Marantz1991.class4_lexical_low_accessibility : sourceToAccessibility Minimalism.CaseSource.lexical = Minimalism.CaseAccessibility.lexical ∧ Minimalism.caseAccessible Minimalism.CaseAccessibility.lexical Minimalism.CaseAccessibility.dependent = false

Georgian Class 4's quirky DAT subject has lexical case, which maps to the lowest agreement accessibility. This connects the case algorithm's output to the agreement hierarchy: lexical case DPs are the hardest for agreement probes to target.

theorem Phenomena.Case.Studies.Marantz1991.class1_aorist_dependent_accessibility : sourceToAccessibility Minimalism.CaseSource.dependent = Minimalism.CaseAccessibility.dependent ∧ Minimalism.caseAccessible Minimalism.CaseAccessibility.dependent Minimalism.CaseAccessibility.unmarked = false

Class 1 aorist subject has dependent case (ERG), which maps to middle accessibility. A probe with threshold = unmarked cannot see ERG-marked DPs.

theorem Phenomena.Case.Studies.Marantz1991.class2_unmarked_highest_accessibility : sourceToAccessibility Minimalism.CaseSource.unmarked = Minimalism.CaseAccessibility.unmarked ∧ Minimalism.caseAccessible Minimalism.CaseAccessibility.unmarked Minimalism.CaseAccessibility.unmarked = true

Class 2 aorist subject has unmarked case (NOM), which maps to highest accessibility. Unmarked-case DPs are always visible.

The full argumentation chain from Voice to surface case:

Voice (θ-assigning?) → NP count → dependent case algorithm → spell-out

Agentive Voice introduces an external argument (1 internal + 1 external
= 2 NPs), enabling dependent case. Non-thematic Voice introduces no
external argument (1 internal only), so no case competitor exists and
the sole NP gets unmarked case.

This is @cite{marantz-1991}'s decomposition of Burzio made explicit:
the "Burzio effect" (no ACC without a thematic subject) follows from
Voice's argument structure, not from Case theory. 

def Phenomena.Case.Studies.Marantz1991.npsFromVoice (voice : Minimalism.VoiceHead) : List Minimalism.NPInDomain

Build NP list from Voice: if Voice assigns θ, include both subject and object; otherwise include only the theme.

Equations

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

theorem Phenomena.Case.Studies.Marantz1991.voice_to_case_transitive : Minimalism.getCaseOf "obj" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative (npsFromVoice Minimalism.voiceAgent)) = some Minimalism.CaseVal.acc ∧ Minimalism.getSourceOf "obj" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative (npsFromVoice Minimalism.voiceAgent)) = some Minimalism.CaseSource.dependent

End-to-end: agentive Voice → 2 NPs → object gets dependent ACC.

theorem Phenomena.Case.Studies.Marantz1991.voice_to_case_unaccusative : Minimalism.getCaseOf "theme" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative (npsFromVoice Minimalism.voiceAnticausative)) = some Minimalism.CaseVal.nom ∧ Minimalism.getSourceOf "theme" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative (npsFromVoice Minimalism.voiceAnticausative)) = some Minimalism.CaseSource.unmarked

End-to-end: anticausative Voice → 1 NP → theme gets unmarked NOM.

theorem Phenomena.Case.Studies.Marantz1991.burzio_from_voice : Minimalism.getCaseOf "obj" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative (npsFromVoice Minimalism.voiceAgent)) = some Minimalism.CaseVal.acc ∧ Minimalism.getCaseOf "theme" (Minimalism.assignCases Minimalism.CaseLanguageType.accusative (npsFromVoice Minimalism.voiceAnticausative)) = some Minimalism.CaseVal.nom

The Burzio effect derived end-to-end: ACC presence tracks Voice's θ-assignment. This is the full chain: Voice → NP count → case.

@cite{marantz-1991}'s central insight about Georgian split ergativity: case direction changes by tense series, but agreement does NOT.

Case: present = accusative (ACC downward), aorist = ergative (ERG upward).
Agreement: `pIsIndexed` (object agreement conditioned by person) is the
SAME function regardless of tense series. There is no correlation between
the "directional" features of INFL for case and the "directional" features
of Agr for agreement.

"Split ergativity of the Georgian sort simply exploits this lack of
correlation." This connects to the agreement data formalized in
`Fragments.Georgian.Agreement` and verified in
`Phenomena.Agreement.Studies.Aissen2003` and
`Phenomena.Agreement.Studies.BejarRezac2009`. 

theorem Phenomena.Case.Studies.Marantz1991.case_direction_changes : georgianLangType Fragments.Georgian.Agreement.TenseSeries.present ≠ georgianLangType Fragments.Georgian.Agreement.TenseSeries.aorist

Case direction changes between present and aorist.

theorem Phenomena.Case.Studies.Marantz1991.agreement_invariant_across_series : Fragments.Georgian.Agreement.pIsIndexed Fragments.Georgian.Agreement.PersonNumber.p1sg = true ∧ Fragments.Georgian.Agreement.pIsIndexed Fragments.Georgian.Agreement.PersonNumber.p2sg = true ∧ Fragments.Georgian.Agreement.pIsIndexed Fragments.Georgian.Agreement.PersonNumber.p3sg = false ∧ georgianLangType Fragments.Georgian.Agreement.TenseSeries.present = Minimalism.CaseLanguageType.accusative ∧ georgianLangType Fragments.Georgian.Agreement.TenseSeries.aorist = Minimalism.CaseLanguageType.ergative

Agreement conditioning does NOT change between present and aorist. pIsIndexed — the function determining which objects trigger agreement prefixes — is defined once for all tense series, not parameterized by tense. This is the formal content of agreement-case independence.

theorem Phenomena.Case.Studies.Marantz1991.subject_agreement_invariant : Fragments.Georgian.Agreement.allPersonNumbers.all Fragments.Georgian.Agreement.subjectIsIndexed = true

Subject agreement is non-differential regardless of tense series.

theorem Phenomena.Case.Studies.Marantz1991.case_splits_but_agreement_does_not : Fragments.Georgian.Agreement.verbClassSubjectCase Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.present ≠ Fragments.Georgian.Agreement.verbClassSubjectCase Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist ∧ (Fragments.Georgian.Agreement.allPersonNumbers.all fun (pn : Fragments.Georgian.Agreement.PersonNumber) => Fragments.Georgian.Agreement.pIsIndexed pn == pn.isSAP) = true

The split is in case only, not in agreement. Case patterns differ across tense series (all 4 verb classes checked), but the agreement function pIsIndexed is a single, tense-independent definition — there is no pIsIndexedForSeries.