Containment orders on Case

[Cah09] [Pan11] [McF18]

The object: a case feature carries a containment structure — its value is a downward-closed stack of nested feature shells, and one value contains another iff its shell stack does. The order is then the partial-rank order Core.Order.partialOrderOfRank over a shell-rank (unranked elements isolated), and the empirical *ABA syncretism law over it is the framework-neutral Morphology.Containment.IsContiguous (syncretism targets only adjacent cells). Both the order gadget and the *ABA predicate name no paper.

This file holds the two case-feature instances of that object, organized by the object, not by author:

• Nominal containment ([Cah09]): NOM ⊂ ACC ⊂ GEN ⊂ DAT ⊂ LOC, via containmentRank/kshells. ERG/ABS/INST/… are off-hierarchy (silent — containmentRank → none), and that silence is the theoretical content.
• Directional containment ([Pan11]): Place ⊂ Goal ⊂ Source ⊂ Route on the orthogonal path dimension, via PathDir/dirRank. The spatial case cells (ine/ela/ill, ade/abl/all, sup/del/sub) decompose as Region × PathDir (spatialDecomp), so cells inert under the nominal hierarchy gain structure.

Both reuse the same partialOrderOfRank gadget and certify the order as the shadow of the shell decomposition (*_iff_kshells_ssubset / *_iff_shells_ssubset) — derived, not stipulated.

Orders are scoped instances (open scoped Case.Caha): theoretical orders are opt-in commitments, never global instances on the inventory. Declarations live in the root Case namespace (the namespace follows the subject; the file stays in Syntax/Case/ as nanosyntactic substrate).

def Case.containmentRank : Case → Option (Fin 5)

Caha's containment rank ([Cah09]). 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). Codomain Option (Fin 5) — the boundedness is encoded in the type, matching Case.hierarchyRank.

Encoding caveat. [Cah09]'s Universal Case sequence is NOM-ACC-GEN-DAT-INST-COM (no LOC); his Russian-specific sequence inserts the prepositional/locative 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 ([Bla94b], which Caha argues 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

• Case.nom.containmentRank = some 0
• Case.acc.containmentRank = some 1
• Case.gen.containmentRank = some 2
• Case.dat.containmentRank = some 3
• Case.loc.containmentRank = some 4
• x✝.containmentRank = none

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

Caha's Slavic-specific Case sequence ([Cah09]; stated for Russian and confirmed 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).

Codomain Option (Fin 6): the six cases of the Slavic noun system are all on-hierarchy in Caha's Slavic encoding (hence Fin 6); the remaining Case cells, which are not part of that system, map to none.

Equations

• Case.nom.cahaSlavicRank = some 0
• Case.acc.cahaSlavicRank = some 1
• Case.gen.cahaSlavicRank = some 2
• Case.loc.cahaSlavicRank = some 3
• Case.dat.cahaSlavicRank = some 4
• Case.inst.cahaSlavicRank = some 5
• x✝.cahaSlavicRank = none

theorem Case.cahaSlavicRank_vs_containmentRank : nom.cahaSlavicRank = some 0 ∧ nom.containmentRank = some 0 ∧ acc.cahaSlavicRank = some 1 ∧ acc.containmentRank = some 1 ∧ gen.cahaSlavicRank = some 2 ∧ gen.containmentRank = some 2 ∧ loc.cahaSlavicRank = some 3 ∧ loc.containmentRank = some 4 ∧ dat.cahaSlavicRank = some 4 ∧ dat.containmentRank = some 3 ∧ inst.cahaSlavicRank = some 5 ∧ inst.containmentRank = 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.

@[reducible, inline]

abbrev Case.cahaLT : Case → 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

• Case.cahaLT = Core.Order.RankLT Case.containmentRank

@[reducible, inline]

abbrev Case.cahaLE : Case → 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

• Case.cahaLE = Core.Order.RankLE Case.containmentRank

The decomposition behind the order

Caha's claim is structural: each case on the hierarchy contains the representations of the cases below it, as a stack of case shells. The rank encoding above is the shadow of that decomposition.

def Case.kshells : Case → Option (Finset (Fin 5))

The shell stack of an on-hierarchy case: the downward-closed set of case shells its representation contains ([Cah09]'s nested functional sequence). Derived as the down-set Iic of the containment rank (Core.Order.rankShells), not stipulated alongside containmentRank — so the two cannot drift, and cahaLT_iff_kshells_ssubset is the structural shadow fact rather than a coincidence to be decided.

Equations

• Case.kshells = Core.Order.rankShells Case.containmentRank

theorem Case.cahaLT_iff_kshells_ssubset (c₁ c₂ : Case) : c₁.cahaLT c₂ ↔ Core.Order.RankLT kshells c₁ c₂

The order is the shadow of the decomposition: the containment order through the numeric rank coincides with the partial-rank order through the shell stacks (< on Finset is strict inclusion ⊂). Now an instance of the generic Core.Order.rankLT_iff_rankShells, since kshells is the rank's down-set decomposition.

The Caha order as scoped instances

A feature bears its theoretical order as an opt-in commitment (open scoped Case.Caha), never as a global instance on the inventory. The instance is Core.Order.partialOrderOfRank, so ≤ is definitionally cahaLE and < is cahaLT.

@[implicit_reducible]

def Case.Caha.instPartialOrderCaha : PartialOrder Case

Equations

• Case.Caha.instPartialOrderCaha = Core.Order.partialOrderOfRank Case.containmentRank

@[implicit_reducible]

def Case.Caha.instDecidableLe (c₁ c₂ : Case) : Decidable (c₁ ≤ c₂)

Equations

• Case.Caha.instDecidableLe c₁ c₂ = Case.Caha.instDecidableLe._aux_1 c₁ c₂

@[implicit_reducible]

def Case.Caha.instDecidableLt (c₁ c₂ : Case) : Decidable (c₁ < c₂)

Equations

• Case.Caha.instDecidableLt c₁ c₂ = Core.Order.instDecidableRelRankLTOfLt Case.containmentRank c₁ c₂

def Case.IsNonnominative (c : Case) : Prop

A case is nonnominative iff its representation contains ACC's, i.e. (.acc : Case) ≤ c in the Caha order. [McF18] argues this natural class underlies NOM-vs-oblique stem allomorphy: a VI rule conditioned on [ACC] captures the split found cross-linguistically (one of his arguments that the nominative is featurally empty).

Equations

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

@[implicit_reducible]

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

Equations

• c.instDecidableIsNonnominative = Case.instDecidableIsNonnominative._aux_1 c

def Case.IsOblique (c : Case) : Prop

A case is oblique iff its representation contains GEN's, i.e. (.gen : Case) ≤ c in the Caha order — the traditional structural-vs-oblique split (NOM/ACC vs GEN and above), stated through the containment encoding ([Cah09] supplies the encoding, not the terminology). 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 = (Case.gen ≤ c)

@[implicit_reducible]

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

Equations

• c.instDecidableIsOblique = Case.instDecidableIsOblique._aux_1 c

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

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

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

Ergative-aligned ABS/ERG are not oblique under the Caha hierarchy (off-hierarchy → incomparable with GEN). This makes the predicate usable for the ergative pronominal paradigms of [SMX+19] (Wardaman, Khinalugh — Studies/SmithMoskalEtAl2019.lean).

Sanity chain: NOM < ACC < GEN < DAT < LOC

Directional containment ([Pan11])

The second instance of the containment object, on the orthogonal path dimension: Place ⊂ Goal ⊂ Source ⊂ Route ([Pan11]'s functional sequence, ex. 2). A Source path structurally contains a Goal path — reflected morphologically where the Source marker contains the Goal marker (Imbabura Quechua Goal -man ⊂ Source -man-da; Estonian -l ⊂ -l-le ⊂ -l-t). Unlike the nominal containment, every path head is on the chain, so the order is total.

inductive Case.PathDir : Type

The path-direction heads, in containment order Place ⊂ Goal ⊂ Source ⊂ Route ([Pan11] ex. 2).

• place : PathDir

  Place: static location (the locative base; no motion).

• goal : PathDir

  Goal: motion to (built on Place).

• source : PathDir

  Source: motion from (built on Goal — the reversal).

• route : PathDir

  Route: motion via/through (built on Source).

@[implicit_reducible]

instance Case.instDecidableEqPathDir : DecidableEq PathDir

Equations

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

def Case.instReprPathDir.repr : PathDir → ℕ → Std.Format

Equations

• Case.instReprPathDir.repr Case.PathDir.place prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.PathDir.place")).group prec✝
• Case.instReprPathDir.repr Case.PathDir.goal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.PathDir.goal")).group prec✝
• Case.instReprPathDir.repr Case.PathDir.source prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.PathDir.source")).group prec✝
• Case.instReprPathDir.repr Case.PathDir.route prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.PathDir.route")).group prec✝

@[implicit_reducible]

instance Case.instReprPathDir : Repr PathDir

Equations

• Case.instReprPathDir = { reprPrec := Case.instReprPathDir.repr }

@[implicit_reducible]

instance Case.instFintypePathDir : Fintype PathDir

Equations

• Case.instFintypePathDir = { elems := { val := ↑Case.PathDir.enumList, nodup := Case.PathDir.enumList_nodup }, complete := Case.instFintypePathDir._proof_1 }

def Case.PathDir.rank : PathDir → Fin 4

Containment rank: how many path heads the direction nests. Place=0 ⊂ Goal=1 ⊂ Source=2 ⊂ Route=3.

Equations

• Case.PathDir.place.rank = 0
• Case.PathDir.goal.rank = 1
• Case.PathDir.source.rank = 2
• Case.PathDir.route.rank = 3

def Case.PathDir.shells (d : PathDir) : Finset (Fin 4)

The shell stack of a path direction: the downward-closed set of path heads its structure contains ([Pan11]'s nested [Route [Source [Goal [Place]]]]). Derived as the down-set Iic of PathDir.rank, not stipulated alongside it; lt_iff_shells_ssubset is then the structural shadow fact (mathlib's Finset.Iic_ssubset_Iic).

Equations

• d.shells = Finset.Iic d.rank

theorem Case.PathDir.lt_iff_shells_ssubset (d₁ d₂ : PathDir) : d₁.rank < d₂.rank ↔ d₁.shells ⊂ d₂.shells

The order is the shadow of the decomposition: directional containment (strict rank) coincides with strict inclusion of shell stacks — the directional analogue of cahaLT_iff_kshells_ssubset, here just Finset.Iic_ssubset_Iic since the shells are Iic of the rank.

Directional denotation ([Pan11] Ch. 5)

The interpret affordance for the directional dimension. Each path head denotes a phase profile over the path interval — whether the Figure occupies the Place-region at the start / middle / end (Pantcheva's +/− sequences). Place is stative (located throughout); Goal is a transition into the region (−−−−−+++++, ends located, ex. 5); Source is the reversal of Goal (+++++−−−−−, starts located, §5.4); Route passes through it (−−−−+++−−−−, located in the middle, ex. 10).

structure Case.PathProfile : Type

Whether the Figure occupies the Place-region at the start, middle, and end of the path — [Pan11]'s +/− phase profile sampled at three points.

• atStart : Bool

  The Figure is in the Place-region at the path's start.

• atMid : Bool

  … at the middle.

• atEnd : Bool

  … at the end.

def Case.instDecidableEqPathProfile.decEq (x✝ x✝¹ : PathProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Case.instDecidableEqPathProfile : DecidableEq PathProfile

Equations

• Case.instDecidableEqPathProfile = Case.instDecidableEqPathProfile.decEq

def Case.instReprPathProfile.repr : PathProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Case.instReprPathProfile : Repr PathProfile

Equations

• Case.instReprPathProfile = { reprPrec := Case.instReprPathProfile.repr }

def Case.PathProfile.reverse (p : PathProfile) : PathProfile

Reverse a profile (swap start and end) — the Source head's semantic operation ([Pan11] §5.4).

Equations

• p.reverse = { atStart := p.atEnd, atMid := p.atMid, atEnd := p.atStart }

def Case.PathDir.denote : PathDir → PathProfile

The denotation of a path direction ([Pan11] Ch. 5): the phase profile of the Figure–Place-region relation.

Equations

• Case.PathDir.place.denote = { atStart := true, atMid := true, atEnd := true }
• Case.PathDir.goal.denote = { atStart := false, atMid := false, atEnd := true }
• Case.PathDir.source.denote = { atStart := true, atMid := false, atEnd := false }
• Case.PathDir.route.denote = { atStart := false, atMid := true, atEnd := false }

theorem Case.PathDir.source_denote_eq_goal_reverse : source.denote = goal.denote.reverse

Source is the reversal of Goal ([Pan11] §5.4): the Source head reverses the Goal path. This grounds the *A&¬A syncretism constraint — a single Goal=Source marker would denote a path and its reverse, a contradiction (cf. Studies/Pantcheva2011.lean).

theorem Case.PathDir.goal_ends_source_starts : goal.denote.atEnd = true ∧ source.denote.atStart = true

Goal ends in the region; Source starts in it — the mirror-image structure of the two mono-transitional paths (§5.4).

def Case.dirOf : Case → Option PathDir

The path direction a spatial case expresses, if any. Robust across the inventory — direction is determinable even on the cells where region is conflated (regionOf is the partial companion). The spatial case cells decompose as Region × PathDir.

Equations

• Case.loc.dirOf = some Case.PathDir.place
• Case.ine.dirOf = some Case.PathDir.place
• Case.ade.dirOf = some Case.PathDir.place
• Case.sup.dirOf = some Case.PathDir.place
• Case.ill.dirOf = some Case.PathDir.goal
• Case.all.dirOf = some Case.PathDir.goal
• Case.sub.dirOf = some Case.PathDir.goal
• Case.ela.dirOf = some Case.PathDir.source
• Case.abl.dirOf = some Case.PathDir.source
• Case.del.dirOf = some Case.PathDir.source
• Case.perl.dirOf = some Case.PathDir.route
• x✝.dirOf = none

The orthogonal Region axis

The Place-internal localization Pantcheva does not decompose (interior/surface/exterior), orthogonal to PathDir. Spatial case systems (Finnish, Hungarian, Daghestanian) cross it with direction.

inductive Case.Region : Type

The spatial region a case localizes in. Orthogonal to PathDir.

• interior : Region

  Interior: in/into/out-of (Finnish inessive/illative/elative).

• surface : Region

  Surface: on/onto/off-of (Hungarian superessive/sublative/delative).

• exterior : Region

  Exterior: at/to/from (Finnish adessive/allative/ablative).

@[implicit_reducible]

instance Case.instDecidableEqRegion : DecidableEq Region

Equations

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

@[implicit_reducible]

instance Case.instReprRegion : Repr Region

Equations

• Case.instReprRegion = { reprPrec := Case.instReprRegion.repr }

def Case.instReprRegion.repr : Region → ℕ → Std.Format

Equations

• Case.instReprRegion.repr Case.Region.interior prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Region.interior")).group prec✝
• Case.instReprRegion.repr Case.Region.surface prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Region.surface")).group prec✝
• Case.instReprRegion.repr Case.Region.exterior prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Case.Region.exterior")).group prec✝

@[implicit_reducible]

instance Case.instFintypeRegion : Fintype Region

Equations

• Case.instFintypeRegion = { elems := { val := ↑Case.Region.enumList, nodup := Case.Region.enumList_nodup }, complete := Case.instFintypeRegion._proof_1 }

def Case.toCase : Region → PathDir → Option Case

Build a spatial case from its Region × PathDir decomposition — the constructor direction spatial-case fragments consume. The 3 × 3 region-specific cells; route is region-neutral in these inventories (none).

Equations

• Case.toCase Case.Region.interior Case.PathDir.place = some Case.ine
• Case.toCase Case.Region.interior Case.PathDir.goal = some Case.ill
• Case.toCase Case.Region.interior Case.PathDir.source = some Case.ela
• Case.toCase Case.Region.surface Case.PathDir.place = some Case.sup
• Case.toCase Case.Region.surface Case.PathDir.goal = some Case.sub
• Case.toCase Case.Region.surface Case.PathDir.source = some Case.del
• Case.toCase Case.Region.exterior Case.PathDir.place = some Case.ade
• Case.toCase Case.Region.exterior Case.PathDir.goal = some Case.all
• Case.toCase Case.Region.exterior Case.PathDir.source = some Case.abl
• Case.toCase x✝ Case.PathDir.route = none

def Case.regionOf : Case → Option Region

The region a case localizes in, under the spatial reading. The exterior series is ade/all/abl (Finnish's external local cases). Conflation caveat: all/abl double as the general allative/ablative (Latin-type, region-neutral); the spatial decomposition reads them as exterior-goal/source, the use the analytical split Features/Case/Basic.lean anticipates separating. loc is the genuinely region-neutral general locative (none).

Equations

• Case.ine.regionOf = some Case.Region.interior
• Case.ela.regionOf = some Case.Region.interior
• Case.ill.regionOf = some Case.Region.interior
• Case.sup.regionOf = some Case.Region.surface
• Case.del.regionOf = some Case.Region.surface
• Case.sub.regionOf = some Case.Region.surface
• Case.ade.regionOf = some Case.Region.exterior
• Case.all.regionOf = some Case.Region.exterior
• Case.abl.regionOf = some Case.Region.exterior
• x✝.regionOf = none

def Case.spatialDecomp (c : Case) : Option (Region × PathDir)

Analyze a spatial case into Region × PathDir, where both are determinable (lossy on region-conflated cells; the faithful inverse of toCase on the 3 × 3 region-specific cells).

Equations

• c.spatialDecomp = match c.regionOf, c.dirOf with | some r, some d => some (r, d) | x, x_1 => none

theorem Case.spatialDecomp_toCase (r : Region) (d : PathDir) : (toCase r d).bind spatialDecomp = Option.map (fun (x : Case) => (r, d)) (toCase r d)

toCase and spatialDecomp are inverse on the region-specific cells — the decomposition round-trips where region is not conflated. (route is region-neutral, hence none on both sides.)