The spell-out pipeline

The PF branch of the Y-model at the domain level: a spell-out domain is the sequence of terminals the syntax hands over, the postsyntactic modules transform it, and Vocabulary Insertion realizes what survives, each position in its neighborhood; the module inventory and its ordering follow the Basque morphotactics. The focus-level rule types (ImpoverishmentRule and kin) rewrite one terminal inside its Neighborhood; the operations here move, remove, and merge the terminals themselves, which no focus-level rule can express.

Each operation carries its position-count law, so terminal/exponent misalignment is arithmetic: neighborhood rewriting and terminal metathesis preserve the count, obliteration and fusion decrease it, and Spellout.length_pf says insertion positions equal terminals after the modules — Fission multiplies exponents within a position (scansion), not positions. winner?_retreat (VocabularyInsertion/Basic.lean) supplies the insertion-side ordering law.

Consumers: Studies/Middleton2026.lean (Basque whole-terminal rules and the Ondarru ordering witness), Studies/HalleMarantz1993.lean (Tns+Agr fusion feeding one insertion).

Main declarations

• SpelloutDomain, mapNeighborhoods — the domain and the zipper lift of focus-level rewriting
• ObliterationRule, TerminalMetathesisRule — whole-terminal deletion (Obliteration) and adjacent-terminal swap, with first-match applicators and count laws
• FusionRule.applyFirstAdjacent — the domain lift of Fusion
• Spellout — the module sequence plus insertion in context; run, pf, runModules_append

Todo

• The LF branch: an Interpreted extension whose interpretation reads the input domain (the Y-model separation by type), seeded by the domain-level allosemy licensing of Studies/Benz2025.lean.
• Stratifying the module list by linearization — Lowering before, Local Dislocation after.

References

• M. Halle and A. Marantz, Distributed Morphology and the pieces of inflection
• K. Arregi and A. Nevins, Morphotactics
• D. Embick and R. Noyer, Movement operations after syntax

@[reducible, inline]

abbrev DistributedMorphology.SpelloutDomain (Bundle : Type u_1) : Type u_1

A spell-out domain: the linear sequence of terminals handed over by the syntax at spell-out.

Equations

• DistributedMorphology.SpelloutDomain Bundle = List Bundle

def DistributedMorphology.mapNeighborhoods {Bundle : Type u_1} {C : Type u_3} (f : Neighborhood Bundle → C) (d : SpelloutDomain Bundle) : List C

Apply f to every terminal in its neighborhood: position i sees the earlier terminals as leftCtx and the later ones as rightCtx, nearest first. The domain lift of a focus-level rule such as Impoverishment, and of Vocabulary Insertion.

Equations

• DistributedMorphology.mapNeighborhoods f d = List.mapIdx (fun (i : ℕ) (b : Bundle) => f { focus := b, leftCtx := (List.take i d).reverse, rightCtx := List.drop (i + 1) d }) d

@[simp]

theorem DistributedMorphology.length_mapNeighborhoods {Bundle : Type u_1} {C : Type u_3} (f : Neighborhood Bundle → C) (d : SpelloutDomain Bundle) : (mapNeighborhoods f d).length = List.length d

Neighborhood rewriting preserves the number of terminals.

structure DistributedMorphology.ObliterationRule (Bundle : Type u_3) : Type u_3

A whole-terminal deletion rule — [AN12]'s Obliteration: the terminal whose neighborhood satisfies condition is removed outright. The focus-level ImpoverishmentRule deletes a feature inside a terminal; this rule deletes the terminal.

• condition : Neighborhood Bundle → Prop

  Does the rule fire at this neighborhood?

• decCond : DecidablePred self.condition

  Decidability witness for condition.

@[instance_reducible]

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

Equations

• rule.instDecidableCondition n = rule.decCond n

def DistributedMorphology.ObliterationRule.ofBool {Bundle : Type u_1} (cond : Neighborhood Bundle → Bool) : ObliterationRule Bundle

Build an obliteration rule from a Boolean condition.

Equations

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

def DistributedMorphology.ObliterationRule.apply {Bundle : Type u_1} (rule : ObliterationRule Bundle) (d : SpelloutDomain Bundle) : SpelloutDomain Bundle

Apply the rule, scanning left to right: the first terminal whose neighborhood fires is dropped; otherwise the domain is unchanged. leftCtx is accumulated nearest first.

Equations

• rule.apply d = DistributedMorphology.ObliterationRule.apply.go rule [] d

def DistributedMorphology.ObliterationRule.apply.go {Bundle : Type u_1} (rule : ObliterationRule Bundle) : List Bundle → SpelloutDomain Bundle → SpelloutDomain Bundle

Scan with the already-passed terminals in left, nearest first.

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.ObliterationRule.apply.go rule a✝ [] = a✝.reverse

theorem DistributedMorphology.ObliterationRule.length_apply_le {Bundle : Type u_1} (rule : ObliterationRule Bundle) (d : SpelloutDomain Bundle) : List.length (rule.apply d) ≤ List.length d

Obliteration never increases the number of terminals.

structure DistributedMorphology.TerminalMetathesisRule (Bundle : Type u_3) : Type u_3

An adjacent-terminal swap rule — the terminal-order metathesis of [AN12]'s Metathesis module (Basque Ergative Metathesis, [Mid26] (13)). condition sees the terminals left of the pair (nearest first), the pair itself, and the terminals to its right.

• condition : List Bundle → Bundle → Bundle → List Bundle → Prop

  Does the rule swap the pair t₁ t₂ in this context?

• decCond (left : List Bundle) (t₁ t₂ : Bundle) (right : List Bundle) : Decidable (self.condition left t₁ t₂ right)

  Decidability witness for condition.

@[instance_reducible]

instance DistributedMorphology.TerminalMetathesisRule.instDecidableCondition {Bundle : Type u_1} (rule : TerminalMetathesisRule Bundle) (left : List Bundle) (t₁ t₂ : Bundle) (right : List Bundle) : Decidable (rule.condition left t₁ t₂ right)

Equations

• rule.instDecidableCondition left t₁ t₂ right = rule.decCond left t₁ t₂ right

def DistributedMorphology.TerminalMetathesisRule.ofBool {Bundle : Type u_1} (cond : List Bundle → Bundle → Bundle → List Bundle → Bool) : TerminalMetathesisRule Bundle

Build a terminal-metathesis rule from a Boolean condition.

Equations

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

def DistributedMorphology.TerminalMetathesisRule.apply {Bundle : Type u_1} (rule : TerminalMetathesisRule Bundle) (d : SpelloutDomain Bundle) : SpelloutDomain Bundle

Apply the rule, scanning left to right: the first adjacent pair whose context fires is swapped; otherwise the domain is unchanged.

Equations

• rule.apply d = DistributedMorphology.TerminalMetathesisRule.apply.go rule [] d

def DistributedMorphology.TerminalMetathesisRule.apply.go {Bundle : Type u_1} (rule : TerminalMetathesisRule Bundle) : List Bundle → SpelloutDomain Bundle → SpelloutDomain Bundle

Scan with the already-passed terminals in left, nearest first.

Equations

• One or more equations did not get rendered due to their size.
• DistributedMorphology.TerminalMetathesisRule.apply.go rule a✝ [] = a✝.reverse
• DistributedMorphology.TerminalMetathesisRule.apply.go rule a✝ [t] = a✝.reverse ++ [t]

@[simp]

theorem DistributedMorphology.TerminalMetathesisRule.length_apply {Bundle : Type u_1} (rule : TerminalMetathesisRule Bundle) (d : SpelloutDomain Bundle) : List.length (rule.apply d) = List.length d

Terminal metathesis preserves the number of terminals.

def DistributedMorphology.FusionRule.applyFirstAdjacent {F : Type u_3} (rule : FusionRule F) : SpelloutDomain (List F) → SpelloutDomain (List F)

The domain lift of Fusion: fuse the first adjacent pair the rule licenses; otherwise the domain is unchanged.

Equations

• rule.applyFirstAdjacent [] = []
• rule.applyFirstAdjacent [b] = [b]
• rule.applyFirstAdjacent (b₁ :: b₂ :: rest) = if rule.condition b₁ b₂ then (b₁ ++ b₂) :: rest else b₁ :: rule.applyFirstAdjacent (b₂ :: rest)

theorem DistributedMorphology.FusionRule.length_applyFirstAdjacent_le {F : Type u_3} (rule : FusionRule F) (d : SpelloutDomain (List F)) : List.length (rule.applyFirstAdjacent d) ≤ List.length d

Fusion never increases the number of terminals.

def DistributedMorphology.runModules {Bundle : Type u_1} (modules : List (SpelloutDomain Bundle → SpelloutDomain Bundle)) (d : SpelloutDomain Bundle) : SpelloutDomain Bundle

Run an ordered module sequence over a domain. The order of the list is the theory's architectural claim ([AN12]'s strict sequence; the Basque ordering witness in Studies/Middleton2026.lean shows reordering it has empirical content).

Equations

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

theorem DistributedMorphology.runModules_append {Bundle : Type u_1} (m₁ m₂ : List (SpelloutDomain Bundle → SpelloutDomain Bundle)) (d : SpelloutDomain Bundle) : runModules (m₁ ++ m₂) d = runModules m₂ (runModules m₁ d)

Module sequences compose by concatenation.

@[simp]

theorem DistributedMorphology.runModules_nil {Bundle : Type u_1} (d : SpelloutDomain Bundle) : runModules [] d = d

structure DistributedMorphology.Spellout (Bundle : Type u_3) (F : Type u_4) : Type (max u_3 u_4)

A PF-branch pipeline over a spell-out domain: the ordered postsyntactic modules, then Vocabulary Insertion at each surviving position, in its neighborhood.

• modules : List (SpelloutDomain Bundle → SpelloutDomain Bundle)

  The ordered postsyntactic module sequence.

• insert : Neighborhood Bundle → List F

  The exponents inserted at a position, seeing its neighbors: one, several under Fission (scansion), none at a non-licensed position.

def DistributedMorphology.Spellout.run {Bundle : Type u_1} {F : Type u_3} (s : Spellout Bundle F) (d : SpelloutDomain Bundle) : SpelloutDomain Bundle

The domain after the module sequence.

Equations

• s.run d = DistributedMorphology.runModules s.modules d

def DistributedMorphology.Spellout.pf {Bundle : Type u_1} {F : Type u_3} (s : Spellout Bundle F) (d : SpelloutDomain Bundle) : List (List F)

The PF output: one insertion slot per surviving position.

Equations

• s.pf d = DistributedMorphology.mapNeighborhoods s.insert (s.run d)

@[simp]

theorem DistributedMorphology.Spellout.length_pf {Bundle : Type u_1} {F : Type u_3} (s : Spellout Bundle F) (d : SpelloutDomain Bundle) : (s.pf d).length = List.length (s.run d)

Exponent slots equal terminals after the modules: the exponent count diverges from the syntactic terminal count only through the modules.