Domain-relativized contiguity

A domain partition assigns each grade of a containment hierarchy a domain tag — abstractly representing the grade's locality unit (spellout domain / phase / accessibility domain). Within a domain, the *ABA contiguity constraint applies; across domain boundaries, ABA-shaped recurrences are admitted.

Motivation

Structural adjacency ([Bob12]) predicts no ABA-shaped recurrences anywhere in a containment hierarchy, but AAB patterns attested in case and number suppletion falsify the universal form of the prediction (Wardaman case, Yagua number; [SMX+19], whose study file carries the data). [SMX+19] attribute the gap to locality, adopting [Mos15b]'s accessibility domains: a category-defining node delimits the material that can condition root suppletion, so *ABA holds within a domain and ABA shapes across a domain boundary are admitted.

What this substrate models, and what it doesn't

A DomainPartition is the output of a locality computation projected onto the grades: which locality unit each grade belongs to. The substrate is theory-neutral about the source — [Mos15b]'s accessibility domains cut the hierarchy at a delimiting node (DomainPartition.threshold), [embick-2010]'s linear adjacency puts every grade in its own one-cell domain, [Bob12]'s structural adjacency uses the trivial partition. Consumers state which projection they want. The trigger-relative rule side is SmithMoskalEtAl2019.DomainLocal.

Main declarations

• DomainPartition n Tag — domain tag per grade; DomainPartition.IsConvex, DomainPartition.threshold — the interval-shaped partitions locality theories generate
• ViolatesABAWithin, IsContiguousWithin — *ABA relativized to same-domain triples, over Morphology.Paradigm
• isContiguousWithin_trivial_iff — under the trivial partition this is exactly Morphology.IsContiguous
• violatesABAWithin_iff_of_convex — for convex partitions the check needs only the outer grades to share a domain

@[reducible, inline]

abbrev Morphology.DomainPartition (n : ℕ) (Tag : Type u_3) : Type u_3

A domain partition assigns each grade of an n-grade hierarchy a domain tag. Polymorphic over the tag type so consumers can use whatever tag type their analysis demands.

Equations

• Morphology.DomainPartition n Tag = (Fin n → Tag)

@[reducible, inline]

abbrev Morphology.SameDomain {n : ℕ} {Tag : Type u_1} (π : DomainPartition n Tag) (i j : Fin n) : Prop

Two grades lie in the same domain.

Equations

• Morphology.SameDomain π i j = (π i = π j)

@[instance_reducible]

instance Morphology.instDecidableSameDomainOfDecidableEq {n : ℕ} {Tag : Type u_1} [DecidableEq Tag] (π : DomainPartition n Tag) (i j : Fin n) : Decidable (SameDomain π i j)

Equations

• Morphology.instDecidableSameDomainOfDecidableEq π i j = inst✝ (π i) (π j)

@[reducible, inline]

abbrev Morphology.DomainPartition.trivial (n : ℕ) : DomainPartition n Unit

The trivial partition: every grade in one domain.

Equations

• Morphology.DomainPartition.trivial n x✝ = ()

def Morphology.DomainPartition.IsConvex {n : ℕ} {Tag : Type u_1} (π : DomainPartition n Tag) : Prop

A partition is convex when its domains are intervals of the hierarchy: anything between two same-domain grades lies in their domain. Locality theories generate convex partitions — an accessibility domain is the initial segment below the delimiting node ([Mos15b]).

Equations

• π.IsConvex = ∀ ⦃i j k : Fin n⦄, i ≤ j → j ≤ k → Morphology.SameDomain π i k → Morphology.SameDomain π i j

def Morphology.DomainPartition.threshold (n t : ℕ) : DomainPartition n Bool

The threshold partition: grades below t inside the root's domain, grades from t up outside it — the shape of an accessibility-domain cut at a category-defining node ([Mos15b]).

Equations

• Morphology.DomainPartition.threshold n t i = decide (↑i < t)

theorem Morphology.DomainPartition.threshold_isConvex (n t : ℕ) : (threshold n t).IsConvex

Threshold partitions are convex.

def Morphology.ViolatesABAWithin {n : ℕ} {Tag : Type u_1} {F : Type u_2} (π : DomainPartition n Tag) (p : Paradigm n F) : Prop

A pattern violates the domain-relativized *ABA constraint: some form recurs across a distinct intervening form, with all three grades in the same domain.

Equations

• Morphology.ViolatesABAWithin π p = ∃ (i : Fin n) (j : Fin n) (k : Fin n), i < j ∧ j < k ∧ Morphology.SameDomain π i j ∧ Morphology.SameDomain π i k ∧ p i = p k ∧ p i ≠ p j

@[instance_reducible]

instance Morphology.instDecidableViolatesABAWithinOfDecidableEq {n : ℕ} {Tag : Type u_1} {F : Type u_2} [DecidableEq Tag] [DecidableEq F] (π : DomainPartition n Tag) (p : Paradigm n F) : Decidable (ViolatesABAWithin π p)

Equations

• Morphology.instDecidableViolatesABAWithinOfDecidableEq π p = id inferInstance

def Morphology.IsContiguousWithin {n : ℕ} {Tag : Type u_1} {F : Type u_2} (π : DomainPartition n Tag) (p : Paradigm n F) : Prop

Domain-relativized contiguity: no within-domain *ABA violation.

Equations

• Morphology.IsContiguousWithin π p = ¬Morphology.ViolatesABAWithin π p

@[instance_reducible]

instance Morphology.instDecidableIsContiguousWithinOfDecidableEq {n : ℕ} {Tag : Type u_1} {F : Type u_2} [DecidableEq Tag] [DecidableEq F] (π : DomainPartition n Tag) (p : Paradigm n F) : Decidable (IsContiguousWithin π p)

Equations

• Morphology.instDecidableIsContiguousWithinOfDecidableEq π p = Morphology.instDecidableIsContiguousWithinOfDecidableEq._aux_1 π p

theorem Morphology.violatesABAWithin_iff_of_convex {n : ℕ} {Tag : Type u_1} {F : Type u_2} {π : DomainPartition n Tag} (hπ : π.IsConvex) (p : Paradigm n F) : ViolatesABAWithin π p ↔ ∃ (i : Fin n) (j : Fin n) (k : Fin n), i < j ∧ j < k ∧ SameDomain π i k ∧ p i = p k ∧ p i ≠ p j

For a convex partition the within-domain *ABA check needs only the outer grades to share a domain: the intervener is trapped between them.

theorem Morphology.isContiguousWithin_trivial_iff {n : ℕ} {F : Type u_2} (p : Paradigm n F) : IsContiguousWithin (DomainPartition.trivial n) p ↔ IsContiguous p

Under the trivial partition, domain-relativized contiguity is exactly the universal contiguity predicate.

Smoke tests

Trivial-partition behavior matches the universal predicate; across-domain examples show ABA-shapes are admitted when the outer grades fall in different domains.