Middleton (2026) — Ordering of Impoverishment Rules in Taos and Basque

@cite{middleton-2026} @cite{arregi-nevins-2012} @cite{halle-marantz-1993} @cite{harbour-2014} @cite{harbour-2016} @cite{kontak-kunkel-1987} @cite{watkins-1984} @cite{harbour-middleton-2026}

This file formalises the architectural argument of @cite{middleton-2026}. Working within Distributed Morphology (@cite{halle-marantz-1993}), @cite{arregi-nevins-2012} propose a strict modular postsyntax in which paradigmatic Impoverishment applies as a block before syntagmatic Impoverishment, and Metathesis follows all Impoverishment. Middleton shows from Taos verbal agreement that the second claim survives but the first does not (§§4.2.1–§4.2.5); the Basque half of the paper (§3.1) re-establishes the second claim — metathesis after impoverishment — using a different language and different rule shapes (whole-terminal deletion + adjacent-terminal swap).

Scope

The full Taos paradigm involves dozens of Vocabulary Insertion rules and a large family of impoverishment / metathesis rules. We do not re-derive the entire paradigm. What lives here:

• The architectural pipelines (runStrict, runInterleaved) live in Theories/Morphology/DM/PostsyntacticDerivation.lean.
• This file gives one schematic pair of rules paraAtomicRule / synMinimalRule that exhibits the divergence predicted by the paper at a real-shaped Taos witness neighborhood. The conditioning features ([+author], [+atomic], [+minimal]) are drawn from the Harbour decomposition the paper uses, but the rules themselves are not literal transcriptions of paper rules — they are minimal witnesses to the para-vs-syn ordering interaction in @cite{middleton-2026} §4.2.1–§4.2.4.
• The general claim — that runStrict is strictly less expressive than runInterleaved whenever a syntagmatic rule needs to feed a paradigmatic one — is runStrict_forces_paraSyn_order / runInterleaved_admits_synPara in the theory file; here we instantiate it on the witness.
• §6 demonstrates how the postsyntactic output feeds Vocabulary Insertion (Subset Principle, @cite{halle-marantz-1993}), again schematically.
• §7 turns to the Basque half of the paper. Where §§1–5 work at the focus level (rules modify a single bundle), Basque needs whole terminal deletion (Participant Dissimilation, rule 16) and adjacent terminal swap (Ergative Metathesis, rule 13). The framework lift lives in Theories/Morphology/DM/LinearPostsyntax.lean; the bundles live in Fragments/Basque/Postsyntax.lean; the rules and the Ondarru s-endu-n (17a) divergence witness are stated here.

What is not modeled:

• The full Taos paradigm and the literal rule statements of @cite{middleton-2026} (rule numbers and conditioning environments vary across the four §4.2 cases).
• Harbour's Reciprocal Containment constraints on feature bundles.
• Real Taos VI competition — only enough VIs to demonstrate the pipeline.

def Middleton2026.paraAtomicRule : Morphology.DM.Impoverishment.ImpoverishmentRule

A paradigmatic rule: deletes [+atomic] whenever the focus contains both [+author] and [+minimal]. The condition refers only to the focus, so the rule is paradigmatic by construction (paradigmatic_isParadigmatic).

This is a minimal stand-in for the paradigmatic rules involved in @cite{middleton-2026} §4.2.1–§4.2.4 — it is not a transcription of any specific paper rule.

Equations

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

theorem Middleton2026.paraAtomicRule_isParadigmatic : Morphology.DM.Impoverishment.Paradigmatic paraAtomicRule

def Middleton2026.synMinimalRule : Morphology.DM.Impoverishment.ImpoverishmentRule

A syntagmatic rule: deletes [+minimal] when the focus contains [+atomic] and there is at least one bundle of object-context to the right (the schematic [O 3i] condition, weakened to bare presence — sufficient for the bleeding/feeding interaction the paper diagnoses). The dependence on rightCtx is what makes the rule syntagmatic, and synMinimalRule_isSyntagmatic proves it.

Equations

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

theorem Middleton2026.synMinimalRule_isSyntagmatic : Morphology.DM.Impoverishment.Syntagmatic synMinimalRule

The two rules are genuinely in distinct phases: synMinimalRule actually depends on its right-context (it is not paradigmatic). Witness: two neighborhoods that share a focus but differ on rightCtx.

def Middleton2026.witnessFocus : Minimalist.FeatureBundle

Witness focus: a 1s-style bundle [+author, +atomic, +minimal] (suppressing [+participant], which is irrelevant to either rule).

Equations

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

def Middleton2026.witness : Morphology.DM.Impoverishment.Neighborhood

Witness neighborhood: the 1s-style focus, with a real 3s bundle to the right standing in for the Taos object slot that conditions synMinimalRule.

Equations

• Middleton2026.witness = { focus := Middleton2026.witnessFocus, rightCtx := [Fragments.Taos.Agreement.argBundle Fragments.Taos.Agreement.person3 Fragments.Taos.Agreement.numSg] }

def Middleton2026.stripParaSyn : Minimalist.FeatureBundle

Run para-then-syn (the order A&N's strict pipeline forces).

Equations

• Middleton2026.stripParaSyn = Morphology.DM.Impoverishment.applyImpoverishmentChain [Middleton2026.paraAtomicRule, Middleton2026.synMinimalRule] Middleton2026.witness

def Middleton2026.stripSynPara : Minimalist.FeatureBundle

Run syn-then-para (the order Middleton's interleaved pipeline can choose).

Equations

• Middleton2026.stripSynPara = Morphology.DM.Impoverishment.applyImpoverishmentChain [Middleton2026.synMinimalRule, Middleton2026.paraAtomicRule] Middleton2026.witness

theorem Middleton2026.stripParaSyn_eq : stripParaSyn = [Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fMinimal true)]

Para-then-syn (= A&N): paraAtomicRule deletes [+atomic] first; synMinimalRule then can't fire (no [+atomic] left in focus). The [+minimal] survives.

theorem Middleton2026.stripSynPara_eq : stripSynPara = [Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fAtomic true)]

Syn-then-para (= Middleton): synMinimalRule fires first (focus has [+atomic], rightCtx non-empty), deleting [+minimal]; paraAtomicRule then can't fire (no [+minimal] left in focus). The [+atomic] survives instead.

theorem Middleton2026.orderings_diverge : stripParaSyn ≠ stripSynPara

The two orders produce different feature bundles at this neighborhood.

def Middleton2026.arregiNevinsPostsyntax : Morphology.DM.PostsyntacticDerivation.ModularPostsyntax

The schematic A&N postsyntax that contains exactly paraAtomicRule in the paradigmatic phase and synMinimalRule in the syntagmatic phase, with no metathesis.

Equations

• Middleton2026.arregiNevinsPostsyntax = { paradigmatic := [Middleton2026.paraAtomicRule], syntagmatic := [Middleton2026.synMinimalRule], metathesis := [] }

def Middleton2026.middletonPostsyntax : Morphology.DM.PostsyntacticDerivation.InterleavedPostsyntax

The schematic Middleton interleaved postsyntax, with the syntagmatic rule scheduled first — the order required by the §4.2.1–§4.2.4 Taos cases.

Equations

• Middleton2026.middletonPostsyntax = { impoverishment := [Middleton2026.synMinimalRule, Middleton2026.paraAtomicRule], metathesis := [] }

theorem Middleton2026.arregiNevins_witness : Morphology.DM.PostsyntacticDerivation.runStrict arregiNevinsPostsyntax witness = [Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fMinimal true)]

A&N's pipeline computes the para-first answer at the witness.

theorem Middleton2026.middleton_witness : Morphology.DM.PostsyntacticDerivation.runInterleaved middletonPostsyntax witness = [Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (Fragments.Taos.Agreement.fAtomic true)]

Middleton's pipeline computes the (different) syn-first answer.

theorem Middleton2026.arregiNevins_neq_middleton_at_witness : Morphology.DM.PostsyntacticDerivation.runStrict arregiNevinsPostsyntax witness ≠ Morphology.DM.PostsyntacticDerivation.runInterleaved middletonPostsyntax witness

Architectural inadequacy of runStrict for Taos. At the witness neighborhood, the strict A&N pipeline and Middleton's interleaved one return different feature bundles. Hence no ModularPostsyntax built from paraAtomicRule (paradigmatic) and synMinimalRule (syntagmatic) — and no extension that adds further rules to the same phases — can yield the syn-first output that Taos requires in @cite{middleton-2026} §4.2.1–§4.2.4.

def Middleton2026.authorAtomicMetathesis : Morphology.DM.Metathesis.MetathesisRule

A metathesis rule that swaps [+author] with [+atomic] when the focus contains all three of [+author], [+atomic], [+minimal]. Schematic of @cite{middleton-2026}'s metathesis rules: a metathesis triggered in the presence of a particular number feature. The dependence on [+minimal] is what couples this rule to synMinimalRule (which deletes [+minimal]), so that the IM/MI orders diverge — the empirically motivated witness of "metathesis after impoverishment, not before."

Equations

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

def Middleton2026.derivIM : Minimalist.FeatureBundle

Impoverishment-then-metathesis (Middleton's and A&N's shared order).

Equations

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

def Middleton2026.derivMI : Minimalist.FeatureBundle

Metathesis-then-impoverishment (the order both authors reject).

Equations

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

theorem Middleton2026.impov_before_meta_diverges_from_meta_before_impov : derivIM ≠ derivMI

The two orders of impoverishment vs. metathesis genuinely diverge at the witness, witnessing the architectural fact that metathesis must follow impoverishment.

def Middleton2026.arregiNevinsOutput : Minimalist.FeatureBundle

The post-postsyntactic focus bundle from A&N's strict pipeline at the witness — extracted as a top-level def so it is the input to Vocabulary Insertion below.

Equations

• Middleton2026.arregiNevinsOutput = Morphology.DM.PostsyntacticDerivation.runStrict Middleton2026.arregiNevinsPostsyntax Middleton2026.witness

def Middleton2026.middletonOutput : Minimalist.FeatureBundle

The post-postsyntactic focus bundle from Middleton's interleaved pipeline at the witness.

Equations

• Middleton2026.middletonOutput = Morphology.DM.PostsyntacticDerivation.runInterleaved Middleton2026.middletonPostsyntax Middleton2026.witness

def Middleton2026.viSet : List (Morphology.DM.VI.FeatureVI Minimalist.FeatureVal String)

A small schematic Vocabulary Item set keyed on FeatureVal. The Subset Principle (@cite{halle-marantz-1993}) selects the longest matching entry. We use Morpheme.surface for the exponents to keep the connection to the Taos morpheme inventory in the Fragment.

Equations

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

theorem Middleton2026.arregiNevinsOutput_inserts_n : Morphology.DM.VI.subsetPrinciple viSet (List.map Minimalist.GramFeature.featureType arregiNevinsOutput) = some Fragments.Taos.Agreement.Morpheme.n.surface

A&N's output feeds VI as [+author, +minimal]; the Subset Principle selects the [+author, +minimal] entry over the elsewhere ô. Surface form: n.

theorem Middleton2026.middletonOutput_inserts_o : Morphology.DM.VI.subsetPrinciple viSet (List.map Minimalist.GramFeature.featureType middletonOutput) = some Fragments.Taos.Agreement.Morpheme.o.surface

Middleton's output feeds VI as [+author, +atomic]; the Subset Principle selects the [+author, +atomic] entry. Surface form: o. The two architectures predict different surface forms at the same input — the empirical bite of the architectural divergence.

theorem Middleton2026.arregiNevins_vs_middleton_surface : Morphology.DM.VI.subsetPrinciple viSet (List.map Minimalist.GramFeature.featureType arregiNevinsOutput) ≠ Morphology.DM.VI.subsetPrinciple viSet (List.map Minimalist.GramFeature.featureType middletonOutput)

The architectural divergence shows up at the level of surface exponents, not just feature bundles: the same input neighborhood yields different morphemes under the two pipelines.

def Middleton2026.participantDissimilation : Morphology.DM.LinearPostsyntax.TermImpovRule

Participant Dissimilation (@cite{middleton-2026} (16), @cite{arregi-nevins-2012} §4.6). Delete a 1p absolutive clitic ([CL +participant +author]) when there is a participant ergative clitic somewhere to the right in the same auxiliary. The rule operates at the terminal level — it deletes a whole bundle, not a feature within one.

Equations

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

def Middleton2026.ergativeMetathesis : Morphology.DM.LinearPostsyntax.TermMetaRule

Ergative Metathesis (@cite{middleton-2026} (13), @cite{arregi-nevins-2012} §3.2). Swap T with an immediately following ergative clitic when T is leftmost in the auxiliary. The leftmost requirement (left.isEmpty) is what lets Participant Dissimilation feed Ergative Metathesis: only after PD deletes the absolutive clitic does T become leftmost.

Equations

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

def Middleton2026.basqueWitnessPhrase : Morphology.DM.LinearPostsyntax.MorphPhrase

The Ondarru witness phrase from @cite{middleton-2026} (17a): s-endu-n [1pABS, T:past, 2sERG]. The complementizer is suppressed — it does not participate in either rule.

Equations

• Middleton2026.basqueWitnessPhrase = [Fragments.Basque.Postsyntax.abs1pAuthor, Fragments.Basque.Postsyntax.tPast, Fragments.Basque.Postsyntax.erg2s]

theorem Middleton2026.basqueImpovThenMeta_eq : Morphology.DM.LinearPostsyntax.runPhraseImpovThenMeta [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase = [Fragments.Basque.Postsyntax.erg2s, Fragments.Basque.Postsyntax.tPast]

PD-then-Meta surface form (the grammatical s-endu-n order). PD deletes the absolutive 1p, leaving [T, ERG]; with T now leftmost, Ergative Metathesis swaps to [ERG, T] — the order that surfaces as s-endu-n.

theorem Middleton2026.basqueMetaThenImpov_eq : Morphology.DM.LinearPostsyntax.runPhraseMetaThenImpov [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase = [Fragments.Basque.Postsyntax.tPast, Fragments.Basque.Postsyntax.erg2s]

*Meta-then-PD surface form (the rejected 17b order). Ergative Metathesis cannot fire at the input — T is not leftmost (the absolutive clitic precedes it). PD then deletes the absolutive clitic, but it is too late to feed metathesis; the result is the T-leftmost order [T, ERG], the form @cite{middleton-2026} marks ungrammatical (would require L-Support repair *d-endu-s-n).

theorem Middleton2026.basque_orderings_diverge : Morphology.DM.LinearPostsyntax.runPhraseImpovThenMeta [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase ≠ Morphology.DM.LinearPostsyntax.runPhraseMetaThenImpov [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase

The two phrase-level pipelines diverge on the Ondarru witness. This is the Basque counterpart to arregiNevins_neq_middleton_at_witness (Taos §4); together they are the two empirical legs of @cite{middleton-2026}'s claim that metathesis must follow impoverishment.