@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 (Core.Case). These map to morphological surface forms (also 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 below as Minimalist.CaseAccessibility from @cite{preminger-2014}). Both rank case types identically; the former determines case assignment priority, the latter determines agreement visibility. The bridge sourceToAccessibility connects the two.

Case-Discrimination Apparatus (relocated from Minimalism/CaseDiscrimination.lean)

The Moravcsik-hierarchy primitives below come from @cite{preminger-2014} (with @cite{bobaljik-2008}, @cite{scott-2023}). They are paper-specific to the case-discrimination tradition that this study is in conversation with, and are not consumed elsewhere in the library, so they live here under namespace Minimalist for symmetry with other Minimalist apparatus.

inductive Minimalist.CaseAccessibility : Type

Case accessibility for agreement.

The hierarchy determines which DPs are visible to agreement probes. Higher accessibility = more likely to be targeted by a probe.

• unmarked : CaseAccessibility

  Unmarked case: NOM (nom-acc) or ABS (erg-abs). Highest.

• dependent : CaseAccessibility

  Dependent case: ACC (nom-acc) or ERG (erg-abs). Middle.

• lexical : CaseAccessibility

  Lexical/oblique case: DAT, GEN, PP, etc. Lowest.

@[implicit_reducible]

instance Minimalist.instDecidableEqCaseAccessibility : DecidableEq CaseAccessibility

Equations

• Minimalist.instDecidableEqCaseAccessibility x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.instReprCaseAccessibility.repr : CaseAccessibility → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCaseAccessibility : Repr CaseAccessibility

Equations

• Minimalist.instReprCaseAccessibility = { reprPrec := Minimalist.instReprCaseAccessibility.repr }

def Minimalist.CaseAccessibility.rank : CaseAccessibility → ℕ

Numeric rank for ordering. Higher = more accessible.

Equations

• Minimalist.CaseAccessibility.unmarked.rank = 2
• Minimalist.CaseAccessibility.dependent.rank = 1
• Minimalist.CaseAccessibility.lexical.rank = 0

def Minimalist.caseAccessible (dpLevel threshold : CaseAccessibility) : Bool

Is a DP with this case level accessible to a probe with the given threshold? Contiguity: a DP is accessible iff its level is at or above the threshold.

Equations

• Minimalist.caseAccessible dpLevel threshold = decide (dpLevel.rank ≥ threshold.rank)

structure Minimalist.CaseAlignment : Type

A case alignment maps argument positions (S, A, P) to case accessibility levels.

• S: intransitive subject (sole argument)
• A: transitive agent (external argument)
• P: transitive patient (internal argument)

• sLevel : CaseAccessibility

  Case accessibility of the intransitive subject.

• aLevel : CaseAccessibility

  Case accessibility of the transitive agent.

• pLevel : CaseAccessibility

  Case accessibility of the transitive patient.

def Minimalist.instReprCaseAlignment.repr : CaseAlignment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Minimalist.instReprCaseAlignment : Repr CaseAlignment

Equations

• Minimalist.instReprCaseAlignment = { reprPrec := Minimalist.instReprCaseAlignment.repr }

def Minimalist.nomAcc : CaseAlignment

Nominative-accusative alignment: S and A both get unmarked (NOM), P gets dependent (ACC).

Equations

• Minimalist.nomAcc = { sLevel := Minimalist.CaseAccessibility.unmarked, aLevel := Minimalist.CaseAccessibility.unmarked, pLevel := Minimalist.CaseAccessibility.dependent }

def Minimalist.ergAbs : CaseAlignment

Ergative-absolutive alignment: S and P both get unmarked (ABS), A gets dependent (ERG).

Equations

• Minimalist.ergAbs = { sLevel := Minimalist.CaseAccessibility.unmarked, aLevel := Minimalist.CaseAccessibility.dependent, pLevel := Minimalist.CaseAccessibility.unmarked }

def Minimalist.tripartite : CaseAlignment

Tripartite alignment: S gets unmarked (ABS), A gets dependent (ERG), P gets dependent (ACC). Mam.

Equations

• Minimalist.tripartite = { sLevel := Minimalist.CaseAccessibility.unmarked, aLevel := Minimalist.CaseAccessibility.dependent, pLevel := Minimalist.CaseAccessibility.dependent }

structure Minimalist.AgreementPattern : Type

Agreement pattern: which argument positions trigger agreement.

• sAgrees : Bool
• aAgrees : Bool
• pAgrees : Bool

@[implicit_reducible]

instance Minimalist.instDecidableEqAgreementPattern : DecidableEq AgreementPattern

Equations

• Minimalist.instDecidableEqAgreementPattern = Minimalist.instDecidableEqAgreementPattern.decEq

def Minimalist.instDecidableEqAgreementPattern.decEq (x✝ x✝¹ : AgreementPattern) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.instReprAgreementPattern : Repr AgreementPattern

Equations

• Minimalist.instReprAgreementPattern = { reprPrec := Minimalist.instReprAgreementPattern.repr }

def Minimalist.instReprAgreementPattern.repr : AgreementPattern → ℕ → Std.Format

Equations

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

def Minimalist.agreementFromThreshold (ca : CaseAlignment) (threshold : CaseAccessibility) : AgreementPattern

Given a case alignment and an accessibility threshold, compute which argument positions are visible to the probe.

Equations

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

def Minimalist.AgreementPattern.isErgAbs (ap : AgreementPattern) : Bool

Is this agreement pattern ergative-absolutive? S and P agree, A does not (S=P≠A).

Equations

• ap.isErgAbs = (ap.sAgrees && ap.pAgrees && !ap.aAgrees)

def Minimalist.AgreementPattern.isNomAcc (ap : AgreementPattern) : Bool

Is this agreement pattern nominative-accusative? S and A agree, P does not (S=A≠P).

Equations

• ap.isNomAcc = (ap.sAgrees && ap.aAgrees && !ap.pAgrees)

def Minimalist.thresholds : List CaseAccessibility

The three possible thresholds.

Equations

• Minimalist.thresholds = [Minimalist.CaseAccessibility.unmarked, Minimalist.CaseAccessibility.dependent, Minimalist.CaseAccessibility.lexical]

theorem Minimalist.nomAcc_a_equals_s (threshold : CaseAccessibility) : (agreementFromThreshold nomAcc threshold).aAgrees = (agreementFromThreshold nomAcc threshold).sAgrees

With NOM-ACC case, A always agrees whenever S agrees (both have unmarked = NOM). Therefore, the pattern S=P≠A (ergative-absolutive agreement) is impossible: you cannot target S without also targeting A.

This is @cite{bobaljik-2008}'s typological gap: NOM-ACC case + ERG-ABS agreement is unattested.

theorem Minimalist.nomAcc_no_ergAbs_agreement (threshold : CaseAccessibility) : (agreementFromThreshold nomAcc threshold).isErgAbs = false

Corollary: ERG-ABS agreement is impossible with NOM-ACC case. No threshold produces S=P≠A under NOM-ACC alignment.

theorem Minimalist.ergAbs_unmarked_yields_abs_agreement : (agreementFromThreshold ergAbs CaseAccessibility.unmarked).isErgAbs = true

With ERG-ABS case, threshold = unmarked yields ABS agreement: S and P agree (both have ABS = unmarked), A does not (ERG = dependent, below threshold). This is ergative-absolutive agreement.

theorem Minimalist.ergAbs_dependent_yields_all : have ap := agreementFromThreshold ergAbs CaseAccessibility.dependent; ap.sAgrees = true ∧ ap.aAgrees = true ∧ ap.pAgrees = true

With ERG-ABS case, threshold = dependent yields agreement with ALL arguments (S, A, P all accessible).

theorem Minimalist.contiguity_unmarked_dependent (threshold : CaseAccessibility) : caseAccessible CaseAccessibility.dependent threshold = true → caseAccessible CaseAccessibility.unmarked threshold = true

Contiguity: if a DP with dependent case is accessible, then any DP with unmarked case is also accessible (unmarked > dependent).

theorem Minimalist.contiguity_lexical (threshold : CaseAccessibility) : caseAccessible CaseAccessibility.lexical threshold = true → caseAccessible CaseAccessibility.dependent threshold = true ∧ caseAccessible CaseAccessibility.unmarked threshold = true

Contiguity: if a DP with lexical case is accessible, then DPs with dependent and unmarked case are also accessible.

structure Minimalist.DativeInterventionContext : Type

Dative intervention: a dative DP blocks the probe's search.

Components:

• dativePresent: a dative DP intervenes between probe and goal
• threshold: the probe's case accessibility threshold
• targetLevel: the case level of the intended goal

• dativePresent : Bool

  A dative (lexical case) DP intervenes.

• threshold : CaseAccessibility

  The probe's case accessibility threshold.

• targetLevel : CaseAccessibility

  Case level of the intended agreement target.

@[implicit_reducible]

instance Minimalist.instReprDativeInterventionContext : Repr DativeInterventionContext

Equations

• Minimalist.instReprDativeInterventionContext = { reprPrec := Minimalist.instReprDativeInterventionContext.repr }

def Minimalist.instReprDativeInterventionContext.repr : DativeInterventionContext → ℕ → Std.Format

Equations

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

def Minimalist.dativeVisibleToProbe (threshold : CaseAccessibility) : Bool

Is the dative visible to the probe? Only if the threshold is low enough to include lexical case.

Equations

• Minimalist.dativeVisibleToProbe threshold = Minimalist.caseAccessible Minimalist.CaseAccessibility.lexical threshold

def Minimalist.dativeIntervenes (ctx : DativeInterventionContext) : Bool

Does dative intervention cause agreement failure?

The dative intervenes (blocks the probe by locality/minimality) if it has matching phi-features. But it cannot be a valid goal because its case (lexical) is below the threshold. The probe fails without crashing.

This is modeled as: if a dative is present AND the dative's case is below the threshold (so the probe can't Agree with it) AND the dative blocks access to the real target by minimality, then agreement fails.

Equations

• Minimalist.dativeIntervenes ctx = (ctx.dativePresent && !Minimalist.dativeVisibleToProbe ctx.threshold)

theorem Minimalist.dative_blocks_at_unmarked : dativeIntervenes { dativePresent := true, threshold := CaseAccessibility.unmarked, targetLevel := CaseAccessibility.unmarked } = true

With a standard threshold (unmarked or dependent), a dative DP causes intervention: it blocks the probe but cannot be agreed with.

theorem Minimalist.dative_blocks_at_dependent : dativeIntervenes { dativePresent := true, threshold := CaseAccessibility.dependent, targetLevel := CaseAccessibility.unmarked } = true

theorem Minimalist.dative_no_intervention_at_lexical : dativeIntervenes { dativePresent := true, threshold := CaseAccessibility.lexical, targetLevel := CaseAccessibility.unmarked } = false

If the threshold includes lexical case, the dative does NOT intervene — it becomes a valid agreement target.

def Minimalist.kaqCaseAlignment : CaseAlignment

Kaqchikel has ergative-absolutive alignment: S and P get ABS (unmarked), A gets ERG (dependent).

Equations

• Minimalist.kaqCaseAlignment = Minimalist.ergAbs

theorem Minimalist.kaq_abs_agreement : (agreementFromThreshold kaqCaseAlignment CaseAccessibility.unmarked).sAgrees = true ∧ (agreementFromThreshold kaqCaseAlignment CaseAccessibility.unmarked).pAgrees = true ∧ (agreementFromThreshold kaqCaseAlignment CaseAccessibility.unmarked).aAgrees = false

Under Kaqchikel's alignment with threshold = unmarked, agreement targets S and P (Set B / absolutive agreement) but not A. This is consistent with the Set B (ABS) paradigm.

theorem Minimalist.kaq_erg_agreement_threshold : (agreementFromThreshold kaqCaseAlignment CaseAccessibility.dependent).aAgrees = true

Kaqchikel Set A agreement targets A (ERG): this requires a separate probe (Voice/v) with threshold = dependent, which sees both unmarked and dependent case DPs.

def Marantz1991.alignmentToLangType : Core.AlignmentFamily → Syntax.Case.CaseLanguageType

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

Equations

• Marantz1991.alignmentToLangType Core.AlignmentFamily.accusative = Syntax.Case.CaseLanguageType.accusative
• Marantz1991.alignmentToLangType Core.AlignmentFamily.ergative = Syntax.Case.CaseLanguageType.ergative

def Marantz1991.georgianLangType (ts : Fragments.Georgian.Agreement.TenseSeries) : Syntax.Case.CaseLanguageType

Georgian language type for a given tense series.

Equations

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

theorem Marantz1991.present_is_accusative : georgianLangType Fragments.Georgian.Agreement.TenseSeries.present = Syntax.Case.CaseLanguageType.accusative

theorem Marantz1991.aorist_is_ergative : georgianLangType Fragments.Georgian.Agreement.TenseSeries.aorist = Syntax.Case.CaseLanguageType.ergative

def Marantz1991.georgianNPs : Fragments.Georgian.Agreement.VerbClass → List Syntax.Case.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

• Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class1 = [{ label := "subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]
• Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class2 = [{ label := "subj", lexicalCase := none }]
• Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class3 = [{ label := "subj", lexicalCase := none }, { label := "empty", lexicalCase := none }]
• Marantz1991.georgianNPs Fragments.Georgian.Agreement.VerbClass.class4 = [{ label := "subj", lexicalCase := some UD.Case.dat }, { label := "obj", lexicalCase := none }]

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

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

Equations

• Marantz1991.georgianCaseResult vc ts = Syntax.Case.assignCases (Marantz1991.georgianLangType ts) (Marantz1991.georgianNPs vc)

def Marantz1991.georgianSpellout : Core.Case → 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

• Marantz1991.georgianSpellout UD.Case.Nom = UD.Case.nom
• Marantz1991.georgianSpellout UD.Case.Acc = UD.Case.dat
• Marantz1991.georgianSpellout UD.Case.Erg = UD.Case.erg
• Marantz1991.georgianSpellout UD.Case.Abs = UD.Case.nom
• Marantz1991.georgianSpellout x✝ = x✝

theorem Marantz1991.acc_surfaces_as_dat : georgianSpellout UD.Case.acc = UD.Case.dat

theorem Marantz1991.abs_surfaces_as_nom : georgianSpellout UD.Case.abs = UD.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 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 (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 Marantz1991.object_derivation_matches : georgianSpellout (Marantz1991.getCase!✝ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.present)) = UD.Case.dat ∧ georgianSpellout (Marantz1991.getCase!✝ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist)) = UD.Case.nom ∧ georgianSpellout (Marantz1991.getCase!✝ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.present)) = UD.Case.nom ∧ georgianSpellout (Marantz1991.getCase!✝ "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.aorist)) = UD.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 Marantz1991.class1_aorist_erg : georgianSpellout (Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist)) = UD.Case.erg

Class 1 aorist: transitive subject gets ERG.

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

Class 2 aorist: unaccusative subject does NOT get ERG.

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

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

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

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

theorem Marantz1991.ergative_requires_competitor : Syntax.Case.getSourceOf "sole" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.ergative [{ label := "sole", lexicalCase := none }]) = some Syntax.Case.CaseSource.unmarked ∧ Syntax.Case.getSourceOf "higher" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.ergative [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]) = some Syntax.Case.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 Marantz1991.burzio_unaccusative_no_acc : Syntax.Case.getCaseOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative [{ label := "theme", lexicalCase := none }]) = some UD.Case.nom ∧ Syntax.Case.getSourceOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative [{ label := "theme", lexicalCase := none }]) = some Syntax.Case.CaseSource.unmarked

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

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

Transitive: external argument provides the case competitor → ACC.

theorem Marantz1991.nonthematic_subject_with_acc : Syntax.Case.getCaseOf "obj" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative [{ label := "derived_subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]) = some UD.Case.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 Marantz1991.npCount (voice : Minimalist.VoiceHead) (internalArgs : ℕ) : ℕ

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

Equations

• Marantz1991.npCount voice internalArgs = if voice.AssignsTheta then 1 + internalArgs else internalArgs

theorem Marantz1991.agentive_two_nps : npCount Minimalist.voiceAgent 1 = 2

theorem Marantz1991.anticausative_one_np : npCount Minimalist.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 Marantz1991.hindiTransitive (aspect : Core.Aspect) : List Syntax.Case.CasedNP

Equations

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

theorem Marantz1991.hindi_perfective_erg : Syntax.Case.getCaseOf "agent" (hindiTransitive Core.Aspect.perfective) = some UD.Case.erg ∧ Syntax.Case.getCaseOf "theme" (hindiTransitive Core.Aspect.perfective) = some UD.Case.abs

theorem Marantz1991.hindi_imperfective_nom_acc : Syntax.Case.getCaseOf "agent" (hindiTransitive Core.Aspect.imperfective) = some UD.Case.nom ∧ Syntax.Case.getCaseOf "theme" (hindiTransitive Core.Aspect.imperfective) = some UD.Case.acc

theorem Marantz1991.hindi_split_is_algorithmic : hindiTransitive Core.Aspect.perfective ≠ hindiTransitive Core.Aspect.imperfective

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

theorem Marantz1991.hindi_perfective_unaccusative_no_erg : have result := Syntax.Case.assignCases (alignmentToLangType (Core.hindiSplit.alignment Core.Aspect.perfective)) [{ label := "theme", lexicalCase := none }]; Syntax.Case.getCaseOf "theme" result = some UD.Case.abs ∧ Syntax.Case.getSourceOf "theme" result = some Syntax.Case.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 Marantz1991.hindi_perfective_unergative_with_phantom : have result := Syntax.Case.assignCases (alignmentToLangType (Core.hindiSplit.alignment Core.Aspect.perfective)) [{ label := "subj", lexicalCase := none }, { label := "empty", lexicalCase := none }]; Syntax.Case.getCaseOf "subj" result = some UD.Case.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 Marantz1991.hindi_perfective_unergative_without_phantom : have result := Syntax.Case.assignCases (alignmentToLangType (Core.hindiSplit.alignment Core.Aspect.perfective)) [{ label := "subj", lexicalCase := none }]; Syntax.Case.getCaseOf "subj" result = some UD.Case.abs ∧ Syntax.Case.getSourceOf "subj" result = some Syntax.Case.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 Marantz1991.phantom_np_parameter : georgianSpellout (Marantz1991.getCase!✝ "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class3 Fragments.Georgian.Agreement.TenseSeries.aorist)) = UD.Case.erg ∧ Syntax.Case.getCaseOf "subj" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.ergative [{ label := "subj", lexicalCase := none }]) = some UD.Case.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 Marantz1991.all_three_sources_attested : Syntax.Case.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.present) = some Syntax.Case.CaseSource.lexical ∧ Syntax.Case.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.aorist) = some Syntax.Case.CaseSource.dependent ∧ Syntax.Case.getSourceOf "subj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class2 Fragments.Georgian.Agreement.TenseSeries.aorist) = some Syntax.Case.CaseSource.unmarked

theorem Marantz1991.lexical_bleeds_dependent_georgian : Syntax.Case.getSourceOf "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class4 Fragments.Georgian.Agreement.TenseSeries.present) = some Syntax.Case.CaseSource.unmarked ∧ Syntax.Case.getSourceOf "obj" (georgianCaseResult Fragments.Georgian.Agreement.VerbClass.class1 Fragments.Georgian.Agreement.TenseSeries.present) = some Syntax.Case.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 Marantz1991.sourceToAccessibility : Syntax.Case.CaseSource → Minimalist.CaseAccessibility

Map case assignment source to agreement accessibility level. The hierarchies are isomorphic: lexical→lexical, dependent→dependent, unmarked→unmarked. Agree-based case (@cite{baker-vinokurova-2010}) behaves like unmarked for accessibility — once T values NOM, the NP is fully visible to higher probes, just like an unmarked-NOM NP.

Equations

• Marantz1991.sourceToAccessibility Syntax.Case.CaseSource.lexical = Minimalist.CaseAccessibility.lexical
• Marantz1991.sourceToAccessibility Syntax.Case.CaseSource.dependent = Minimalist.CaseAccessibility.dependent
• Marantz1991.sourceToAccessibility Syntax.Case.CaseSource.unmarked = Minimalist.CaseAccessibility.unmarked
• Marantz1991.sourceToAccessibility Syntax.Case.CaseSource.agree = Minimalist.CaseAccessibility.unmarked

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

The mapping preserves the rank ordering.

theorem Marantz1991.class4_lexical_low_accessibility : sourceToAccessibility Syntax.Case.CaseSource.lexical = Minimalist.CaseAccessibility.lexical ∧ Minimalist.caseAccessible Minimalist.CaseAccessibility.lexical Minimalist.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 Marantz1991.class1_aorist_dependent_accessibility : sourceToAccessibility Syntax.Case.CaseSource.dependent = Minimalist.CaseAccessibility.dependent ∧ Minimalist.caseAccessible Minimalist.CaseAccessibility.dependent Minimalist.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 Marantz1991.class2_unmarked_highest_accessibility : sourceToAccessibility Syntax.Case.CaseSource.unmarked = Minimalist.CaseAccessibility.unmarked ∧ Minimalist.caseAccessible Minimalist.CaseAccessibility.unmarked Minimalist.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 Marantz1991.npsFromVoice (voice : Minimalist.VoiceHead) : List Syntax.Case.NPInDomain

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

Equations

• Marantz1991.npsFromVoice voice = if voice.AssignsTheta then [{ label := "subj", lexicalCase := none }, { label := "obj", lexicalCase := none }] else [{ label := "theme", lexicalCase := none }]

theorem Marantz1991.voice_to_case_transitive : Syntax.Case.getCaseOf "obj" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative (npsFromVoice Minimalist.voiceAgent)) = some UD.Case.acc ∧ Syntax.Case.getSourceOf "obj" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative (npsFromVoice Minimalist.voiceAgent)) = some Syntax.Case.CaseSource.dependent

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

theorem Marantz1991.voice_to_case_unaccusative : Syntax.Case.getCaseOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative (npsFromVoice Minimalist.voiceAnticausative)) = some UD.Case.nom ∧ Syntax.Case.getSourceOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative (npsFromVoice Minimalist.voiceAnticausative)) = some Syntax.Case.CaseSource.unmarked

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

theorem Marantz1991.burzio_from_voice : Syntax.Case.getCaseOf "obj" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative (npsFromVoice Minimalist.voiceAgent)) = some UD.Case.acc ∧ Syntax.Case.getCaseOf "theme" (Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative (npsFromVoice Minimalist.voiceAnticausative)) = some UD.Case.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
`Aissen2003` and
`BejarRezac2009`. 

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

Case direction changes between present and aorist.

theorem 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 = Syntax.Case.CaseLanguageType.accusative ∧ georgianLangType Fragments.Georgian.Agreement.TenseSeries.aorist = Syntax.Case.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 Marantz1991.subject_agreement_invariant : Fragments.Georgian.Agreement.allPersonNumbers.all Fragments.Georgian.Agreement.subjectIsIndexed = true

Subject agreement is non-differential regardless of tense series.

theorem 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.