Metathesis (Distributed Morphology)

@cite{harris-halle-2005} @cite{arregi-nevins-2012} @cite{middleton-2026}

Metathesis is a postsyntactic operation that swaps the linear order of two adjacent terminals before Vocabulary Insertion. It is part of the linearization-and-after stage of the modular postsyntax of @cite{arregi-nevins-2012}: structural operations (Impoverishment) feed linear ones (Metathesis), not vice versa.

Like ImpoverishmentRule, a metathesis rule is keyed on a Neighborhood and carries a decidable condition. The structural change is to swap two distinguished feature types in the focus bundle: the rule names a pair of feature types and exchanges the positions of the first occurrences of each.

This file provides only the rule type, smart constructor, and applicator. The architectural claim that metathesis follows impoverishment is encoded in Theories/Morphology/DM/PostsyntacticDerivation.lean and verified against the Taos data in Phenomena/Allomorphy/Studies/Middleton2026.lean.

structure Morphology.DM.Metathesis.MetathesisRule : Type

A Metathesis rule swaps the linear order of two feature types in the focus bundle when its condition holds.

swapFst and swapSnd name the two feature types (matched via FeatureVal.sameType) whose first occurrences in the focus should exchange positions. The directionality matches the Arregi & Nevins notation [[X] ⟩ ⟨ [Y]] / Z: read "swap X and Y in environment Z."

• condition : Impoverishment.Neighborhood → Prop
• decCond : DecidablePred self.condition
• swapFst : Minimalist.FeatureVal
• swapSnd : Minimalist.FeatureVal

@[implicit_reducible]

instance Morphology.DM.Metathesis.instDecidableCondition (rule : MetathesisRule) (n : Impoverishment.Neighborhood) : Decidable (rule.condition n)

Equations

• Morphology.DM.Metathesis.instDecidableCondition rule n = rule.decCond n

def Morphology.DM.Metathesis.focusRule (focusCheck : Minimalist.FeatureBundle → Bool) (swapFst swapSnd : Minimalist.FeatureVal) : MetathesisRule

Build a metathesis rule from a Boolean condition over the focus bundle (paradigmatic-style — the most common case in the Taos rules of @cite{middleton-2026}, where the condition refers only to the feature inventory of the same node being reordered).

Equations

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

def Morphology.DM.Metathesis.indexOfType (fb : Minimalist.FeatureBundle) (fv : Minimalist.FeatureVal) : Option ℕ

Index of the first feature in fb whose type matches fv.

Equations

• Morphology.DM.Metathesis.indexOfType fb fv = List.findIdx? (fun (f : Minimalist.GramFeature) => f.featureType.sameType fv) fb

def Morphology.DM.Metathesis.swapAt {α : Type u_1} (l : List α) (i j : ℕ) : List α

Swap the elements at positions i and j in a list. Out-of-bounds indices leave the list unchanged.

Equations

• Morphology.DM.Metathesis.swapAt l i j = match l[i]?, l[j]? with | some xi, some xj => (l.set i xj).set j xi | x, x_1 => l

def Morphology.DM.Metathesis.applyMetathesis (rule : MetathesisRule) (n : Impoverishment.Neighborhood) : Minimalist.FeatureBundle

Apply a metathesis rule at a neighborhood: when the condition holds, locate the first occurrences of swapFst and swapSnd in the focus and exchange their positions; otherwise return the focus unchanged.

Equations

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

def Morphology.DM.Metathesis.applyMetathesisChain (rules : List MetathesisRule) (n : Impoverishment.Neighborhood) : Minimalist.FeatureBundle

Apply a sequence of metathesis rules left-to-right. Each rule sees the focus as updated by prior rules; surrounding context is held fixed (one cycle of metathesis, in DM terms). Specializes the generic runChain from Impoverishment.lean.

Equations

• Morphology.DM.Metathesis.applyMetathesisChain rules n = Morphology.DM.Impoverishment.runChain Morphology.DM.Metathesis.applyMetathesis rules n

theorem Morphology.DM.Metathesis.applyMetathesisChain_append (rs₁ rs₂ : List MetathesisRule) (n : Impoverishment.Neighborhood) : applyMetathesisChain (rs₁ ++ rs₂) n = applyMetathesisChain rs₂ { focus := applyMetathesisChain rs₁ n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }

applyMetathesisChain distributes over list concatenation.

def Morphology.DM.Metathesis.MetathesisRule.applyToBundle (rule : MetathesisRule) (fb : Minimalist.FeatureBundle) : Minimalist.FeatureBundle

Convenience: apply a rule to a bare focus bundle with no context.

Equations

• rule.applyToBundle fb = Morphology.DM.Metathesis.applyMetathesis rule (Morphology.DM.Impoverishment.Neighborhood.ofBundle fb)