Paradigm contiguity: the *ABA generalization

Across graded paradigms — degree (positive < comparative < superlative, [Bob12]), case (NOM < ACC < GEN < DAT, [Cah09]), path roles ([Pan11]) — the cross-linguistic *ABA generalization says a form never recurs across a distinct intervening form: each form's fiber is order-convex (IsContiguous). [Gra19] reconstructs *ABA across these domains as feasible monotonicity: the form assignment is monotone with respect to some linear order on the output forms (his def. (6); the cell order is what is fixed). Over linearly ordered cells, that is equivalent to the assignment being the kernel of a monotone score (FeasiblyMonotone) — isContiguous_iff_feasiblyMonotone, stated here as the general theorem behind Graf's instance-by-instance verification, independently of any insertion mechanism.

Theory-laden derivations of contiguity (vocabulary insertion under the Elsewhere Condition over containment hierarchies) live in Morphology/Exponence/Containment/Contiguity.lean; the n = 3 degree and n = 4 case specializations in Morphology/Paradigm/Degree.lean and Morphology/Paradigm/Case.lean.

Main declarations

• IsContiguous — no ABA configuration: fibers are convex
• FeasiblyMonotone, isContiguous_iff_feasiblyMonotone — [Gra19]'s monotonicity reconstruction of *ABA
• IsContiguous.comp_monotone, isContiguous_comp_left — composition API

def Morphology.IsContiguous {n : ℕ} {F : Type u_1} (p : Paradigm n F) : Prop

A paradigm is contiguous when no form recurs across a distinct intervening form: if the cells at i ≤ k agree, every cell between them agrees too, so each form's fiber is an interval of cells. ABA (![a, b, a]) violates this; AAA, ABB, ABC — and AAB — satisfy it. (*AAB is excluded by vocabulary-level conditions, not by contiguity; see Morphology/Exponence/Containment/Contiguity.lean.)

Equations

• Morphology.IsContiguous p = ∀ ⦃i j k : Fin n⦄, i ≤ j → j ≤ k → p i = p k → p i = p j

@[implicit_reducible]

instance Morphology.instDecidableIsContiguousOfDecidableEq {n : ℕ} {F : Type u_1} [DecidableEq F] (p : Paradigm n F) : Decidable (IsContiguous p)

Equations

• Morphology.instDecidableIsContiguousOfDecidableEq p = Morphology.instDecidableIsContiguousOfDecidableEq._aux_1 p

theorem Morphology.IsContiguous.comp_monotone {n : ℕ} {F : Type u_1} {m : ℕ} {p : Paradigm n F} (hp : IsContiguous p) {f : Fin m → Fin n} (hf : Monotone f) : IsContiguous (p ∘ f)

Precomposition with a monotone regrading preserves contiguity.

theorem Morphology.isContiguous_comp_left {n : ℕ} {F : Type u_1} {β : Type u_2} [PartialOrder β] {g : Fin n → β} (hg : Monotone g) {h : β → F} (hh : Set.InjOn h (Set.range g)) : IsContiguous (h ∘ g)

A paradigm that factors as a monotone score followed by a map injective on the score's range is contiguous.

Graf's monotonicity reconstruction

[Gra19] recasts the *ABA generalization — across adjectival gradation, person-pronoun syncretism, case syncretism, and noun stem allomorphy — as feasible monotonicity of the form assignment from a fixed cell order ([BS18b] is the feature-combinatoric counterpart, deriving which cell arrangements exclude ABA without stipulating containment). The kernel formulation below is this file's gloss: forms are bins, so feasible monotonicity over linearly ordered cells is the existence of a monotone score with the paradigm's kernel. The prefix-image score i ↦ #{forms among cells 0..i} is monotone and has the same kernel as a contiguous paradigm, and conversely any paradigm sharing its kernel with a monotone score has convex fibers. (Graf's case hierarchies are partial orders going beyond this linear setting, and his PCC/GCC treatment is a different object — monotone maps into the fixed two-element truth-value algebra, i.e. upper sets; see Studies/Graf2019.lean.)

def Morphology.FeasiblyMonotone {n : ℕ} {F : Type u_1} (p : Paradigm n F) : Prop

Feasible monotonicity ([Gra19] def. (6)), in monotone-score form: some monotone score identifies exactly the cells the paradigm identifies. Equivalent to Graf's literal statement — monotone with respect to some linear order on the output forms — over finitely many cells, since forms are bins and only the kernel matters.

Equations

• Morphology.FeasiblyMonotone p = ∃ (g : Fin n → ℕ), Monotone g ∧ ∀ (i j : Fin n), p i = p j ↔ g i = g j

theorem Morphology.isContiguous_iff_feasiblyMonotone {n : ℕ} {F : Type u_1} (p : Paradigm n F) : IsContiguous p ↔ FeasiblyMonotone p

*[Gra19]'s monotonicity reconstruction of ABA: a paradigm is contiguous iff it is feasibly monotonic. Forward direction via the prefix-image score; backward direction is the sandwich argument that makes monotone kernels convex.