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 is a rewrite of the domain at the first of its neighborhoods (Neighborhood.along) that satisfies the rule's condition.

Each operation carries its position-count law, so terminal/exponent misalignment is arithmetic: terminal metathesis preserves the count, obliteration and fusion never increase 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.

A focus-level rule can also be timed against insertion: applied to the domain before insertion, where the terminals beside a rewritten one see it rewritten, or to each terminal at its own insertion only, where they see it as it was. The two timings differ only for insertion that reads the context.

Main definitions

• SpelloutDomain, rewriteFirst: the domain, and rewriting it at its first neighborhood satisfying a condition.
• ObliterationRule, TerminalMetathesisRule: whole-terminal deletion and adjacent-terminal swap, each a decidable condition on a neighborhood.
• FusionRule.applyFirstAdjacent: the domain lift of Fusion.
• Spellout, Spellout.run, Spellout.pf: the module sequence, then insertion in context.
• Spellout.rewriteBefore, Spellout.rewriteAt: a focus-level rule applied before insertion, and at each terminal's own insertion.

Main results

• length_rewriteFirst_le, length_rewriteFirst: the count laws, which hold because each neighborhood reassembles to the domain (Neighborhood.toList_of_mem_along).
• Spellout.length_pf: insertion positions equal terminals after the modules.
• Spellout.pf_rewriteBefore_eq_pf_rewriteAt: the two timings of a focus-level rule give the same exponents where insertion reads the focus alone.

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 is the linear sequence of terminals the syntax hands over at spell-out.

Equations

• DistributedMorphology.SpelloutDomain Bundle = List Bundle

Rewriting at the first neighborhood

def DistributedMorphology.rewriteFirst {Bundle : Type u_1} (p : Neighborhood Bundle → Prop) [DecidablePred p] (f : Neighborhood Bundle → SpelloutDomain Bundle) (d : SpelloutDomain Bundle) : SpelloutDomain Bundle

rewriteFirst p f d replaces the domain d by f n for its first neighborhood n satisfying p, scanning left to right, and leaves it unchanged if there is none. Obliteration, terminal metathesis, and the domain lift of Fusion are its instances.

Equations

• DistributedMorphology.rewriteFirst p f d = (List.find? (fun (n : DistributedMorphology.Neighborhood Bundle) => decide (p n)) (DistributedMorphology.Neighborhood.along d)).elim d f

theorem DistributedMorphology.length_rewriteFirst_le {Bundle : Type u_1} {p : Neighborhood Bundle → Prop} [DecidablePred p] {f : Neighborhood Bundle → SpelloutDomain Bundle} (hf : ∀ (n : Neighborhood Bundle), List.length (f n) ≤ n.toList.length) (d : SpelloutDomain Bundle) : List.length (rewriteFirst p f d) ≤ List.length d

A rewrite that never lengthens a neighborhood's string never lengthens the domain.

theorem DistributedMorphology.length_rewriteFirst {Bundle : Type u_1} {p : Neighborhood Bundle → Prop} [DecidablePred p] {f : Neighborhood Bundle → SpelloutDomain Bundle} (hf : ∀ (n : Neighborhood Bundle), List.length (f n) = n.toList.length) (d : SpelloutDomain Bundle) : List.length (rewriteFirst p f d) = List.length d

A rewrite that preserves the length of each neighborhood's string preserves the number of terminals.

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

An obliteration rule, in the sense of [AN12], removes outright the terminal whose neighborhood satisfies condition. The focus-level ImpoverishmentRule deletes a feature inside a terminal, and this rule deletes the terminal.

• condition : Neighborhood Bundle → Prop

  The neighborhoods whose focus is removed.

• decCond : DecidablePred self.condition

@[instance_reducible]

instance DistributedMorphology.ObliterationRule.instDecidablePredNeighborhoodCondition {Bundle : Type u_1} (rule : ObliterationRule Bundle) : DecidablePred rule.condition

Equations

• rule.instDecidablePredNeighborhoodCondition = rule.decCond

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

Applying the rule drops the first terminal whose neighborhood satisfies its condition, and otherwise leaves the domain unchanged.

Equations

• rule.apply = DistributedMorphology.rewriteFirst rule.condition fun (n : DistributedMorphology.Neighborhood Bundle) => n.leftCtx.reverse ++ n.rightCtx

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_2) : Type u_2

A terminal metathesis rule, the terminal-order metathesis of [AN12]'s Metathesis module, swaps the focus of a neighborhood satisfying condition with the terminal to its right.

• condition : Neighborhood Bundle → Prop

  The neighborhoods whose focus swaps with the terminal to its right.

• decCond : DecidablePred self.condition

@[instance_reducible]

instance DistributedMorphology.TerminalMetathesisRule.instDecidablePredNeighborhoodCondition {Bundle : Type u_1} (rule : TerminalMetathesisRule Bundle) : DecidablePred rule.condition

Equations

• rule.instDecidablePredNeighborhoodCondition = rule.decCond

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

Applying the rule swaps the first focus that has a terminal to its right and whose neighborhood satisfies its condition with that terminal, and otherwise leaves the domain unchanged.

Equations

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

@[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_2} (rule : FusionRule F) : SpelloutDomain (List F) → SpelloutDomain (List F)

The domain lift of Fusion fuses the first terminal that fuses with the terminal to its right, and otherwise leaves the domain unchanged.

Equations

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

theorem DistributedMorphology.FusionRule.length_applyFirstAdjacent_le {F : Type u_2} (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_2) (F : Type u_3) : Type (max u_2 u_3)

A PF-branch pipeline runs the ordered postsyntactic modules over a spell-out domain, 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, which sees its neighbors. There is one, several under Fission, or none at a position that licenses none.

def DistributedMorphology.Spellout.run {Bundle : Type u_1} {F : Type u_2} (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_2} (s : Spellout Bundle F) (d : SpelloutDomain Bundle) : List (List F)

The PF output has one insertion slot per surviving position.

Equations

• s.pf d = List.map s.insert (DistributedMorphology.Neighborhood.along (s.run d))

@[simp]

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

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

The timing of a focus-level rule

def DistributedMorphology.Spellout.rewriteBefore {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) : Spellout Bundle F

s.rewriteBefore r applies the focus-level rule r to every terminal after the modules of s and before insertion, so that a terminal beside a rewritten one sees it rewritten.

Equations

• DistributedMorphology.Spellout.rewriteBefore r s = { modules := s.modules ++ [fun (d : List Bundle) => List.map r (DistributedMorphology.Neighborhood.along d)], insert := s.insert }

def DistributedMorphology.Spellout.rewriteAt {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) : Spellout Bundle F

s.rewriteAt r applies the focus-level rule r to each terminal at its own insertion only, so that a terminal beside it sees it as it was.

Equations

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

@[simp]

theorem DistributedMorphology.Spellout.run_rewriteBefore {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) (d : SpelloutDomain Bundle) : (rewriteBefore r s).run d = List.map r (Neighborhood.along (s.run d))

@[simp]

theorem DistributedMorphology.Spellout.run_rewriteAt {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) (d : SpelloutDomain Bundle) : (rewriteAt r s).run d = s.run d

@[simp]

theorem DistributedMorphology.Spellout.insert_rewriteBefore {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) : (rewriteBefore r s).insert = s.insert

@[simp]

theorem DistributedMorphology.Spellout.insert_rewriteAt {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) (n : Neighborhood Bundle) : (rewriteAt r s).insert n = s.insert { focus := r n, leftCtx := n.leftCtx, rightCtx := n.rightCtx }

theorem DistributedMorphology.Spellout.pf_rewriteBefore_eq_pf_rewriteAt {Bundle : Type u_1} {F : Type u_2} (r : Neighborhood Bundle → Bundle) (s : Spellout Bundle F) (hs : ∀ (n n' : Neighborhood Bundle), n.focus = n'.focus → s.insert n = s.insert n') (d : SpelloutDomain Bundle) : (rewriteBefore r s).pf d = (rewriteAt r s).pf d

The timing of a focus-level rule matters only to insertion that reads the context. Where insertion reads the focus alone, the rule yields the same exponents applied before insertion and at insertion.