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

[Mid26] [AN12] [HM93] [Har14a] [Har16a] [KK87] [Wat84] [HM26]

This file formalises the architectural argument of [Mid26]. Working within Distributed Morphology ([HM93]), [AN12] 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:

• 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 [Mid26] §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; instantiated on the witness below.
• A small VI set demonstrates how the postsyntactic output feeds Vocabulary Insertion (Subset Principle, [HM93]), again schematically.
• The Basque half of the paper requires whole terminal deletion (Participant Dissimilation, rule 16) and adjacent terminal swap (Ergative Metathesis, rule 13) — operations the focus-level Taos sections cannot express. The framework lift — MorphPhrase, TermImpovRule, TermMetaRule with their applicators — is inlined at the end of the file; 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 [Mid26] (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.

Metathesis Rule

MetathesisRule parallels ImpoverishmentRule: keyed on a Neighborhood, 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. The directionality matches [AN12]'s [[X] ⟩ ⟨ [Y]] / Z notation: "swap X and Y in environment Z."

structure Middleton2026.MetathesisRule : Type

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

@[implicit_reducible]

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

Equations

• Middleton2026.instDecidableCondition rule n = rule.decCond n

def Middleton2026.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 [Mid26], 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 Middleton2026.indexOfType (l : List Minimalist.GramFeature) (fv : Minimalist.FeatureVal) : Option ℕ

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

Equations

• Middleton2026.indexOfType l fv = List.findIdx? (fun (f : Minimalist.GramFeature) => f.featureType.sameType fv) l

def Middleton2026.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

• Middleton2026.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 Middleton2026.swapInBundle (fb : Minimalist.FeatureBundle) (swapFst swapSnd : Minimalist.FeatureVal) : List Minimalist.GramFeature

Reorder the focus exponents by swapping the first occurrences of swapFst and swapSnd (their linear positions in the terminal's exponent string). Metathesis is inherently an operation on linear order, so it acts on the ordered toGramFeatures view.

Equations

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

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

Apply a metathesis rule at a neighborhood, returning the resulting bundle. When the condition holds, swap the positions of swapFst and swapSnd in the focus exponent string.

NB: the canonical FeatureBundle is a total assignment keyed by feature dimension, hence order-insensitive; folding the swapped exponent list back via ofGramFeatures therefore launders the reordering away. The bundle-level result is thus a no-op whenever the swapped types differ, which is correct for the pipeline below (runStrict/runInterleaved only ever carry an empty metathesis chain). The empirically contentful, order-sensitive focus-level metathesis of [Mid26] is stated on the exponent-string view directly (derivIM/derivMI).

Equations

• Middleton2026.applyMetathesis rule n = if rule.condition n then Minimalist.FeatureBundle.ofGramFeatures (Middleton2026.swapInBundle n.focus rule.swapFst rule.swapSnd) else n.focus

def Middleton2026.applyMetathesisChain (rules : List MetathesisRule) (n : Morphology.DM.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). Specializes runChain.

Equations

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

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

applyMetathesisChain distributes over list concatenation.

def Middleton2026.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 = Middleton2026.applyMetathesis rule (Morphology.DM.Impoverishment.Neighborhood.ofBundle fb)

Strict vs Interleaved Postsyntactic Pipelines

Two architectures for the postsyntactic component:

• runStrict ([AN12], Fig. 1). Postsyntax is a strict modular pipeline: paradigmatic Impoverishment → syntagmatic Impoverishment → Metathesis → VI. Within Feature Markedness, paradigmatic rules apply as a block before any syntagmatic rule.

• runInterleaved ([Mid26]). Impoverishment rules apply in whatever order the analysis demands — paradigmatic and syntagmatic may interleave. Metathesis still follows all impoverishment (this ordering is preserved).

The two pipelines coincide on inputs whose impoverishment list is in para-then-syn order (runStrict_eq_interleaved_paraSyn). They diverge when a syntagmatic rule must precede a paradigmatic one ([Mid26] §4.2.1–§4.2.4) or when a paradigmatic rule must precede a syntagmatic one and one cannot guarantee the strict block ordering ([Mid26] §4.2.5).

structure Middleton2026.ModularPostsyntax : Type

The Arregi & Nevins postsyntax (their Fig. 1, simplified to the two contested layers): paradigmatic Impoverishment, then syntagmatic Impoverishment, then Metathesis. Exponence Conversion and Morphological Concord are abstracted away — their internal ordering is not at issue in [Mid26].

• paradigmatic : List Morphology.DM.Impoverishment.ImpoverishmentRule
• syntagmatic : List Morphology.DM.Impoverishment.ImpoverishmentRule
• metathesis : List MetathesisRule

def Middleton2026.runStrict (M : ModularPostsyntax) (n : Morphology.DM.Impoverishment.Neighborhood) : Minimalist.FeatureBundle

A&N's strict pipeline: para-block, then syn-block, then metathesis.

Equations

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

structure Middleton2026.InterleavedPostsyntax : Type

Middleton's interleaved postsyntax: a single impoverishment list (whose entries may be paradigmatic or syntagmatic in any order), then metathesis.

• impoverishment : List Morphology.DM.Impoverishment.ImpoverishmentRule
• metathesis : List MetathesisRule

def Middleton2026.runInterleaved (M : InterleavedPostsyntax) (n : Morphology.DM.Impoverishment.Neighborhood) : Minimalist.FeatureBundle

Equations

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

def Middleton2026.ModularPostsyntax.toInterleaved (M : ModularPostsyntax) : InterleavedPostsyntax

Promote a strict pipeline to an interleaved one in para-then-syn order. The two then compute the same output.

Equations

• M.toInterleaved = { impoverishment := M.paradigmatic ++ M.syntagmatic, metathesis := M.metathesis }

theorem Middleton2026.runStrict_eq_interleaved_paraSyn (M : ModularPostsyntax) (n : Morphology.DM.Impoverishment.Neighborhood) : runStrict M n = runInterleaved M.toInterleaved n

The strict pipeline is exactly the interleaved pipeline run on the paradigmatic-then-syntagmatic concatenation. Hence runStrict is strictly less expressive than runInterleaved: anything strict can derive, interleaved can derive too (with the same rules).

@[simp]

theorem Middleton2026.runStrict_singleton (p s : Morphology.DM.Impoverishment.ImpoverishmentRule) (n : Morphology.DM.Impoverishment.Neighborhood) : runStrict { paradigmatic := [p], syntagmatic := [s], metathesis := [] } n = Morphology.DM.Impoverishment.applyImpoverishmentChain [p, s] n

A two-rule strict pipeline (one paradigmatic, one syntagmatic, no metathesis) reduces to applying [p, s] in order.

@[simp]

theorem Middleton2026.runInterleaved_no_metathesis (rs : List Morphology.DM.Impoverishment.ImpoverishmentRule) (n : Morphology.DM.Impoverishment.Neighborhood) : runInterleaved { impoverishment := rs, metathesis := [] } n = Morphology.DM.Impoverishment.applyImpoverishmentChain rs n

An interleaved pipeline with no metathesis reduces to the impoverishment chain.

theorem Middleton2026.runStrict_forces_paraSyn_order (p s : Morphology.DM.Impoverishment.ImpoverishmentRule) (n : Morphology.DM.Impoverishment.Neighborhood) : runStrict { paradigmatic := [p], syntagmatic := [s], metathesis := [] } n = Morphology.DM.Impoverishment.applyImpoverishmentChain [p, s] n

The structural inadequacy of runStrict. Whenever a paradigmatic rule p and a syntagmatic rule s produce different outputs depending on whether they fire in [s, p] or [p, s] order at some neighborhood n, the strict pipeline ⟨[p], [s], []⟩ is forced to yield the [p, s] answer — the [s, p] derivation is unreachable.

This is the formal counterpart of [Mid26]'s argument that A&N's modular ordering cannot derive Taos: the four cases in §4.2.1–§4.2.4 require precisely the syn-before-para derivation that runStrict excludes by construction.

theorem Middleton2026.runInterleaved_admits_synPara (p s : Morphology.DM.Impoverishment.ImpoverishmentRule) (n : Morphology.DM.Impoverishment.Neighborhood) : runInterleaved { impoverishment := [s, p], metathesis := [] } n = Morphology.DM.Impoverishment.applyImpoverishmentChain [s, p] n

The interleaved pipeline can deliver the syn-first derivation that runStrict cannot.

theorem Middleton2026.runStrict_neq_runInterleaved_of_diverges (p s : Morphology.DM.Impoverishment.ImpoverishmentRule) (n : Morphology.DM.Impoverishment.Neighborhood) (h : Morphology.DM.Impoverishment.applyImpoverishmentChain [p, s] n ≠ Morphology.DM.Impoverishment.applyImpoverishmentChain [s, p] n) : runStrict { paradigmatic := [p], syntagmatic := [s], metathesis := [] } n ≠ runInterleaved { impoverishment := [s, p], metathesis := [] } n

Inadequacy theorem. If [p, s] and [s, p] give different focuses at n, then the strict pipeline ⟨[p], [s], []⟩ cannot match the interleaved pipeline ⟨[s, p], []⟩ at n.

def Middleton2026.runImpovThenMeta (rs : List Morphology.DM.Impoverishment.ImpoverishmentRule) (ms : List MetathesisRule) (n : Morphology.DM.Impoverishment.Neighborhood) : Minimalist.FeatureBundle

A two-step pipeline that runs impoverishment then metathesis at a neighborhood (the order both A&N and Middleton endorse).

Equations

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

def Middleton2026.runMetaThenImpov (rs : List Morphology.DM.Impoverishment.ImpoverishmentRule) (ms : List MetathesisRule) (n : Morphology.DM.Impoverishment.Neighborhood) : Minimalist.FeatureBundle

The reversed two-step pipeline: metathesis first, then impoverishment (the order both A&N and Middleton reject — supported by Basque in §3.1 and by Taos in §3.2 of [Mid26]).

Equations

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

theorem Middleton2026.runImpov_neq_runMeta_of_diverges (r : Morphology.DM.Impoverishment.ImpoverishmentRule) (m : MetathesisRule) (n : Morphology.DM.Impoverishment.Neighborhood) (h : applyMetathesisChain [m] { focus := Morphology.DM.Impoverishment.applyImpoverishment r n, leftCtx := n.leftCtx, rightCtx := n.rightCtx } ≠ Morphology.DM.Impoverishment.applyImpoverishment r { focus := applyMetathesis m n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }) : runImpovThenMeta [r] [m] n ≠ runMetaThenImpov [r] [m] n

Metathesis-after-impoverishment is non-trivial. If a single impoverishment rule r and a single metathesis rule m produce different focuses depending on order at n, then runImpovThenMeta and runMetaThenImpov differ — i.e., the architectural choice has empirical content.

Two Schematic Rules in Distinct Phases

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 [Mid26] §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.

A Real-Shaped Taos Witness

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 := [Taos.Agreement.argBundle Taos.Agreement.person3 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

The Two Orderings Yield Different Outputs

theorem Middleton2026.stripParaSyn_eq : stripParaSyn = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (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.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (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.

A&N's Strict Pipeline Cannot Reach the Syn-First Output

def Middleton2026.arregiNevinsPostsyntax : 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 : 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 : runStrict arregiNevinsPostsyntax witness = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (Taos.Agreement.fMinimal true)]

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

theorem Middleton2026.middleton_witness : runInterleaved middletonPostsyntax witness = Minimalist.FeatureBundle.ofGramFeatures [Minimalist.GramFeature.valued (Taos.Agreement.fAuthor true), Minimalist.GramFeature.valued (Taos.Agreement.fAtomic true)]

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

theorem Middleton2026.arregiNevins_neq_middleton_at_witness : runStrict arregiNevinsPostsyntax witness ≠ 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 [Mid26] §4.2.1–§4.2.4.

Metathesis Still Follows Impoverishment (the Uphold)

def Middleton2026.authorAtomicMetathesis : MetathesisRule

A metathesis rule that swaps [+author] with [+atomic] when the focus contains all three of [+author], [+atomic], [+minimal]. Schematic of [Mid26]'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.

Metathesis reorders the exponent string of a terminal; the canonical FeatureBundle (a dimension-keyed total assignment) is order-insensitive and cannot witness that reordering. The order-sensitive content of [Mid26]'s "metathesis must follow impoverishment" claim is therefore stated on the ordered exponent view List GramFeature. (The whole-terminal Basque half below, where order lives at the phrase level in List FeatureBundle, is unaffected and witnesses the same claim with a different rule shape.)

def Middleton2026.applyMetathesisExp (rule : MetathesisRule) (l : List Minimalist.GramFeature) : List Minimalist.GramFeature

Apply a metathesis rule to an ordered exponent string: when the rule's condition holds at the corresponding bundle, swap the first occurrences of swapFst and swapSnd in the list; otherwise leave it unchanged.

Equations

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

def Middleton2026.applyImpovExp (rule : Morphology.DM.Impoverishment.ImpoverishmentRule) (l : List Minimalist.GramFeature) : List Minimalist.GramFeature

Apply an impoverishment rule to an ordered exponent string in the witness context: when the rule fires, drop every exponent of the target's dimension, preserving the order of the survivors.

Equations

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

def Middleton2026.witnessExp : List Minimalist.GramFeature

Witness exponent string: [+author, +atomic, +minimal], the ordered view of witnessFocus.

Equations

• Middleton2026.witnessExp = Middleton2026.witnessFocus.toGramFeatures

def Middleton2026.derivIM : List Minimalist.GramFeature

Impoverishment-then-metathesis (Middleton's and A&N's shared order), on the exponent string.

Equations

• Middleton2026.derivIM = Middleton2026.applyMetathesisExp Middleton2026.authorAtomicMetathesis (Middleton2026.applyImpovExp Middleton2026.synMinimalRule Middleton2026.witnessExp)

def Middleton2026.derivMI : List Minimalist.GramFeature

Metathesis-then-impoverishment (the order both authors reject), on the exponent string.

Equations

• Middleton2026.derivMI = Middleton2026.applyImpovExp Middleton2026.synMinimalRule (Middleton2026.applyMetathesisExp Middleton2026.authorAtomicMetathesis Middleton2026.witnessExp)

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. In derivIM, synMinimalRule first deletes [+minimal], bleeding the metathesis condition, so the exponents stay in [+author, +atomic] order; in derivMI, metathesis fires first and swaps them to [+atomic, +author] before [+minimal] is deleted.

Postsyntax Feeds Vocabulary Insertion

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 = Middleton2026.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 = Middleton2026.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 ([HM93]) 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.toGramFeatures) = some 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.toGramFeatures) = some 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.toGramFeatures) ≠ Morphology.DM.VI.subsetPrinciple viSet (List.map Minimalist.GramFeature.featureType middletonOutput.toGramFeatures)

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.

Basque — Whole-Terminal Postsyntax (Middleton §3.1)

The Basque half of the paper operates on whole terminals, not features within a terminal. We lift the focus-level Neighborhood-based machinery of Impoverishment.lean / Metathesis.lean to phrase-level scans, then state Participant Dissimilation, Ergative Metathesis, and the Ondarru divergence witness.

Embick & Noyer 2001 call rules of TermMetaRule's shape "Local Dislocation". TermMetaRule is the FeatureBundle-typed instantiation with the applicator.

@[reducible, inline]

abbrev Middleton2026.MorphPhrase : Type

A Basque morphological phrase: a linear sequence of terminal FeatureBundles, head-leftmost in linear (post-linearisation) order.

Equations

• Middleton2026.MorphPhrase = List Minimalist.FeatureBundle

structure Middleton2026.TermImpovRule : Type

A terminal-level Impoverishment rule: deletes a whole terminal when its Neighborhood (focus = the candidate terminal, leftCtx/rightCtx = its phrase-mates) satisfies condition. Parallel to the focus-level ImpoverishmentRule whose target is a feature within one terminal; here the target is the terminal itself. Motivating case: Basque Participant Dissimilation, [Mid26] (16).

• condition : Morphology.DM.Impoverishment.Neighborhood → Prop
• decCond : DecidablePred self.condition

@[implicit_reducible]

instance Middleton2026.instDecidableCondition_1 (rule : TermImpovRule) (n : Morphology.DM.Impoverishment.Neighborhood) : Decidable (rule.condition n)

Equations

• Middleton2026.instDecidableCondition_1 rule n = rule.decCond n

def Middleton2026.applyTermImpov (rule : TermImpovRule) (phrase : MorphPhrase) : MorphPhrase

Apply a TermImpovRule, scanning the phrase left-to-right. The first terminal whose neighborhood satisfies the rule is dropped; if no terminal matches, the phrase is returned unchanged.

Equations

• Middleton2026.applyTermImpov rule phrase = Middleton2026.applyTermImpov.go rule [] phrase

def Middleton2026.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.
• Middleton2026.applyTermImpov.go rule left [] = left

structure Middleton2026.TermMetaRule : Type

A terminal-level Metathesis rule: swaps two adjacent terminals when the condition holds at their joint context. By convention t1 is the immediate left of t2. Motivating case: Basque Ergative Metathesis, [Mid26] (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 Middleton2026.instDecidableCondition_2 (rule : TermMetaRule) (left : List Minimalist.FeatureBundle) (t1 t2 : Minimalist.FeatureBundle) (right : List Minimalist.FeatureBundle) : Decidable (rule.condition left t1 t2 right)

Equations

• Middleton2026.instDecidableCondition_2 rule left t1 t2 right = rule.decCond left t1 t2 right

def Middleton2026.applyTermMeta (rule : TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

Apply a TermMetaRule, scanning the phrase left-to-right. Swap the first adjacent pair whose joint context satisfies the condition.

Equations

• Middleton2026.applyTermMeta rule phrase = Middleton2026.applyTermMeta.go rule [] phrase

def Middleton2026.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.
• Middleton2026.applyTermMeta.go rule left [] = left
• Middleton2026.applyTermMeta.go rule left [t] = left ++ [t]

def Middleton2026.runPhraseImpovThenMeta (impovs : List TermImpovRule) (metas : List TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

Run impoverishment first, then metathesis — the endorsed pipeline of both [AN12] and [Mid26].

Equations

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

def Middleton2026.runPhraseMetaThenImpov (impovs : List TermImpovRule) (metas : List TermMetaRule) (phrase : MorphPhrase) : MorphPhrase

Run metathesis first, then impoverishment — the order both authors reject; the Basque Ondarru *s-endu-s-n form [Mid26] (17b) is the diagnostic witness.

Equations

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

def Middleton2026.participantDissimilation : TermImpovRule

Participant Dissimilation ([Mid26] (16), [AN12] §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 : TermMetaRule

Ergative Metathesis ([Mid26] (13), [AN12] §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 : MorphPhrase

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

Equations

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

theorem Middleton2026.basqueImpovThenMeta_eq : runPhraseImpovThenMeta [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase = [Basque.Postsyntax.erg2s, 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 : runPhraseMetaThenImpov [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase = [Basque.Postsyntax.tPast, 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 [Mid26] marks ungrammatical (would require L-Support repair *d-endu-s-n).

theorem Middleton2026.basque_orderings_diverge : runPhraseImpovThenMeta [participantDissimilation] [ergativeMetathesis] basqueWitnessPhrase ≠ 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; together they are the two empirical legs of [Mid26]'s claim that metathesis must follow impoverishment.