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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqCategorizer : DecidableEq Categorizer

Equations

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

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

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprCategorizer : Repr Categorizer

Equations

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

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

Map a categorizer to its syntactic category.

Equations

• Morphology.DM.Categorizer.n.toCategory = Minimalist.Cat.N
• Morphology.DM.Categorizer.v.toCategory = Minimalist.Cat.V
• Morphology.DM.Categorizer.a.toCategory = Minimalist.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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqGenderDimension : DecidableEq GenderDimension

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqPolarity : DecidableEq Polarity

Equations

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

@[implicit_reducible]

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

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 ⋯

@[implicit_reducible]

instance Morphology.DM.instDecidableEqGenderVal : DecidableEq GenderVal

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprGenderVal : Repr GenderVal

Equations

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

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

Equations

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

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

@[implicit_reducible]

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.instReprInterpretability.repr : Interpretability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprInterpretability : Repr Interpretability

Equations

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

inductive Morphology.DM.Contrastivity : Type

Feature contrastivity (@cite{konnelly-cowper-2020} §4, following @cite{wiltschko-2008}).

Orthogonal to Interpretability. A feature can be both interpretable (visible at LF when present) and non-contrastive (its absence carries no semantic content).

• Contrastive: absence is meaningful — "not [F]" is distinct from having no specification. In a context where [F] could appear, its absence is interpreted as ¬F. Gender features at K&C Stage 1.
• NonContrastive: a modifier/adjunct whose presence adds meaning but whose absence is vacuous — it simply doesn't restrict the denotation. Gender features at K&C Stage 3.

• contrastive : Contrastivity
• nonContrastive : Contrastivity

@[implicit_reducible]

instance Morphology.DM.instDecidableEqContrastivity : DecidableEq Contrastivity

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprContrastivity : Repr Contrastivity

Equations

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

def Morphology.DM.instReprContrastivity.repr : Contrastivity → ℕ → Std.Format

Equations

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

def Morphology.DM.Contrastivity.obligatory : Contrastivity → Bool

Whether a contrastive feature's presence is obligatory for referents with known values.

A contrastive feature whose absence is meaningful (¬F) must be present when the referent has a known value — otherwise absence would wrongly convey ¬F. A non-contrastive feature is an optional modifier whose absence is vacuous, so it need not be present even for known values.

@cite{wiltschko-2008}; applied to gender by @cite{konnelly-cowper-2020}.

Equations

• Morphology.DM.Contrastivity.contrastive.obligatory = true
• Morphology.DM.Contrastivity.nonContrastive.obligatory = false

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

@[implicit_reducible]

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 ⋯

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

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprGenderFeature : Repr GenderFeature

Equations

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

def Morphology.DM.GenderFeature.IsNatural (g : GenderFeature) : Prop

Whether a gender feature is interpretable (natural).

Equations

• g.IsNatural = (g.interp = Morphology.DM.Interpretability.i)

@[implicit_reducible]

instance Morphology.DM.instDecidablePredGenderFeatureIsNatural : DecidablePred GenderFeature.IsNatural

Equations

• Morphology.DM.instDecidablePredGenderFeatureIsNatural x✝ = Morphology.DM.instDecidablePredGenderFeatureIsNatural._aux_1 x✝

def Morphology.DM.GenderFeature.IsArbitrary (g : GenderFeature) : Prop

Whether a gender feature is uninterpretable (arbitrary).

Equations

• g.IsArbitrary = (g.interp = Morphology.DM.Interpretability.u)

@[implicit_reducible]

instance Morphology.DM.instDecidablePredGenderFeatureIsArbitrary : DecidablePred GenderFeature.IsArbitrary

Equations

• Morphology.DM.instDecidablePredGenderFeatureIsArbitrary x✝ = Morphology.DM.instDecidablePredGenderFeatureIsArbitrary._aux_1 x✝

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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqNumberOnN : DecidableEq NumberOnN

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprNumberOnN : Repr NumberOnN

Equations

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

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

Equations

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

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

@[implicit_reducible]

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 ⋯

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

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.

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

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprCatHead : Repr CatHead

Equations

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

def Morphology.DM.CatHead.toCategory (ch : CatHead) : Minimalist.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

@[implicit_reducible]

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.instReprLicensingType.repr : LicensingType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprLicensingType : Repr LicensingType

Equations

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

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)

def Morphology.DM.CatHead.licensesIntrusion (ch : CatHead) : Bool

Whether a categorizer head licenses templatic [t]-intrusion in the sense of @cite{faust-2026} (11). The intruder is the exponent of n[+gen] (Kramer's n_uFem and similar): only nominal categorizers bearing a gender feature can host the bound-root /t/ exponent (@cite{lowenstamm-2014} sister-bound-root analysis). Verbal stems are blocked because gender is realized on the higher Agr head (@cite{kramer-2020}; @cite{faust-2026} (11)).

The predicate is cat = .n ∧ phi.gender ≠ none. Used by Phonology.Templates.RootTemplateMatch.intrusionLicensed to filter RootTemplateMatch candidates with intruder-source associations.

Equations

• ch.licensesIntrusion = (decide (ch.cat = Morphology.DM.Categorizer.n) && ch.phi.gender.isSome)

Which canonical CatHeads license intrusion

Per-head verification of licensesIntrusion against Kramer's taxonomy. Each theorem breaks if the corresponding canonical CatHead's cat or phi.gender field ever changes — making the licensing predictions of @cite{faust-2026} (11) sensitive to the upstream Kramer-2015 data.

theorem Morphology.DM.n_uFem_licenses_intrusion : CatHead.n_uFem.licensesIntrusion = true

u[+FEM] n licenses intrusion (canonical Set 1 feminine — Hebrew /t/ exponent of taQTiL nouns, Amharic /t/ exponent of gerunds and INFs).

theorem Morphology.DM.n_iFem_licenses_intrusion : CatHead.n_iFem.licensesIntrusion = true

i[+FEM] n licenses intrusion (interpretable feminine).

theorem Morphology.DM.n_iMasc_licenses_intrusion : CatHead.n_iMasc.licensesIntrusion = true

i[−FEM] n licenses intrusion (interpretable masculine — Faust's argument is feature-symmetric: any [+gen] specification on n licenses an inherent exponent).

theorem Morphology.DM.n_plain_blocks_intrusion : CatHead.n_plain.licensesIntrusion = false

Plain n (no gender feature) does NOT license intrusion.

theorem Morphology.DM.v_plain_blocks_intrusion : CatHead.v_plain.licensesIntrusion = false

Verbal categorizer: never licenses intrusion (gender lives on Agr, not on v — @cite{faust-2026} (11)).

theorem Morphology.DM.a_plain_blocks_intrusion : CatHead.a_plain.licensesIntrusion = false

Adjectival categorizer: no inherent gender exponent.

theorem Morphology.DM.licensesIntrusion_iff_n_and_gen (ch : CatHead) : ch.licensesIntrusion = true ↔ ch.cat = Categorizer.n ∧ ch.phi.gender.isSome = true

Faust's central morphological prediction: intrusion is well-formed iff the categorizer is n AND carries a gender feature. The iff reduces to a Boolean computation on CatHead.cat and CatHead.phi.gender.

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 ∧ { interp := Interpretability.i, val := { dim := GenderDimension.fem, pol := Polarity.neg } }.IsNatural

Natural gender features are interpretable.

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

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 ∧ gf.IsArbitrary)

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) : gf.licensingType = LicensingType.semantic

Natural gender → semantic licensing.

theorem Morphology.DM.arbitrary_arbitrary_licensing (gf : GenderFeature) (h : gf.IsArbitrary) : 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) : Minimalist.PhiFeature

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

Equations

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

def Morphology.DM.GenderFeature.toGramFeature (gf : GenderFeature) : Minimalist.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 = Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.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 = Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.phi (Minimalist.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 = Minimalist.GramFeature.valued (Minimalist.FeatureVal.phi (Minimalist.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 = Minimalist.GramFeature.unvalued (Minimalist.FeatureVal.phi (Minimalist.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

@[implicit_reducible]

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.instReprImpoverishmentContext.repr : ImpoverishmentContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

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).

@[implicit_reducible]

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.

@[implicit_reducible]

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 : RootClassification

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

• categorizer : Categorizer

  The categorizing head that gives it syntactic category

@[implicit_reducible]

instance Morphology.DM.instBEqCategorizedRoot : BEq CategorizedRoot

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprCategorizedRoot : Repr CategorizedRoot

Equations

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

def Morphology.DM.CategorizedRoot.category (cr : CategorizedRoot) : Minimalist.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 : RootClassification) (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 : RootClassification) (c1 c2 : Categorizer) : { root := r, categorizer := c1 }.root.arity = { root := r, categorizer := c2 }.root.arity

Complement arity (c-selection) is a root-level property, not contributed by the categorizer (@cite{harley-2014} §3). The root determines whether it takes an internal argument (selectsTheme vs noTheme); the categorizer does not alter this.

Note: This theorem covers arity, not l-selection (which specific preposition heads the PP complement). @cite{hewett-2026} shows that l-selection in Semitic can vary by verbal template, falsifying any theory locating l-selection entirely at the root level. See Hewett2026.

Evidence for root-level arity:

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.

theorem Morphology.DM.theme_selecting_root_always_selects (r : RootClassification) (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

@[implicit_reducible]

instance Morphology.DM.instDecidableEqRecategorization : DecidableEq Recategorization

Equations

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

@[implicit_reducible]

instance Morphology.DM.instReprRecategorization : Repr Recategorization

Equations

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

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

Equations

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

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 : RootClassification) : ∃ (cr : CategorizedRoot), { root := r, categorizer := Categorizer.n }.recategorize Recategorization.denominal = some cr ∧ cr.category = Minimalist.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 : Minimalist.voiceAgent.IsPhasal

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 ∧ Minimalist.voiceAgent.IsPhasal

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 : Minimalist.voiceAgent.HasD ∧ Minimalist.voiceAgent.AssignsTheta

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).

The bridge between DM phi-features on n and descriptive SurfaceGender is mediated by Vocabulary Insertion (VI). Different VI systems yield different surface genders from the same underlying features.

Three VI patterns are attested (@cite{kramer-2015} Chs 5-7):

• Set 1 (Amharic, Spanish): [+FEM] → feminine, else → masculine (2 genders)
• Set 2 (Maa, Wari'): [−FEM] → masculine, else → feminine (2 genders)
• 3-gender (Russian, Mangarayi, Lavukaleve): [+FEM] → feminine, [−FEM] → masculine, no feature → neuter (3 genders)

For animacy-based systems (Teop, Algonquian), [+ANIM] → animate, [−ANIM]/none → inanimate (2 genders).

def Morphology.DM.CatHead.surfaceGenderSet1 (ch : CatHead) : Features.SurfaceGender

Set 1 VI: [+FEM] → feminine, else → masculine. Default gender: masculine (plain n has no [+FEM]). Languages: Amharic, Spanish. (@cite{kramer-2015} Ch 6)

Equations

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

def Morphology.DM.CatHead.surfaceGenderSet2 (ch : CatHead) : Features.SurfaceGender

Set 2 VI: [−FEM] → masculine, else → feminine. Default gender: feminine (plain n has no [−FEM]). Languages: Maa, Wari'. (@cite{kramer-2015} Ch 6)

Equations

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

def Morphology.DM.CatHead.surfaceGenderThree (ch : CatHead) : Features.SurfaceGender

Three-gender VI: [+FEM] → feminine, [−FEM] → masculine, none → neuter. Languages: Russian, Mangarayi, Lavukaleve. (@cite{kramer-2015} Ch 7)

Equations

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

def Morphology.DM.CatHead.surfaceGenderAnimacy (ch : CatHead) : Features.SurfaceGender

Animacy VI: [+ANIM] → animate, else → inanimate. Languages: Teop, Algonquian, Lealao Chinantec. (@cite{kramer-2015} Ch 5)

Equations

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

theorem Morphology.DM.set1_verification : CatHead.n_iFem.surfaceGenderSet1 = Features.SurfaceGender.feminine ∧ CatHead.n_iMasc.surfaceGenderSet1 = Features.SurfaceGender.masculine ∧ CatHead.n_uFem.surfaceGenderSet1 = Features.SurfaceGender.feminine ∧ CatHead.n_plain.surfaceGenderSet1 = Features.SurfaceGender.masculine

theorem Morphology.DM.set2_verification : CatHead.n_iFem.surfaceGenderSet2 = Features.SurfaceGender.feminine ∧ CatHead.n_iMasc.surfaceGenderSet2 = Features.SurfaceGender.masculine ∧ CatHead.n_uNegFem.surfaceGenderSet2 = Features.SurfaceGender.masculine ∧ CatHead.n_plain.surfaceGenderSet2 = Features.SurfaceGender.feminine

theorem Morphology.DM.three_gender_verification : CatHead.n_iFem.surfaceGenderThree = Features.SurfaceGender.feminine ∧ CatHead.n_iMasc.surfaceGenderThree = Features.SurfaceGender.masculine ∧ CatHead.n_uFem.surfaceGenderThree = Features.SurfaceGender.feminine ∧ CatHead.n_uNegFem.surfaceGenderThree = Features.SurfaceGender.masculine ∧ CatHead.n_plain.surfaceGenderThree = Features.SurfaceGender.neuter

theorem Morphology.DM.animacy_verification : CatHead.n_iAnim.surfaceGenderAnimacy = Features.SurfaceGender.animate ∧ CatHead.n_iInanim.surfaceGenderAnimacy = Features.SurfaceGender.inanimate ∧ CatHead.n_uAnim.surfaceGenderAnimacy = Features.SurfaceGender.animate ∧ CatHead.n_plain.surfaceGenderAnimacy = Features.SurfaceGender.inanimate

theorem Morphology.DM.set1_set2_default_contrast : CatHead.n_plain.surfaceGenderSet1 ≠ CatHead.n_plain.surfaceGenderSet2

Set 1 and Set 2 agree on natural gender (i[+FEM] → feminine, i[−FEM] → masculine) but differ on the default (plain n). @cite{kramer-2015} Ch 6: the polarity of u determines which gender is arbitrary vs default.

def Morphology.DM.CatHead.toGenderInfoSet1 (ch : CatHead) : Features.GenderInfo

Composed morphism: DM categorizer → discourse-level gender knowledge.

The chain CatHead → SurfaceGender → GenderInfo composes the structural mechanism (how gender is encoded on n) with the discourse layer (what participants know about a referent's gender). A noun whose categorizer head determines a surface gender always yields .known g at the discourse level.

This is parameterized over a VI schema (Set 1, Set 2, Three, Animacy) because the structural → surface mapping is language-specific.

Equations

• ch.toGenderInfoSet1 = ch.surfaceGenderSet1.toGenderInfo

def Morphology.DM.CatHead.toGenderInfoSet2 (ch : CatHead) : Features.GenderInfo

Equations

• ch.toGenderInfoSet2 = ch.surfaceGenderSet2.toGenderInfo

def Morphology.DM.CatHead.toGenderInfoThree (ch : CatHead) : Features.GenderInfo

Equations

• ch.toGenderInfoThree = ch.surfaceGenderThree.toGenderInfo

def Morphology.DM.CatHead.toGenderInfoAnimacy (ch : CatHead) : Features.GenderInfo

Equations

• ch.toGenderInfoAnimacy = ch.surfaceGenderAnimacy.toGenderInfo

theorem Morphology.DM.catHead_gender_always_known_set1 (ch : CatHead) : ∃ (g : Features.SurfaceGender), ch.toGenderInfoSet1 = Features.GenderInfo.known g

The composition always yields .known _ — a DM categorizer head always determines a concrete surface gender, so gender is never unspecified at the discourse level when the morphosyntax is fully resolved. Gender underspecification (@cite{arnold-2026}) arises from the discourse, not from the grammar.

theorem Morphology.DM.catHead_gender_always_known_three (ch : CatHead) : ∃ (g : Features.SurfaceGender), ch.toGenderInfoThree = Features.GenderInfo.known g