Case Allomorphy and Syncretism — Substrate

@cite{blake-1994} @cite{caha-2009} @cite{bobaljik-2012}

Framework-neutral substrate for talking about allomorphy and syncretism patterns over morphological case. Provides:

• AllomorphyPattern: a 4-tuple of form-class indices over the four core cases (NOM, ACC, GEN, DAT); decidable ViolatesABA / IsContiguous predicates derived from Morphology.Containment.
• HierarchyAdjacent / InventoryAdjacent: adjacency relations on cases, the latter relativized to a particular language's inventory.
• Syncretism: a record-pair of cases that share an exponent.
• A handful of well-known syncretism patterns (NOM/ACC, COM/INST) and decidability theorems for adjacency on small inventories.

What explains the *ABA gap is contested between DM (post-syntactic VI + Elsewhere ordering — @cite{bobaljik-2012}) and Nanosyntax (phrasal spellout + Superset Principle — @cite{caha-2009}). This file commits to neither; per-paper analyses live in Phenomena/Case/Studies/.

structure Core.Case.Allomorphy.AllomorphyPattern : Type

An allomorphy pattern over the four core cases (NOM, ACC, GEN, DAT), represented as a form-class index for each case.

• nom : ℕ
• acc : ℕ
• gen : ℕ
• dat : ℕ

def Core.Case.Allomorphy.instDecidableEqAllomorphyPattern.decEq (x✝ x✝¹ : AllomorphyPattern) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.Case.Allomorphy.instDecidableEqAllomorphyPattern : DecidableEq AllomorphyPattern

Equations

• Core.Case.Allomorphy.instDecidableEqAllomorphyPattern = Core.Case.Allomorphy.instDecidableEqAllomorphyPattern.decEq

def Core.Case.Allomorphy.instReprAllomorphyPattern.repr : AllomorphyPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Case.Allomorphy.instReprAllomorphyPattern : Repr AllomorphyPattern

Equations

• Core.Case.Allomorphy.instReprAllomorphyPattern = { reprPrec := Core.Case.Allomorphy.instReprAllomorphyPattern.repr }

def Core.Case.Allomorphy.AllomorphyPattern.ViolatesABA (p : AllomorphyPattern) : Prop

A pattern violates *ABA when its 4-position projection violates the generic contiguity predicate. By construction this reduces by rfl to the generic substrate's ViolatesABA on the list.

Equations

• p.ViolatesABA = Morphology.Containment.ViolatesABA [p.nom, p.acc, p.gen, p.dat]

@[implicit_reducible]

instance Core.Case.Allomorphy.instDecidableViolatesABA (p : AllomorphyPattern) : Decidable p.ViolatesABA

Equations

• Core.Case.Allomorphy.instDecidableViolatesABA p = Core.Case.Allomorphy.instDecidableViolatesABA._aux_1 p

def Core.Case.Allomorphy.AllomorphyPattern.IsContiguous (p : AllomorphyPattern) : Prop

Is a pattern contiguous? Each form class occupies a contiguous span on the hierarchy. Equivalent to ¬ViolatesABA.

Equations

• p.IsContiguous = ¬p.ViolatesABA

@[implicit_reducible]

instance Core.Case.Allomorphy.instDecidableIsContiguous (p : AllomorphyPattern) : Decidable p.IsContiguous

Equations

• Core.Case.Allomorphy.instDecidableIsContiguous p = Core.Case.Allomorphy.instDecidableIsContiguous._aux_1 p

case_violatesABA_iff_generic was previously a named Iff.rfl bridge here. Dropped: by construction AllomorphyPattern.ViolatesABA is the generic predicate applied to the 4-cell projection (definitionally), so the bridge unfolds for free at every use site via Iff.rfl or rfl-shaped simp rewrites. Naming a rfl bridge polluted the API surface for no benefit.

def Core.Case.Allomorphy.abbPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.abbPattern = { nom := 0, acc := 1, gen := 1, dat := 1 }

def Core.Case.Allomorphy.aabPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.aabPattern = { nom := 0, acc := 0, gen := 0, dat := 1 }

def Core.Case.Allomorphy.aabbPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.aabbPattern = { nom := 0, acc := 0, gen := 1, dat := 1 }

def Core.Case.Allomorphy.ababPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.ababPattern = { nom := 0, acc := 1, gen := 0, dat := 1 }

def Core.Case.Allomorphy.abaPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.abaPattern = { nom := 0, acc := 1, gen := 0, dat := 0 }

def Core.Case.Allomorphy.babPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.babPattern = { nom := 1, acc := 0, gen := 1, dat := 0 }

def Core.Case.Allomorphy.uniformPattern : AllomorphyPattern

Equations

• Core.Case.Allomorphy.uniformPattern = { nom := 0, acc := 0, gen := 0, dat := 0 }

Smoke tests for the named patterns: each evaluates as the AllomorphyPattern shape its name implies. Demoted from theorem to example because nothing in the codebase consumes them by name.

theorem Core.Case.Allomorphy.containment_refines_blake : hierarchyRank UD.Case.nom ≥ hierarchyRank UD.Case.acc ∧ hierarchyRank UD.Case.acc ≥ hierarchyRank UD.Case.gen ∧ hierarchyRank UD.Case.gen ≥ hierarchyRank UD.Case.dat

Containment rank preserves Blake's typological ordering on the core cases (NOM, ACC, GEN, DAT): the orderings are inverses. Blake ranks by "how likely a language is to have it" (NOM most common → highest), while the containment view ranks by "how much structure it contains" (NOM least complex → lowest). This is a theorem about the Blake hierarchy, framework-neutral.

structure Core.Case.Allomorphy.Syncretism : Type

A syncretism pattern: two cases share a morphological exponent.

• case1 : Case
• case2 : Case
• neq : self.case1 ≠ self.case2

@[implicit_reducible]

instance Core.Case.Allomorphy.instReprSyncretism : Repr Syncretism

Equations

• Core.Case.Allomorphy.instReprSyncretism = { reprPrec := Core.Case.Allomorphy.instReprSyncretism.repr }

def Core.Case.Allomorphy.instReprSyncretism.repr : Syncretism → ℕ → Std.Format

Equations

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

def Core.Case.Allomorphy.HierarchyAdjacent (c1 c2 : Case) : Prop

Are two cases adjacent on the hierarchy (same rank or ranks differ by 1)?

Equations

• Core.Case.Allomorphy.HierarchyAdjacent c1 c2 = (c1.hierarchyRank = c2.hierarchyRank ∨ c1.hierarchyRank + 1 = c2.hierarchyRank ∨ c2.hierarchyRank + 1 = c1.hierarchyRank)

@[implicit_reducible]

instance Core.Case.Allomorphy.instDecidableRelHierarchyAdjacent : DecidableRel HierarchyAdjacent

Equations

• Core.Case.Allomorphy.instDecidableRelHierarchyAdjacent x✝¹ x✝ = Core.Case.Allomorphy.instDecidableRelHierarchyAdjacent._aux_1 x✝¹ x✝

def Core.Case.Allomorphy.InventoryAdjacent (inv : Finset Case) (c1 c2 : Case) : Prop

Relaxed adjacency: no case in the inventory falls strictly between the two syncretic cases on the hierarchy.

Equations

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

@[implicit_reducible]

instance Core.Case.Allomorphy.instDecidableInventoryAdjacent (inv : Finset Case) (c1 c2 : Case) : Decidable (InventoryAdjacent inv c1 c2)

Equations

• Core.Case.Allomorphy.instDecidableInventoryAdjacent inv c1 c2 = id inferInstance

def Core.Case.Allomorphy.nomAccSyncretism : Syncretism

Equations

• Core.Case.Allomorphy.nomAccSyncretism = { case1 := UD.Case.nom, case2 := UD.Case.acc, neq := Core.Case.Allomorphy.nomAccSyncretism._proof_1 }

def Core.Case.Allomorphy.comInstSyncretism : Syncretism

Equations

• Core.Case.Allomorphy.comInstSyncretism = { case1 := UD.Case.com, case2 := UD.Case.inst, neq := Core.Case.Allomorphy.comInstSyncretism._proof_1 }

Adjacency-on-canonical-hierarchy smoke tests. The named theorems below have no codebase consumers (Tamil/Case.lean defines its own locally-named com_inst_adjacent, not a use of this one); all are examples. The one consumed lemma is same_tier_adjacent, kept as theorem because it is parametric over the hierarchy ranks (not a fixed pair).

theorem Core.Case.Allomorphy.same_tier_adjacent (c1 c2 : Case) (h : c1.hierarchyRank = c2.hierarchyRank) : HierarchyAdjacent c1 c2

Same-tier cases are always strictly adjacent. (Parametric over the rank — kept as named theorem for downstream re-use.)

Five fixed AllomorphyPattern shapes that show up in the syncretism literature. Demoted to example for the same reason as the smoke tests above: no by-name consumers.