Shared Slavic Case Inventories

[CC93] [Bla94b]

The 6-case core (NOM/ACC/GEN/DAT/LOC/INST) attested across all modern Slavic case-bearing languages, plus a 7-case extension (with VOC) for Ukrainian/Polish/Czech/Serbo-Croat. Factored from per-language Fragments to remove byte-identical duplication.

Per-language sources (chapters of [CC93]): [She93] (p. 956), [Rot93] (p. 696), [Sho93a] (p. 466), [Bro93b] (p. 319), [Tim93] (p. 836), [Pri93] (p. 399).

Caha-containment lemmas live in Studies/Caha2009.lean (paper-anchored, keeps this substrate file Theory-import-free).

Inventories

@[reducible, inline]

abbrev Slavic.Case.coreInventory : Finset Case

The 6-case core: NOM, ACC, GEN, DAT, LOC, INST.

Equations

• Slavic.Case.coreInventory = {Case.nom, Case.acc, Case.gen, Case.dat, Case.loc, Case.inst}

@[reducible, inline]

abbrev Slavic.Case.sevenCaseInventory : Finset Case

The 6-case core extended with vocative; the inventory of Ukrainian, Polish, Czech, and Serbo-Croat. Does not satisfy Case.IsValidInventory — see sevenCaseInventory_not_isValid.

Equations

• Slavic.Case.sevenCaseInventory = {Case.nom, Case.acc, Case.gen, Case.dat, Case.loc, Case.inst, Case.voc}

API

theorem Slavic.Case.coreInventory_card : coreInventory.card = 6

theorem Slavic.Case.sevenCaseInventory_card : sevenCaseInventory.card = 7

Blake (typological hierarchy)

theorem Slavic.Case.coreInventory_isValid : Case.IsValidInventory coreInventory

theorem Slavic.Case.sevenCaseInventory_not_isValid : ¬Case.IsValidInventory sevenCaseInventory

VOC at Blake-rank 0 leaves a gap at rank 1 (COM/spatial), breaking contiguity.