Dependent Case Theory

@cite{marantz-1991} @cite{baker-2015}

The dependent case algorithm: case is determined by the structural configuration of NPs within a Spell-Out domain, applied via a disjunctive priority hierarchy:

1. Lexical case: assigned by a particular head (P, V) — highest priority
2. Dependent case: assigned to an NP that stands in a c-command relation with another caseless NP in the same domain
   • Accusative languages: lower NP gets ACC
   • Ergative languages: higher NP gets ERG
   • Tripartite languages: higher NP gets ERG and lower gets ACC
3. Unmarked case: default for any NP still without case
   • Accusative languages: NOM
   • Ergative languages: ABS
   • Tripartite languages: ABS

This file is the theory — the language-typology enum, the configural rules, and the case-assignment algorithm. Empirical applications, cross-linguistic validation, and competing analyses live in Phenomena/Case/Studies/.

Where to Find What

• Studies/Marantz1991.lean — the original proposal: abstract vs. morphological case, Georgian split-ergative spellout, the case realization hierarchy as the parallel to the agreement accessibility hierarchy
• Studies/Baker2015.lean — the typological survey: cross-linguistic derivations across accusative (German, Turkish), ergative (Basque), and split-ergative (Hindi, Georgian) columns
• Studies/BakerVinokurova2010.lean — the Sakha case study, including the dependent-case-with-Agree hybrid
• Studies/Woolford1997.lean — four-way case systems (Nez Perce): ERG-as-inherent challenges the dependent-case derivation of ergative
• Studies/Scott2023.lean — voice-based case in Mam: a sibling theory in which Voice and Infl assign case directly by argument position, with dependent_case_ignores_voice staging the contrast
• Studies/Ozaki2026.lean — Japanese departure verbs: dependent ACC on the source of dyadic unaccusatives, with lexical ABL from kara bleeding dependent case
• Studies/Caha2009.lean — typological prediction at the inventory level, using the PartialOrder Core.Case instance from Core/Case/Order.lean and the RespectsCahaContainment predicate now defined in Caha2009.lean itself. The dependent case algorithm produces values in Core.Case; their relative ranking is the canonical containment order, which Caha's *ABA constraint applies to.

Companion Infrastructure

• Theories/Syntax/Minimalism/Voice.lean — Voice flavors and phase-hood, used by the Agree-based competitor and by Voice-based case (Scott 2023)
• Theories/Syntax/Minimalism/CaseFilter.lean — the Agree-based licensing requirement that every DP must receive Case
• Theories/Syntax/Case/Licensing.lean — Kalin's hybrid licensing framework: one obligatory primary licenser per clause + secondary licensers as a last-resort response to convergence failure, deriving DOM patterns as the surface signature of secondary-licenser activation
• Core/Case/Order.lean — the containment hierarchy (PartialOrder Core.Case); Core/Case/Allomorphy.lean — the framework-neutral AllomorphyPattern and *ABA substrate; Phenomena/Case/Studies/ Caha2009.lean — the Caha-specific RespectsCahaContainment predicate that consumes Core.Case values

inductive Syntax.Case.CaseSource : Type

The source of case assignment, ordered by priority. Lexical case (assigned by P, V) takes priority over dependent case, which takes priority over unmarked (default) case.

• lexical : CaseSource
• dependent : CaseSource
• unmarked : CaseSource
• agree : CaseSource

@[implicit_reducible]

instance Syntax.Case.instDecidableEqCaseSource : DecidableEq CaseSource

Equations

• Syntax.Case.instDecidableEqCaseSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Case.instReprCaseSource.repr : CaseSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprCaseSource : Repr CaseSource

Equations

• Syntax.Case.instReprCaseSource = { reprPrec := Syntax.Case.instReprCaseSource.repr }

inductive Syntax.Case.CaseLanguageType : Type

Language type determines which dependent and unmarked cases are used.

• Accusative: dependent = ACC (on lower NP), unmarked = NOM
• Ergative: dependent = ERG (on higher NP), unmarked = ABS
• Tripartite: dependent = ERG (on higher) + ACC (on lower), unmarked = ABS (@cite{scott-2023}: SJA Mam; cf. Nez Perce)

• accusative : CaseLanguageType
• ergative : CaseLanguageType
• tripartite : CaseLanguageType

@[implicit_reducible]

instance Syntax.Case.instDecidableEqCaseLanguageType : DecidableEq CaseLanguageType

Equations

• Syntax.Case.instDecidableEqCaseLanguageType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Case.instReprCaseLanguageType.repr : CaseLanguageType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprCaseLanguageType : Repr CaseLanguageType

Equations

• Syntax.Case.instReprCaseLanguageType = { reprPrec := Syntax.Case.instReprCaseLanguageType.repr }

structure Syntax.Case.NPInDomain : Type

An NP within a Spell-Out domain, before case assignment. List position encodes structural height: earlier = higher = c-commands later.

If a P head (e.g., Japanese kara) assigns lexical case to the NP, lexicalCase is some c; otherwise it is none.

• label : String

  Label identifying this NP

• lexicalCase : Option Core.Case

  Lexical case pre-assigned by a P or V head (e.g., ABL from kara)

def Syntax.Case.instDecidableEqNPInDomain.decEq (x✝ x✝¹ : NPInDomain) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Syntax.Case.instDecidableEqNPInDomain : DecidableEq NPInDomain

Equations

• Syntax.Case.instDecidableEqNPInDomain = Syntax.Case.instDecidableEqNPInDomain.decEq

def Syntax.Case.instReprNPInDomain.repr : NPInDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprNPInDomain : Repr NPInDomain

Equations

• Syntax.Case.instReprNPInDomain = { reprPrec := Syntax.Case.instReprNPInDomain.repr }

structure Syntax.Case.CasedNP : Type

Result of case assignment: an NP with its case value and source.

• label : String
• case : Core.Case
• source : CaseSource

def Syntax.Case.instDecidableEqCasedNP.decEq (x✝ x✝¹ : CasedNP) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Syntax.Case.instDecidableEqCasedNP : DecidableEq CasedNP

Equations

• Syntax.Case.instDecidableEqCasedNP = Syntax.Case.instDecidableEqCasedNP.decEq

def Syntax.Case.instReprCasedNP.repr : CasedNP → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprCasedNP : Repr CasedNP

Equations

• Syntax.Case.instReprCasedNP = { reprPrec := Syntax.Case.instReprCasedNP.repr }

def Syntax.Case.getCaseOf (label : String) (results : List CasedNP) : Option Core.Case

Look up the assigned case for an NP by label.

Equations

• Syntax.Case.getCaseOf label results = Option.map (fun (x : Syntax.Case.CasedNP) => x.case) (List.find? (fun (x : Syntax.Case.CasedNP) => x.label == label) results)

def Syntax.Case.getSourceOf (label : String) (results : List CasedNP) : Option CaseSource

Look up the case source for an NP by label.

Equations

• Syntax.Case.getSourceOf label results = Option.map (fun (x : Syntax.Case.CasedNP) => x.source) (List.find? (fun (x : Syntax.Case.CasedNP) => x.label == label) results)

def Syntax.Case.anyLacksCaseIn (nps : List NPInDomain) : Bool

Does any NP in the list lack lexical case? Used to check whether a dependent case competitor exists.

Equations

• Syntax.Case.anyLacksCaseIn nps = nps.any fun (x : Syntax.Case.NPInDomain) => x.lexicalCase.isNone

def Syntax.Case.dependentAccusative (higherNPs : List NPInDomain) (np : NPInDomain) : Option Core.Case

Dependent accusative: assigned to an NP that is c-commanded by another caseless NP in the same domain.

In our list representation, NP at index i is c-commanded by all NPs at index j < i. So NP_i gets ACC if it has no lexical case and some NP before it also has no lexical case.

Equations

• Syntax.Case.dependentAccusative higherNPs np = if (np.lexicalCase.isNone && Syntax.Case.anyLacksCaseIn higherNPs) = true then some UD.Case.acc else none

def Syntax.Case.dependentErgative (np : NPInDomain) (lowerNPs : List NPInDomain) : Option Core.Case

Dependent ergative: assigned to an NP that c-commands another caseless NP. NP_i gets ERG if it has no lexical case and some NP after it also has no lexical case.

Equations

• Syntax.Case.dependentErgative np lowerNPs = if (np.lexicalCase.isNone && Syntax.Case.anyLacksCaseIn lowerNPs) = true then some UD.Case.erg else none

def Syntax.Case.unmarkedCaseFor (lang : CaseLanguageType) : Core.Case

Unmarked (default) case for a given language type.

• Accusative languages: NOM
• Ergative languages: ABS
• Tripartite languages: ABS (only intransitive S gets unmarked case)

Equations

• Syntax.Case.unmarkedCaseFor Syntax.Case.CaseLanguageType.accusative = UD.Case.nom
• Syntax.Case.unmarkedCaseFor Syntax.Case.CaseLanguageType.ergative = UD.Case.abs
• Syntax.Case.unmarkedCaseFor Syntax.Case.CaseLanguageType.tripartite = UD.Case.abs

def Syntax.Case.assignOneCase (lang : CaseLanguageType) (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) : CasedNP

Assign case to a single NP given the NPs structurally above and below it. Applies the three-step priority: lexical → dependent → unmarked.

Equations

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

def Syntax.Case.assignCasesAux (lang : CaseLanguageType) (higher remaining : List NPInDomain) : List CasedNP

Assign case to all NPs in a Spell-Out domain. Processes the list left-to-right, maintaining context of higher NPs and remaining lower NPs for each position.

Equations

• Syntax.Case.assignCasesAux lang higher [] = []
• Syntax.Case.assignCasesAux lang higher (np :: rest) = Syntax.Case.assignOneCase lang higher rest np :: Syntax.Case.assignCasesAux lang (higher ++ [np]) rest

def Syntax.Case.assignCases (lang : CaseLanguageType) (nps : List NPInDomain) : List CasedNP

Top-level case assignment for a list of NPs in a Spell-Out domain. List order encodes structural height: first = highest = c-commands all others.

Equations

• Syntax.Case.assignCases lang nps = Syntax.Case.assignCasesAux lang [] nps

ACC Variant

"Taro-ga mura-o hanare-ta" (Taro-NOM village-ACC leave-PAST)

Two bare NPs in the TP Spell-Out domain:

• Leaver NP (higher, raised to Spec-TP)
• Source NP (lower, complement of V)
• Source gets dependent ACC; Leaver gets unmarked NOM

def Syntax.Case.accVariantNPs : List NPInDomain

Equations

• Syntax.Case.accVariantNPs = [{ label := "leaver", lexicalCase := none }, { label := "source", lexicalCase := none }]

def Syntax.Case.accVariantResult : List CasedNP

Equations

• Syntax.Case.accVariantResult = Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative Syntax.Case.accVariantNPs

ABL Variant

"Taro-ga mura-kara hanare-ta" (Taro-NOM village-from leave-PAST)

One bare NP + one PP (lexical ABL from kara):

• Leaver NP (higher, raised to Spec-TP)
• Source PP (lower, kara assigns lexical ABL)
• Source has lexical ABL (bleeds dependent case); Leaver gets unmarked NOM

def Syntax.Case.ablVariantNPs : List NPInDomain

Equations

• Syntax.Case.ablVariantNPs = [{ label := "leaver", lexicalCase := none }, { label := "source", lexicalCase := some UD.Case.abl }]

def Syntax.Case.ablVariantResult : List CasedNP

Equations

• Syntax.Case.ablVariantResult = Syntax.Case.assignCases Syntax.Case.CaseLanguageType.accusative Syntax.Case.ablVariantNPs

theorem Syntax.Case.lexical_bleeds_dependent (lang : CaseLanguageType) (c : Core.Case) (higherNPs lowerNPs : List NPInDomain) : (assignOneCase lang higherNPs lowerNPs { label := "x", lexicalCase := some c }).source = CaseSource.lexical

Lexical case bleeds dependent case: an NP with lexical case is never assigned dependent case, regardless of structural configuration.

theorem Syntax.Case.acc_variant_source_gets_acc : getCaseOf "source" accVariantResult = some UD.Case.acc

ACC variant: source (lower NP) gets dependent accusative.

theorem Syntax.Case.acc_variant_source_is_dependent : getSourceOf "source" accVariantResult = some CaseSource.dependent

ACC variant: source case is dependent (not lexical or unmarked).

theorem Syntax.Case.acc_variant_leaver_gets_nom : getCaseOf "leaver" accVariantResult = some UD.Case.nom

ACC variant: leaver (higher NP) gets unmarked nominative.

theorem Syntax.Case.acc_variant_leaver_is_unmarked : getSourceOf "leaver" accVariantResult = some CaseSource.unmarked

ACC variant: leaver case is unmarked.

theorem Syntax.Case.abl_variant_source_gets_abl : getCaseOf "source" ablVariantResult = some UD.Case.abl

ABL variant: source gets lexical ablative (from kara).

theorem Syntax.Case.abl_variant_source_is_lexical : getSourceOf "source" ablVariantResult = some CaseSource.lexical

ABL variant: source case is lexical (from P head kara).

theorem Syntax.Case.abl_variant_leaver_gets_nom : getCaseOf "leaver" ablVariantResult = some UD.Case.nom

ABL variant: leaver gets unmarked nominative.

theorem Syntax.Case.no_voice_needed_for_acc : have nps := [{ label := "subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]; getCaseOf "obj" (assignCases CaseLanguageType.accusative nps) = some UD.Case.acc ∧ getSourceOf "obj" (assignCases CaseLanguageType.accusative nps) = some CaseSource.dependent

Dependent ACC does not require agentive Voice — it only requires two caseless NPs in the same Spell-Out domain. The Voice head's flavor is irrelevant to the case algorithm.

theorem Syntax.Case.acc_variant_all_cased : accVariantResult.length = 2

All NPs receive case in the ACC variant.

theorem Syntax.Case.abl_variant_all_cased : ablVariantResult.length = 2

All NPs receive case in the ABL variant.

Tripartite: Theory-Level Properties

In a tripartite system, both dependent ergative and dependent accusative are active simultaneously: the higher NP gets ERG, the lower gets ACC, and an NP with no case competitor gets unmarked ABS. These are properties of the algorithm, not of any particular language. Language-specific derivations (e.g., SJA Mam) belong in Phenomena/Case/Bridge/.

theorem Syntax.Case.tripartite_higher_gets_erg : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "higher" (assignCases CaseLanguageType.tripartite nps) = some UD.Case.erg

Tripartite transitive: higher NP gets dependent ERG.

theorem Syntax.Case.tripartite_lower_gets_acc : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "lower" (assignCases CaseLanguageType.tripartite nps) = some UD.Case.acc

Tripartite transitive: lower NP gets dependent ACC.

theorem Syntax.Case.tripartite_sole_gets_abs : have nps := [{ label := "sole", lexicalCase := none }]; getCaseOf "sole" (assignCases CaseLanguageType.tripartite nps) = some UD.Case.abs

Tripartite intransitive: sole NP gets unmarked ABS.

theorem Syntax.Case.tripartite_three_distinct : have tr := assignCases CaseLanguageType.tripartite [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; have intr := assignCases CaseLanguageType.tripartite [{ label := "sole", lexicalCase := none }]; getCaseOf "higher" tr ≠ getCaseOf "lower" tr ∧ getCaseOf "higher" tr ≠ getCaseOf "sole" intr ∧ getCaseOf "lower" tr ≠ getCaseOf "sole" intr

All three cases are distinct — the defining property of tripartite. ERG ≠ ACC ≠ ABS, derived purely from the algorithm.

theorem Syntax.Case.tripartite_subsumes_both : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "higher" (assignCases CaseLanguageType.tripartite nps) = getCaseOf "higher" (assignCases CaseLanguageType.ergative nps) ∧ getCaseOf "lower" (assignCases CaseLanguageType.tripartite nps) = getCaseOf "lower" (assignCases CaseLanguageType.accusative nps)

Tripartite subsumes both ergative and accusative dependent case: ERG on the higher NP matches pure ergative; ACC on the lower NP matches pure accusative.

theorem Syntax.Case.acc_abl_mutually_exclusive : getCaseOf "source" accVariantResult = some UD.Case.acc ∧ getCaseOf "source" ablVariantResult = some UD.Case.abl

ACC and ABL are mutually exclusive on the source: the same structural position receives exactly one of ACC (dependent) or ABL (lexical), never both. This follows from the priority ordering — lexical case preempts dependent case entirely.

theorem Syntax.Case.leaver_nom_invariant : getCaseOf "leaver" accVariantResult = some UD.Case.nom ∧ getCaseOf "leaver" ablVariantResult = some UD.Case.nom

The leaver gets NOM in both variants. The alternation affects only the source argument; the subject case is invariant.

theorem Syntax.Case.ergative_mirror : have nps := [{ label := "higher", lexicalCase := none }, { label := "lower", lexicalCase := none }]; getCaseOf "higher" (assignCases CaseLanguageType.ergative nps) = some UD.Case.erg ∧ getCaseOf "lower" (assignCases CaseLanguageType.ergative nps) = some UD.Case.abs

Ergative mirror: in an ergative language with two caseless NPs, the higher NP gets dependent ERG and the lower gets unmarked ABS. This is the typological inverse of the accusative pattern.

theorem Syntax.Case.single_np_nom : have nps := [{ label := "sole", lexicalCase := none }]; getCaseOf "sole" (assignCases CaseLanguageType.accusative nps) = some UD.Case.nom ∧ getSourceOf "sole" (assignCases CaseLanguageType.accusative nps) = some CaseSource.unmarked

A single caseless NP in an accusative language gets NOM — the standard intransitive case. No dependent case arises because there is no case competitor.

theorem Syntax.Case.case_is_configural : getCaseOf "source" accVariantResult ≠ getCaseOf "source" ablVariantResult

Case is purely configural: two NPs with identical labels but different lexical case inputs produce different outputs. The algorithm is sensitive only to the NP inventory, not to verb type or Voice flavor.

def Syntax.Case.structuralCasesFor : CaseLanguageType → List Core.Case

The structural (non-lexical) cases that the dependent case algorithm can assign for each language type. These are exactly the cases that appear in the none (no lexical case) branch of assignOneCase.

Equations

• Syntax.Case.structuralCasesFor Syntax.Case.CaseLanguageType.accusative = [UD.Case.nom, UD.Case.acc]
• Syntax.Case.structuralCasesFor Syntax.Case.CaseLanguageType.ergative = [UD.Case.abs, UD.Case.erg]
• Syntax.Case.structuralCasesFor Syntax.Case.CaseLanguageType.tripartite = [UD.Case.abs, UD.Case.erg, UD.Case.acc]

theorem Syntax.Case.accusative_nonlexical_cases (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) (h : np.lexicalCase = none) : have result := assignOneCase CaseLanguageType.accusative higherNPs lowerNPs np; result.case = UD.Case.nom ∨ result.case = UD.Case.acc

In an accusative language, any NP without lexical case receives either NOM (unmarked) or ACC (dependent).

theorem Syntax.Case.ergative_nonlexical_cases (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) (h : np.lexicalCase = none) : have result := assignOneCase CaseLanguageType.ergative higherNPs lowerNPs np; result.case = UD.Case.abs ∨ result.case = UD.Case.erg

In an ergative language, any NP without lexical case receives either ABS (unmarked) or ERG (dependent).

theorem Syntax.Case.tripartite_nonlexical_cases (higherNPs lowerNPs : List NPInDomain) (np : NPInDomain) (h : np.lexicalCase = none) : have result := assignOneCase CaseLanguageType.tripartite higherNPs lowerNPs np; result.case = UD.Case.abs ∨ result.case = UD.Case.erg ∨ result.case = UD.Case.acc

In a tripartite language, any NP without lexical case receives ABS (unmarked), ERG (dependent on a lower NP), or ACC (dependent on a higher NP).

inductive Syntax.Case.NomAssignment : Type

How nominative case is assigned in a language. @cite{baker-vinokurova-2010}: in Sakha (and Mongolian, per @cite{gong-2022}), NOM is assigned by finite T via Agree, not as an unmarked default. This distinction matters for Wholesale Late Merger: Agree-based NOM is tied to a specific functional head, while unmarked NOM is a last-resort default.

• agreeT : NomAssignment
• unmarkedDefault : NomAssignment

@[implicit_reducible]

instance Syntax.Case.instDecidableEqNomAssignment : DecidableEq NomAssignment

Equations

• Syntax.Case.instDecidableEqNomAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Case.instReprNomAssignment : Repr NomAssignment

Equations

• Syntax.Case.instReprNomAssignment = { reprPrec := Syntax.Case.instReprNomAssignment.repr }

def Syntax.Case.instReprNomAssignment.repr : NomAssignment → ℕ → Std.Format

Equations

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

inductive Syntax.Case.DatAssignment : Type

How dative case is assigned. @cite{gong-2022}: DAT is nonstructural in Mongolian — it does not participate in dependent case competition and is not available at intermediate scrambling positions for WLM.

• nonstructural : DatAssignment
• dependent : DatAssignment

@[implicit_reducible]

instance Syntax.Case.instDecidableEqDatAssignment : DecidableEq DatAssignment

Equations

• Syntax.Case.instDecidableEqDatAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Case.instReprDatAssignment.repr : DatAssignment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprDatAssignment : Repr DatAssignment

Equations

• Syntax.Case.instReprDatAssignment = { reprPrec := Syntax.Case.instReprDatAssignment.repr }

inductive Syntax.Case.AccAssignment : Type

How accusative case is assigned. @cite{baker-vinokurova-2010}: in Sakha (and Mongolian, per @cite{gong-2022}), ACC is dependent case (Marantz-style); the standard Chomskyan alternative is that ACC is assigned by v/Voice via Agree (often paired with Burzio's Generalization).

• dependent : AccAssignment
• agreeV : AccAssignment

@[implicit_reducible]

instance Syntax.Case.instDecidableEqAccAssignment : DecidableEq AccAssignment

Equations

• Syntax.Case.instDecidableEqAccAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Case.instReprAccAssignment : Repr AccAssignment

Equations

• Syntax.Case.instReprAccAssignment = { reprPrec := Syntax.Case.instReprAccAssignment.repr }

def Syntax.Case.instReprAccAssignment.repr : AccAssignment → ℕ → Std.Format

Equations

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

inductive Syntax.Case.GenAssignment : Type

How genitive case is assigned. @cite{baker-vinokurova-2010}: in Sakha, GEN is assigned by D via Agree to the possessor (parallel to T-Agree NOM at the clausal level). Russian numeric and partitive GEN is nonstructural.

• agreeD : GenAssignment
• nonstructural : GenAssignment

@[implicit_reducible]

instance Syntax.Case.instDecidableEqGenAssignment : DecidableEq GenAssignment

Equations

• Syntax.Case.instDecidableEqGenAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Syntax.Case.instReprGenAssignment.repr : GenAssignment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprGenAssignment : Repr GenAssignment

Equations

• Syntax.Case.instReprGenAssignment = { reprPrec := Syntax.Case.instReprGenAssignment.repr }

structure Syntax.Case.CaseSystemConfig : Type

A language-specific case system configuration. Bundles the alignment type with the per-case mechanism choices.

Each of the four structural cases (NOM, GEN, ACC, DAT) gets an independent mechanism plug-in. Marantz's purely-configurational picture, Chomsky's purely-Agree picture, and B&V's two-modality Sakha grammar all fall out as parameterizations of this single structure:

Theory	nom	gen	acc	dat
Marantz pure	unmarkedDefault	(—)	dependent	dependent
Chomsky pure	agreeT	agreeD	agreeV	nonstructural
Sakha (B&V)	agreeT	agreeD	dependent	dependent
Mongolian	agreeT	agreeD	dependent	nonstructural

accMode and genMode default to the most common values across the library so that existing instances need not specify them.

• langType : CaseLanguageType
• nomMode : NomAssignment
• datMode : DatAssignment
• accMode : AccAssignment
• genMode : GenAssignment

@[implicit_reducible]

instance Syntax.Case.instDecidableEqCaseSystemConfig : DecidableEq CaseSystemConfig

Equations

• Syntax.Case.instDecidableEqCaseSystemConfig = Syntax.Case.instDecidableEqCaseSystemConfig.decEq

def Syntax.Case.instDecidableEqCaseSystemConfig.decEq (x✝ x✝¹ : CaseSystemConfig) : Decidable (x✝ = x✝¹)

Equations

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

def Syntax.Case.instReprCaseSystemConfig.repr : CaseSystemConfig → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprCaseSystemConfig : Repr CaseSystemConfig

Equations

• Syntax.Case.instReprCaseSystemConfig = { reprPrec := Syntax.Case.instReprCaseSystemConfig.repr }

Phased case assignment

@cite{baker-vinokurova-2010} formalize Sakha case as cycling over two phases: VP (the smaller phase) and CP. Two configurational rules apply (paper (4a)/(4b), restated as (85)):

• (4a) DAT rule: if NP1 c-commands NP2 in the same VP-phase, value NP1 as DAT unless NP2 is already marked.
• (4b) ACC rule: if NP1 c-commands NP2 in the same phase, value NP2 as ACC unless NP1 is already marked.

(4a) bleeds (4b) on the VP cycle by Elsewhere ordering — its context (one specific phase) is more restrictive than (4b)'s (any phase).

After dependent case has applied, Agree (paper (5)/(86)) values remaining unvalued NPs:

• T agrees with the highest unvalued NP visible at CP, valuing NOM.
• D agrees with its dependent NP inside a DP, valuing GEN.

Each NP carries a basePhase (where it was merged) and a shifted flag (did it move to a higher phase before evaluation). PIC: NPs that stayed inside VP are not visible on the CP cycle.

inductive Syntax.Case.CasePhase : Type

Cycle in the @cite{baker-vinokurova-2010} two-phase model. Distinct from the more articulated Minimalist.Phase structure in Phase.lean; this is just the binary VP-vs-CP distinction that the case algorithm cycles over.

• vp : CasePhase
• cp : CasePhase

@[implicit_reducible]

instance Syntax.Case.instDecidableEqCasePhase : DecidableEq CasePhase

Equations

• Syntax.Case.instDecidableEqCasePhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Syntax.Case.instReprCasePhase : Repr CasePhase

Equations

• Syntax.Case.instReprCasePhase = { reprPrec := Syntax.Case.instReprCasePhase.repr }

def Syntax.Case.instReprCasePhase.repr : CasePhase → ℕ → Std.Format

Equations

• Syntax.Case.instReprCasePhase.repr Syntax.Case.CasePhase.vp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Syntax.Case.CasePhase.vp")).group prec✝
• Syntax.Case.instReprCasePhase.repr Syntax.Case.CasePhase.cp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Syntax.Case.CasePhase.cp")).group prec✝

structure Syntax.Case.PhasedNPextends Syntax.Case.NPInDomain : Type

An NP equipped with phase information. basePhase records where the NP was merged; shifted marks NPs that have moved to a higher phase before case evaluation. isArgumental flags whether the NP bears a θ-role w.r.t. some case-assigning head — only argumental NPs are case competitors for rules (4a)/(4b). Bare-NP adverbs (e.g., 'yesterday', 'two kilometers') are non-argumental. @cite{baker-vinokurova-2010} (8)–(9) and footnote 5.

inDP flags NPs that participate only in DP-internal case assignment (possessors): these are skipped by every clausal pass and are valued by applyGenAgree when genMode := .agreeD.

• label : String
• lexicalCase : Option Core.Case
• basePhase : CasePhase
• shifted : Bool
• isArgumental : Bool
• inDP : Bool

@[implicit_reducible]

instance Syntax.Case.instDecidableEqPhasedNP : DecidableEq PhasedNP

Equations

• Syntax.Case.instDecidableEqPhasedNP = Syntax.Case.instDecidableEqPhasedNP.decEq

def Syntax.Case.instDecidableEqPhasedNP.decEq (x✝ x✝¹ : PhasedNP) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprPhasedNP : Repr PhasedNP

Equations

• Syntax.Case.instReprPhasedNP = { reprPrec := Syntax.Case.instReprPhasedNP.repr }

def Syntax.Case.instReprPhasedNP.repr : PhasedNP → ℕ → Std.Format

Equations

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

def Syntax.Case.PhasedNP.visibleOnVP (p : PhasedNP) : Bool

Visible on the VP cycle: NPs whose basePhase is vp. Even shifted NPs are visible at this point — shift happens at the boundary between cycles.

Equations

• p.visibleOnVP = (p.basePhase == Syntax.Case.CasePhase.vp)

def Syntax.Case.PhasedNP.visibleOnCP (p : PhasedNP) : Bool

Visible on the CP cycle: NPs in cp, plus VP-base NPs that shifted out of VP. Unshifted VP NPs were transferred (PIC).

Equations

• p.visibleOnCP = (p.basePhase == Syntax.Case.CasePhase.cp || p.shifted)

structure Syntax.Case.PhasedState : Type

Mutable state during phased case assignment. case = none means "not yet valued"; lexical case starts with the value pre-set.

• np : PhasedNP
• case : Option (Core.Case × CaseSource)

def Syntax.Case.instReprPhasedState.repr : PhasedState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Syntax.Case.instReprPhasedState : Repr PhasedState

Equations

• Syntax.Case.instReprPhasedState = { reprPrec := Syntax.Case.instReprPhasedState.repr }

def Syntax.Case.PhasedState.marked (s : PhasedState) : Bool

An NP is "marked" iff its case has been valued (lexically, by dependent rule, or by agreement). The "unless...marked" clauses of (4a)/(4b) check this.

Equations

• s.marked = s.case.isSome

def Syntax.Case.initStates (nps : List PhasedNP) : List PhasedState

Initialize: pre-fill lexical case from the NP's lexicalCase field; everything else starts unvalued.

Equations

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

def Syntax.Case.setCaseAt (i : ℕ) (c : Core.Case) (src : CaseSource) (states : List PhasedState) : List PhasedState

Replace the case of the NP at index i with (c, src).

Equations

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

def Syntax.Case.unmarkedEligible (cycle : CasePhase) (s : PhasedState) : Bool

The eligibility predicate used by unmarkedVisible: a state is eligible iff it is visible on the cycle, argumental, not DP- internal, and not yet marked. Factored out so structural proofs (e.g. applyAccRule_preserves_marked_at) can manipulate the condition without unfolding pattern lambdas.

Equations

• Syntax.Case.unmarkedEligible Syntax.Case.CasePhase.vp s = (s.np.visibleOnVP && s.np.isArgumental && !s.np.inDP && !s.marked)
• Syntax.Case.unmarkedEligible Syntax.Case.CasePhase.cp s = (s.np.visibleOnCP && s.np.isArgumental && !s.np.inDP && !s.marked)

def Syntax.Case.unmarkedVisible (cycle : CasePhase) (states : List PhasedState) : List ℕ

Indices of unmarked, argumental, clause-level NPs visible on a given cycle, in c-command order (highest first, since list-position encodes height). Non-argumental NPs (bare-NP adverbs) and DP- internal NPs (possessors) are filtered out: per @cite{baker-vinokurova-2010} (8)–(9), rules (4a)/(4b) apply only between argumental NPs at the clausal level.

Equations

• Syntax.Case.unmarkedVisible cycle states = List.filterMap (fun (p : Syntax.Case.PhasedState × ℕ) => if Syntax.Case.unmarkedEligible cycle p.1 = true then some p.2 else none) states.zipIdx

def Syntax.Case.applyDatRule (cfg : CaseSystemConfig) (states : List PhasedState) : List PhasedState

Apply the DAT rule (4a) on the VP cycle: if there are at least two unmarked NPs visible at vP, mark the highest as DAT.

Equations

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

def Syntax.Case.applyAccRule (cfg : CaseSystemConfig) (cycle : CasePhase) (states : List PhasedState) : List PhasedState

Apply the ACC rule (4b) on a given cycle: if there are at least two unmarked NPs visible, mark the lowest as ACC.

Equations

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

def Syntax.Case.applyAccAgree (cfg : CaseSystemConfig) (states : List PhasedState) : List PhasedState

Apply v-Agree: the lowest CP-visible unmarked argumental NP gets ACC via Agree. This is the standard Chomskyan picture (@cite{chomsky-2000}; @cite{chomsky-2001}): v probes downward into its complement and Agrees with the closest goal. The dependent- accusative algorithm (applyAccRule) is the alternative to this pass; the two are mutually exclusive on a given grammar via the accMode parameter.

Equations

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

def Syntax.Case.applyNomAgree (cfg : CaseSystemConfig) (states : List PhasedState) : List PhasedState

Apply T-Agree (paper (5)/(86)): the highest unmarked NP visible on the CP cycle gets NOM via Agree.

Equations

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

def Syntax.Case.applyGenAgree (cfg : CaseSystemConfig) (states : List PhasedState) : List PhasedState

Apply D-Agree (paper (5)/(86)): every unmarked DP-internal NP (possessor) is valued GEN by its dominating D head. The clausal algorithm sees DP-internals as opaque (filtered from unmarkedVisible); this pass is the DP-internal counterpart to applyNomAgree. The Russian numeric/partitive GEN, by contrast, is .nonstructural and lives in lexicalCase.

Equations

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

def Syntax.Case.applyDefault (cfg : CaseSystemConfig) (states : List PhasedState) : List PhasedState

Default case for any NP still unmarked at the end of the derivation. Uses unmarkedCaseFor from § 6.

Equations

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

def Syntax.Case.PhasedState.toCased (s : PhasedState) : Option CasedNP

Materialize a PhasedState as a CasedNP (or omit if no case was ever assigned — caller should ensure applyDefault ran).

Equations

• s.toCased = Option.map (fun (x : Core.Case × Syntax.Case.CaseSource) => match x with | (c, src) => { label := s.np.label, case := c, source := src }) s.case

def Syntax.Case.assignCasesPhased (cfg : CaseSystemConfig) (nps : List PhasedNP) : List CasedNP

The B&V phased algorithm: VP cycle (DAT then ACC), CP cycle (ACC), v-Agree → ACC (only when accMode := .agreeV), T-Agree → NOM, D-Agree → GEN, then a default sweep.

applyAccRule and applyAccAgree are mutually exclusive on the cases they touch (gated by accMode), so their relative order only matters when neither fires. The order chosen — dependent rules first, then Agree — mirrors the standard Chomskyan picture where v probes after VP-internal structure has been built.

Equations

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

Length preservation (one CasedNP per input PhasedNP) and totality (every input NP receives exactly one case) are the key well-formedness properties of assignCasesPhased. They fall out structurally: each per-pass operation preserves list length, and applyDefault guarantees no state escapes uncased.

theorem Syntax.Case.initStates_length (nps : List PhasedNP) : (initStates nps).length = nps.length

theorem Syntax.Case.setCaseAt_length (i : ℕ) (c : Core.Case) (src : CaseSource) (states : List PhasedState) : (setCaseAt i c src states).length = states.length

theorem Syntax.Case.applyDatRule_length (cfg : CaseSystemConfig) (states : List PhasedState) : (applyDatRule cfg states).length = states.length

theorem Syntax.Case.applyAccRule_length (cfg : CaseSystemConfig) (cycle : CasePhase) (states : List PhasedState) : (applyAccRule cfg cycle states).length = states.length

theorem Syntax.Case.applyAccAgree_length (cfg : CaseSystemConfig) (states : List PhasedState) : (applyAccAgree cfg states).length = states.length

theorem Syntax.Case.applyNomAgree_length (cfg : CaseSystemConfig) (states : List PhasedState) : (applyNomAgree cfg states).length = states.length

theorem Syntax.Case.applyGenAgree_length (cfg : CaseSystemConfig) (states : List PhasedState) : (applyGenAgree cfg states).length = states.length

theorem Syntax.Case.applyDefault_length (cfg : CaseSystemConfig) (states : List PhasedState) : (applyDefault cfg states).length = states.length

theorem Syntax.Case.applyDefault_all_some (cfg : CaseSystemConfig) (states : List PhasedState) (s : PhasedState) : s ∈ applyDefault cfg states → s.case.isSome = true

After the final default sweep, every state's case is valued.

theorem Syntax.Case.assignCasesPhased_length (cfg : CaseSystemConfig) (nps : List PhasedNP) : (assignCasesPhased cfg nps).length = nps.length

Soundness (length preservation). The phased algorithm produces exactly one CasedNP per input PhasedNP. No NP is dropped or duplicated; the algorithm is total.

The Elsewhere ordering of (4a) over (4b) on the VP cycle is not a stipulated rule-ordering preference: it falls out from the fact that unmarkedVisible filters out marked NPs, so any pass that only modifies indices in unmarkedVisible cannot overwrite a previously- valued NP. We prove this once for applyAccRule (it never overwrites a marked state) and use it to derive the bleeding theorem for arbitrary inputs.

theorem Syntax.Case.applyAccRule_preserves_marked_at (cfg : CaseSystemConfig) (cycle : CasePhase) (states : List PhasedState) (i : ℕ) (s : PhasedState) (h_get : states[i]? = some s) (h_marked : s.marked = true) : (applyAccRule cfg cycle states)[i]? = some s

(4b) ACC never overwrites a marked NP. This is the structural content of the Elsewhere ordering: once a state has been valued (lexically, by (4a) DAT, or by Agree), unmarkedVisible no longer includes its index, so applyAccRule cannot touch it.

theorem Syntax.Case.applyAccAgree_preserves_marked_at (cfg : CaseSystemConfig) (states : List PhasedState) (i : ℕ) (s : PhasedState) (h_get : states[i]? = some s) (h_marked : s.marked = true) : (applyAccAgree cfg states)[i]? = some s

v-Agree, like (4b), only touches unmarkedVisible indices and so cannot overwrite a marked NP.

theorem Syntax.Case.applyNomAgree_preserves_marked_at (cfg : CaseSystemConfig) (states : List PhasedState) (i : ℕ) (s : PhasedState) (h_get : states[i]? = some s) (h_marked : s.marked = true) : (applyNomAgree cfg states)[i]? = some s

T-Agree only touches unmarkedVisible .cp indices.

theorem Syntax.Case.applyGenAgree_preserves_marked_at (cfg : CaseSystemConfig) (states : List PhasedState) (i : ℕ) (s : PhasedState) (h_get : states[i]? = some s) (h_marked : s.marked = true) : (applyGenAgree cfg states)[i]? = some s

D-Agree only modifies unmarked DP-internal states.

theorem Syntax.Case.applyDefault_preserves_marked_at (cfg : CaseSystemConfig) (states : List PhasedState) (i : ℕ) (s : PhasedState) (h_get : states[i]? = some s) (h_marked : s.marked = true) : (applyDefault cfg states)[i]? = some s

The default sweep only modifies unmarked states.

theorem Syntax.Case.dat_persists_through_vp_acc (cfg : CaseSystemConfig) (states : List PhasedState) (i : ℕ) (s : PhasedState) (h_get : (applyDatRule cfg states)[i]? = some s) (h_dat : s.case = some (UD.Case.dat, CaseSource.dependent)) : (applyAccRule cfg CasePhase.vp (applyDatRule cfg states))[i]? = some s

DAT bleeds ACC on the VP cycle, structurally. For every input state list, the NP marked DAT by applyDatRule keeps its DAT case through the subsequent VP-cycle applyAccRule call.

theorem Syntax.Case.dat_persists_through_assignCasesPhased (cfg : CaseSystemConfig) (nps : List PhasedNP) (i : ℕ) (s : PhasedState) (h_get : (applyDatRule cfg (initStates nps))[i]? = some s) (h_dat : s.case = some (UD.Case.dat, CaseSource.dependent)) : have s0 := initStates nps; have s1 := applyDatRule cfg s0; have s2 := applyAccRule cfg CasePhase.vp s1; have s3 := applyAccRule cfg CasePhase.cp s2; have s4 := applyAccAgree cfg s3; have s5 := applyNomAgree cfg s4; have s6 := applyGenAgree cfg s5; have s7 := applyDefault cfg s6; s7[i]? = some s

DAT marking persists all the way through assignCasesPhased. Whatever NP applyDatRule values DAT survives every subsequent pass — both ACC cycles, both Agree probes, and the default sweep — because each pass only modifies states it sees as unmarked. The Sakha-specific empirical theorem ditrans_goal_dat follows from this structural fact applied to the ditransitive input.