Case paradigms

Framework-neutral substrate for allomorphy patterns over the four core cases (NOM, ACC, GEN, DAT): the n = 4 specialization of Morphology.Paradigm, mirroring Morphology/Paradigm/Degree.lean for degree. AllomorphyPattern is the ergonomic record form; AllomorphyPattern.toParadigm connects it to the general substrate, and the decidable IsContiguous / ViolatesABA predicates are defined through that projection, so the generic theory applies by construction.

What explains the *ABA gap is contested between DM (post-syntactic VI + Elsewhere ordering — [Bob12]) and Nanosyntax (phrasal spellout + Superset Principle — [Cah09]). This file commits to neither; per-paper analyses live in Studies/. Case-hierarchy adjacency and inventory relations live with the Blake-rank API in Features/Case/Basic.lean.

structure Morphology.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 Morphology.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 Morphology.Case.Allomorphy.instDecidableEqAllomorphyPattern : DecidableEq AllomorphyPattern

Equations

• Morphology.Case.Allomorphy.instDecidableEqAllomorphyPattern = Morphology.Case.Allomorphy.instDecidableEqAllomorphyPattern.decEq

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

Equations

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

@[implicit_reducible]

instance Morphology.Case.Allomorphy.instReprAllomorphyPattern : Repr AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.AllomorphyPattern.toParadigm (p : AllomorphyPattern) : Paradigm 4 ℕ

The general-substrate form of an allomorphy pattern: the n = 4 instance of Morphology.Paradigm.

Equations

• p.toParadigm = ![p.nom, p.acc, p.gen, p.dat]

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

Is a pattern contiguous? Each form class occupies a contiguous span on the hierarchy — the generic Morphology.IsContiguous (Paradigm/Contiguity.lean), by construction.

Equations

• p.IsContiguous = Morphology.IsContiguous p.toParadigm

@[implicit_reducible]

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

Equations

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

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

A pattern violates *ABA: some form class recurs across a distinct intervening one. Equivalent to ¬IsContiguous.

Equations

• p.ViolatesABA = ¬p.IsContiguous

@[implicit_reducible]

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

Equations

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

def Morphology.Case.Allomorphy.abbPattern : AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.aabPattern : AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.aabbPattern : AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.ababPattern : AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.abaPattern : AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.babPattern : AllomorphyPattern

Equations

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

def Morphology.Case.Allomorphy.uniformPattern : AllomorphyPattern

Equations

• Morphology.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.

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.