Fission (Distributed Morphology)

Fission is the postsyntactic DM operation that splits a single terminal node into multiple positions of exponence, each independently subject to Vocabulary Insertion ([Noy92], [Hal97]; adopted in [HM93]). The classical motivation is [Noy92]'s analysis of Afro-Asiatic prefix-conjugation agreement, where a single AGR node surfaces as one, two, or three separate affixes. [AN12]'s Plural Fission splits the number feature [−singular] off the person features of second/third-person plural pronominal clitics in Basque auxiliaries (their §3.3.4), yielding the plural exponent at a second terminal-of-exponence.

A FissionRule is parameterized over the fissioned feature bundle, the structural context licensing Fission, and the realization output. Conditions are Prop-valued with carried DecidablePred witnesses, matching the ImpoverishmentRule shape in Linglib/Morphology/DM/Impoverishment.lean.

Main declarations

• FissionRule Bundle Ctx Out — the generic rule structure
• FissionRule.apply — partial application returning Option Out
• FissionRule.apply_eq_some_iff, FissionRule.apply_eq_none_iff, FissionRule.isSome_apply — the characterization API

Implementation notes

The realization output Out is opaque: this interface stipulates the fissioned exponents via realize rather than deriving them from iterated Vocabulary Insertion discharging features against a residue, as in [Noy92]'s original mechanism. Consumed by Studies/MunozPerez2026.lean (Chilean Spanish stylistic applicatives).

Todo

• Derive realize from a vocabulary: iterate insertion over the feature residue so the number of exponents is a theorem, not a parameter. Noyer's Tamazight Berber prefix conjugation (one-to-three affix fission) is the canonical stress test.
• Toward a second consumer: [AN12]'s Plural Fission is a feature-pair split with the residue copied into both output nodes (their §3.3.4), so hosting it needs a two-node output and a computed residue rather than an opaque realize. (Their Ergative/Dative Doubling is not Fission: a post-Linearization Generalized-Reduplication repair of the T-Noninitiality constraint.)

structure Morphology.DM.FissionRule (Bundle : Type u_1) (Ctx : Type u_2) (Out : Type u_3) : Type (max (max u_1 u_2) u_3)

A Fission rule is parameterized over:

• Bundle — the fissioned morphological feature bundle (e.g., φ-features);
• Ctx — the structural context licensing Fission;
• Out — the realization output.

Both contextOk and bundleOk are Prop-valued with carried DecidablePred witnesses, matching the ImpoverishmentRule template (see Impoverishment.lean).

• contextOk : Ctx → Prop

  The structural condition licensing Fission.

• decContext : DecidablePred self.contextOk

  Decidability witness for contextOk.

• bundleOk : Bundle → Prop

  The condition on the fissioned bundle (e.g., [+PART, +SING]).

• decBundle : DecidablePred self.bundleOk

  Decidability witness for bundleOk.

• realize : Bundle → Out

  Realization: map each licensed bundle to its output.

@[implicit_reducible]

instance Morphology.DM.FissionRule.instDecidableContextOk {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} (rule : FissionRule Bundle Ctx Out) (c : Ctx) : Decidable (rule.contextOk c)

Equations

• rule.instDecidableContextOk c = rule.decContext c

@[implicit_reducible]

instance Morphology.DM.FissionRule.instDecidableBundleOk {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} (rule : FissionRule Bundle Ctx Out) (p : Bundle) : Decidable (rule.bundleOk p)

Equations

• rule.instDecidableBundleOk p = rule.decBundle p

def Morphology.DM.FissionRule.apply {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} (rule : FissionRule Bundle Ctx Out) (p : Bundle) (c : Ctx) : Option Out

Apply Fission: yield the realization when both the structural and bundle conditions hold; otherwise none.

Equations

• rule.apply p c = if rule.contextOk c ∧ rule.bundleOk p then some (rule.realize p) else none

theorem Morphology.DM.FissionRule.apply_pos {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} {rule : FissionRule Bundle Ctx Out} {p : Bundle} {c : Ctx} (hc : rule.contextOk c) (hb : rule.bundleOk p) : rule.apply p c = some (rule.realize p)

theorem Morphology.DM.FissionRule.apply_neg {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} {rule : FissionRule Bundle Ctx Out} {p : Bundle} {c : Ctx} (h : ¬(rule.contextOk c ∧ rule.bundleOk p)) : rule.apply p c = none

@[simp]

theorem Morphology.DM.FissionRule.apply_eq_some_iff {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} {rule : FissionRule Bundle Ctx Out} {p : Bundle} {c : Ctx} {out : Out} : rule.apply p c = some out ↔ (rule.contextOk c ∧ rule.bundleOk p) ∧ rule.realize p = out

@[simp]

theorem Morphology.DM.FissionRule.apply_eq_none_iff {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} {rule : FissionRule Bundle Ctx Out} {p : Bundle} {c : Ctx} : rule.apply p c = none ↔ ¬(rule.contextOk c ∧ rule.bundleOk p)

theorem Morphology.DM.FissionRule.isSome_apply {Bundle : Type u_1} {Ctx : Type u_2} {Out : Type u_3} {rule : FissionRule Bundle Ctx Out} {p : Bundle} {c : Ctx} : (rule.apply p c).isSome = true ↔ rule.contextOk c ∧ rule.bundleOk p