Dargwa (Tanti) Case Inventory @cite{sumbatova-2021}

Dargwa (Tanti dialect; Nakh-Dagestanian) has a consistently ergative alignment system — unlike Georgian's tense-conditioned split. All transitive verbs mark the A-argument with ergative -li and leave the P-argument unmarked (absolutive). There is no split conditioning.

Grammatical Cases (Table 4.3 of @cite{sumbatova-2021})

Case	Morpheme	Function
absolutive	∅	S-argument, P-argument, nominal pred.
ergative	-li	A-argument, instrument
genitive	-la, -lla	nominal modifier, possessor
dative	-ž	experiencer, recipient, benefactive
comitative	-c:ele	comitative, instrument
adverbial	-le	nominal predicate, secondary predicate

Locative System

In addition to the 6 grammatical cases above, Dargwa has a rich spatial case system. Locative forms decompose into three morphological layers:

STEM — LOCALIZATION — ORIENTATION — DIRECTION

Eight localizations (SUPER, SUB, ANTE, IN, INTER, AD, APUD, POST) × four orientations (LATIVE, ELATIVE, ESSIVE, TRANSLATIVE) × four directions (UP, DOWN, HITHER, THITHER).

This yields a large paradigm, though not all cells are filled.

def Fragments.Dargwa.Case.caseInventory : List Core.Case

Dargwa grammatical case inventory: ABS(∅), ERG(-li), GEN(-la, -lla), DAT(-ž), COM(-c:ele), ADV(-le).

We use Core.Case values. The adverbial case is mapped to ess (essive) as the closest typological equivalent — it marks "being-in-a-state" predicates, analogous to the Finnish essive.

Genitive has two allomorphs: -la and -lla.

Equations

• Fragments.Dargwa.Case.caseInventory = [Core.Case.abs, Core.Case.erg, Core.Case.gen, Core.Case.dat, Core.Case.com, Core.Case.ess]

theorem Fragments.Dargwa.Case.inventory_not_strictly_contiguous : Core.validInventory caseInventory = false

Dargwa's grammatical case inventory violates strict contiguity on Blake's hierarchy: COM (rank 1) and ESS (rank 0) are present without LOC (rank 3) or ABL/INST (rank 2). This is expected: Dargwa's rich locative system (8 localizations × 4 orientations) functionally covers spatial and source meanings that LOC and ABL encode in other languages. The grammatical vs. locative split is a structural feature of Nakh-Dagestanian languages.

def Fragments.Dargwa.Case.alignment : Core.AlignmentFamily

Dargwa alignment: consistently ergative — no tense/aspect split. Transitive A-arguments always take ergative -li; S and P arguments take unmarked absolutive.

Equations

• Fragments.Dargwa.Case.alignment = Core.AlignmentFamily.ergative

def Fragments.Dargwa.Case.agentCase : Core.Case

Case of the transitive agent (A-argument): always ergative.

Equations

• Fragments.Dargwa.Case.agentCase = Core.Case.erg

def Fragments.Dargwa.Case.patientCase : Core.Case

Case of the S-argument and P-argument: always absolutive.

Equations

• Fragments.Dargwa.Case.patientCase = Core.Case.abs

inductive Fragments.Dargwa.Case.Localization : Type

Localization values: spatial domain w.r.t. the reference point. Tanti has 8 localizations (@cite{sumbatova-2021} §4.4.3.3).

• super : Localization
• sub : Localization
• ante : Localization
• in_ : Localization
• inter : Localization
• ad : Localization
• apud : Localization
• post : Localization

instance Fragments.Dargwa.Case.instDecidableEqLocalization : DecidableEq Localization

Equations

• Fragments.Dargwa.Case.instDecidableEqLocalization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Dargwa.Case.instBEqLocalization : BEq Localization

Equations

• Fragments.Dargwa.Case.instBEqLocalization = { beq := Fragments.Dargwa.Case.instBEqLocalization.beq }

def Fragments.Dargwa.Case.instBEqLocalization.beq : Localization → Localization → Bool

Equations

• Fragments.Dargwa.Case.instBEqLocalization.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Dargwa.Case.instReprLocalization : Repr Localization

Equations

• Fragments.Dargwa.Case.instReprLocalization = { reprPrec := Fragments.Dargwa.Case.instReprLocalization.repr }

def Fragments.Dargwa.Case.instReprLocalization.repr : Localization → Nat → Std.Format

Equations

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

inductive Fragments.Dargwa.Case.Orientation : Type

Orientation values: motion w.r.t. the reference point. Tanti has 4 orientations (@cite{sumbatova-2021} §4.4.3.3).

• lative : Orientation
• elative : Orientation
• essive : Orientation
• translative : Orientation

instance Fragments.Dargwa.Case.instDecidableEqOrientation : DecidableEq Orientation

Equations

• Fragments.Dargwa.Case.instDecidableEqOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.Dargwa.Case.instBEqOrientation : BEq Orientation

Equations

• Fragments.Dargwa.Case.instBEqOrientation = { beq := Fragments.Dargwa.Case.instBEqOrientation.beq }

def Fragments.Dargwa.Case.instBEqOrientation.beq : Orientation → Orientation → Bool

Equations

• Fragments.Dargwa.Case.instBEqOrientation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Dargwa.Case.instReprOrientation : Repr Orientation

Equations

• Fragments.Dargwa.Case.instReprOrientation = { reprPrec := Fragments.Dargwa.Case.instReprOrientation.repr }

def Fragments.Dargwa.Case.instReprOrientation.repr : Orientation → Nat → Std.Format

Equations

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

inductive Fragments.Dargwa.Case.Direction : Type

Direction values: motion w.r.t. the speaker. Tanti has 4 directions (@cite{sumbatova-2021} §4.4.3.3).

• up : Direction
• down : Direction
• hither : Direction
• thither : Direction

instance Fragments.Dargwa.Case.instDecidableEqDirection : DecidableEq Direction

Equations

• Fragments.Dargwa.Case.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Dargwa.Case.instBEqDirection.beq : Direction → Direction → Bool

Equations

• Fragments.Dargwa.Case.instBEqDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Dargwa.Case.instBEqDirection : BEq Direction

Equations

• Fragments.Dargwa.Case.instBEqDirection = { beq := Fragments.Dargwa.Case.instBEqDirection.beq }

def Fragments.Dargwa.Case.instReprDirection.repr : Direction → Nat → Std.Format

Equations

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

instance Fragments.Dargwa.Case.instReprDirection : Repr Direction

Equations

• Fragments.Dargwa.Case.instReprDirection = { reprPrec := Fragments.Dargwa.Case.instReprDirection.repr }

structure Fragments.Dargwa.Case.LocativeForm : Type

A full locative form combines all three layers.

• localization : Localization
• orientation : Orientation
• direction : Option Direction

def Fragments.Dargwa.Case.instReprLocativeForm.repr : LocativeForm → Nat → Std.Format

Equations

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

instance Fragments.Dargwa.Case.instReprLocativeForm : Repr LocativeForm

Equations

• Fragments.Dargwa.Case.instReprLocativeForm = { reprPrec := Fragments.Dargwa.Case.instReprLocativeForm.repr }

def Fragments.Dargwa.Case.LocativeForm.wellFormed (lf : LocativeForm) : Bool

Well-formedness of a locative form, encoding all combinatorial constraints from @cite{sumbatova-2021} §4.4.3.3:

Direction: absent in essive and translative, obligatory in elative, optional in lative.

Localization × Orientation: translative combines only with SUB, ANTE, POST. POST combines only with translative.

Equations

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

def Fragments.Dargwa.Case.Orientation.translativeRestricted (loc : Localization) : Bool

Translative combines only with SUB, ANTE, and POST.

Equations

• Fragments.Dargwa.Case.Orientation.translativeRestricted Fragments.Dargwa.Case.Localization.sub = true
• Fragments.Dargwa.Case.Orientation.translativeRestricted Fragments.Dargwa.Case.Localization.ante = true
• Fragments.Dargwa.Case.Orientation.translativeRestricted Fragments.Dargwa.Case.Localization.post = true
• Fragments.Dargwa.Case.Orientation.translativeRestricted loc = false

theorem Fragments.Dargwa.Case.has_core_ergative : (caseInventory.any fun (x : Core.Case) => x == Core.Case.abs) = true ∧ (caseInventory.any fun (x : Core.Case) => x == Core.Case.erg) = true

The inventory contains both core ergative cases.

theorem Fragments.Dargwa.Case.consistently_ergative : alignment = Core.AlignmentFamily.ergative

Dargwa is consistently ergative (no split).

theorem Fragments.Dargwa.Case.eight_localizations : [Localization.super, Localization.sub, Localization.ante, Localization.in_, Localization.inter, Localization.ad, Localization.apud, Localization.post].length = 8

All 8 localizations are distinct (no collapse).

theorem Fragments.Dargwa.Case.translative_restricted_sub : Orientation.translativeRestricted Localization.sub = true

Translative combines only with SUB, ANTE, and POST (@cite{sumbatova-2021} ex. 13).

theorem Fragments.Dargwa.Case.translative_restricted_ante : Orientation.translativeRestricted Localization.ante = true

theorem Fragments.Dargwa.Case.translative_restricted_post : Orientation.translativeRestricted Localization.post = true

theorem Fragments.Dargwa.Case.translative_blocked_super : Orientation.translativeRestricted Localization.super = false

theorem Fragments.Dargwa.Case.post_lative_illformed : { localization := Localization.post, orientation := Orientation.lative, direction := none }.wellFormed = false

POST + LATIVE is ill-formed (POST only combines with translative).

theorem Fragments.Dargwa.Case.post_translative_wellformed : { localization := Localization.post, orientation := Orientation.translative, direction := none }.wellFormed = true

POST + TRANSLATIVE is the only well-formed POST combination.

theorem Fragments.Dargwa.Case.elative_needs_direction : { localization := Localization.super, orientation := Orientation.elative, direction := none }.wellFormed = false

Elative requires a direction marker.

theorem Fragments.Dargwa.Case.essive_rejects_direction : { localization := Localization.super, orientation := Orientation.essive, direction := some Direction.hither }.wellFormed = false

Essive rejects direction markers.

theorem Fragments.Dargwa.Case.super_elative_hither : { localization := Localization.super, orientation := Orientation.elative, direction := some Direction.hither }.wellFormed = true

SUPER-ELATIVE-HITHER (ex. 16: 'from the bridge hither') is well-formed.

theorem Fragments.Dargwa.Case.super_essive : { localization := Localization.super, orientation := Orientation.essive, direction := none }.wellFormed = true

SUPER-ESSIVE (ex. 12: 'on the bridge, position') is well-formed.

theorem Fragments.Dargwa.Case.sub_translative : { localization := Localization.sub, orientation := Orientation.translative, direction := none }.wellFormed = true

SUB-TRANSLATIVE (ex. 13: 'under the bridge, motion') is well-formed.

theorem Fragments.Dargwa.Case.translative_super_illformed : { localization := Localization.super, orientation := Orientation.translative, direction := none }.wellFormed = false

Translative + SUPER is ill-formed.