Categorizing Heads (Distributed Morphology) @cite{harley-2014}

@cite{embick-2004} @cite{marantz-1997} @cite{kramer-2015}

@cite{harley-2014} "On the identity of roots" addresses three questions about roots in DM:

1. What are roots? (§2) Root terminal nodes are individuated by arbitrary indices, not by phonological or semantic content. The Categorization Assumption holds: roots must merge with a categorizing head (n, v, a) to enter the syntax.

2. Can roots take complements? (§3) Yes — roots can Merge directly with internal arguments without mediation by a functional head. Evidence: one-replacement in argument structure nominals, verb-object idioms, Hiaki suppletive verbs conditioned by the root's complement.

3. What delimits the domain of special interpretation? (§4) VoiceP, not the first categorizing head. Idiosyncratic interpretation can extend past the first categorizer (evidence: multiply derived words like editorial, classifieds, nationalize). Voice is the phase head.

DM Three-Lists Architecture (@cite{marantz-1997}, @cite{harley-2014} §5)

• List 1: Root terminal nodes — syntactic atoms with opaque indices
• List 2: Vocabulary Items — phonological realizations competing for insertion
• List 3: Encyclopedia entries — interpretations conditioned by context

Phi-Features on n (@cite{kramer-2015} Ch 3)

@cite{kramer-2015} argues that grammatical gender is a phi-feature located on the nominalizing head n, not on roots. The feature system is parameterized across languages by dimension (what binary feature is used):

Language	Dimension	Four types of n
Amharic	[±FEM]	n i[+FEM], n i[−FEM], n, n u[+FEM]
Spanish	[±FEM]	n i[+FEM], n i[−FEM], n, n u[+FEM]
Maa	[±FEM]	n i[+FEM], n i[−FEM], n, n u[−FEM]
Algonquian	[±ANIM]	n i[+ANIM], n i[−ANIM], n, n u[+ANIM]

(@cite{kramer-2015} Chs 3, 5-7; @cite{adamson-2024} extends this to Teop [±ANIM] and Jarawara [±MASC])

This module formalizes the categorization layer, its phi-feature content, and its relationship to Voice. List 2 (Vocabulary Insertion) is formalized in VocabularyInsertion.lean.

inductive Morphology.DM.Categorizer : Type

A categorizing head that merges with an acategorial root to project syntactic structure. The three options correspond to the functional heads n, v, a in Distributed Morphology (@cite{marantz-1997}, @cite{harley-2014} §2).

• n : Categorizer
• v : Categorizer
• a : Categorizer

instance Morphology.DM.instDecidableEqCategorizer : DecidableEq Categorizer

Equations

• Morphology.DM.instDecidableEqCategorizer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Morphology.DM.instBEqCategorizer : BEq Categorizer

Equations

• Morphology.DM.instBEqCategorizer = { beq := Morphology.DM.instBEqCategorizer.beq }

def Morphology.DM.instBEqCategorizer.beq : Categorizer → Categorizer → Bool

Equations

• Morphology.DM.instBEqCategorizer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Morphology.DM.instReprCategorizer.repr : Categorizer → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprCategorizer : Repr Categorizer

Equations

• Morphology.DM.instReprCategorizer = { reprPrec := Morphology.DM.instReprCategorizer.repr }

def Morphology.DM.Categorizer.toCategory : Categorizer → Minimalism.Cat

Map a categorizer to its syntactic category.

Equations

• Morphology.DM.Categorizer.n.toCategory = Minimalism.Cat.N
• Morphology.DM.Categorizer.v.toCategory = Minimalism.Cat.V
• Morphology.DM.Categorizer.a.toCategory = Minimalism.Cat.A

inductive Morphology.DM.GenderDimension : Type

Gender feature dimension. Different languages locate different binary features on n (@cite{kramer-2015} Chs 3, 5-7):

• FEM: [±FEM] dimension (Amharic, Spanish, Maa, Dieri, Wari', Lavukaleve)
• MASC: [±MASC] dimension (Jarawara; @cite{adamson-2024})
• ANIM: [±ANIM] dimension (Algonquian, Teop, Lealao Chinantec)

• fem : GenderDimension
• masc : GenderDimension
• anim : GenderDimension

instance Morphology.DM.instDecidableEqGenderDimension : DecidableEq GenderDimension

Equations

• Morphology.DM.instDecidableEqGenderDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Morphology.DM.instBEqGenderDimension : BEq GenderDimension

Equations

• Morphology.DM.instBEqGenderDimension = { beq := Morphology.DM.instBEqGenderDimension.beq }

def Morphology.DM.instBEqGenderDimension.beq : GenderDimension → GenderDimension → Bool

Equations

• Morphology.DM.instBEqGenderDimension.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Morphology.DM.instReprGenderDimension : Repr GenderDimension

Equations

• Morphology.DM.instReprGenderDimension = { reprPrec := Morphology.DM.instReprGenderDimension.repr }

def Morphology.DM.instReprGenderDimension.repr : GenderDimension → ℕ → Std.Format

Equations

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

inductive Morphology.DM.Polarity : Type

Polarity of a gender feature value. The binary [±VAL] system from @cite{kramer-2015} Ch 3.

Note: polarity is about the feature value (+/−), not about markedness. In Set 1 languages, u[+FEM] is the arbitrary gender; in Set 2, u[−FEM] is. Neither polarity is inherently "marked."

• pos : Polarity
• neg : Polarity

instance Morphology.DM.instDecidableEqPolarity : DecidableEq Polarity

Equations

• Morphology.DM.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.instBEqPolarity.beq : Polarity → Polarity → Bool

Equations

• Morphology.DM.instBEqPolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Morphology.DM.instBEqPolarity : BEq Polarity

Equations

• Morphology.DM.instBEqPolarity = { beq := Morphology.DM.instBEqPolarity.beq }

instance Morphology.DM.instReprPolarity : Repr Polarity

Equations

• Morphology.DM.instReprPolarity = { reprPrec := Morphology.DM.instReprPolarity.repr }

def Morphology.DM.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

structure Morphology.DM.GenderVal : Type

A gender feature value: a dimension (what kind of feature) combined with a polarity (positive or negative).

Examples:

• ⟨.fem, .pos⟩ = [+FEM] (female, as in Amharic innat 'mother')
• ⟨.fem, .neg⟩ = [−FEM] (male, as in Amharic abbat 'father')
• ⟨.anim, .pos⟩ = [+ANIM] (animate, as in Teop body-part nouns)
• ⟨.masc, .pos⟩ = [+MASC] (masculine, as in Jarawara)

• dim : GenderDimension
• pol : Polarity

instance Morphology.DM.instDecidableEqGenderVal : DecidableEq GenderVal

Equations

• Morphology.DM.instDecidableEqGenderVal = Morphology.DM.instDecidableEqGenderVal.decEq

def Morphology.DM.instDecidableEqGenderVal.decEq (x✝ x✝¹ : GenderVal) : Decidable (x✝ = x✝¹)

Equations

• Morphology.DM.instDecidableEqGenderVal.decEq { dim := a, pol := a_1 } { dim := b, pol := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Morphology.DM.instBEqGenderVal.beq : GenderVal → GenderVal → Bool

Equations

• Morphology.DM.instBEqGenderVal.beq { dim := a, pol := a_1 } { dim := b, pol := b_1 } = (a == b && a_1 == b_1)
• Morphology.DM.instBEqGenderVal.beq x✝¹ x✝ = false

instance Morphology.DM.instBEqGenderVal : BEq GenderVal

Equations

• Morphology.DM.instBEqGenderVal = { beq := Morphology.DM.instBEqGenderVal.beq }

def Morphology.DM.instReprGenderVal.repr : GenderVal → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprGenderVal : Repr GenderVal

Equations

• Morphology.DM.instReprGenderVal = { reprPrec := Morphology.DM.instReprGenderVal.repr }

inductive Morphology.DM.Interpretability : Type

Feature interpretability (@cite{kramer-2015} §3.4.2).

• Interpretable (natural gender): legible at LF, restricts the denotation to male/female referents. Licensed by Encyclopedia (List 3).
• Uninterpretable (arbitrary gender): invisible at LF, visible only at PF. Licensed by Vocabulary Insertion (List 2).

• i : Interpretability
• u : Interpretability

instance Morphology.DM.instDecidableEqInterpretability : DecidableEq Interpretability

Equations

• Morphology.DM.instDecidableEqInterpretability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.instBEqInterpretability.beq : Interpretability → Interpretability → Bool

Equations

• Morphology.DM.instBEqInterpretability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Morphology.DM.instBEqInterpretability : BEq Interpretability

Equations

• Morphology.DM.instBEqInterpretability = { beq := Morphology.DM.instBEqInterpretability.beq }

def Morphology.DM.instReprInterpretability.repr : Interpretability → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprInterpretability : Repr Interpretability

Equations

• Morphology.DM.instReprInterpretability = { reprPrec := Morphology.DM.instReprInterpretability.repr }

structure Morphology.DM.GenderFeature : Type

A gender feature annotated for interpretability.

@cite{kramer-2015} Ch 3 identifies four attested combinations on n (per dimension):

• i[+VAL]: natural gender, positive polarity (e.g. female)
• i[−VAL]: natural gender, negative polarity (e.g. male)
• u[+VAL]: arbitrary gender, positive polarity (Set 1: Amharic, Spanish)
• u[−VAL]: arbitrary gender, negative polarity (Set 2: Maa, Wari')

A fifth option is plain n with no gender feature at all (the default).

• interp : Interpretability
• val : GenderVal

instance Morphology.DM.instDecidableEqGenderFeature : DecidableEq GenderFeature

Equations

• Morphology.DM.instDecidableEqGenderFeature = Morphology.DM.instDecidableEqGenderFeature.decEq

def Morphology.DM.instDecidableEqGenderFeature.decEq (x✝ x✝¹ : GenderFeature) : Decidable (x✝ = x✝¹)

Equations

• Morphology.DM.instDecidableEqGenderFeature.decEq { interp := a, val := a_1 } { interp := b, val := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Morphology.DM.instBEqGenderFeature : BEq GenderFeature

Equations

• Morphology.DM.instBEqGenderFeature = { beq := Morphology.DM.instBEqGenderFeature.beq }

def Morphology.DM.instBEqGenderFeature.beq : GenderFeature → GenderFeature → Bool

Equations

• Morphology.DM.instBEqGenderFeature.beq { interp := a, val := a_1 } { interp := b, val := b_1 } = (a == b && a_1 == b_1)
• Morphology.DM.instBEqGenderFeature.beq x✝¹ x✝ = false

def Morphology.DM.instReprGenderFeature.repr : GenderFeature → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprGenderFeature : Repr GenderFeature

Equations

• Morphology.DM.instReprGenderFeature = { reprPrec := Morphology.DM.instReprGenderFeature.repr }

def Morphology.DM.GenderFeature.isNatural : GenderFeature → Bool

Whether a gender feature is interpretable (natural).

Equations

• { interp := Morphology.DM.Interpretability.i, val := val }.isNatural = true
• { interp := Morphology.DM.Interpretability.u, val := val }.isNatural = false

def Morphology.DM.GenderFeature.isArbitrary : GenderFeature → Bool

Whether a gender feature is uninterpretable (arbitrary).

Equations

• { interp := Morphology.DM.Interpretability.i, val := val }.isArbitrary = false
• { interp := Morphology.DM.Interpretability.u, val := val }.isArbitrary = true

inductive Morphology.DM.NumberOnN : Type

Number feature on the n head (@cite{kramer-2015} §3.5).

Split plurality: irregular plurals are marked on n (within the categorization domain), while regular plurals are marked on Num (outside nP). Only irregular number lives on the categorizer.

• sg : NumberOnN
• pl : NumberOnN

instance Morphology.DM.instDecidableEqNumberOnN : DecidableEq NumberOnN

Equations

• Morphology.DM.instDecidableEqNumberOnN x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Morphology.DM.instBEqNumberOnN : BEq NumberOnN

Equations

• Morphology.DM.instBEqNumberOnN = { beq := Morphology.DM.instBEqNumberOnN.beq }

def Morphology.DM.instBEqNumberOnN.beq : NumberOnN → NumberOnN → Bool

Equations

• Morphology.DM.instBEqNumberOnN.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Morphology.DM.instReprNumberOnN.repr : NumberOnN → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprNumberOnN : Repr NumberOnN

Equations

• Morphology.DM.instReprNumberOnN = { reprPrec := Morphology.DM.instReprNumberOnN.repr }

structure Morphology.DM.PhiBundle : Type

Phi-features hosted on a categorizing head.

Following @cite{kramer-2015} Ch 3, the n head is the locus of gender features and (for irregular nouns) number features. The v and a heads do not host phi-features in the standard analysis.

• gender : Option GenderFeature
• number : Option NumberOnN

instance Morphology.DM.instDecidableEqPhiBundle : DecidableEq PhiBundle

Equations

• Morphology.DM.instDecidableEqPhiBundle = Morphology.DM.instDecidableEqPhiBundle.decEq

def Morphology.DM.instDecidableEqPhiBundle.decEq (x✝ x✝¹ : PhiBundle) : Decidable (x✝ = x✝¹)

Equations

• Morphology.DM.instDecidableEqPhiBundle.decEq { gender := a, number := a_1 } { gender := b, number := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Morphology.DM.instBEqPhiBundle.beq : PhiBundle → PhiBundle → Bool

Equations

• Morphology.DM.instBEqPhiBundle.beq { gender := a, number := a_1 } { gender := b, number := b_1 } = (a == b && a_1 == b_1)
• Morphology.DM.instBEqPhiBundle.beq x✝¹ x✝ = false

instance Morphology.DM.instBEqPhiBundle : BEq PhiBundle

Equations

• Morphology.DM.instBEqPhiBundle = { beq := Morphology.DM.instBEqPhiBundle.beq }

instance Morphology.DM.instReprPhiBundle : Repr PhiBundle

Equations

• Morphology.DM.instReprPhiBundle = { reprPrec := Morphology.DM.instReprPhiBundle.repr }

def Morphology.DM.instReprPhiBundle.repr : PhiBundle → ℕ → Std.Format

Equations

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

instance Morphology.DM.instInhabitedPhiBundle : Inhabited PhiBundle

Equations

• Morphology.DM.instInhabitedPhiBundle = { default := { } }

structure Morphology.DM.CatHead : Type

A categorizing head enriched with phi-features and selectional properties.

This extends the basic three-way Categorizer distinction with the feature content that @cite{kramer-2015} argues sits on the categorizer head. For n heads, this includes gender and (for irregular nouns) number. For v and a heads, the phi-bundle is typically empty.

The selectsD field captures the selectional feature {D} from @cite{adamson-2024} (following Myler 2016): when true, the n head creates a specifier position for an iPossessor DP in Spec,nP.

• cat : Categorizer
• phi : PhiBundle
• selectsD : Bool

instance Morphology.DM.instDecidableEqCatHead : DecidableEq CatHead

Equations

• Morphology.DM.instDecidableEqCatHead = Morphology.DM.instDecidableEqCatHead.decEq

def Morphology.DM.instDecidableEqCatHead.decEq (x✝ x✝¹ : CatHead) : Decidable (x✝ = x✝¹)

Equations

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

instance Morphology.DM.instBEqCatHead : BEq CatHead

Equations

• Morphology.DM.instBEqCatHead = { beq := Morphology.DM.instBEqCatHead.beq }

def Morphology.DM.instBEqCatHead.beq : CatHead → CatHead → Bool

Equations

• Morphology.DM.instBEqCatHead.beq { cat := a, phi := a_1, selectsD := a_2 } { cat := b, phi := b_1, selectsD := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Morphology.DM.instBEqCatHead.beq x✝¹ x✝ = false

def Morphology.DM.instReprCatHead.repr : CatHead → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprCatHead : Repr CatHead

Equations

• Morphology.DM.instReprCatHead = { reprPrec := Morphology.DM.instReprCatHead.repr }

def Morphology.DM.CatHead.toCategory (ch : CatHead) : Minimalism.Cat

The syntactic category of a phi-enriched categorizer head.

Equations

• ch.toCategory = ch.cat.toCategory

def Morphology.DM.CatHead.iPoss (phi : PhiBundle := { }) : CatHead

An iPossessable n head: has {D} (selectsD = true) by construction. Use this for any n that licenses an iPossessor in Spec,nP. The phi-bundle determines gender; selectsD is not a free parameter.

Examples:

• Teop body-part n: .iPoss { gender := some ⟨.u, ⟨.anim, .pos⟩⟩ }
• Jarawara iPossessable n: .iPoss (no gender feature → feminine)
• Inherited-gender n: .iPoss (gender comes from iPossessor via Agree)

Equations

• Morphology.DM.CatHead.iPoss phi = { cat := Morphology.DM.Categorizer.n, phi := phi, selectsD := true }

theorem Morphology.DM.CatHead.iPoss_selectsD (phi : PhiBundle) : (iPoss phi).selectsD = true

iPossessable n-heads always have selectsD = true, by construction.

FEM dimension (Amharic, Spanish, Romance; @cite{kramer-2015} Chs 3, 6)

def Morphology.DM.CatHead.n_iFem : CatHead

n with interpretable [+FEM]: female natural gender. Examples: Amharic -it suffix on animate female nouns.

Equations

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

def Morphology.DM.CatHead.n_iMasc : CatHead

n with interpretable [−FEM]: male natural gender. Examples: Amharic animate male nouns.

Note: iMasc is a mnemonic for the gender this n yields (masculine), not the feature dimension. The feature is i[−FEM] — negative polarity in the FEM dimension. For the separate MASC dimension used in Jarawara (@cite{adamson-2024}), see n_uMasc.

Equations

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

def Morphology.DM.CatHead.n_plain : CatHead

Plain n: no gender feature. Default nominal categorizer. Examples: inanimate nouns with no gender marking.

Equations

• Morphology.DM.CatHead.n_plain = { cat := Morphology.DM.Categorizer.n }

def Morphology.DM.CatHead.n_uFem : CatHead

n with uninterpretable [+FEM]: feminine arbitrary gender. Examples: Amharic nouns arbitrarily assigned to feminine class (door, lip, sun, ear, eye). In Set 1 languages (@cite{kramer-2015} Chs 5-6), the u-feature has positive polarity, making feminine the arbitrary gender and masculine the default. Languages: Amharic, Spanish.

Equations

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

def Morphology.DM.CatHead.n_uNegFem : CatHead

n with uninterpretable [−FEM]: masculine arbitrary gender in the FEM dimension. In Set 2 languages (@cite{kramer-2015} Ch 6), the u-feature has negative polarity, making masculine the arbitrary gender and feminine the default. Languages: Maa, Wari' (@cite{kramer-2015} Chs 6-7).

Equations

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

theorem Morphology.DM.u_fem_polarity_contrast : CatHead.n_uFem ≠ CatHead.n_uNegFem

u[+FEM] and u[−FEM] are distinct n heads: Set 1 vs Set 2.

ANIM dimension (Teop, Algonquian, Lealao Chinantec;

@cite{kramer-2015} Chs 5-6; @cite{adamson-2024} §3.1) 

def Morphology.DM.CatHead.n_iAnim : CatHead

n with interpretable [+ANIM]: animate natural gender. Examples: Teop gender I nouns (article a).

Equations

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

def Morphology.DM.CatHead.n_iInanim : CatHead

n with interpretable [−ANIM]: inanimate natural gender. Examples: Teop gender II nouns (article o).

Equations

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

def Morphology.DM.CatHead.n_uAnim : CatHead

n with uninterpretable [+ANIM]: animate arbitrary gender. Examples: Teop body-part n when iPossessed (@cite{adamson-2024} §3.1).

Equations

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

MASC dimension (Jarawara; @cite{adamson-2024} §3.2)

Note: Maa uses the FEM dimension (Set 2: u[−FEM]), not the MASC
dimension. The MASC dimension is used only by Jarawara in our
current coverage (@cite{adamson-2024} §3.2). 

def Morphology.DM.CatHead.n_uMasc : CatHead

n with uninterpretable [+MASC]: masculine arbitrary gender. In Jarawara, masculine is the marked gender; feminine is unmarked (plain n).

Equations

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

def Morphology.DM.CatHead.v_plain : CatHead

Verbal categorizer (no phi-features).

Equations

• Morphology.DM.CatHead.v_plain = { cat := Morphology.DM.Categorizer.v }

def Morphology.DM.CatHead.a_plain : CatHead

Adjectival categorizer (no phi-features).

Equations

• Morphology.DM.CatHead.a_plain = { cat := Morphology.DM.Categorizer.a }

inductive Morphology.DM.LicensingType : Type

Two types of root–n licensing condition (@cite{kramer-2015} §3.4.1).

• Semantic licensing (Encyclopedia / List 3): restricts interpretation. A root with a female natural gender referent must combine with n i[+FEM] because the Encyclopedia entry is only defined in that context.
• Arbitrary licensing (PF / List 2): restricts exponence. A root is listed in a VI rule's context as requiring [+FEM] on n, even though there is no semantic motivation.

• semantic : LicensingType
• arbitrary : LicensingType

instance Morphology.DM.instDecidableEqLicensingType : DecidableEq LicensingType

Equations

• Morphology.DM.instDecidableEqLicensingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.instBEqLicensingType.beq : LicensingType → LicensingType → Bool

Equations

• Morphology.DM.instBEqLicensingType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Morphology.DM.instBEqLicensingType : BEq LicensingType

Equations

• Morphology.DM.instBEqLicensingType = { beq := Morphology.DM.instBEqLicensingType.beq }

instance Morphology.DM.instReprLicensingType : Repr LicensingType

Equations

• Morphology.DM.instReprLicensingType = { reprPrec := Morphology.DM.instReprLicensingType.repr }

def Morphology.DM.instReprLicensingType.repr : LicensingType → ℕ → Std.Format

Equations

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

structure Morphology.DM.RootLicense (RootIdx : Type) : Type

A root–n licensing condition: specifies that a particular root (identified by index) is licensed to combine with an n head bearing specific features, and the type of licensing (semantic or arbitrary).

• rootIdx : RootIdx
• requiredGender : Option GenderFeature
• licensingType : LicensingType

def Morphology.DM.CatHead.satisfiesLicense (ch : CatHead) (req : Option GenderFeature) : Bool

Whether a CatHead satisfies a licensing condition's gender requirement.

Equations

• ch.satisfiesLicense none = ch.phi.gender.isNone
• ch.satisfiesLicense (some gf) = (ch.phi.gender == some gf)

theorem Morphology.DM.four_n_types_are_nominal : CatHead.n_iFem.cat = Categorizer.n ∧ CatHead.n_iMasc.cat = Categorizer.n ∧ CatHead.n_plain.cat = Categorizer.n ∧ CatHead.n_uFem.cat = Categorizer.n

All four Amharic n types are nominal categorizers.

theorem Morphology.DM.four_n_types_distinct : CatHead.n_iFem ≠ CatHead.n_iMasc ∧ CatHead.n_iFem ≠ CatHead.n_plain ∧ CatHead.n_iFem ≠ CatHead.n_uFem ∧ CatHead.n_iMasc ≠ CatHead.n_plain ∧ CatHead.n_iMasc ≠ CatHead.n_uFem ∧ CatHead.n_plain ≠ CatHead.n_uFem

The four Amharic n types are pairwise distinct.

theorem Morphology.DM.natural_gender_interpretable : { interp := Interpretability.i, val := { dim := GenderDimension.fem, pol := Polarity.pos } }.isNatural = true ∧ { interp := Interpretability.i, val := { dim := GenderDimension.fem, pol := Polarity.neg } }.isNatural = true

Natural gender features are interpretable.

theorem Morphology.DM.arbitrary_gender_uninterpretable : { interp := Interpretability.u, val := { dim := GenderDimension.fem, pol := Polarity.pos } }.isArbitrary = true

Arbitrary gender features are uninterpretable.

theorem Morphology.DM.plain_n_no_gender : CatHead.n_plain.phi.gender = none

Plain n has no gender feature — it is the default/unmarked case.

theorem Morphology.DM.natural_arbitrary_exclusive (gf : GenderFeature) : ¬(gf.isNatural = true ∧ gf.isArbitrary = true)

Natural and arbitrary gender are mutually exclusive on any feature.

def Morphology.DM.GenderFeature.licensingType : GenderFeature → LicensingType

Interpretable gender is semantically licensed; uninterpretable gender is arbitrarily licensed (@cite{kramer-2015} §3.4.1).

Equations

• { interp := Morphology.DM.Interpretability.i, val := val }.licensingType = Morphology.DM.LicensingType.semantic
• { interp := Morphology.DM.Interpretability.u, val := val }.licensingType = Morphology.DM.LicensingType.arbitrary

theorem Morphology.DM.natural_semantic_licensing (gf : GenderFeature) (h : gf.isNatural = true) : gf.licensingType = LicensingType.semantic

Natural gender → semantic licensing.

theorem Morphology.DM.arbitrary_arbitrary_licensing (gf : GenderFeature) (h : gf.isArbitrary = true) : gf.licensingType = LicensingType.arbitrary

Arbitrary gender → arbitrary licensing.

def Morphology.DM.GenderVal.toNat : GenderVal → ℕ

Canonical encoding of gender values as natural numbers for the Minimalism PhiFeature.gender constructor. Each dimension × polarity pair maps to a unique Nat.

Equations

• { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos }.toNat = 0
• { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg }.toNat = 1
• { dim := Morphology.DM.GenderDimension.masc, pol := Morphology.DM.Polarity.pos }.toNat = 2
• { dim := Morphology.DM.GenderDimension.masc, pol := Morphology.DM.Polarity.neg }.toNat = 3
• { dim := Morphology.DM.GenderDimension.anim, pol := Morphology.DM.Polarity.pos }.toNat = 4
• { dim := Morphology.DM.GenderDimension.anim, pol := Morphology.DM.Polarity.neg }.toNat = 5

theorem Morphology.DM.genderVal_toNat_injective (v1 v2 : GenderVal) (h : v1.toNat = v2.toNat) : v1 = v2

The encoding is injective: distinct gender values get distinct Nats.

def Morphology.DM.GenderFeature.toPhiFeature (gf : GenderFeature) : Minimalism.PhiFeature

Map a DM gender feature to a Minimalist phi-feature.

Equations

• gf.toPhiFeature = Minimalism.PhiFeature.gender gf.val.toNat

def Morphology.DM.GenderFeature.toGramFeature (gf : GenderFeature) : Minimalism.GramFeature

Map a DM gender feature to a valued or unvalued grammatical feature, determined by interpretability: interpretable gender is valued (legible at LF), uninterpretable gender is unvalued (probe).

Equations

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

theorem Morphology.DM.interpretable_gender_valued (gf : GenderFeature) (h : gf.interp = Interpretability.i) : gf.toGramFeature = Minimalism.GramFeature.valued (Minimalism.FeatureVal.phi (Minimalism.PhiFeature.gender gf.val.toNat))

Interpretable gender maps to a valued feature.

theorem Morphology.DM.uninterpretable_gender_unvalued (gf : GenderFeature) (h : gf.interp = Interpretability.u) : gf.toGramFeature = Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.phi (Minimalism.PhiFeature.gender gf.val.toNat))

Uninterpretable gender maps to an unvalued feature.

theorem Morphology.DM.n_iFem_valued : { interp := Interpretability.i, val := { dim := GenderDimension.fem, pol := Polarity.pos } }.toGramFeature = Minimalism.GramFeature.valued (Minimalism.FeatureVal.phi (Minimalism.PhiFeature.gender 0))

Amharic n i[+FEM] produces a valued gender feature.

theorem Morphology.DM.n_uFem_unvalued : { interp := Interpretability.u, val := { dim := GenderDimension.fem, pol := Polarity.pos } }.toGramFeature = Minimalism.GramFeature.unvalued (Minimalism.FeatureVal.phi (Minimalism.PhiFeature.gender 0))

Amharic n u[+FEM] produces an unvalued gender feature (probe).

Cross-dimensional verification

theorem Morphology.DM.anim_n_types_distinct : CatHead.n_iAnim ≠ CatHead.n_iFem ∧ CatHead.n_iAnim ≠ CatHead.n_iMasc ∧ CatHead.n_uAnim ≠ CatHead.n_uFem

Animacy-dimension n types are distinct from FEM-dimension types.

theorem Morphology.DM.anim_not_plain : CatHead.n_iAnim ≠ CatHead.n_plain ∧ CatHead.n_uAnim ≠ CatHead.n_plain

Animacy-dimension n types are distinct from plain n.

inductive Morphology.DM.ImpoverishmentContext : Type

A morphosyntactic context that can trigger impoverishment.

@cite{adamson-2024} ex. 63: [MASC] → ∅ in context of [PL] or [PARTICIPANT]. Each context is a separate impoverishment rule.

• plural : ImpoverishmentContext
• participant : ImpoverishmentContext

instance Morphology.DM.instDecidableEqImpoverishmentContext : DecidableEq ImpoverishmentContext

Equations

• Morphology.DM.instDecidableEqImpoverishmentContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DM.instBEqImpoverishmentContext.beq : ImpoverishmentContext → ImpoverishmentContext → Bool

Equations

• Morphology.DM.instBEqImpoverishmentContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Morphology.DM.instBEqImpoverishmentContext : BEq ImpoverishmentContext

Equations

• Morphology.DM.instBEqImpoverishmentContext = { beq := Morphology.DM.instBEqImpoverishmentContext.beq }

def Morphology.DM.instReprImpoverishmentContext.repr : ImpoverishmentContext → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprImpoverishmentContext : Repr ImpoverishmentContext

Equations

• Morphology.DM.instReprImpoverishmentContext = { reprPrec := Morphology.DM.instReprImpoverishmentContext.repr }

structure Morphology.DM.ImpoverishmentRule : Type

Impoverishment: postsyntactic deletion of morphosyntactic features.

In DM, impoverishment rules apply after syntax but before Vocabulary Insertion, deleting features from terminal nodes. This can neutralize gender distinctions in certain contexts.

@cite{adamson-2024} ex. 63: Jarawara [MASC] → ∅ in the context of [PL] or [PARTICIPANT].

• targetGender : GenderVal

  The feature to be deleted.

• context : ImpoverishmentContext

  The conditioning context (feature that triggers deletion).

instance Morphology.DM.instDecidableEqImpoverishmentRule : DecidableEq ImpoverishmentRule

Equations

• Morphology.DM.instDecidableEqImpoverishmentRule = Morphology.DM.instDecidableEqImpoverishmentRule.decEq

def Morphology.DM.instDecidableEqImpoverishmentRule.decEq (x✝ x✝¹ : ImpoverishmentRule) : Decidable (x✝ = x✝¹)

Equations

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

def Morphology.DM.instBEqImpoverishmentRule.beq : ImpoverishmentRule → ImpoverishmentRule → Bool

Equations

• Morphology.DM.instBEqImpoverishmentRule.beq { targetGender := a, context := a_1 } { targetGender := b, context := b_1 } = (a == b && a_1 == b_1)
• Morphology.DM.instBEqImpoverishmentRule.beq x✝¹ x✝ = false

instance Morphology.DM.instBEqImpoverishmentRule : BEq ImpoverishmentRule

Equations

• Morphology.DM.instBEqImpoverishmentRule = { beq := Morphology.DM.instBEqImpoverishmentRule.beq }

instance Morphology.DM.instReprImpoverishmentRule : Repr ImpoverishmentRule

Equations

• Morphology.DM.instReprImpoverishmentRule = { reprPrec := Morphology.DM.instReprImpoverishmentRule.repr }

def Morphology.DM.instReprImpoverishmentRule.repr : ImpoverishmentRule → ℕ → Std.Format

Equations

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

def Morphology.DM.ImpoverishmentRule.apply (rule : ImpoverishmentRule) (phi : PhiBundle) (contextActive : Bool) : PhiBundle

Apply impoverishment: if the rule matches, delete the gender feature.

Equations

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

structure Morphology.DM.CategorizedRoot : Type

A root that has been merged with a categorizing head, yielding a syntactically projectable unit (@cite{harley-2014} §2).

• root : Root

  The acategorial root (arity, change-type, etc.)

• categorizer : Categorizer

  The categorizing head that gives it syntactic category

def Morphology.DM.instBEqCategorizedRoot.beq : CategorizedRoot → CategorizedRoot → Bool

Equations

• Morphology.DM.instBEqCategorizedRoot.beq { root := a, categorizer := a_1 } { root := b, categorizer := b_1 } = (a == b && a_1 == b_1)
• Morphology.DM.instBEqCategorizedRoot.beq x✝¹ x✝ = false

instance Morphology.DM.instBEqCategorizedRoot : BEq CategorizedRoot

Equations

• Morphology.DM.instBEqCategorizedRoot = { beq := Morphology.DM.instBEqCategorizedRoot.beq }

instance Morphology.DM.instReprCategorizedRoot : Repr CategorizedRoot

Equations

• Morphology.DM.instReprCategorizedRoot = { reprPrec := Morphology.DM.instReprCategorizedRoot.repr }

def Morphology.DM.instReprCategorizedRoot.repr : CategorizedRoot → ℕ → Std.Format

Equations

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

def Morphology.DM.CategorizedRoot.category (cr : CategorizedRoot) : Minimalism.Cat

The syntactic category of a categorized root, derived from its categorizer.

Equations

• cr.category = cr.categorizer.toCategory

theorem Morphology.DM.same_root_different_category (r : Root) (c1 c2 : Categorizer) (h : c1 ≠ c2) : { root := r, categorizer := c1 }.category ≠ { root := r, categorizer := c2 }.category

Same root + different categorizer → different syntactic category. This is the formal content of the claim that √HAMMER can surface as either a noun (hammer) or a verb (to hammer) — same root, different category, determined entirely by the categorizer (@cite{harley-2014} §2).

theorem Morphology.DM.complement_selection_at_root_level (r : Root) (c1 c2 : Categorizer) : { root := r, categorizer := c1 }.root.arity = { root := r, categorizer := c2 }.root.arity

Complement selection is a root-level property, not contributed by the categorizer (@cite{harley-2014} §3). Evidence:

1. one-replacement in argument structure nominals: "the proud owner of a large dog" → "the proud one" — one replaces nP including √OWN + complement, showing the root took its complement directly.
2. Verb-object idioms: kick the bucket — √KICK selects the bucket directly under vP, not via mediation by v.
3. Hiaki suppletive verbs: suppletive forms are conditioned by the root's complement (singular vs. plural object), showing locality between root and argument below the categorizer.

In our formalization, RootArity.selectsTheme captures this: the root obligatorily selects an internal argument at the root level, and this persists regardless of which categorizer it merges with.

theorem Morphology.DM.theme_selecting_root_always_selects (r : Root) (c : Categorizer) (h : r.arity = RootArity.selectsTheme) : { root := r, categorizer := c }.root.arity.hasInternalArg = true

A theme-selecting root maintains its complement requirement regardless of whether it surfaces as a noun, verb, or adjective (@cite{harley-2014} §3).

inductive Morphology.DM.Recategorization : Type

Layered derivational morphology: a root categorized by one head can be further categorized by another, yielding derived forms. For example, √SHELF + n → shelf, then + v → to shelve (denominal verb).

Harley (2014 §4) uses multiply derived words (editor-ial, class-ifi-eds, national-ize) to argue that idiosyncratic interpretation can extend past the first categorizer — the phase boundary is at Voice, not at the inner categorizer.

• denominal : Recategorization
• deadjectival : Recategorization
• deverbal_n : Recategorization
• deverbal_a : Recategorization

instance Morphology.DM.instDecidableEqRecategorization : DecidableEq Recategorization

Equations

• Morphology.DM.instDecidableEqRecategorization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Morphology.DM.instBEqRecategorization : BEq Recategorization

Equations

• Morphology.DM.instBEqRecategorization = { beq := Morphology.DM.instBEqRecategorization.beq }

def Morphology.DM.instBEqRecategorization.beq : Recategorization → Recategorization → Bool

Equations

• Morphology.DM.instBEqRecategorization.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Morphology.DM.instReprRecategorization.repr : Recategorization → ℕ → Std.Format

Equations

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

instance Morphology.DM.instReprRecategorization : Repr Recategorization

Equations

• Morphology.DM.instReprRecategorization = { reprPrec := Morphology.DM.instReprRecategorization.repr }

def Morphology.DM.Recategorization.source : Recategorization → Categorizer

The source categorizer of a re-categorization.

Equations

• Morphology.DM.Recategorization.denominal.source = Morphology.DM.Categorizer.n
• Morphology.DM.Recategorization.deadjectival.source = Morphology.DM.Categorizer.a
• Morphology.DM.Recategorization.deverbal_n.source = Morphology.DM.Categorizer.v
• Morphology.DM.Recategorization.deverbal_a.source = Morphology.DM.Categorizer.v

def Morphology.DM.Recategorization.target : Recategorization → Categorizer

The target categorizer of a re-categorization.

Equations

• Morphology.DM.Recategorization.denominal.target = Morphology.DM.Categorizer.v
• Morphology.DM.Recategorization.deadjectival.target = Morphology.DM.Categorizer.v
• Morphology.DM.Recategorization.deverbal_n.target = Morphology.DM.Categorizer.n
• Morphology.DM.Recategorization.deverbal_a.target = Morphology.DM.Categorizer.a

def Morphology.DM.CategorizedRoot.recategorize (cr : CategorizedRoot) (rc : Recategorization) : Option CategorizedRoot

Apply a re-categorization to a categorized root. Returns none if the root's current categorizer doesn't match the expected source.

Equations

• cr.recategorize rc = if cr.categorizer = rc.source then some { root := cr.root, categorizer := rc.target } else none

theorem Morphology.DM.denominal_requires_n (cr cr' : CategorizedRoot) (h : cr.recategorize Recategorization.denominal = some cr') : cr.categorizer = Categorizer.n

Denominal verbs start from n-categorized roots.

theorem Morphology.DM.recategorization_changes_category (cr : CategorizedRoot) (rc : Recategorization) (cr' : CategorizedRoot) (h : cr.recategorize rc = some cr') : cr'.categorizer = rc.target

Re-categorization yields the target categorizer.

theorem Morphology.DM.denominal_yields_verbal (r : Root) : ∃ (cr : CategorizedRoot), { root := r, categorizer := Categorizer.n }.recategorize Recategorization.denominal = some cr ∧ cr.category = Minimalism.Cat.V

A denominal verb and a directly verbal root yield the same syntactic category (V), but have different internal structure. √HAMMER + v gives V directly; √HAMMER + n + v also gives V but via layered derivation. This structural ambiguity is invisible at the category level (@cite{harley-2014} §2).

theorem Morphology.DM.deadjectival_source_target : Recategorization.deadjectival.source = Categorizer.a ∧ Recategorization.deadjectival.target = Categorizer.v

Deadjectival derivation (a → v) connects to @cite{embick-2004}'s resultStative structure: what RootTypology calls AdjectivalStructure.resultStative is, in DM terms, a root first categorized by a, then further categorized by v.

def Morphology.DM.Categorizer.isPhaseHead : Categorizer → Bool

Categorizers are never phase heads (@cite{harley-2014} §4).

Equations

• x✝.isPhaseHead = false

theorem Morphology.DM.categorizer_never_phase (c : Categorizer) : c.isPhaseHead = false

No categorizer is a phase head (@cite{harley-2014} §4).

theorem Morphology.DM.agentive_voice_is_phase : Minimalism.voiceAgent.phaseHead = true

Agentive Voice IS a phase head — it demarcates the boundary above which interpretation must be compositional (@cite{harley-2014} §4).

theorem Morphology.DM.phase_boundary_at_voice_not_categorizer (c : Categorizer) : c.isPhaseHead = false ∧ Minimalism.voiceAgent.phaseHead = true

The phase-boundary asymmetry: Voice can be a phase head while categorizers never are. This is why idiosyncratic interpretation extends past categorizers but not past Voice (@cite{harley-2014} §4).

theorem Morphology.DM.voice_introduces_external_arg : Minimalism.voiceAgent.hasD = true ∧ Minimalism.voiceAgent.assignsTheta = true

Voice introduces the external argument (@cite{harley-2014} §4, following @cite{kratzer-1996}). The categorizer does NOT introduce arguments — complement selection is a root property (§3).