Feature-decomposition exponence and the Subset Principle

The realizational engine for privative feature-decomposition accounts of syncretism ([Cah09], [Bob12]): a cell space is decomposed into feature sets D : Cell → Finset K, and a rule applies where its feature specification is contained in the cell's — the Subset Principle. Competition is [Hal97]'s feature counting: the applicable rule of greatest specification wins, as the shared core's selectBy on feats.card.

Where the linear containment engine (Exponence/Containment/) orders spans by a single threshold, this engine orders arbitrary feature sets by inclusion, so card-maximization is genuine specificity only when the applicable specifications happen to be nested; the general soundness lives in the IsWinner strict-competition predicate rather than the core's linear selectBy_isElsewhereWinner. The linear engine embeds as the chain decomposition chainDecomp i = Finset.Iic i (Exponence/Containment/Selection.lean).

Main declarations

• Rule — a feature specification plus an exponent; Applies is Subset containment
• pattern — the surface exponent at each cell, selectBy on feats.card
• IsWinner — strict feature-count competition
• noABA — the order-theoretic *ABA exclusion for a cell triple whose decomposition nests the middle cell between the outer two

structure Morphology.Decomposition.Rule {K : Type u_1} (Cell : Type u_2) (D : Cell → Finset K) (F : Type u_3) : Type (max u_1 u_3)

A rule of exponence over a feature decomposition D: a feature specification and an exponent. Applicability is the Subset Principle — the rule's features are a subset of the cell's ([Hal97]).

• feats : Finset K

  The rule's feature specification.

• exponent : F

  The exponent inserted.

@[implicit_reducible]

instance Morphology.Decomposition.instDecidableEqRule {K✝ : Type u_2} {Cell✝ : Type u_3} {D✝ : Cell✝ → Finset K✝} {F✝ : Type u_4} [DecidableEq K✝] [DecidableEq Cell✝] [DecidableEq F✝] : DecidableEq (Rule Cell✝ D✝ F✝)

Equations

• Morphology.Decomposition.instDecidableEqRule = Morphology.Decomposition.instDecidableEqRule.decEq

def Morphology.Decomposition.instDecidableEqRule.decEq {K✝ : Type u_2} {Cell✝ : Type u_3} {D✝ : Cell✝ → Finset K✝} {F✝ : Type u_4} [DecidableEq K✝] [DecidableEq Cell✝] [DecidableEq F✝] (x✝ x✝¹ : Rule Cell✝ D✝ F✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Morphology.Decomposition.instRuleRule {K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} : Exponence.Rule (Rule Cell D F) Cell F

Equations

• Morphology.Decomposition.instRuleRule = { exponent := Morphology.Decomposition.Rule.exponent, Applies := fun (r : Morphology.Decomposition.Rule Cell D F) (c : Cell) => r.feats ⊆ D c }

@[implicit_reducible]

instance Morphology.Decomposition.instDecidableRelRuleApplies {K : Type u_1} [DecidableEq K] {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} : DecidableRel Exponence.Applies

Equations

• Morphology.Decomposition.instDecidableRelRuleApplies r c = r.feats.instDecidableLE (D c)

@[simp]

theorem Morphology.Decomposition.applies_iff {K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} {r : Rule Cell D F} {c : Cell} : Exponence.Applies r c ↔ r.feats ⊆ D c

@[implicit_reducible]

instance Morphology.Decomposition.instPreorderRule {K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} : Preorder (Rule Cell D F)

The specificity preorder: applicability-set inclusion, so the engine participates in the shared core's Elsewhere selection theory (Exponence/Select.lean). Unlike the linear containment order this is only a preorder — incomparable specifications (No Case Containment) are the point.

Equations

• Morphology.Decomposition.instPreorderRule = Morphology.Exponence.toPreorder

theorem Morphology.Decomposition.le_iff {K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} {r s : Rule Cell D F} : r ≤ s ↔ ∀ ⦃c : Cell⦄, Exponence.Applies r c → Exponence.Applies s c

Specificity unfolds to applicability-set inclusion: r ≤ s iff r applies wherever s does.

def Morphology.Decomposition.pattern {K : Type u_1} [DecidableEq K] {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} (v : List (Rule Cell D F)) (c : Cell) : Option F

The surface pattern of a vocabulary: at each cell, the exponent of the most highly specified applicable rule — the Elsewhere Principle as selectBy on feature cardinality ([Hal97]'s counting formulation).

Equations

• Morphology.Decomposition.pattern v c = Option.map Morphology.Decomposition.Rule.exponent (Morphology.Exponence.selectBy (fun (r : Morphology.Decomposition.Rule Cell D F) => r.feats.card) v c)

def Morphology.Decomposition.IsWinner {K : Type u_1} {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} (v : List (Rule Cell D F)) (c : Cell) (r : Rule Cell D F) : Prop

Strict competition: r beats every other applicable rule on feature cardinality.

Equations

• Morphology.Decomposition.IsWinner v c r = (r ∈ v ∧ r.feats ⊆ D c ∧ ∀ s ∈ v, s.feats ⊆ D c → s ≠ r → s.feats.card < r.feats.card)

theorem Morphology.Decomposition.noABA {K : Type u_1} [DecidableEq K] {Cell : Type u_2} {F : Type u_3} {D : Cell → Finset K} {v : List (Rule Cell D F)} {A B : Rule Cell D F} {x y z : Cell} (h1 : D y ⊆ D z) (h2 : D x ∩ D z ⊆ D y) (hx : IsWinner v x A) (hz : IsWinner v z A) (hy : IsWinner v y B) : B = A

*ABA, order-theoretically: whenever the middle cell y nests between the outer cells — D y ⊆ D z (appliers at y persist to z) and D x ∩ D z ⊆ D y (appliers at both outer cells reach y) — a rule winning both x and z also wins y, so no exponent can interrupt an A_A pattern with a distinct middle B. The hypotheses are the shared profile of Strong and Weak Case Containment; No Case Containment violates the first.