Senturia and Marcolli (2025): The Algebraic Structure of Morphosyntax

This file formalizes the Distributed Morphology operations of [SM25], which models morphology inside the Merge algebra of [MCB25]. A morphological object is built by the same free non-associative commutative magma as a syntactic object, with features in place of lexical items, and differs from it only in labeling: an internal vertex carries the union of its children's feature bundles (Definition 2.1), so a bundle is derived from the tree (bundle, bundle_fuse). A morphosyntactic tree inserts morphological objects at the leaves of a syntactic tree under the syntax-morphology feature correspondence (Definitions 2.4 and 3.4; FeatureCorrespondence, Morphosyntactic, Matched), and forgetting the inserted morphology is the morphism of algebras over the Merge operad of Definition 3.9 (toSyntactic).

On this carrier the four operations reduce to two. Fusion is the magma product itself (Definition 5.2, fuse), which is why it is the one operation available inside syntax. Fission restricts the tree vertex-wise along a partition of its bundle with a copied residue (Definition 5.6, restrict) and duplicates exactly that residue (msFeatures_fissionSite_copy). Impoverishment keeps one fission output and obliteration empties an insertion (Propositions 5.13 and 5.20), so both derive from fission (Proposition 5.21). Fission followed by fusion restores the bundle but not the tree (bundle_fuse_restrict, fuse_restrict_ne, the paper's Example 5.7). Closing the site relations under congruence gives the post-syntactic and Distributed Morphology semigroups of Definition 6.1 as rewrite relations (PostSyntactic, Derivation): along the first the total feature set is invariant while the boundary between syntax and morphology moves one leaf at a time (PostSyntactic.toFinset_msFeatures_eq, Step.numLeaves_fuse, Step.numLeaves_fiss); along the second the feature set can only shrink (Derivation.toFinset_msFeatures_subset).

Implementation notes

• Morphological objects are unordered trees over F ⊕ Unit, features at the leaves and bare structural vertices elsewhere. IsMorphological does not constrain arity, so the theorems cover the paper's binary objects and the non-branching extended objects of Definition 2.8 alike. Restriction keeps a structural vertex whose leaves all vanish as a childless vertex where the quotient of Definition 5.6 removes it; both carry the empty bundle.
• A morphosyntactic tree is kept in labeled form, each syntactic leaf carrying its datum and the inserted object, none for the empty insertion of Remark 5.12; this carries the same data as splicing the object below the leaf.
• The operations are stated as transformations of morphosyntactic trees, the first of the paper's two equivalent perspectives; the semigroups act on trees rather than on the assembly operations of Definition 4.2.

TODO

The workspace Hopf algebra with obliteration via the coproduct, and the colored correspondence between the syntactic and morphosyntactic algebras over the Merge operad (Theorem 3.16).

References

• [SM25]
• [MCB25]
• [Hew23]

Morphological objects and the derived bundle labeling

A morphological object is a nonplanar tree with single features at the leaves and bare structural vertices elsewhere — the alphabet F ⊕ Unit, exactly the carrier shape of syntactic objects with features in place of the lexical items. Definition 2.1 of [SM25] labels each internal vertex with the union of its children's bundles, so every vertex label is determined by the leaves below it; bundle is the root's.

inductive SenturiaMarcolli2025.IsMorphological {F : Type u_1} : RoseTree (F ⊕ Unit) → Prop

Features occur only at leaves: internal vertices are structural. Arity is not constrained, so the predicate covers the paper's binary objects and the non-branching extended objects of Definition 2.8 that restriction produces.

• leaf {F : Type u_1} (x : F ⊕ Unit) : IsMorphological (RoseTree.node x [])
• node {F : Type u_1} {cs : List (RoseTree (F ⊕ Unit))} (hne : cs ≠ []) (h : ∀ c ∈ cs, IsMorphological c) : IsMorphological (RoseTree.node (Sum.inr ()) cs)

def SenturiaMarcolli2025.leafFeatures {F : Type u_1} (t : RoseTree (F ⊕ Unit)) : Multiset F

The multiset of leaf features of a planar tree.

Equations

• SenturiaMarcolli2025.leafFeatures t = Multiset.filterMap Sum.getLeft? t.leaves

def SenturiaMarcolli2025.bundle {F : Type u_1} [DecidableEq F] (S : UnorderedTree (F ⊕ Unit)) : Finset F

The feature bundle of a morphological object: the set of features at its leaves, the root label of [SM25] Definition 2.1.

Equations

• SenturiaMarcolli2025.bundle S = (Multiset.filterMap Sum.getLeft? S.leaves).toFinset

@[simp]

theorem SenturiaMarcolli2025.bundle_mk {F : Type u_1} [DecidableEq F] (t : RoseTree (F ⊕ Unit)) : bundle (UnorderedTree.mk t) = (leafFeatures t).toFinset

@[simp]

theorem SenturiaMarcolli2025.bundle_leaf {F : Type u_1} [DecidableEq F] (f : F) : bundle (UnorderedTree.leaf (Sum.inl f)) = {f}

@[simp]

theorem SenturiaMarcolli2025.bundle_leaf_inr {F : Type u_1} [DecidableEq F] : bundle (UnorderedTree.leaf (Sum.inr ())) = ∅

def SenturiaMarcolli2025.features {F : Type u_1} (S : UnorderedTree (F ⊕ Unit)) : Multiset F

The multiset of leaf features of a morphological object; bundle is its underlying set. Fission with an overlapping partition duplicates features, which only the multiset records.

Equations

• SenturiaMarcolli2025.features S = Multiset.filterMap Sum.getLeft? S.leaves

@[simp]

theorem SenturiaMarcolli2025.features_mk {F : Type u_1} (t : RoseTree (F ⊕ Unit)) : features (UnorderedTree.mk t) = leafFeatures t

theorem SenturiaMarcolli2025.bundle_eq_toFinset_features {F : Type u_1} [DecidableEq F] (S : UnorderedTree (F ⊕ Unit)) : bundle S = (features S).toFinset

theorem SenturiaMarcolli2025.leafFeatures_node_inr {F : Type u_1} (cs : List (RoseTree (F ⊕ Unit))) : leafFeatures (RoseTree.node (Sum.inr ()) cs) = (List.map leafFeatures cs).sum

A structural vertex contributes nothing to the bundle: the leaf features of a structural node are the concatenation of its children's, whether or not children remain.

Fusion

Fusion merges the bundles at two adjacent leaves of the syntactic tree into one ([SM25] §5.1, Swahili negation si- fusing NEG with first-singular agreement). On morphological objects it is the magma operation itself — grafting under a fresh structural root — which is why fusion is the one DM operation available inside syntax.

noncomputable def SenturiaMarcolli2025.fuse {F : Type u_1} (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : UnorderedTree (F ⊕ Unit)

Fusion of two morphological objects: the magma product, grafting both under a structural root ([SM25] Definition 5.2).

Equations

• SenturiaMarcolli2025.fuse S₁ S₂ = UnorderedTree.node (Sum.inr ()) {S₁, S₂}

theorem SenturiaMarcolli2025.bundle_fuse {F : Type u_1} [DecidableEq F] (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : bundle (fuse S₁ S₂) = bundle S₁ ∪ bundle S₂

The fused bundle is the union of the input bundles — the labeling law itself, so fusion needs nothing beyond the magma.

theorem SenturiaMarcolli2025.features_fuse {F : Type u_1} (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : features (fuse S₁ S₂) = features S₁ + features S₂

Fusion is additive on the feature multiset: nothing is lost, duplicated, or created.

Fission

Fission splits one bundle into two along a partition B ∖ A = B₁ ⊔ B₂, with the residue A copied into both outputs ([SM25] §5.2; the discontinuous agreement of Ṣanʕānī Arabic after [Hew23], where person and number of a single head surface as prefix and suffix). Each output is the input tree restricted vertex-wise to the kept features: leaves outside the kept set are deleted, structural vertices stay, and vanished subtrees may leave non-branching structural vertices behind — the extended morphological objects.

def SenturiaMarcolli2025.keep {F : Type u_1} [DecidableEq F] (C : Finset F) : F ⊕ Unit → Option (F ⊕ Unit)

Keep a leaf feature iff it lies in C; structural vertices always survive.

Equations

• SenturiaMarcolli2025.keep C (Sum.inl f) = if f ∈ C then some (Sum.inl f) else none
• SenturiaMarcolli2025.keep C (Sum.inr val) = some (Sum.inr ())

def SenturiaMarcolli2025.restrict {F : Type u_1} [DecidableEq F] (C : Finset F) (S : UnorderedTree (F ⊕ Unit)) : Option (UnorderedTree (F ⊕ Unit))

Restriction of a morphological object to the features in C: the construction of a single fission output ([SM25] Definition 5.6, with C = Bᵢ ∪ A). none only for a single leaf outside C.

Equations

• SenturiaMarcolli2025.restrict C S = UnorderedTree.filterMap (SenturiaMarcolli2025.keep C) S

theorem SenturiaMarcolli2025.bundle_restrict {F : Type u_1} [DecidableEq F] {C : Finset F} {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) {S' : UnorderedTree (F ⊕ Unit)} (h : restrict C (UnorderedTree.mk t) = some S') : bundle S' = bundle (UnorderedTree.mk t) ∩ C

The bundle of a fission output is the input bundle restricted to the kept features: the vertex law B_w ∩ (Bᵢ ∪ A) of [SM25] Definition 5.6, at the root.

theorem SenturiaMarcolli2025.features_restrict {F : Type u_1} [DecidableEq F] (C : Finset F) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) : (restrict C (UnorderedTree.mk t)).elim 0 features = Multiset.filter (fun (x : F) => x ∈ C) (features (UnorderedTree.mk t))

Multiset form of bundle_restrict: restriction filters the feature multiset, none counting as empty.

theorem SenturiaMarcolli2025.restrict_copies_shared {F : Type u_1} [DecidableEq F] {A C₁ C₂ : Finset F} (h₁ : A ⊆ C₁) (h₂ : A ⊆ C₂) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) {S₁' S₂' : UnorderedTree (F ⊕ Unit)} (e₁ : restrict C₁ (UnorderedTree.mk t) = some S₁') (e₂ : restrict C₂ (UnorderedTree.mk t) = some S₂') : A ∩ bundle (UnorderedTree.mk t) ⊆ bundle S₁' ∩ bundle S₂'

Features copied into both sides of the fission partition survive in both outputs: the residue of a discontinuously realized bundle is pronounced on both exponents.

Impoverishment as fission plus fusion

[SM25] Propositions 5.20–5.21: impoverishment and obliteration are not independent operations. Discarding a subbundle is keeping one fission output (bundle_restrict with the kept part as C); the trace-maintaining variant fissions and refuses at the same vertex, restoring the bundle without restoring the tree. Obliteration replaces a whole morphological object by the unit of the workspace algebra, which lives in the second slice.

theorem SenturiaMarcolli2025.bundle_fuse_restrict {F : Type u_1} [DecidableEq F] {C₁ C₂ : Finset F} {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) (hcover : bundle (UnorderedTree.mk t) ⊆ C₁ ∪ C₂) {S₁' S₂' : UnorderedTree (F ⊕ Unit)} (e₁ : restrict C₁ (UnorderedTree.mk t) = some S₁') (e₂ : restrict C₂ (UnorderedTree.mk t) = some S₂') : bundle (fuse S₁' S₂') = bundle (UnorderedTree.mk t)

Fission followed by fusion restores the bundle: the trace-maintaining impoverishment composite leaves the feature content intact.

The tree is not restored

Fission at a partition whose residue is copied into both outputs, then fusion, restores the bundle but not the tree: the copied feature now occupies a leaf on each side, so the composite has strictly more leaves. The witness is [SM25] Example 5.7: [φ, α, β, γ] with kept sets [φ, γ] and [φ, α, β].

inductive SenturiaMarcolli2025.Feat : Type

• phi : Feat
• alpha : Feat
• beta : Feat
• gamma : Feat

@[instance_reducible]

instance SenturiaMarcolli2025.instDecidableEqFeat : DecidableEq Feat

Equations

• SenturiaMarcolli2025.instDecidableEqFeat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SenturiaMarcolli2025.instReprFeat : Repr Feat

Equations

• SenturiaMarcolli2025.instReprFeat = { reprPrec := SenturiaMarcolli2025.instReprFeat.repr }

def SenturiaMarcolli2025.instReprFeat.repr : Feat → ℕ → Std.Format

Equations

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

def SenturiaMarcolli2025.exTree : RoseTree (Feat ⊕ Unit)

Equations

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

theorem SenturiaMarcolli2025.fuse_restrict_ne (S₁' S₂' : UnorderedTree (Feat ⊕ Unit)) (e₁ : restrict {Feat.phi, Feat.gamma} (UnorderedTree.mk exTree) = some S₁') (e₂ : restrict {Feat.phi, Feat.alpha, Feat.beta} (UnorderedTree.mk exTree) = some S₂') : fuse S₁' S₂' ≠ UnorderedTree.mk exTree

Restriction to {φ, γ} and {φ, α, β} followed by fusion yields a five-leaf object: φ is realized on both sides, so the composite is not the original four-leaf tree even though its bundle is (bundle_fuse_restrict).

The syntax-morphology correspondence and morphosyntactic trees

A morphosyntactic tree inserts morphological objects at the leaves of a syntactic tree, constrained by a matching rule between the bundle at the root of the inserted object and the syntactic datum at the leaf ([SM25] Definitions 2.4 and 3.4). We keep the insertion as a leaf label — syntactic datum paired with the inserted object — which carries the same data as splicing the object below the leaf.

structure SenturiaMarcolli2025.FeatureCorrespondence (F : Type u_2) (Λ : Type u_3) [DecidableEq F] : Type (max u_2 u_3)

The syntax-morphology feature correspondence: which feature bundles can be matched with which lexical items and syntactic features ([SM25] Definition 2.4). Matching is multivalued in both directions, but every syntactic datum carries some bundle.

• matching : Finset F → Λ → Prop

  matching B lex iff the bundle B can decorate a leaf carrying the syntactic datum lex.

• matching_surjective (lex : Λ) : ∃ (B : Finset F), self.matching B lex

  Every syntactic datum carries some bundle.

@[reducible, inline]

abbrev SenturiaMarcolli2025.Morphosyntactic (F : Type u_2) (Λ : Type u_3) : Type (max u_2 u_3)

A morphosyntactic tree in labeled form: each syntactic leaf carries its datum together with the inserted morphological object, none where morphology was obliterated ([SM25] Definition 3.4; the empty insertion is Remark 5.12).

Equations

• SenturiaMarcolli2025.Morphosyntactic F Λ = UnorderedTree (Λ × Option (UnorderedTree (F ⊕ Unit)) ⊕ Unit)

def SenturiaMarcolli2025.insertion {F : Type u_1} {Λ : Type u_2} (lex : Λ) (mo : Option (UnorderedTree (F ⊕ Unit))) : Morphosyntactic F Λ

A leaf of a morphosyntactic tree: a syntactic datum with an optional morphological insertion.

Equations

• SenturiaMarcolli2025.insertion lex mo = UnorderedTree.leaf (Sum.inl (lex, mo))

def SenturiaMarcolli2025.toSyntactic {F : Type u_1} {Λ : Type u_2} : Morphosyntactic F Λ → UnorderedTree (Λ ⊕ Unit)

The forgetful projection to the syntactic tree: drop the inserted morphology. This is [SM25] Definition 3.9's morphism of algebras over the Merge operad, in labeled form.

Equations

• SenturiaMarcolli2025.toSyntactic = UnorderedTree.map (Sum.map Prod.fst id)

@[simp]

theorem SenturiaMarcolli2025.toSyntactic_insertion {F : Type u_1} {Λ : Type u_2} (lex : Λ) (mo : Option (UnorderedTree (F ⊕ Unit))) : toSyntactic (insertion lex mo) = UnorderedTree.leaf (Sum.inl lex)

def SenturiaMarcolli2025.insertionFeatures {F : Type u_1} {Λ : Type u_2} : Λ × Option (UnorderedTree (F ⊕ Unit)) ⊕ Unit → Multiset F

The feature content of one leaf label.

Equations

• SenturiaMarcolli2025.insertionFeatures (Sum.inl (fst, some S)) = SenturiaMarcolli2025.features S
• SenturiaMarcolli2025.insertionFeatures (Sum.inl (fst, none)) = 0
• SenturiaMarcolli2025.insertionFeatures (Sum.inr val) = 0

@[simp]

theorem SenturiaMarcolli2025.insertionFeatures_inl {F : Type u_1} {Λ : Type u_2} (lex : Λ) (mo : Option (UnorderedTree (F ⊕ Unit))) : insertionFeatures (Sum.inl (lex, mo)) = mo.elim 0 features

def SenturiaMarcolli2025.msFeatures {F : Type u_1} {Λ : Type u_2} (T : Morphosyntactic F Λ) : Multiset F

The total feature content of a morphosyntactic tree: everything its inserted morphological objects carry, with multiplicity.

Equations

• SenturiaMarcolli2025.msFeatures T = (Multiset.map SenturiaMarcolli2025.insertionFeatures (UnorderedTree.leaves T)).sum

@[simp]

theorem SenturiaMarcolli2025.msFeatures_insertion {F : Type u_1} {Λ : Type u_2} (lex : Λ) (mo : Option (UnorderedTree (F ⊕ Unit))) : msFeatures (insertion lex mo) = mo.elim 0 features

def SenturiaMarcolli2025.Matched {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (Γ : FeatureCorrespondence F Λ) (T : Morphosyntactic F Λ) : Prop

Every inserted morphological object matches its leaf's syntactic datum.

Equations

• SenturiaMarcolli2025.Matched Γ T = ∀ (lex : Λ) (S : UnorderedTree (F ⊕ Unit)), Sum.inl (lex, some S) ∈ UnorderedTree.leaves T → Γ.matching (SenturiaMarcolli2025.bundle S) lex

theorem SenturiaMarcolli2025.matched_insertion_iff {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (Γ : FeatureCorrespondence F Λ) (lex : Λ) (S : UnorderedTree (F ⊕ Unit)) : Matched Γ (insertion lex (some S)) ↔ Γ.matching (bundle S) lex

The DM operations at their application site

The four DM operations transform the assembly of a morphosyntactic tree at one site ([SM25] §5–§6). Fusion turns a syntactic cherry over two insertions into a single insertion of the magma product; fission turns one insertion into a cherry over its two restrictions. Under toSyntactic the first collapses a cherry and the second grows one — the movable syntax-morphology boundary — while msFeatures records what happens to the feature content.

noncomputable def SenturiaMarcolli2025.fusionSite {F : Type u_1} {Λ : Type u_2} (lex₁ lex₂ : Λ) (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : Morphosyntactic F Λ

The application site of fusion: a syntactic cherry with insertions at both leaves.

Equations

• SenturiaMarcolli2025.fusionSite lex₁ lex₂ S₁ S₂ = UnorderedTree.node (Sum.inr ()) {SenturiaMarcolli2025.insertion lex₁ (some S₁), SenturiaMarcolli2025.insertion lex₂ (some S₂)}

noncomputable def SenturiaMarcolli2025.fissionSite {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex₁ lex₂ : Λ) (C₁ C₂ : Finset F) (S : UnorderedTree (F ⊕ Unit)) : Morphosyntactic F Λ

The application site of fission on S along the kept sets C₁, C₂: a syntactic cherry whose leaves carry the two restrictions; an empty restriction is an empty insertion.

Equations

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

theorem SenturiaMarcolli2025.msFeatures_fusionSite {F : Type u_1} {Λ : Type u_2} (lex₁ lex₂ : Λ) (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : msFeatures (fusionSite lex₁ lex₂ S₁ S₂) = features S₁ + features S₂

theorem SenturiaMarcolli2025.msFeatures_fuse {F : Type u_1} {Λ : Type u_2} (lexHead lex₁ lex₂ : Λ) (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : msFeatures (insertion lexHead (some (fuse S₁ S₂))) = msFeatures (fusionSite lex₁ lex₂ S₁ S₂)

Fusion preserves the total feature content at the site: the fused insertion, under whichever of the two data projects (the head function's choice in [SM25] Definition 5.2), carries exactly what the cherry carried.

theorem SenturiaMarcolli2025.toSyntactic_fusionSite {F : Type u_1} {Λ : Type u_2} (lex₁ lex₂ : Λ) (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : toSyntactic (fusionSite lex₁ lex₂ S₁ S₂) = UnorderedTree.node (Sum.inr ()) {UnorderedTree.leaf (Sum.inl lex₁), UnorderedTree.leaf (Sum.inl lex₂)}

Fusion raises the syntax-morphology boundary: the syntactic projection collapses from a cherry to a single leaf while the feature content stays constant (msFeatures_fuse).

theorem SenturiaMarcolli2025.matched_fused_iff {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (Γ : FeatureCorrespondence F Λ) (lexHead : Λ) (S₁ S₂ : UnorderedTree (F ⊕ Unit)) : Matched Γ (insertion lexHead (some (fuse S₁ S₂))) ↔ Γ.matching (bundle S₁ ∪ bundle S₂) lexHead

The necessary condition for fusion: the fused site is matched exactly when the union of the two bundles matches the projecting datum ([SM25]'s condition (B_{v₁} ∪ B_{v₂}, α_v) ∈ Γ_SM following Definition 5.2).

theorem SenturiaMarcolli2025.msFeatures_fissionSite {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex₁ lex₂ : Λ) (C₁ C₂ : Finset F) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) : msFeatures (fissionSite lex₁ lex₂ C₁ C₂ (UnorderedTree.mk t)) = Multiset.filter (fun (x : F) => x ∈ C₁) (features (UnorderedTree.mk t)) + Multiset.filter (fun (x : F) => x ∈ C₂) (features (UnorderedTree.mk t))

theorem SenturiaMarcolli2025.msFeatures_fission_partition {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex₁ lex₂ : Λ) {C₁ C₂ : Finset F} (hdisj : Disjoint C₁ C₂) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) (hcover : ∀ f ∈ features (UnorderedTree.mk t), f ∈ C₁ ∪ C₂) : msFeatures (fissionSite lex₁ lex₂ C₁ C₂ (UnorderedTree.mk t)) = features (UnorderedTree.mk t)

Fission along a disjoint cover of the bundle preserves the feature multiset: the boundary moves down (toSyntactic grows a cherry) with no change in feature content. An overlapping partition instead duplicates the shared residue (restrict_copies_shared), which is how the copied features of discontinuous agreement come to be pronounced twice.

theorem SenturiaMarcolli2025.msFeatures_impoverish_le {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex : Λ) (kept : Finset F) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) : msFeatures (insertion lex (restrict kept (UnorderedTree.mk t))) ≤ msFeatures (insertion lex (some (UnorderedTree.mk t)))

Impoverishment at a leaf only removes features: keeping one fission output ([SM25] Proposition 5.20, first case) bounds the feature content by the original.

theorem SenturiaMarcolli2025.toSyntactic_obliterate {F : Type u_1} {Λ : Type u_2} (lex : Λ) (S : UnorderedTree (F ⊕ Unit)) : toSyntactic (insertion lex none) = toSyntactic (insertion lex (some S))

Obliteration removes the entire insertion while the syntactic leaf and its datum stay in place — [SM25]'s reading of Proposition 5.13, on which no morphology is inserted and the syntactic tree is untouched.

@[simp]

theorem SenturiaMarcolli2025.msFeatures_obliterate {F : Type u_1} {Λ : Type u_2} (lex : Λ) : msFeatures (insertion lex none) = 0

One-step transformations and the post-syntactic semigroup

The DM operations act anywhere in a morphosyntactic tree: a step applies a site transformation at the root of some subtree. Compositions of such steps form [SM25] Definition 6.1's semigroups — the post-syntactic semigroup generated by fusion and fission, and the full Distributed Morphology semigroup adding impoverishment and obliteration. Their action is the movable syntax-morphology boundary: PostSyntactic preserves the total feature set exactly, and Derivation can only shrink it.

inductive SenturiaMarcolli2025.Step {F : Type u_1} {Λ : Type u_2} (R : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop) : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

Close a site relation under congruence: apply it at the root or inside one subtree.

• here {F : Type u_1} {Λ : Type u_2} {R : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop} {T T' : Morphosyntactic F Λ} : R T T' → Step R T T'
• congr {F : Type u_1} {Λ : Type u_2} {R : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop} {x : Λ × Option (UnorderedTree (F ⊕ Unit)) ⊕ Unit} {cs : Multiset (Morphosyntactic F Λ)} {T T' : Morphosyntactic F Λ} : Step R T T' → Step R (UnorderedTree.node x (T ::ₘ cs)) (UnorderedTree.node x (T' ::ₘ cs))

inductive SenturiaMarcolli2025.FuseAt {F : Type u_1} {Λ : Type u_2} : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

The fusion site relation: a syntactic cherry over two insertions rewrites to a single insertion of the magma product, projecting one of the two data.

• mk {F : Type u_1} {Λ : Type u_2} (lexHead lex₁ lex₂ : Λ) (S₁ S₂ : UnorderedTree (F ⊕ Unit)) (hhead : lexHead = lex₁ ∨ lexHead = lex₂) : FuseAt (fusionSite lex₁ lex₂ S₁ S₂) (insertion lexHead (some (fuse S₁ S₂)))

inductive SenturiaMarcolli2025.FissAt {F : Type u_1} [DecidableEq F] {Λ : Type u_2} : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

The fission site relation: an insertion rewrites to a syntactic cherry over the two restrictions determined by a partition B ∖ A = B₁ ⊔ B₂ of its bundle with copied residue A ([SM25] Definition 5.6).

• mk {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex lex₁ lex₂ : Λ) (A B₁ B₂ : Finset F) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) (hlex : lex = lex₁ ∨ lex = lex₂) (h₁ : Disjoint A B₁) (h₂ : Disjoint A B₂) (h₁₂ : Disjoint B₁ B₂) (hcover : ∀ f ∈ features (UnorderedTree.mk t), f ∈ A ∪ B₁ ∪ B₂) : FissAt (insertion lex (some (UnorderedTree.mk t))) (fissionSite lex₁ lex₂ (B₁ ∪ A) (B₂ ∪ A) (UnorderedTree.mk t))

inductive SenturiaMarcolli2025.ImpovAt {F : Type u_1} [DecidableEq F] {Λ : Type u_2} : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

The impoverishment site relation: the insertion is replaced by one of its fission outputs.

• mk {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex : Λ) (kept : Finset F) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) : ImpovAt (insertion lex (some (UnorderedTree.mk t))) (insertion lex (restrict kept (UnorderedTree.mk t)))

inductive SenturiaMarcolli2025.OblitAt {F : Type u_1} {Λ : Type u_2} : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

The obliteration site relation: the insertion is emptied, the syntactic leaf and its datum staying in place.

• mk {F : Type u_1} {Λ : Type u_2} (lex : Λ) (mo : Option (UnorderedTree (F ⊕ Unit))) : OblitAt (insertion lex mo) (insertion lex none)

theorem SenturiaMarcolli2025.msFeatures_fissionSite_copy {F : Type u_1} [DecidableEq F] {Λ : Type u_2} (lex₁ lex₂ : Λ) {A B₁ B₂ : Finset F} (h₁ : Disjoint A B₁) (h₂ : Disjoint A B₂) (h₁₂ : Disjoint B₁ B₂) {t : RoseTree (F ⊕ Unit)} (ht : IsMorphological t) (hcover : ∀ f ∈ features (UnorderedTree.mk t), f ∈ A ∪ B₁ ∪ B₂) : msFeatures (fissionSite lex₁ lex₂ (B₁ ∪ A) (B₂ ∪ A) (UnorderedTree.mk t)) = features (UnorderedTree.mk t) + Multiset.filter (fun (x : F) => x ∈ A) (features (UnorderedTree.mk t))

Fission duplicates exactly the copied residue: with B ∖ A partitioned into B₁ ⊔ B₂ and A copied to both sides, the site's feature multiset grows by precisely the A-part. A = ∅ recovers content invariance (msFeatures_fission_partition).

Feature bookkeeping along the semigroups

theorem SenturiaMarcolli2025.FuseAt.msFeatures_eq {F : Type u_1} {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : FuseAt T T') : msFeatures T' = msFeatures T

theorem SenturiaMarcolli2025.FissAt.toFinset_msFeatures_eq {F : Type u_1} [DecidableEq F] {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : FissAt T T') : (msFeatures T').toFinset = (msFeatures T).toFinset

theorem SenturiaMarcolli2025.ImpovAt.msFeatures_le {F : Type u_1} [DecidableEq F] {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : ImpovAt T T') : msFeatures T' ≤ msFeatures T

theorem SenturiaMarcolli2025.OblitAt.msFeatures_le {F : Type u_1} {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : OblitAt T T') : msFeatures T' ≤ msFeatures T

theorem SenturiaMarcolli2025.Step.msFeatures_eq {F : Type u_1} {Λ : Type u_2} {R : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop} (hR : ∀ {T T' : Morphosyntactic F Λ}, R T T' → msFeatures T' = msFeatures T) {T T' : Morphosyntactic F Λ} (h : Step R T T') : msFeatures T' = msFeatures T

A site-level feature-content identity transfers through the congruence closure.

theorem SenturiaMarcolli2025.Step.msFeatures_le {F : Type u_1} {Λ : Type u_2} {R : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop} (hR : ∀ {T T' : Morphosyntactic F Λ}, R T T' → msFeatures T' ≤ msFeatures T) {T T' : Morphosyntactic F Λ} (h : Step R T T') : msFeatures T' ≤ msFeatures T

theorem SenturiaMarcolli2025.Step.toFinset_msFeatures_eq {F : Type u_1} [DecidableEq F] {Λ : Type u_2} {R : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop} (hR : ∀ {T T' : Morphosyntactic F Λ}, R T T' → (msFeatures T').toFinset = (msFeatures T).toFinset) {T T' : Morphosyntactic F Λ} (h : Step R T T') : (msFeatures T').toFinset = (msFeatures T).toFinset

theorem SenturiaMarcolli2025.Step.numLeaves_fuse {F : Type u_1} {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : Step FuseAt T T') : UnorderedTree.numLeaves T' + 1 = UnorderedTree.numLeaves T

Fusion moves the boundary up: one syntactic leaf fewer, wherever it applies.

theorem SenturiaMarcolli2025.Step.numLeaves_fiss {F : Type u_1} [DecidableEq F] {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : Step FissAt T T') : UnorderedTree.numLeaves T + 1 = UnorderedTree.numLeaves T'

Fission moves the boundary down: one syntactic leaf more, wherever it applies.

The two semigroups and the movable boundary

def SenturiaMarcolli2025.PostSyntactic {F : Type u_1} [DecidableEq F] {Λ : Type u_2} : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

The post-syntactic semigroup: compositions of fusion and fission steps ([SM25] Definition 6.1).

Equations

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

def SenturiaMarcolli2025.Derivation {F : Type u_1} [DecidableEq F] {Λ : Type u_2} : Morphosyntactic F Λ → Morphosyntactic F Λ → Prop

A derivation of the full Distributed Morphology semigroup: post-syntactic steps together with impoverishment and obliteration ([SM25] Definition 6.1).

Equations

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

theorem SenturiaMarcolli2025.PostSyntactic.toFinset_msFeatures_eq {F : Type u_1} [DecidableEq F] {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : PostSyntactic T T') : (msFeatures T').toFinset = (msFeatures T).toFinset

The movable boundary, feature side: the post-syntactic semigroup never creates or destroys a feature. Any composition of fusions and fissions leaves the total feature set invariant — the operations only move the boundary between syntax and morphology.

theorem SenturiaMarcolli2025.Derivation.toFinset_msFeatures_subset {F : Type u_1} [DecidableEq F] {Λ : Type u_2} {T T' : Morphosyntactic F Λ} (h : Derivation T T') : (msFeatures T').toFinset ⊆ (msFeatures T).toFinset

Along the full Distributed Morphology semigroup the feature set can only shrink: fusion and fission preserve it, impoverishment and obliteration delete.

The economy of bivalent features

[SM25] Remark 2.3: with n feature categories and three valuations (+, −, unvalued), the bivalent inventory has n + 3 generating objects against the 3 n features a privative encoding needs, strictly fewer for more than one category.

theorem SenturiaMarcolli2025.bivalent_economy {n : ℕ} (h : 1 < n) : n + 3 < 3 * n

The bivalent inventory is the smaller one as soon as there is more than one feature category.