Caha Containment Order on Case

@cite{caha-2009} @cite{mcfadden-2018}

The canonical order on Core.Case: state-of-the-art syntax (configurational case + nanosyntactic spellout) assumes Caha's containment as the default. Each case on the hierarchy literally contains the representations of all cases below it:

[[[[[ NOM ] ACC ] GEN ] DAT ] LOC ]

Cases without a containmentRank (ERG, ABS, INST, COM, …) are silent — incomparable with on-hierarchy cases under ≤, except for reflexivity. That silence is the theoretical content: Caha's hierarchy is silent on those cases, and the PartialOrder structure preserves the silence.

Other orders (Blake's typological frequency in Core/Case/Hierarchy.lean, per-language syncretism graphs) live as named defs used locally via letI rather than as competing instances on Case.

def Core.Case.containmentRank : Case → Option ℕ

Caha's containment rank (@cite{caha-2009}). Cases higher on the containment hierarchy have representations that include all lower cases.

[[[[[ NOM ] ACC ] GEN ] DAT ] LOC ]

Returns none for cases not on the containment hierarchy (e.g., ERG/ABS in ergative systems, or minor cases whose containment structure is less well established).

Encoding caveat. @cite{caha-2009} (10b), p. 10 gives the Universal Case sequence NOM-ACC-GEN-DAT-INST-COM (no LOC); the Russian-specific sequence (16) p. 12 inserts PREP between GEN and DAT. The encoding below — NOM=0, ACC=1, GEN=2, DAT=3, LOC=4, INST=none — matches neither verbatim; it is closer to Blake's typological hierarchy (@cite{blake-1994} §5.8, which Caha himself argues on p. 31 should coincide with his sequence). For Slavic 6-case inventories the encoding choice is verdict-equivalent; inventories with INST or COM without LOC may diverge. For paradigm-shape work that needs Caha's actual Slavic ordering, see cahaSlavicRank below.

Equations

• Core.Case.containmentRank UD.Case.Nom = some 0
• Core.Case.containmentRank UD.Case.Acc = some 1
• Core.Case.containmentRank UD.Case.Gen = some 2
• Core.Case.containmentRank UD.Case.Dat = some 3
• Core.Case.containmentRank UD.Case.Loc = some 4
• x✝.containmentRank = none

def Core.Case.cahaSlavicRank : Case → Option (Fin 6)

Caha's Slavic-specific Case sequence (@cite{caha-2009} (16) p. 12 for Russian; (7) p. 238 confirms the same for Serbian): NOM – ACC – GEN – PREP/LOC – DAT – INS. Differs from containmentRank in placing LOC between GEN and DAT (not at top) and INST at the top (not off-hierarchy). Use this rank for paradigm-shape contiguity claims referencing Caha's Slavic data; use containmentRank for inventory downward-closure verdicts (where the choice is Slavic-equivalent).

Returns Fin 6 rather than Option Nat: all six cases are on-hierarchy in Caha's Slavic encoding; there are no off-hierarchy cases for the Slavic noun system. The Option is preserved for consistency with containmentRank's API and to flag non-Slavic cases as not-in-the-Slavic-sequence.

Equations

• Core.Case.cahaSlavicRank UD.Case.Nom = some 0
• Core.Case.cahaSlavicRank UD.Case.Acc = some 1
• Core.Case.cahaSlavicRank UD.Case.Gen = some 2
• Core.Case.cahaSlavicRank UD.Case.Loc = some 3
• Core.Case.cahaSlavicRank UD.Case.Dat = some 4
• Core.Case.cahaSlavicRank UD.Case.Ins = some 5
• x✝.cahaSlavicRank = none

theorem Core.Case.cahaSlavicRank_vs_containmentRank : cahaSlavicRank UD.Case.nom = some 0 ∧ containmentRank UD.Case.nom = some 0 ∧ cahaSlavicRank UD.Case.acc = some 1 ∧ containmentRank UD.Case.acc = some 1 ∧ cahaSlavicRank UD.Case.gen = some 2 ∧ containmentRank UD.Case.gen = some 2 ∧ cahaSlavicRank UD.Case.loc = some 3 ∧ containmentRank UD.Case.loc = some 4 ∧ cahaSlavicRank UD.Case.dat = some 4 ∧ containmentRank UD.Case.dat = some 3 ∧ cahaSlavicRank UD.Case.inst = some 5 ∧ containmentRank UD.Case.inst = none

cahaSlavicRank and containmentRank agree on the four core cases (NOM=0, ACC=1, GEN=2 in both) and disagree on LOC/DAT/INST. The disagreement is deliberate: containmentRank is verdict-equivalent on Slavic inventories for downward-closure (RespectsCahaContainment), while cahaSlavicRank is needed for paradigm-shape contiguity claims that respect Caha's actual Slavic sequence.

def Core.Case.cahaLT (c₁ c₂ : Case) : Prop

Strict containment on Caha-rank Cases: both must have a rank, and the first's must be strictly smaller. False whenever either side is off-hierarchy.

Equations

• c₁.cahaLT c₂ = match c₁.containmentRank, c₂.containmentRank with | some n, some m => n < m | x, x_1 => False

@[implicit_reducible]

instance Core.Case.instDecidableCahaLT : DecidableRel cahaLT

Equations

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

def Core.Case.cahaLE (c₁ c₂ : Case) : Prop

The Caha containment order. c₁ ≤ c₂ iff either they are equal, or cahaLT c₁ c₂. Off-hierarchy cases are reflexively ≤ themselves and incomparable with everything else.

Equations

• c₁.cahaLE c₂ = (c₁ = c₂ ∨ c₁.cahaLT c₂)

@[implicit_reducible]

instance Core.Case.instDecidableRelCahaLE : DecidableRel cahaLE

Equations

• x✝¹.instDecidableRelCahaLE x✝ = Core.Case.instDecidableRelCahaLE._aux_1 x✝¹ x✝

@[implicit_reducible]

instance Core.Case.instLE : LE Case

Equations

• Core.Case.instLE = { le := Core.Case.cahaLE }

@[implicit_reducible]

instance Core.Case.instDecidableLe (c₁ c₂ : Case) : Decidable (c₁ ≤ c₂)

Equations

• c₁.instDecidableLe c₂ = c₁.instDecidableRelCahaLE c₂

theorem Core.Case.cahaLE_refl (c : Case) : c ≤ c

theorem Core.Case.cahaLT_trans {a b c : Case} : a.cahaLT b → b.cahaLT c → a.cahaLT c

theorem Core.Case.cahaLE_trans (a b c : Case) : a ≤ b → b ≤ c → a ≤ c

theorem Core.Case.cahaLE_antisymm (a b : Case) : a ≤ b → b ≤ a → a = b

@[implicit_reducible]

instance Core.Case.instPreorder : Preorder Case

Equations

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

@[implicit_reducible]

instance Core.Case.instPartialOrder : PartialOrder Case

Equations

• Core.Case.instPartialOrder = { toPreorder := Core.Case.instPreorder, le_antisymm := ⋯ }

def Core.Case.IsNonnominative (c : Case) : Prop

A case is nonnominative iff its representation contains ACC's, i.e. (.acc : Case) ≤ c in the Caha order. @cite{mcfadden-2018} argues this is the key natural class for stem allomorphy: a VI rule conditioned on [ACC] captures the NOM-vs-oblique split found cross-linguistically.

Equations

• c.IsNonnominative = (UD.Case.acc ≤ c)

@[implicit_reducible]

instance Core.Case.instDecidableIsNonnominative (c : Case) : Decidable c.IsNonnominative

Equations

• c.instDecidableIsNonnominative = Core.Case.instDecidableIsNonnominative._aux_1 c

def Core.Case.IsOblique (c : Case) : Prop

A case is oblique iff its representation contains GEN's, i.e. (.gen : Case) ≤ c in the Caha order. Per @cite{caha-2009}'s Unmarked-Dependent vs Oblique split, NOM/ACC are unmarked-dependent and GEN/DAT/LOC/INS/COM/etc. are oblique. Ergative-aligned ABS/ERG are off-hierarchy in containmentRank and so satisfy ¬ IsOblique (consistent with their parallel-to-NOM/ACC structural status).

Equations

• c.IsOblique = (UD.Case.gen ≤ c)

@[implicit_reducible]

instance Core.Case.instDecidableIsOblique (c : Case) : Decidable c.IsOblique

Equations

• c.instDecidableIsOblique = Core.Case.instDecidableIsOblique._aux_1 c

theorem Core.Case.isOblique_split_core : ¬IsOblique UD.Case.nom ∧ ¬IsOblique UD.Case.acc ∧ IsOblique UD.Case.gen ∧ IsOblique UD.Case.dat

The four core McFadden-hierarchy cases stratify cleanly between non-oblique (NOM, ACC) and oblique (GEN, DAT).

theorem Core.Case.isOblique_erg_abs_false : ¬IsOblique UD.Case.erg ∧ ¬IsOblique UD.Case.abs

Ergative-aligned ABS/ERG are not oblique under the Caha hierarchy (off-hierarchy → incomparable with GEN). This makes the predicate usable for SMSE 2019-style ergative paradigms (Wardaman, Khinalugh).

theorem Core.Case.nom_le_acc : UD.Case.nom ≤ UD.Case.acc

theorem Core.Case.acc_le_gen : UD.Case.acc ≤ UD.Case.gen

theorem Core.Case.gen_le_dat : UD.Case.gen ≤ UD.Case.dat

theorem Core.Case.dat_le_loc : UD.Case.dat ≤ UD.Case.loc

theorem Core.Case.erg_incomparable_nom : ¬UD.Case.erg ≤ UD.Case.nom

Off-hierarchy cases (ERG) are incomparable with on-hierarchy cases.

theorem Core.Case.nom_incomparable_erg : ¬UD.Case.nom ≤ UD.Case.erg