Impoverishment

Impoverishment deletes features from a terminal before Vocabulary Insertion — the Distributed Morphology mechanism for syncretism: a context that loses a distinguishing feature falls together with its neighbor at VI, forcing retreat to the more general exponent. A rule is evaluated against a Neighborhood (DistributedMorphology/Neighborhood.lean) — the focus terminal plus its adjacent terminals — and the focus/context split makes the paradigmatic/syntagmatic distinction structural: a rule whose condition factors through the focus is paradigmatic as a theorem about the rule, not an annotation. Deletion only removes: every dimension of the output is the input's value or absent (chain_pointwise), which is what makes the post-impoverishment VI winner the retreat-to-the-general exponent (winner?_retreat).

Main definitions

• ImpoverishmentRule — a conditioned feature deletion, parametric in the bundle and target types; ImpoverishmentRule.apply instantiates it with a deletion operation
• ImpoverishmentRule.Paradigmatic, ImpoverishmentRule.Syntagmatic — condition factors through the focus, or genuinely reads context
• deleteFeature, chain — the Minimalist-bundle instantiation and its rule chains

Main statements

• ImpoverishmentRule.paradigmatic_isParadigmatic — rules built focus-only are paradigmatic by construction
• chain_pointwise — impoverishment only deletes: chains never introduce or alter feature values
• runChain_append — chains compose sequentially (the ground for the strict-vs-interleaved equivalence in Middleton2026)

Implementation notes

The rule is parametric so that non-Minimalist bundle types (a future DM Terminal) instantiate it; the deletion operation is a parameter of apply, not of the rule, since it is shared across a rule system. Middleton2026's MetathesisRule follows the same template with a different rewrite. On the tree carrier, impoverishment is derivable from fission and the coproduct (Studies/SenturiaMarcolli2025.lean).

References

• K. Arregi and A. Nevins, Morphotactics
• G. Scott, Pronoun reduction in Mam

Impoverishment rules

structure DistributedMorphology.ImpoverishmentRule (Bundle : Type u_3) (Target : Type u_4) : Type (max u_3 u_4)

An Impoverishment rule: delete target from the focus terminal when condition holds over the neighborhood. The condition is Prop-valued with a DecidablePred witness carried alongside, so applications reduce by decide on concrete inputs; the deletion operation itself is supplied to ImpoverishmentRule.apply.

• condition : Neighborhood Bundle → Prop

  Does this rule apply at the given neighborhood?

• decCond : DecidablePred self.condition

  Decidability witness, exposed as an instance (see below).

• target : Target

  What is deleted from the focus bundle.

@[instance_reducible]

instance DistributedMorphology.instDecidableCondition {Bundle : Type u_1} {Target : Type u_2} (rule : ImpoverishmentRule Bundle Target) (n : Neighborhood Bundle) : Decidable (rule.condition n)

Expose the rule's decidability as an instance so that if rule.condition n then ... else ... elaborates.

Equations

• DistributedMorphology.instDecidableCondition rule n = rule.decCond n

def DistributedMorphology.ImpoverishmentRule.apply {Bundle : Type u_1} {Target : Type u_2} (delete : Bundle → Target → Bundle) (rule : ImpoverishmentRule Bundle Target) (n : Neighborhood Bundle) : Bundle

Apply a rule at a neighborhood, deleting with delete: when the condition holds, the focus loses the target; otherwise it is unchanged.

Equations

• DistributedMorphology.ImpoverishmentRule.apply delete rule n = if rule.condition n then delete n.focus rule.target else n.focus

Paradigmatic and syntagmatic rules

The structural counterpart of [AN12]'s distinction between rules conditioned by a single node and rules conditioned by the node's surroundings — a theorem about a rule, not a flag.

def DistributedMorphology.ImpoverishmentRule.Paradigmatic {Bundle : Type u_1} {Target : Type u_2} (r : ImpoverishmentRule Bundle Target) : Prop

A rule is paradigmatic iff its condition factors through the focus bundle: any two neighborhoods with the same focus agree on the condition.

Equations

• r.Paradigmatic = ∀ (n₁ n₂ : DistributedMorphology.Neighborhood Bundle), n₁.focus = n₂.focus → (r.condition n₁ ↔ r.condition n₂)

def DistributedMorphology.ImpoverishmentRule.Syntagmatic {Bundle : Type u_1} {Target : Type u_2} (r : ImpoverishmentRule Bundle Target) : Prop

A rule is syntagmatic iff it is not paradigmatic: some neighborhoods agree on focus but disagree on the condition, so the condition genuinely depends on context.

Equations

• r.Syntagmatic = ¬r.Paradigmatic

def DistributedMorphology.ImpoverishmentRule.paradigmatic {Bundle : Type u_1} {Target : Type u_2} (focusCheck : Bundle → Bool) (target : Target) : ImpoverishmentRule Bundle Target

Build a paradigmatic rule from a focus-only Boolean check; the Paradigmatic proof is paradigmatic_isParadigmatic.

Equations

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

theorem DistributedMorphology.ImpoverishmentRule.paradigmatic_isParadigmatic {Bundle : Type u_1} {Target : Type u_2} (focusCheck : Bundle → Bool) (target : Target) : (paradigmatic focusCheck target).Paradigmatic

A rule built by paradigmatic is paradigmatic by construction.

def DistributedMorphology.ImpoverishmentRule.syntagmatic {Bundle : Type u_1} {Target : Type u_2} (cond : Neighborhood Bundle → Bool) (target : Target) : ImpoverishmentRule Bundle Target

Build a (potentially) syntagmatic rule from a full-neighborhood Boolean check. Whether the result is genuinely syntagmatic depends on cond — verify with a separate Syntagmatic proof if needed.

Equations

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

Rule chains

def DistributedMorphology.runChain {Bundle : Type u_1} {R : Type u_3} (apply : R → Neighborhood Bundle → Bundle) (rules : List R) (n : Neighborhood Bundle) : Bundle

Generic postsyntactic chain: apply a list of rules to a neighborhood, threading the focus bundle through each step while holding the surrounding context fixed. One cycle of Impoverishment and one cycle of Metathesis (Middleton2026) share this shape.

Equations

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

theorem DistributedMorphology.runChain_append {Bundle : Type u_1} {R : Type u_3} (apply : R → Neighborhood Bundle → Bundle) (rs₁ rs₂ : List R) (n : Neighborhood Bundle) : runChain apply (rs₁ ++ rs₂) n = runChain apply rs₂ { focus := runChain apply rs₁ n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }

Concatenated chains run sequentially: the second chain starts where the first left off. This underwrites the strict-vs-interleaved equivalence (Middleton2026.runStrict_eq_interleaved_paraSyn).

@[simp]

theorem DistributedMorphology.runChain_nil {Bundle : Type u_1} {R : Type u_3} (apply : R → Neighborhood Bundle → Bundle) (n : Neighborhood Bundle) : runChain apply [] n = n.focus

The empty chain is the identity on the focus.

The Minimalist-bundle instantiation

Deletion on Minimalist.FeatureBundle zeroes the target's dimension slot. A rule whose focus might carry a different value of that dimension should guard in its condition: deletion is by dimension, not by value match.

def DistributedMorphology.deleteFeature (fb : Minimalist.FeatureBundle) (target : Minimalist.FeatureVal) : Minimalist.FeatureBundle

Delete the target's dimension from a bundle: set its slot to absent.

Equations

• DistributedMorphology.deleteFeature fb target = Function.update fb target.dimension Features.FeatureSlot.absent

def DistributedMorphology.applyImpoverishment (rule : ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal) (n : Neighborhood Minimalist.FeatureBundle) : Minimalist.FeatureBundle

Apply an Impoverishment rule at a neighborhood of Minimalist bundles.

Equations

• DistributedMorphology.applyImpoverishment rule n = DistributedMorphology.ImpoverishmentRule.apply DistributedMorphology.deleteFeature rule n

def DistributedMorphology.applyImpoverishmentChain (rules : List (ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal)) (n : Neighborhood Minimalist.FeatureBundle) : Minimalist.FeatureBundle

Apply a sequence of impoverishment rules. Specializes runChain.

Equations

• DistributedMorphology.applyImpoverishmentChain rules n = DistributedMorphology.runChain DistributedMorphology.applyImpoverishment rules n

theorem DistributedMorphology.applyImpoverishmentChain_append (rs₁ rs₂ : List (ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal)) (n : Neighborhood Minimalist.FeatureBundle) : applyImpoverishmentChain (rs₁ ++ rs₂) n = applyImpoverishmentChain rs₂ { focus := applyImpoverishmentChain rs₁ n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }

applyImpoverishmentChain distributes over list concatenation.

def DistributedMorphology.ImpoverishmentRule.applyToBundle (rule : ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal) (fb : Minimalist.FeatureBundle) : Minimalist.FeatureBundle

Convenience: apply a rule to a bare focus bundle with no surrounding context, for paradigmatic rules where context is irrelevant.

Equations

• rule.applyToBundle fb = DistributedMorphology.applyImpoverishment rule (DistributedMorphology.Neighborhood.ofBundle fb)

Impoverishment only deletes

Each dimension of an impoverished bundle is the input's value or absent: rules and chains never introduce or alter feature content — the monotone destructiveness that forces retreat to the more general exponent at VI.

theorem DistributedMorphology.deleteFeature_pointwise (fb : Minimalist.FeatureBundle) (target : Minimalist.FeatureVal) (d : Minimalist.FeatureType) : deleteFeature fb target d = fb d ∨ deleteFeature fb target d = Features.FeatureSlot.absent

Deletion leaves every dimension as it was, or absent.

theorem DistributedMorphology.applyImpoverishment_pointwise (rule : ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal) (n : Neighborhood Minimalist.FeatureBundle) (d : Minimalist.FeatureType) : applyImpoverishment rule n d = n.focus d ∨ applyImpoverishment rule n d = Features.FeatureSlot.absent

One rule application leaves every dimension as it was, or absent.

theorem DistributedMorphology.chain_pointwise (rules : List (ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal)) (n : Neighborhood Minimalist.FeatureBundle) (d : Minimalist.FeatureType) : applyImpoverishmentChain rules n d = n.focus d ∨ applyImpoverishmentChain rules n d = Features.FeatureSlot.absent

A chain leaves every dimension as it was, or absent.

theorem DistributedMorphology.deleteFeature_idempotent (fb : Minimalist.FeatureBundle) (target : Minimalist.FeatureVal) : deleteFeature (deleteFeature fb target) target = deleteFeature fb target

Deleting a feature twice is deleting it once.

Redundancy-based impoverishment

def DistributedMorphology.allRecoverable (recoverable pronFeatures : List Minimalist.FeatureVal) : Bool

A feature is redundant when it is recoverable from another source, such as agreement morphology on the verb. This is the mechanism underlying pronoun reduction in Mam ([Sco23]): when all features of the pronominal base are also expressed by agreement, the base is deleted at PF.

Equations

• DistributedMorphology.allRecoverable recoverable pronFeatures = pronFeatures.all fun (f : Minimalist.FeatureVal) => recoverable.any fun (x : Minimalist.FeatureVal) => f.sameType x

def DistributedMorphology.redundancyRule (source : List Minimalist.FeatureVal) (target : Minimalist.FeatureVal) : ImpoverishmentRule Minimalist.FeatureBundle Minimalist.FeatureVal

Build a redundancy-based Impoverishment rule. The condition only inspects the focus bundle, so the rule is paradigmatic by construction.

Equations

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

theorem DistributedMorphology.redundancyRule_isParadigmatic (source : List Minimalist.FeatureVal) (target : Minimalist.FeatureVal) : (redundancyRule source target).Paradigmatic

Redundancy rules are paradigmatic.