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, and insertion retreats to the more general exponent (winner?_retreat). A rule is evaluated at a Neighborhood, the focus terminal with the terminals beside it, so whether a rule is paradigmatic, its condition reading the focus alone, is a theorem about the rule. On a list bundle a rule erases one occurrence of its target, subtraction in the free commutative monoid on the features that DistributedMorphology/Fission.lean decomposes.

Main definitions

• ImpoverishmentRule: a decidable condition on a neighborhood and the target it deletes; ImpoverishmentRule.apply takes the deletion as a parameter.
• ImpoverishmentRule.ofFocus: the rule whose condition reads the focus alone.
• ImpoverishmentRule.Paradigmatic, ImpoverishmentRule.Syntagmatic: the condition factors through the focus, or reads the context.
• runChain: a rule sequence threaded through the focus.

Main results

• ImpoverishmentRule.paradigmatic_ofFocus: a focus-only rule is paradigmatic.
• ImpoverishmentRule.coe_apply_erase, ImpoverishmentRule.apply_erase_sublist: on a list bundle a rule erases one occurrence of its target, so impoverishment only deletes.

Implementation notes

The deletion is a parameter of apply, not of the rule, since a rule system shares it; Studies/Middleton2026.lean deletes from the slots of the Taos agreement prefix. On the tree carrier, impoverishment derives from fission and the coproduct (Studies/SenturiaMarcolli2025.lean).

References

• K. Arregi and A. Nevins, Morphotactics

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

An Impoverishment rule deletes target from the focus of a neighborhood satisfying its decidable condition.

• condition : Neighborhood Bundle → Prop

  The neighborhoods at which the rule fires.

• decCond : DecidablePred self.condition
• target : Target

  The feature the rule deletes from the focus.

@[instance_reducible]

instance DistributedMorphology.ImpoverishmentRule.instDecidablePredNeighborhoodCondition {Bundle : Type u_1} {Target : Type u_2} (rule : ImpoverishmentRule Bundle Target) : DecidablePred rule.condition

Equations

• rule.instDecidablePredNeighborhoodCondition = rule.decCond

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

With the deletion delete, a rule removes its target from the focus where its condition holds, and otherwise leaves the focus as it is.

Equations

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

def DistributedMorphology.ImpoverishmentRule.ofFocus {Bundle : Type u_1} {Target : Type u_2} (p : Bundle → Prop) [DecidablePred p] (target : Target) : ImpoverishmentRule Bundle Target

ofFocus p target deletes target wherever the focus satisfies p.

Equations

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

Paradigmatic and syntagmatic rules

The structural counterpart of [AN12]'s distinction between rules conditioned by a single node and rules conditioned by its surroundings.

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, two neighborhoods with the same focus agreeing on it.

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, so that its condition reads the context.

Equations

• r.Syntagmatic = ¬r.Paradigmatic

theorem DistributedMorphology.ImpoverishmentRule.paradigmatic_ofFocus {Bundle : Type u_1} {Target : Type u_2} (p : Bundle → Prop) [DecidablePred p] (target : Target) : (ofFocus p target).Paradigmatic

List bundles

theorem DistributedMorphology.ImpoverishmentRule.apply_erase_sublist {α : Type u_3} [BEq α] (rule : ImpoverishmentRule (List α) α) (n : Neighborhood (List α)) : (apply List.erase rule n).Sublist n.focus

Impoverishment only deletes. On a list bundle, erasing the target leaves a sublist of the focus.

theorem DistributedMorphology.ImpoverishmentRule.coe_apply_erase {α : Type u_3} [DecidableEq α] (rule : ImpoverishmentRule (List α) α) (n : Neighborhood (List α)) : ↑(apply List.erase rule n) = if rule.condition n then (↑n.focus).erase rule.target else ↑n.focus

In the free commutative monoid on the features, a rule erases one occurrence of its target from the focus where its condition holds.

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

A chain applies a list of rules to a neighborhood, threading the focus through each step while holding the context fixed.

Equations

• DistributedMorphology.runChain apply rules n = List.foldl (fun (focus : Bundle) (rule : R) => apply rule { focus := focus, leftCtx := n.leftCtx, rightCtx := n.rightCtx }) n.focus rules

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 starting where the first left off.

@[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.