Phrase-Level Postsyntactic Operations

@cite{halle-marantz-1993} @cite{arregi-nevins-2012} @cite{middleton-2026}

Sister to Impoverishment.lean and Metathesis.lean, which operate at the focus level — modifying features within a single terminal node. This file lifts both operations to the phrase level — deleting whole terminals (e.g., Basque Participant Dissimilation, @cite{arregi-nevins-2012} §4.6, @cite{middleton-2026} (16)) or swapping adjacent terminals (e.g., Basque Ergative Metathesis, @cite{arregi-nevins-2012} §3.2, @cite{middleton-2026} (13)).

The two-tier framework matches DM's actual practice: some impoverishment rules delete features (Taos), others delete entire terminals (Basque Participant Dissimilation). Likewise, some metathesis rules swap features within a node (Taos ω/π reordering) and others swap whole terminals (Basque Ergative Metathesis).

The phrase-level rules use a PhraseFocus view: a target terminal zoomed with leftCtx (terminals to its left) and rightCtx (terminals to its right). Rules scan a phrase left-to-right and apply at the first matching position.

The architectural claim that impoverishment precedes metathesis (upheld by both A&N and Middleton) is encoded as runPhraseImpovThenMeta vs runPhraseMetaThenImpov, with a divergence theorem available for empirical witnesses.

@[reducible, inline]

abbrev Morphology.DM.LinearPostsyntax.MorphPhrase : Type

A morphological phrase: a linear sequence of terminal nodes, each a FeatureBundle. The element order is the linear (post-linearization) order; phrase.head? is leftmost.

Equations

• Morphology.DM.LinearPostsyntax.MorphPhrase = List Minimalist.FeatureBundle

structure Morphology.DM.LinearPostsyntax.PhraseFocus : Type

A view of a phrase from a chosen target terminal. leftCtx is the list of terminals to the left of the focus, in original order; rightCtx is to the right.

• leftCtx : List Minimalist.FeatureBundle
• focus : Minimalist.FeatureBundle
• rightCtx : List Minimalist.FeatureBundle

def Morphology.DM.LinearPostsyntax.instReprPhraseFocus.repr : PhraseFocus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.LinearPostsyntax.instReprPhraseFocus : Repr PhraseFocus

Equations

• Morphology.DM.LinearPostsyntax.instReprPhraseFocus = { reprPrec := Morphology.DM.LinearPostsyntax.instReprPhraseFocus.repr }

structure Morphology.DM.LinearPostsyntax.TermImpovRule : Type

A terminal-level Impoverishment rule: deletes a whole terminal when its phrase neighborhood matches condition. Models the DM rules that target nodes rather than individual features (e.g., Basque Participant Dissimilation, @cite{middleton-2026} (16)).

• condition : PhraseFocus → Prop
• decCond : DecidablePred self.condition

@[implicit_reducible]

instance Morphology.DM.LinearPostsyntax.instDecidableCondition (rule : TermImpovRule) (pf : PhraseFocus) : Decidable (rule.condition pf)

Equations

• Morphology.DM.LinearPostsyntax.instDecidableCondition rule pf = rule.decCond pf

def Morphology.DM.LinearPostsyntax.termImpov (cond : PhraseFocus → Bool) : TermImpovRule

Build a TermImpovRule from a Boolean predicate over PhraseFocus.

Equations

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

def Morphology.DM.LinearPostsyntax.applyTermImpov (rule : TermImpovRule) (phrase : MorphPhrase) : MorphPhrase

Apply a terminal-deletion rule, scanning left-to-right. If no terminal matches, return the phrase unchanged.

Equations

• Morphology.DM.LinearPostsyntax.applyTermImpov rule phrase = Morphology.DM.LinearPostsyntax.applyTermImpov.go rule [] phrase

def Morphology.DM.LinearPostsyntax.applyTermImpov.go (rule : TermImpovRule) (left rest : List Minimalist.FeatureBundle) : List Minimalist.FeatureBundle

Equations

• One or more equations did not get rendered due to their size.
• Morphology.DM.LinearPostsyntax.applyTermImpov.go rule left [] = left

structure Morphology.DM.LinearPostsyntax.TermMetaRule : Type

A terminal-level Metathesis rule: swaps two adjacent terminals when the condition holds at their joint context. The condition takes (leftCtx, t1, t2, rightCtx) — by convention t1 is the immediate left of t2. Models the DM rules that reorder whole terminals (e.g., Basque Ergative Metathesis, @cite{middleton-2026} (13)).

• condition : List Minimalist.FeatureBundle → Minimalist.FeatureBundle → Minimalist.FeatureBundle → List Minimalist.FeatureBundle → Prop
• decCond (left : List Minimalist.FeatureBundle) (t1 t2 : Minimalist.FeatureBundle) (right : List Minimalist.FeatureBundle) : Decidable (self.condition left t1 t2 right)

@[implicit_reducible]

instance Morphology.DM.LinearPostsyntax.instDecidableCondition_1 (rule : TermMetaRule) (left : List Minimalist.FeatureBundle) (t1 t2 : Minimalist.FeatureBundle) (right : List Minimalist.FeatureBundle) : Decidable (rule.condition left t1 t2 right)

Equations

• Morphology.DM.LinearPostsyntax.instDecidableCondition_1 rule left t1 t2 right = rule.decCond left t1 t2 right

def Morphology.DM.LinearPostsyntax.termMeta (cond : List Minimalist.FeatureBundle → Minimalist.FeatureBundle → Minimalist.FeatureBundle → List Minimalist.FeatureBundle → Bool) : TermMetaRule

Build a TermMetaRule from a Boolean predicate.

Equations

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

def Morphology.DM.LinearPostsyntax.applyTermMeta (rule : TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

Apply a terminal-swap rule: scan left-to-right, swap the first adjacent pair whose joint context satisfies rule.condition.

Equations

• Morphology.DM.LinearPostsyntax.applyTermMeta rule phrase = Morphology.DM.LinearPostsyntax.applyTermMeta.go rule [] phrase

def Morphology.DM.LinearPostsyntax.applyTermMeta.go (rule : TermMetaRule) (left rest : List Minimalist.FeatureBundle) : List Minimalist.FeatureBundle

Equations

• One or more equations did not get rendered due to their size.
• Morphology.DM.LinearPostsyntax.applyTermMeta.go rule left [] = left
• Morphology.DM.LinearPostsyntax.applyTermMeta.go rule left [t] = left ++ [t]

def Morphology.DM.LinearPostsyntax.runPhraseChain {R : Type} (apply : R → MorphPhrase → MorphPhrase) (rules : List R) (phrase : MorphPhrase) : MorphPhrase

Apply a list of phrase-level rules left-to-right, threading the phrase through each step. Specializes to impoverishment and metathesis chains below.

Equations

• Morphology.DM.LinearPostsyntax.runPhraseChain apply rules phrase = List.foldl (fun (p : Morphology.DM.LinearPostsyntax.MorphPhrase) (rule : R) => apply rule p) phrase rules

theorem Morphology.DM.LinearPostsyntax.runPhraseChain_append {R : Type} (apply : R → MorphPhrase → MorphPhrase) (rs₁ rs₂ : List R) (phrase : MorphPhrase) : runPhraseChain apply (rs₁ ++ rs₂) phrase = runPhraseChain apply rs₂ (runPhraseChain apply rs₁ phrase)

Concatenating two chains is the same as running them sequentially.

@[simp]

theorem Morphology.DM.LinearPostsyntax.runPhraseChain_nil {R : Type} (apply : R → MorphPhrase → MorphPhrase) (phrase : MorphPhrase) : runPhraseChain apply [] phrase = phrase

The empty chain is the identity.

def Morphology.DM.LinearPostsyntax.applyTermImpovChain (rules : List TermImpovRule) (phrase : MorphPhrase) : MorphPhrase

Apply a sequence of terminal-deletion rules to a phrase.

Equations

• Morphology.DM.LinearPostsyntax.applyTermImpovChain rules phrase = Morphology.DM.LinearPostsyntax.runPhraseChain Morphology.DM.LinearPostsyntax.applyTermImpov rules phrase

def Morphology.DM.LinearPostsyntax.applyTermMetaChain (rules : List TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

Apply a sequence of terminal-swap rules to a phrase.

Equations

• Morphology.DM.LinearPostsyntax.applyTermMetaChain rules phrase = Morphology.DM.LinearPostsyntax.runPhraseChain Morphology.DM.LinearPostsyntax.applyTermMeta rules phrase

def Morphology.DM.LinearPostsyntax.runPhraseImpovThenMeta (impovs : List TermImpovRule) (metas : List TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

The endorsed pipeline (both A&N and @cite{middleton-2026}): impoverishment first, then metathesis.

Equations

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

def Morphology.DM.LinearPostsyntax.runPhraseMetaThenImpov (impovs : List TermImpovRule) (metas : List TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

The rejected pipeline: metathesis first, then impoverishment. The Basque data of @cite{middleton-2026} §3.1 (and @cite{arregi-nevins-2012} §3.1.1) shows this order produces wrong surface forms.

Equations

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

theorem Morphology.DM.LinearPostsyntax.runPhraseImpov_neq_runPhraseMeta_of_diverges (impovs : List TermImpovRule) (metas : List TermMetaRule) (phrase : MorphPhrase) (h : applyTermMetaChain metas (applyTermImpovChain impovs phrase) ≠ applyTermImpovChain impovs (applyTermMetaChain metas phrase)) : runPhraseImpovThenMeta impovs metas phrase ≠ runPhraseMetaThenImpov impovs metas phrase

Divergence claim. When the two orders produce different phrases on a given input, the architectural choice has empirical content: one of the pipelines must be wrong, so the data picks the order.