Modular Postsyntax — A&N (2012) vs Middleton (2026)

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

Two architectures for the postsyntactic component of Distributed Morphology:

• runStrict (Arregi & Nevins 2012, 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 (Middleton 2026). Impoverishment rules apply in whatever order the analysis demands — paradigmatic and syntagmatic may interleave. Metathesis still follows all impoverishment (this ordering, supported by both Basque and Taos, 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 (@cite{middleton-2026} §4.2.1–§4.2.4) or when a paradigmatic rule must precede a syntagmatic one and one cannot guarantee the strict block ordering (@cite{middleton-2026} §4.2.5). Together these five cases force interleaving: neither a fixed para-then-syn ordering (A&N) nor its reverse can satisfy all five witnesses simultaneously.

This file states the architectures and proves the divergence as a self-contained existential, parametric in the rule shapes; the Taos witnesses are in Phenomena/Allomorphy/Studies/Middleton2026.lean.

structure Morphology.DM.PostsyntacticDerivation.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 @cite{middleton-2026}.

• paradigmatic : List Impoverishment.ImpoverishmentRule
• syntagmatic : List Impoverishment.ImpoverishmentRule
• metathesis : List Metathesis.MetathesisRule

def Morphology.DM.PostsyntacticDerivation.runStrict (M : ModularPostsyntax) (n : 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 Morphology.DM.PostsyntacticDerivation.InterleavedPostsyntax : Type

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

• impoverishment : List Impoverishment.ImpoverishmentRule
• metathesis : List Metathesis.MetathesisRule

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

Equations

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

def Morphology.DM.PostsyntacticDerivation.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 Morphology.DM.PostsyntacticDerivation.runStrict_eq_interleaved_paraSyn (M : ModularPostsyntax) (n : 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).

Proof: applyImpoverishmentChain_append reduces the strict pipeline's two-block fold to a single fold on the concatenation.

@[simp]

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

A two-rule strict pipeline (one paradigmatic, one syntagmatic, no metathesis) reduces to applying [p, s] in order. This is the workhorse equation behind runStrict_forces_paraSyn_order and its consumers in study files.

@[simp]

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

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

theorem Morphology.DM.PostsyntacticDerivation.runStrict_forces_paraSyn_order (p s : Impoverishment.ImpoverishmentRule) (n : Impoverishment.Neighborhood) : runStrict { paradigmatic := [p], syntagmatic := [s], metathesis := [] } n = 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 @cite{middleton-2026}'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 Morphology.DM.PostsyntacticDerivation.runInterleaved_admits_synPara (p s : Impoverishment.ImpoverishmentRule) (n : Impoverishment.Neighborhood) : runInterleaved { impoverishment := [s, p], metathesis := [] } n = Impoverishment.applyImpoverishmentChain [s, p] n

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

theorem Morphology.DM.PostsyntacticDerivation.runStrict_neq_runInterleaved_of_diverges (p s : Impoverishment.ImpoverishmentRule) (n : Impoverishment.Neighborhood) (h : Impoverishment.applyImpoverishmentChain [p, s] n ≠ 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. This packages runStrict_forces_paraSyn_order and runInterleaved_admits_synPara into the actual divergence claim.

def Morphology.DM.PostsyntacticDerivation.runImpovThenMeta (rs : List Impoverishment.ImpoverishmentRule) (ms : List Metathesis.MetathesisRule) (n : 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 Morphology.DM.PostsyntacticDerivation.runMetaThenImpov (rs : List Impoverishment.ImpoverishmentRule) (ms : List Metathesis.MetathesisRule) (n : 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 @cite{middleton-2026}).

Equations

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

theorem Morphology.DM.PostsyntacticDerivation.runImpov_neq_runMeta_of_diverges (r : Impoverishment.ImpoverishmentRule) (m : Metathesis.MetathesisRule) (n : Impoverishment.Neighborhood) (h : Metathesis.applyMetathesisChain [m] { focus := Impoverishment.applyImpoverishment r n, leftCtx := n.leftCtx, rightCtx := n.rightCtx } ≠ Impoverishment.applyImpoverishment r { focus := Metathesis.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.