Kramer 2020: Grammatical Gender — A Close Look at Gender Assignment

@cite{kramer-2020} @cite{kramer-2015} @cite{corbett-1991} @cite{harris-1991}

Formalizes the core contributions of @cite{kramer-2020}, a review article that sharpens and extends @cite{kramer-2015}'s structural approach to gender assignment. Three main results:

1. The Semantic Core Generalization (ex. 2/28): every language with grammatical gender assigns gender semantically to at least some nouns, based on animacy, humanness, and/or social gender/biological sex.

2. Lexical vs structural gender assignment (§3): a comparison of @cite{harris-1991}'s lexical rules with @cite{kramer-2015}'s structural n-based approach, identifying three phenomena that differentiate them: phonological assignment (§3.3.1), hybrid nouns (§3.3.2), and the Semantic Core (§3.3.3).

3. Cross-linguistic variation in arbitrary assignment (Table 2): remainder nouns vary along two dimensions — same vs different gender(s), recycled vs novel vs both.

Integration

• Typology ↔ DM bridge: SemanticBasis.toGenderDimension connects the typological SemanticBasis (from Phenomena/Gender/Typology.lean) to the DM GenderDimension (from Theories/Morphology/DM/Categorizer.lean), making explicit that the semantic core properties are the same things parameterized as feature dimensions in the structural approach.

• DM → Minimalism bridge: GenderFeature.toGramFeature (in Categorizer.lean) maps DM gender features to Minimalist GramFeature, with interpretable gender → valued and uninterpretable → unvalued.

• Semantic Core verified: semantic_core_holds proves the generalization over the existing 21-language sample from Typology.lean.

The typological SemanticBasis and the DM GenderDimension describe the same underlying distinction from different perspectives: typology asks what semantic property organizes the system, while DM asks what binary feature sits on n. @cite{kramer-2020} makes this connection explicit by analyzing sex-based systems as [±FEM] or [±MASC], and animacy-based systems as [±ANIM].

The mapping is partial in two ways:

1. SemanticBasis.shape and .rationality have no standard DM feature dimension (no [±SHAPE] or [±RATIONAL] in the literature).

2. SemanticBasis.humanness maps to .anim because @cite{kramer-2015} does not posit a [±HUMAN] dimension — the closest is [±ANIM]. This is a limitation of the current DM feature inventory, not a claim that humanness is a subset of animacy (e.g. Akɔɔse distinguishes human vs nonhuman, which is orthogonal to animate vs inanimate).

def Typology.Gender.SemanticBasis.isCore : SemanticBasis → Bool

Whether a SemanticBasis falls within the semantic core.

@cite{kramer-2020} ex. 3 identifies three core properties; shape and rationality are additional semantic bases (§2.2.1) that go beyond the core but never constitute the only basis for a gender system.

Equations

• Typology.Gender.SemanticBasis.sex.isCore = true
• Typology.Gender.SemanticBasis.animacy.isCore = true
• Typology.Gender.SemanticBasis.humanness.isCore = true
• Typology.Gender.SemanticBasis.shape.isCore = false
• Typology.Gender.SemanticBasis.rationality.isCore = false

def Typology.Gender.GenderProfile.satisfiesSemanticCore (p : GenderProfile) : Bool

The Semantic Core Generalization: a gender profile satisfies it iff it either has no gender system, or at least one of its semantic bases falls within the core {animacy, humanness, social gender/sex}.

Equations

• p.satisfiesSemanticCore = (p.genderCount == Typology.Gender.GenderCount.none || p.semanticBases.any Typology.Gender.SemanticBasis.isCore)

def Typology.Gender.SemanticBasis.toGenderDimension : SemanticBasis → Option Morphology.DM.GenderDimension

Map a typological semantic basis to its corresponding DM gender dimension, when one exists. (@cite{kramer-2020} §3)

The .humanness → .anim mapping reflects a gap in @cite{kramer-2015}'s feature inventory: no [±HUMAN] dimension is posited, so humanness-based systems are approximated by [±ANIM].

Equations

• Typology.Gender.SemanticBasis.sex.toGenderDimension = some Morphology.DM.GenderDimension.fem
• Typology.Gender.SemanticBasis.animacy.toGenderDimension = some Morphology.DM.GenderDimension.anim
• Typology.Gender.SemanticBasis.humanness.toGenderDimension = some Morphology.DM.GenderDimension.anim
• Typology.Gender.SemanticBasis.shape.toGenderDimension = none
• Typology.Gender.SemanticBasis.rationality.toGenderDimension = none

def Morphology.DM.GenderDimension.toSemanticBasis : GenderDimension → Typology.Gender.SemanticBasis

Inverse direction: map a DM gender dimension to its typological basis. (@cite{kramer-2020} §3)

Equations

• Morphology.DM.GenderDimension.fem.toSemanticBasis = Typology.Gender.SemanticBasis.sex
• Morphology.DM.GenderDimension.masc.toSemanticBasis = Typology.Gender.SemanticBasis.sex
• Morphology.DM.GenderDimension.anim.toSemanticBasis = Typology.Gender.SemanticBasis.animacy

theorem Phenomena.Gender.Studies.Kramer2020.semantic_core_holds : (Corbett1991.allProfiles.all fun (x : Typology.Gender.GenderProfile) => x.satisfiesSemanticCore) = true

Semantic Core Generalization (@cite{kramer-2020} ex. 2/28): every language in the sample satisfies the semantic core.

theorem Phenomena.Gender.Studies.Kramer2020.no_gender_without_core : (Corbett1991.allProfiles.all fun (p : Typology.Gender.GenderProfile) => if (p.genderCount != Typology.Gender.GenderCount.none) = true then p.semanticBases.any Typology.Gender.SemanticBasis.isCore else true) = true

No language has gender without at least one core semantic basis.

theorem Phenomena.Gender.Studies.Kramer2020.core_properties_have_dimensions : Typology.Gender.SemanticBasis.sex.toGenderDimension.isSome = true ∧ Typology.Gender.SemanticBasis.animacy.toGenderDimension.isSome = true ∧ Typology.Gender.SemanticBasis.humanness.toGenderDimension.isSome = true

Core semantic properties correspond to DM feature dimensions: every core basis has a toGenderDimension target.

theorem Phenomena.Gender.Studies.Kramer2020.noncore_properties_no_dimension : Typology.Gender.SemanticBasis.shape.toGenderDimension.isNone = true ∧ Typology.Gender.SemanticBasis.rationality.toGenderDimension.isNone = true

Non-core properties lack a standard DM dimension.

theorem Phenomena.Gender.Studies.Kramer2020.roundtrip_sex_fem : Typology.Gender.SemanticBasis.sex.toGenderDimension = some Morphology.DM.GenderDimension.fem

Round-trip: .sex → .fem (the default parameterization).

theorem Phenomena.Gender.Studies.Kramer2020.roundtrip_anim : Morphology.DM.GenderDimension.anim.toSemanticBasis.toGenderDimension = some Morphology.DM.GenderDimension.anim

Round-trip: .anim → .animacy → .anim.

inductive Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource : Type

Whether remainder nouns use recycled genders, novel genders, or both. (@cite{kramer-2020} Table 2)

• recycled : RemainderGenderSource
• novel : RemainderGenderSource
• both : RemainderGenderSource

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderGenderSource : DecidableEq RemainderGenderSource

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderGenderSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource.repr : RemainderGenderSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource : Repr RemainderGenderSource

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource.repr }

structure Phenomena.Gender.Studies.Kramer2020.RemainderPattern : Type

How remainder nouns (those not assigned gender by the semantic core) are distributed across genders (@cite{kramer-2020} Table 2).

Two independent parameters:

1. Are all remainder nouns in the same gender, or spread across genders?
2. Is the remainder gender recycled, novel, or a mix of both?

• sameGender : Bool

  Are all remainder nouns assigned to a single gender?

• genderSource : RemainderGenderSource

  Source of the remainder gender(s).

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern : DecidableEq RemainderPattern

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern = Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern.decEq

def Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern.decEq (x✝ x✝¹ : RemainderPattern) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern.repr : RemainderPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern : Repr RemainderPattern

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern.repr }

def Phenomena.Gender.Studies.Kramer2020.dieri : RemainderPattern

Dieri (Pama-Nyungan): all remainder nouns are masculine (= same gender used for male humans). Same gender, recycled. (@cite{kramer-2020} Table 2)

Equations

• Phenomena.Gender.Studies.Kramer2020.dieri = { sameGender := true, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.recycled }

def Phenomena.Gender.Studies.Kramer2020.tamil : RemainderPattern

Tamil (Dravidian): remainder nouns go to neuter — a novel gender not used for the male/female semantic core. Same gender, novel. (@cite{kramer-2020} Table 2; Asher 1982)

Equations

• Phenomena.Gender.Studies.Kramer2020.tamil = { sameGender := true, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.novel }

def Phenomena.Gender.Studies.Kramer2020.spanishRemainder : RemainderPattern

Spanish: remainder nouns are split arbitrarily across masculine and feminine — both recycled genders. Different genders, recycled. (@cite{kramer-2020} Table 1, Table 2; @cite{harris-1991})

Equations

• Phenomena.Gender.Studies.Kramer2020.spanishRemainder = { sameGender := false, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.recycled }

def Phenomena.Gender.Studies.Kramer2020.akoose : RemainderPattern

Akɔɔse (Niger-Congo: Bantu): remainder nouns spread across at least 7 noun classes — novel genders. Different genders, novel. (@cite{kramer-2020} Table 2; Hedinger 2008)

Equations

• Phenomena.Gender.Studies.Kramer2020.akoose = { sameGender := false, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.novel }

def Phenomena.Gender.Studies.Kramer2020.blackfoot : RemainderPattern

Blackfoot (Algic: Algonquian): inanimate nouns are assigned either a novel inanimate gender or a recycled animate gender. Different genders, both recycled and novel. (@cite{kramer-2020} Table 2; Frantz 2017)

Equations

• Phenomena.Gender.Studies.Kramer2020.blackfoot = { sameGender := false, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.both }

theorem Phenomena.Gender.Studies.Kramer2020.table2_all_cells : dieri ≠ tamil ∧ dieri ≠ spanishRemainder ∧ dieri ≠ akoose ∧ dieri ≠ blackfoot ∧ tamil ≠ spanishRemainder ∧ tamil ≠ akoose ∧ tamil ≠ blackfoot ∧ spanishRemainder ≠ akoose ∧ spanishRemainder ≠ blackfoot ∧ akoose ≠ blackfoot

All five attested cells of Table 2 are distinct patterns.

@cite{kramer-2020} §3.2 contrasts two theoretical approaches:

Lexical (@cite{harris-1991}): gender assigned via lexical rules that map semantic features (e.g. [FEMALE]) to grammatical gender features (e.g. [F]). Each noun is listed with its gender feature in the lexicon. Gender is a property of the lexical entry.

Structural (@cite{kramer-2015}): gender is a phi-feature on the categorizing head n. A root combines with an n bearing gender features via syntactic Merge. Gender is a property of the syntactic structure.

Three phenomena differentiate them (§3.3):

1. Phonological gender assignment
2. Hybrid nouns (e.g. Russian vrač)
3. The Semantic Core Generalization

structure Phenomena.Gender.Studies.Kramer2020.LexicalGenderRule : Type

A lexical gender rule: maps a semantic feature to a grammatical gender feature in a specified context. (@cite{harris-1991})

The semanticBasis identifies which semantic property triggers the rule; targetDimension identifies which DM gender dimension is assigned; context describes the conditioning environment.

• semanticBasis : Typology.Gender.SemanticBasis

  Semantic trigger (e.g. sex → social gender triggers the rule)

• targetDimension : Morphology.DM.GenderDimension

  DM gender dimension assigned (e.g. fem)

• context : Typology.Gender.SemanticBasis

  Context restriction (e.g. humanness)

def Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule.decEq (x✝ x✝¹ : LexicalGenderRule) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule : DecidableEq LexicalGenderRule

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule = Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule.decEq

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule : Repr LexicalGenderRule

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule.repr : LexicalGenderRule → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.harrisHumanGenderRule : LexicalGenderRule

Harris's Human Gender rule for Spanish: [FEMALE] → [F] / __ [HUMAN] The semantic feature [FEMALE] triggers assignment of the grammatical gender feature [F] (feminine) in the context of [HUMAN] nouns. (@cite{harris-1991}; @cite{kramer-2020} ex. 23)

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.harris_rule_uses_core_bases : harrisHumanGenderRule.semanticBasis.isCore = true ∧ harrisHumanGenderRule.context.isCore = true

Harris's rule connects two core semantic bases: assignment is triggered by social gender/sex and conditioned on humanness.

inductive Phenomena.Gender.Studies.Kramer2020.DiagnosticStatus : Type

The status of a diagnostic phenomenon for a theoretical approach. @cite{kramer-2020} §3.3 argues that some phenomena are genuinely diagnostic while others are inconclusive.

• handled : DiagnosticStatus
• problematic : DiagnosticStatus
• inconclusive : DiagnosticStatus

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqDiagnosticStatus : DecidableEq DiagnosticStatus

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqDiagnosticStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus.repr : DiagnosticStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus : Repr DiagnosticStatus

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus.repr }

structure Phenomena.Gender.Studies.Kramer2020.ApproachCapabilities : Type

A gender assignment approach, characterized by how it handles each of the three diagnostic phenomena from §3.3.

• phonologicalAssignment : DiagnosticStatus

  §3.3.1: phonological gender assignment

• hybridAgreement : DiagnosticStatus

  §3.3.2: hybrid nouns (simultaneous dual agreement)

• predictsSemanticCore : DiagnosticStatus

  §3.3.3: the Semantic Core Generalization

def Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities.decEq (x✝ x✝¹ : ApproachCapabilities) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities : DecidableEq ApproachCapabilities

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities = Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities.decEq

def Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities.repr : ApproachCapabilities → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities : Repr ApproachCapabilities

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities.repr }

def Phenomena.Gender.Studies.Kramer2020.lexicalApproach : ApproachCapabilities

The lexical approach (@cite{harris-1991}).

• Phonological assignment: handled (lexical rules can reference phonology), but @cite{kramer-2020} §3.3.1 argues the phenomenon may not exist — Hausa -ā is morphophonological realization, not assignment.
• Hybrid agreement: problematic — a lexical entry has one gender feature; a single entry cannot be both [M] and [F] (@cite{kramer-2020} §3.3.2)
• Semantic Core: problematic — nothing prevents a language from having only arbitrary gender rules without any semantic connection (@cite{kramer-2020} §3.3.3)

Equations

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

def Phenomena.Gender.Studies.Kramer2020.structuralApproach : ApproachCapabilities

The structural approach (@cite{kramer-2015}).

• Phonological assignment: inconclusive — syntax cannot see phonology, but @cite{kramer-2020} §3.3.1 argues the phenomenon is better analyzed as morphophonological realization of a gender feature on n, so the structural approach is not genuinely challenged.
• Hybrid agreement: handled — a root can combine with different n heads, or a social-gender projection can override morphosyntactic gender (@cite{kramer-2020} §3.3.2)
• Semantic Core: handled — via the Thesis of Radical Interpretability: if a language has gender features, at least some must be interpretable, which forces semantic assignment for at least some nouns (@cite{kramer-2020} §3.3.3)

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.approaches_differ : lexicalApproach.phonologicalAssignment ≠ structuralApproach.phonologicalAssignment ∧ lexicalApproach.hybridAgreement ≠ structuralApproach.hybridAgreement ∧ lexicalApproach.predictsSemanticCore ≠ structuralApproach.predictsSemanticCore

The approaches differ on all three diagnostic phenomena.

theorem Phenomena.Gender.Studies.Kramer2020.structural_edge : structuralApproach.hybridAgreement = DiagnosticStatus.handled ∧ structuralApproach.predictsSemanticCore = DiagnosticStatus.handled ∧ lexicalApproach.hybridAgreement = DiagnosticStatus.problematic ∧ lexicalApproach.predictsSemanticCore = DiagnosticStatus.problematic

The structural approach handles 2 of the 3 diagnostic phenomena; the lexical approach handles 1. Phonological assignment is inconclusive for both (the structural approach because syntax can't see phonology; the lexical approach because Kramer argues the phenomenon doesn't exist as described). This is the basis for @cite{kramer-2020} §3.4's conclusion that "structural gender assignment has a slight edge."

def Phenomena.Gender.Studies.Kramer2020.radicalInterpretability (features : List Morphology.DM.GenderFeature) : Prop

Radical Interpretability (Brody 1997; Pesetsky & Torrego 2001, 2007): each syntactic feature must receive a semantic interpretation in some syntactic location.

In formal terms: if a feature F has an uninterpretable instantiation in a language, then F also has an interpretable instantiation in that language. The converse need not hold.

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.amharic_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }]

Amharic's n types satisfy Radical Interpretability: the uninterpretable u[+FEM] is accompanied by interpretable i[+FEM] and i[−FEM] in the same dimension.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }]

Spanish's n types (Set 1) satisfy Radical Interpretability: u[+FEM] is accompanied by i[+FEM] in the same dimension.

theorem Phenomena.Gender.Studies.Kramer2020.russian_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }]

Russian's n types (5-n) satisfy Radical Interpretability: both u[+FEM] and u[−FEM] are paired with i[+FEM] and i[−FEM].

theorem Phenomena.Gender.Studies.Kramer2020.no_purely_arbitrary_under_ri (features : List Morphology.DM.GenderFeature) (hRI : radicalInterpretability features) (hNonempty : ∃ gf ∈ features, True) (hAllU : ∀ gf ∈ features, gf.interp = Morphology.DM.Interpretability.u) : False

The Semantic Core follows from Radical Interpretability + structural assignment: if a language has any gender feature (even uninterpretable), it must have an interpretable one in the same dimension, which forces at least some nouns to be assigned gender semantically.

Contrapositively: a language with only uninterpretable gender (pure arbitrary assignment, no semantic core) violates Radical Interpretability.

theorem Phenomena.Gender.Studies.Kramer2020.ri_implies_interpretable_exists (features : List Morphology.DM.GenderFeature) (hRI : radicalInterpretability features) (hNonempty : ∃ gf ∈ features, True) : ∃ gf ∈ features, gf.interp = Morphology.DM.Interpretability.i

Positive direction of the RI → Semantic Core derivation: if a language has gender features and satisfies Radical Interpretability, then it has at least one interpretable gender feature (which, being interpretable, forces semantic gender assignment for at least some nouns). (@cite{kramer-2020} §3.3.3)

structure Phenomena.Gender.Studies.Kramer2020.SameRootNominal : Type

Same-root nominals: nouns that can be assigned different grammatical genders depending on the social gender of their referent. (@cite{kramer-2020} §2.2.3; @cite{kramer-2015}; @cite{corbett-1991})

In the structural approach, the root itself is ungendered; gender depends on which n head it merges with. Same-root nominals combine with alternative n heads depending on the referent.

Examples: Amharic hakim 'doctor' (ex. 13), Spanish estudiante 'student', Greek odigós 'driver'.

• form : String

  The noun form

• language : String

  Language

• possibleNHeads : List Morphology.DM.CatHead

  Possible gender assignments (> 1 for same-root nominals)

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal : Repr SameRootNominal

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal.repr : SameRootNominal → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.SameRootNominal.isSameRoot (n : SameRootNominal) : Bool

Whether this is a genuine same-root nominal (multiple n options).

Equations

• n.isSameRoot = decide (n.possibleNHeads.length > 1)

def Phenomena.Gender.Studies.Kramer2020.amharicHakim : SameRootNominal

Amharic hakim 'doctor': combines with either i[+FEM] or i[−FEM] depending on the referent. (@cite{kramer-2020} ex. 13)

Equations

• Phenomena.Gender.Studies.Kramer2020.amharicHakim = { form := "hakim", language := "Amharic", possibleNHeads := [Morphology.DM.CatHead.n_iFem, Morphology.DM.CatHead.n_iMasc] }

theorem Phenomena.Gender.Studies.Kramer2020.hakim_is_same_root : amharicHakim.isSameRoot = true

theorem Phenomena.Gender.Studies.Kramer2020.same_root_two_n_heads : amharicHakim.possibleNHeads.length = 2

Same-root nominals pose a challenge for lexical approaches: a single lexical entry cannot carry both [M] and [F]. The structural approach handles them by allowing the same root to merge with different n heads.

theorem Phenomena.Gender.Studies.Kramer2020.hakim_distinct_genders : Morphology.DM.CatHead.n_iFem ≠ Morphology.DM.CatHead.n_iMasc

The two n heads for hakim are distinct gender features.

Hybrid nouns are distinct from same-root nominals. Where same-root nominals alternate gender depending on the referent (Amharic hakim is EITHER masculine OR feminine), hybrid nouns trigger BOTH genders SIMULTANEOUSLY on different agreement targets in the same sentence.

@cite{kramer-2020} ex. 16/27: Russian vrač 'doctor' očen' xoroš-aja glavn-yj vrač very good-F head-M doctor 'a very good head doctor'

Here xoroš-aja shows feminine agreement and glavn-yj shows masculine agreement with the SAME noun vrač in the SAME clause.

@cite{kramer-2020} §3.3.2 argues this is problematic for lexical approaches (a lexical entry has one gender feature) but handled by structural approaches (a social-gender projection can coexist with morphosyntactic gender on n).

structure Phenomena.Gender.Studies.Kramer2020.HybridNoun : Type

A hybrid noun: a single lexical item that triggers different genders on different agreement targets simultaneously. (@cite{kramer-2020} §2.2.3, §3.3.2; @cite{corbett-1991})

• form : String

  The noun form

• language : String

  Language

• morphGender : Morphology.DM.GenderVal

  Morphosyntactic gender (from n head)

• semGender : Morphology.DM.GenderVal

  Semantic gender (from social-gender projection, triggered by referent)

• distinct : self.morphGender ≠ self.semGender

  The two genders must differ for hybrid agreement to arise.

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun : Repr HybridNoun

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun.repr : HybridNoun → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.russianVrac : HybridNoun

Russian vrač 'doctor': morphologically masculine (from n), but can trigger feminine agreement when referring to a female doctor. (@cite{kramer-2020} ex. 15-16/27; @cite{corbett-1991})

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.hybrid_nouns_favor_structural : structuralApproach.hybridAgreement = DiagnosticStatus.handled ∧ lexicalApproach.hybridAgreement = DiagnosticStatus.problematic

Hybrid nouns are problematic for lexical approaches: a lexical entry can bear only one gender feature, but hybrid nouns need two genders simultaneously. The structural approach handles this via separate projections for morphosyntactic and social gender. (@cite{kramer-2020} §3.3.2)

structure Phenomena.Gender.Studies.Kramer2020.NInventory : Type

An inventory of n heads for a language, with the number of surface genders that result from VI (@cite{kramer-2015} Chs 5-7).

The key insight: surface gender count is determined by VI rules, not directly by the n inventory. Two languages can have the SAME set of n heads but different numbers of surface genders (e.g., Dieri 2 vs Mangarayi 3).

• language : String
• nHeads : List Morphology.DM.CatHead
• surfaceGenders : ℕ

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprNInventory : Repr NInventory

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprNInventory = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprNInventory.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprNInventory.repr : NInventory → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.NInventory.hasArbitraryGender (inv : NInventory) : Bool

Does this inventory include any arbitrary (uninterpretable) gender?

Equations

• inv.hasArbitraryGender = inv.nHeads.any fun (ch : Morphology.DM.CatHead) => match ch.phi.gender with | some gf => decide gf.IsArbitrary | none => false

def Phenomena.Gender.Studies.Kramer2020.NInventory.purelySemanticGender (inv : NInventory) : Bool

Is this a purely semantic gender system (no u-features)?

Equations

• inv.purelySemanticGender = !inv.hasArbitraryGender

def Phenomena.Gender.Studies.Kramer2020.dieriNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.mangarayiNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.amharicNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.spanishNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.hausaNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.maaNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.lealaoNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.ojibweNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.lavukaleveNs : NInventory

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.same_ns_different_genders : dieriNs.nHeads = mangarayiNs.nHeads ∧ dieriNs.surfaceGenders ≠ mangarayiNs.surfaceGenders

Same n inventory, different surface genders: Dieri (2) vs Mangarayi (3). This demonstrates that surface gender count depends on VI, not the inventory itself.

theorem Phenomena.Gender.Studies.Kramer2020.set1_shared : amharicNs.nHeads = spanishNs.nHeads ∧ amharicNs.nHeads = hausaNs.nHeads

Set 1 languages share the same n inventory (@cite{kramer-2015} Ch 6). Hausa is included by extrapolation from Kramer's Table 3 (p. 56) grouping (Hausa is not analyzed in @cite{kramer-2015} itself).

theorem Phenomena.Gender.Studies.Kramer2020.dieri_purely_semantic : dieriNs.purelySemanticGender = true

3-n languages have purely semantic gender (no u-features). (@cite{kramer-2015} Ch 5)

theorem Phenomena.Gender.Studies.Kramer2020.lealao_purely_semantic : lealaoNs.purelySemanticGender = true

Lealao Chinantec is also purely semantic (animacy-based, Ch 5).

theorem Phenomena.Gender.Studies.Kramer2020.ojibwe_has_uAnim : ojibweNs.hasArbitraryGender = true

Ojibwe is a 4-n animacy language with arbitrary animate assignment (u[+ANIM]). (@cite{kramer-2015} Ch 6, §6.4)

theorem Phenomena.Gender.Studies.Kramer2020.ojibwe_four_ns : ojibweNs.nHeads.length = 4

Ojibwe has the same structure as Set 1 sex-based languages (Amharic, Spanish) but in the animacy dimension: i[+ANIM], i[−ANIM], plain n, u[+ANIM].

theorem Phenomena.Gender.Studies.Kramer2020.lavukaleve_maximal : lavukaleveNs.nHeads.length = 5

Lavukaleve is maximal: 5 n heads (both u[+FEM] and u[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.more_ns_same_genders : amharicNs.nHeads.length > dieriNs.nHeads.length ∧ amharicNs.surfaceGenders = dieriNs.surfaceGenders

More n heads does not entail more surface genders: Amharic has 4 ns but only 2 surface genders.

def Phenomena.Gender.Studies.Kramer2020.Spanish.nHead (n : Fragments.Spanish.Gender.SpanishNoun) : Morphology.DM.CatHead

DM Set-1 categorizing-head projection from the theory-neutral Spanish Fragment fields. Same Set-1 partition as Hausa.nHead (Spanish is the canonical Set 1 language per @cite{kramer-2015} Ch. 6, alongside Amharic). The four cells of (attestedGender × isNaturalGender) cover the four Set-1 n-heads.

Equations

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

def Phenomena.Gender.Studies.Kramer2020.Spanish.sameRootNHeads : Fragments.Spanish.Gender.SameRootEntry → List Morphology.DM.CatHead

Same-root nominals project to BOTH possible n-heads (the polymorphic same-root pattern @cite{kramer-2015} §3.4 / @cite{kramer-2020} §2.2.3). The framework decision lives here, not in the Fragment.

Equations

• Phenomena.Gender.Studies.Kramer2020.Spanish.sameRootNHeads x✝ = [Morphology.DM.CatHead.n_iFem, Morphology.DM.CatHead.n_iMasc]

def Phenomena.Gender.Studies.Kramer2020.Russian.nHead (n : Fragments.Slavic.Russian.Gender.RussianNoun) : Morphology.DM.CatHead

DM 5-n categorizing-head projection from theory-neutral Russian Fragment fields. Russian uses 3-gender VI (vs Spanish's Set 1 binary), so the (attestedGender × isNaturalGender) cells project to five n-heads: i[+FEM], i[−FEM], u[+FEM], u[−FEM], plain n. Verified against @cite{kramer-2015} Ch. 7.

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.hombre_natural_masculine : (Spanish.nHead Fragments.Spanish.Gender.hombre).phi.gender = some { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }

Derive from fragment via Spanish.nHead projection: hombre 'man' has natural masculine gender (i[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.mujer_natural_feminine : (Spanish.nHead Fragments.Spanish.Gender.mujer).phi.gender = some { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }

mujer 'woman' has natural feminine gender (i[+FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.mesa_arbitrary_feminine : (Spanish.nHead Fragments.Spanish.Gender.mesa).phi.gender = some { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }

mesa 'table' has arbitrary feminine gender (u[+FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.libro_default_masculine : (Spanish.nHead Fragments.Spanish.Gender.libro).phi.gender = none

libro 'book' has default masculine (plain n).

def Phenomena.Gender.Studies.Kramer2020.spanishSameRoot (e : Fragments.Spanish.Gender.SameRootEntry) : SameRootNominal

Bridge: convert a Spanish SameRootEntry to the cross-linguistic SameRootNominal type. The possibleNHeads come from the Studies projection Spanish.sameRootNHeads.

Equations

• Phenomena.Gender.Studies.Kramer2020.spanishSameRoot e = { form := e.form, language := "Spanish", possibleNHeads := Phenomena.Gender.Studies.Kramer2020.Spanish.sameRootNHeads e }

theorem Phenomena.Gender.Studies.Kramer2020.soldado_is_same_root : (Spanish.sameRootNHeads Fragments.Spanish.Gender.soldado).head? ≠ (Spanish.sameRootNHeads Fragments.Spanish.Gender.soldado).getLast?

Spanish soldado 'soldier' as a same-root nominal: the root √SOLDAD can combine with i[+FEM] or i[−FEM]. The two licensed n-heads are distinct.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_same_roots_genuine : (spanishSameRoot Fragments.Spanish.Gender.soldado).isSameRoot = true ∧ (spanishSameRoot Fragments.Spanish.Gender.estudiante).isSameRoot = true ∧ (spanishSameRoot Fragments.Spanish.Gender.artista).isSameRoot = true

Spanish same-root nominals are genuine same-root nominals (they have two possible n heads).

theorem Phenomena.Gender.Studies.Kramer2020.spanish_four_n_types : spanishNs.nHeads.length = 4

Spanish has the full Set 1 inventory: 4 n types.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_fragment_covers_inventory : (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => Spanish.nHead x == Morphology.DM.CatHead.n_iFem) = true ∧ (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => Spanish.nHead x == Morphology.DM.CatHead.n_iMasc) = true ∧ (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => Spanish.nHead x == Morphology.DM.CatHead.n_uFem) = true ∧ (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => Spanish.nHead x == Morphology.DM.CatHead.n_plain) = true

The fragment inventory covers all four Set-1 n-types via projection.

@cite{kramer-2015} §3.4 identifies four classes of roots, distinguished by which n heads they are licensed to combine with:

1. Female-denoting roots (√WOMAN, √QUEEN): semantic licensing (List 3) requires n i[+FEM]. The Encyclopedia entry only provides a denotation in the context of an n head bearing [+FEM].
2. Male-denoting roots (√MAN, √KING): semantic licensing requires n i[−FEM].
3. Arbitrarily feminine roots (√TABLE, √CHAIR): PF licensing (List 2) requires n u[+FEM]. A VI rule specifies the exponent in the context of [+FEM] on n.
4. Default roots (√BOOK, √CAR): no licensing requirement. Combine with plain n (the elsewhere case).

This classification generates the licensing tables found in Tables 3.1 (Amharic, 3 ns) and 6.2 (Spanish, 4 ns).

inductive Phenomena.Gender.Studies.Kramer2020.RootClass : Type

Root classes from @cite{kramer-2015} §3.4, parameterized by which n head the root is licensed to combine with.

The first four classes are from Tables 3.1/6.2 (3-n and Set 1 4-n systems). arbitraryMasc extends the typology to 5-n systems (Russian, Lavukaleve) and Set 2 4-n systems (Maa, Wari'), where u[−FEM] is also attested.

• femaleReferent : RootClass
• maleReferent : RootClass
• arbitraryFem : RootClass
• arbitraryMasc : RootClass
• default : RootClass

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqRootClass : DecidableEq RootClass

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Gender.Studies.Kramer2020.instReprRootClass : Repr RootClass

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprRootClass = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprRootClass.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.RootClass.licensedNHead : RootClass → Morphology.DM.CatHead

The n head each root class is licensed to combine with.

Equations

• Phenomena.Gender.Studies.Kramer2020.RootClass.femaleReferent.licensedNHead = Morphology.DM.CatHead.n_iFem
• Phenomena.Gender.Studies.Kramer2020.RootClass.maleReferent.licensedNHead = Morphology.DM.CatHead.n_iMasc
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryFem.licensedNHead = Morphology.DM.CatHead.n_uFem
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryMasc.licensedNHead = Morphology.DM.CatHead.n_uNegFem
• Phenomena.Gender.Studies.Kramer2020.RootClass.default.licensedNHead = Morphology.DM.CatHead.n_plain

def Phenomena.Gender.Studies.Kramer2020.RootClass.licensing : RootClass → Morphology.DM.LicensingType

The licensing type for each root class.

Equations

• Phenomena.Gender.Studies.Kramer2020.RootClass.femaleReferent.licensing = Morphology.DM.LicensingType.semantic
• Phenomena.Gender.Studies.Kramer2020.RootClass.maleReferent.licensing = Morphology.DM.LicensingType.semantic
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryFem.licensing = Morphology.DM.LicensingType.arbitrary
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryMasc.licensing = Morphology.DM.LicensingType.arbitrary
• Phenomena.Gender.Studies.Kramer2020.RootClass.default.licensing = Morphology.DM.LicensingType.arbitrary

theorem Phenomena.Gender.Studies.Kramer2020.natural_roots_semantic : RootClass.femaleReferent.licensing = Morphology.DM.LicensingType.semantic ∧ RootClass.maleReferent.licensing = Morphology.DM.LicensingType.semantic

Natural-gender roots are semantically licensed.

theorem Phenomena.Gender.Studies.Kramer2020.arbitrary_roots_pf : RootClass.arbitraryFem.licensing = Morphology.DM.LicensingType.arbitrary ∧ RootClass.arbitraryMasc.licensing = Morphology.DM.LicensingType.arbitrary ∧ RootClass.default.licensing = Morphology.DM.LicensingType.arbitrary

Arbitrary and default roots are PF-licensed.

theorem Phenomena.Gender.Studies.Kramer2020.root_classes_distinct_n : RootClass.femaleReferent.licensedNHead ≠ RootClass.maleReferent.licensedNHead ∧ RootClass.femaleReferent.licensedNHead ≠ RootClass.arbitraryFem.licensedNHead ∧ RootClass.femaleReferent.licensedNHead ≠ RootClass.arbitraryMasc.licensedNHead ∧ RootClass.femaleReferent.licensedNHead ≠ RootClass.default.licensedNHead ∧ RootClass.maleReferent.licensedNHead ≠ RootClass.arbitraryFem.licensedNHead ∧ RootClass.maleReferent.licensedNHead ≠ RootClass.arbitraryMasc.licensedNHead ∧ RootClass.maleReferent.licensedNHead ≠ RootClass.default.licensedNHead ∧ RootClass.arbitraryFem.licensedNHead ≠ RootClass.arbitraryMasc.licensedNHead ∧ RootClass.arbitraryFem.licensedNHead ≠ RootClass.default.licensedNHead ∧ RootClass.arbitraryMasc.licensedNHead ≠ RootClass.default.licensedNHead

Each root class maps to a distinct n head.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_mujer : Spanish.nHead Fragments.Spanish.Gender.mujer = RootClass.femaleReferent.licensedNHead

Verify that the Spanish fragment's nouns project to their expected root classes via Spanish.nHead.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_hombre : Spanish.nHead Fragments.Spanish.Gender.hombre = RootClass.maleReferent.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_mesa : Spanish.nHead Fragments.Spanish.Gender.mesa = RootClass.arbitraryFem.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_libro : Spanish.nHead Fragments.Spanish.Gender.libro = RootClass.default.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_femaleReferent : (Morphology.DM.CatHead.n_iFem.phi.gender.get ⋯).licensingType = RootClass.femaleReferent.licensing

Bridge: the licensing type of a root class agrees with the licensing type derived from its n head's gender feature. For gendered root classes, the GenderFeature.licensingType (defined in Categorizer.lean) produces the same result as RootClass.licensing.

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_maleReferent : (Morphology.DM.CatHead.n_iMasc.phi.gender.get ⋯).licensingType = RootClass.maleReferent.licensing

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_arbitraryFem : (Morphology.DM.CatHead.n_uFem.phi.gender.get ⋯).licensingType = RootClass.arbitraryFem.licensing

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_arbitraryMasc : (Morphology.DM.CatHead.n_uNegFem.phi.gender.get ⋯).licensingType = RootClass.arbitraryMasc.licensing

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_otec : Russian.nHead Fragments.Slavic.Russian.Gender.otec = RootClass.maleReferent.licensedNHead

Russian fragment nouns project to their root classes via Russian.nHead.

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_mat' : Russian.nHead Fragments.Slavic.Russian.Gender.mat' = RootClass.femaleReferent.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_zakon : Russian.nHead Fragments.Slavic.Russian.Gender.zakon = RootClass.arbitraryMasc.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_škola : Russian.nHead Fragments.Slavic.Russian.Gender.škola = RootClass.arbitraryFem.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_vino : Russian.nHead Fragments.Slavic.Russian.Gender.vino = RootClass.default.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.persona_exception : Spanish.nHead Fragments.Spanish.Gender.persona = RootClass.arbitraryFem.licensedNHead ∧ Fragments.Spanish.Gender.persona.gloss = "person"

persona is human-denoting but has u[+FEM] (arbitrary feminine), not i[+FEM] (natural feminine). This is the key exception to the pattern that human-denoting nouns get interpretable gender features. (@cite{kramer-2020} §3.2, p. 59; @cite{kramer-2015} §6.2)

In root-class terms: persona's root is licensed as arbitraryFem despite denoting humans — its root is only licensed to combine with n u[+FEM], never n i[+FEM] or n i[−FEM].

The NInventory (from the DM analysis of n heads, @cite{kramer-2015}) and the GenderProfile (from WALS typology, @cite{corbett-2013}) describe the same languages from different theoretical perspectives. The key bridge: the NInventory.surfaceGenders count should match GenderProfile.rawGenderCount for the same language.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_ninventory_matches_profile : spanishNs.surfaceGenders = Phenomena.Gender.Studies.Kramer2020.spanish✝.rawGenderCount

Spanish: the DM n-inventory predicts the same number of surface genders as the WALS typological profile.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_surface_genders_consistent : Typology.Gender.GenderCount.two.Contains spanishNs.surfaceGenders

Spanish surface genders are consistent with the WALS gender count bin.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_structural_vs_surface : spanishNs.nHeads.length > spanishNs.surfaceGenders

For Spanish, the n-inventory has 4 structural heads mapping to 2 surface genders — a many-to-one mapping mediated by VI (@cite{kramer-2015} Ch 6). This is the central insight: structural richness (4 n types) does not imply surface richness (only 2 genders).

theorem Phenomena.Gender.Studies.Kramer2020.spanish_assignment_consistent : spanishNs.hasArbitraryGender = true ∧ Phenomena.Gender.Studies.Kramer2020.spanish✝.assignment = Typology.Gender.AssignmentSystem.semanticAndFormal

NInventory ↔ AssignmentSystem bridge: having arbitrary (u) features in the n-inventory corresponds to semanticAndFormal assignment in the WALS typology. 3-n languages with no u-features are semanticOnly. (@cite{kramer-2020} §2.3; @cite{corbett-2013} Ch 32)

In Set 1 languages (Spanish, Amharic), masculine is the DEFAULT gender: nouns with plain n (no gender feature) surface as masculine. The derivation:

1. The root combines with plain n (no gender feature on n).
2. At PF, Vocabulary Insertion looks for a matching exponent.
3. The [+FEM] exponent requires [+FEM] on n — it does NOT match.
4. The elsewhere/default exponent (masculine) is inserted.

In Set 2 languages (Maa, Wari'), the same logic yields feminine as default:

1. The root combines with plain n (no gender feature on n).
2. The [−FEM] exponent requires [−FEM] on n — it does NOT match.
3. The elsewhere/default exponent (feminine) is inserted.

The polarity of the u-feature determines which gender is arbitrary vs default.

theorem Phenomena.Gender.Studies.Kramer2020.set1_plain_n_masculine : Morphology.DM.CatHead.n_plain.surfaceGenderSet1 = Features.SurfaceGender.masculine

Plain n → masculine (the default).

theorem Phenomena.Gender.Studies.Kramer2020.set1_iFem_feminine : Morphology.DM.CatHead.n_iFem.surfaceGenderSet1 = Features.SurfaceGender.feminine

i[+FEM] → feminine (natural female).

theorem Phenomena.Gender.Studies.Kramer2020.set1_iMasc_masculine : Morphology.DM.CatHead.n_iMasc.surfaceGenderSet1 = Features.SurfaceGender.masculine

i[−FEM] → masculine (natural male).

theorem Phenomena.Gender.Studies.Kramer2020.set1_uFem_feminine : Morphology.DM.CatHead.n_uFem.surfaceGenderSet1 = Features.SurfaceGender.feminine

u[+FEM] → feminine (arbitrary feminine).

theorem Phenomena.Gender.Studies.Kramer2020.set2_plain_n_feminine : Morphology.DM.CatHead.n_plain.surfaceGenderSet2 = Features.SurfaceGender.feminine

Plain n → feminine (the default in Set 2).

theorem Phenomena.Gender.Studies.Kramer2020.set2_uNegFem_masculine : Morphology.DM.CatHead.n_uNegFem.surfaceGenderSet2 = Features.SurfaceGender.masculine

u[−FEM] → masculine (arbitrary masculine in Set 2).

theorem Phenomena.Gender.Studies.Kramer2020.set2_iMasc_masculine : Morphology.DM.CatHead.n_iMasc.surfaceGenderSet2 = Features.SurfaceGender.masculine

i[−FEM] → masculine (natural male, same in both sets).

theorem Phenomena.Gender.Studies.Kramer2020.set2_iFem_feminine : Morphology.DM.CatHead.n_iFem.surfaceGenderSet2 = Features.SurfaceGender.feminine

i[+FEM] → feminine (natural female, same in both sets).

theorem Phenomena.Gender.Studies.Kramer2020.spanish_derivation_chain : (Spanish.nHead Fragments.Spanish.Gender.mujer).surfaceGenderSet1 = Features.SurfaceGender.feminine ∧ (Spanish.nHead Fragments.Spanish.Gender.hombre).surfaceGenderSet1 = Features.SurfaceGender.masculine ∧ (Spanish.nHead Fragments.Spanish.Gender.mesa).surfaceGenderSet1 = Features.SurfaceGender.feminine ∧ (Spanish.nHead Fragments.Spanish.Gender.libro).surfaceGenderSet1 = Features.SurfaceGender.masculine ∧ (Spanish.nHead Fragments.Spanish.Gender.persona).surfaceGenderSet1 = Features.SurfaceGender.feminine ∧ (Spanish.nHead Fragments.Spanish.Gender.ángel).surfaceGenderSet1 = Features.SurfaceGender.masculine

Verify the full derivation chain for Spanish fragment nouns: the surface gender computed via Spanish.nHead projection then Set 1 VI matches the entry's attestedGender.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_projection_round_trips : (Fragments.Spanish.Gender.allNouns.all fun (n : Fragments.Spanish.Gender.SpanishNoun) => (Spanish.nHead n).surfaceGenderSet1 == n.attestedGender) = true

Stronger meta-theorem: for every Spanish entry, the projection composed with Set 1 VI recovers the entry's attestedGender. The Fragment-side empirical fact (attestedGender) and the Studies-side structural derivation (Spanish.nHead + Set 1 VI) agree.

theorem Phenomena.Gender.Studies.Kramer2020.fixed_gender_from_n_head : (Spanish.nHead Fragments.Spanish.Gender.persona).surfaceGenderSet1 = Features.SurfaceGender.feminine ∧ (Spanish.nHead Fragments.Spanish.Gender.ángel).surfaceGenderSet1 = Features.SurfaceGender.masculine

Fixed-gender nouns: persona surfaces as feminine despite denoting persons of any sex; ángel surfaces as masculine.

Russian is a 5-n language with 3 surface genders — the same inventory as Lavukaleve, supporting @cite{kramer-2015}'s prediction that n-inventory size and surface gender count are independent (mediated by VI).

def Phenomena.Gender.Studies.Kramer2020.russianNs : NInventory

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.russian_lavukaleve_same_ns : russianNs.nHeads = lavukaleveNs.nHeads

Russian and Lavukaleve share the same n-inventory (5 heads).

theorem Phenomena.Gender.Studies.Kramer2020.russian_lavukaleve_same_surface : russianNs.surfaceGenders = lavukaleveNs.surfaceGenders

Both have 3 surface genders despite the 5-n inventory.

theorem Phenomena.Gender.Studies.Kramer2020.russian_structural_vs_surface : russianNs.nHeads.length > russianNs.surfaceGenders

Russian has 5 structural heads mapping to 3 surface genders.

theorem Phenomena.Gender.Studies.Kramer2020.russian_ninventory_matches_profile : russianNs.surfaceGenders = Phenomena.Gender.Studies.Kramer2020.russian✝.rawGenderCount

Russian: the DM n-inventory predicts the same number of surface genders as the WALS typological profile.

theorem Phenomena.Gender.Studies.Kramer2020.russian_surface_genders_consistent : Typology.Gender.GenderCount.three.Contains russianNs.surfaceGenders

Russian n-inventory matches the WALS gender count bin.

theorem Phenomena.Gender.Studies.Kramer2020.russian_assignment_consistent : russianNs.hasArbitraryGender = true ∧ Phenomena.Gender.Studies.Kramer2020.russian✝.assignment = Typology.Gender.AssignmentSystem.semanticAndFormal

Russian has u-features → semanticAndFormal assignment, consistent with the WALS profile.

theorem Phenomena.Gender.Studies.Kramer2020.vrač_morph_masculine : (Russian.nHead Fragments.Slavic.Russian.Gender.vrač).phi.gender = some { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }

Projection-derived: vrač has morphological masculine (u[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.vrač_matches_hybrid : russianVrac.morphGender = { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } ∧ (Russian.nHead Fragments.Slavic.Russian.Gender.vrač).phi.gender = some { interp := Morphology.DM.Interpretability.u, val := russianVrac.morphGender }

vrač is a hybrid noun: its morphological gender (u[−FEM] = masculine) differs from the semantic gender triggered by a female referent ([+FEM]). This matches the russianVrac definition from §7.

theorem Phenomena.Gender.Studies.Kramer2020.zakon_fragment_masculine : (Russian.nHead Fragments.Slavic.Russian.Gender.zakon).surfaceGenderThree = Features.SurfaceGender.masculine

Projection-derived: zakon (Class I) surfaces as masculine via 3-gender VI.

theorem Phenomena.Gender.Studies.Kramer2020.vino_fragment_neuter : (Russian.nHead Fragments.Slavic.Russian.Gender.vino).surfaceGenderThree = Features.SurfaceGender.neuter

Projection-derived: vino (default) surfaces as neuter via 3-gender VI.

theorem Phenomena.Gender.Studies.Kramer2020.russian_projection_round_trips : (Fragments.Slavic.Russian.Gender.allNouns.all fun (n : Fragments.Slavic.Russian.Gender.RussianNoun) => (Russian.nHead n).surfaceGenderThree == n.attestedGender) = true

Russian projection round-trip: every Russian entry's projection, composed with 3-gender VI, recovers the entry's attestedGender.

theorem Phenomena.Gender.Studies.Kramer2020.russian_fragment_covers_inventory : (Fragments.Slavic.Russian.Gender.allNouns.any fun (x : Fragments.Slavic.Russian.Gender.RussianNoun) => Russian.nHead x == Morphology.DM.CatHead.n_iFem) = true ∧ (Fragments.Slavic.Russian.Gender.allNouns.any fun (x : Fragments.Slavic.Russian.Gender.RussianNoun) => Russian.nHead x == Morphology.DM.CatHead.n_iMasc) = true ∧ (Fragments.Slavic.Russian.Gender.allNouns.any fun (x : Fragments.Slavic.Russian.Gender.RussianNoun) => Russian.nHead x == Morphology.DM.CatHead.n_uFem) = true ∧ (Fragments.Slavic.Russian.Gender.allNouns.any fun (x : Fragments.Slavic.Russian.Gender.RussianNoun) => Russian.nHead x == Morphology.DM.CatHead.n_uNegFem) = true ∧ (Fragments.Slavic.Russian.Gender.allNouns.any fun (x : Fragments.Slavic.Russian.Gender.RussianNoun) => Russian.nHead x == Morphology.DM.CatHead.n_plain) = true

Projection-derived: Russian Fragment covers all 5 n-types.

The NInventory.surfaceGenders field is currently stipulated. Here we derive the surface gender count from VI rules applied to each n-head, verifying that the computed count matches the stipulated count.

The key VI patterns from @cite{kramer-2015}:

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

def Phenomena.Gender.Studies.Kramer2020.NInventory.computeSurfaceGenders (inv : NInventory) (viMap : Morphology.DM.CatHead → ℕ) : ℕ

A VI gender-class assignment: maps each n-head to a surface gender class (encoded as Nat). Two n-heads yielding the same Nat surface as the same gender.

Equations

• inv.computeSurfaceGenders viMap = (List.map viMap inv.nHeads).eraseDups.length

def Phenomena.Gender.Studies.Kramer2020.viSet1 (ch : Morphology.DM.CatHead) : ℕ

Set 1 VI: [+FEM] → 0 (feminine), everything else → 1 (masculine).

Equations

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

def Phenomena.Gender.Studies.Kramer2020.viSet2 (ch : Morphology.DM.CatHead) : ℕ

Set 2 VI: [−FEM] → 1 (masculine), everything else → 0 (feminine).

Equations

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

def Phenomena.Gender.Studies.Kramer2020.viThreeGender (ch : Morphology.DM.CatHead) : ℕ

3-gender VI: [+FEM] → 0, [−FEM] → 1, no feature → 2.

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.spanish_vi_derived : spanishNs.computeSurfaceGenders viSet1 = spanishNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.amharic_vi_derived : amharicNs.computeSurfaceGenders viSet1 = amharicNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.hausa_vi_derived : hausaNs.computeSurfaceGenders viSet1 = hausaNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.maa_vi_derived : maaNs.computeSurfaceGenders viSet2 = maaNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.russian_vi_derived : russianNs.computeSurfaceGenders viThreeGender = russianNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.mangarayi_vi_derived : mangarayiNs.computeSurfaceGenders viThreeGender = mangarayiNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.lavukaleve_vi_derived : lavukaleveNs.computeSurfaceGenders viThreeGender = lavukaleveNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.dieri_vi_derived : dieriNs.computeSurfaceGenders viSet1 = dieriNs.surfaceGenders

Dieri: same 3-n inventory as Mangarayi but 2 surface genders under Set 1 VI (where plain n → masculine, not neuter).

theorem Phenomena.Gender.Studies.Kramer2020.dieri_mangarayi_vi_contrast : dieriNs.nHeads = mangarayiNs.nHeads ∧ dieriNs.computeSurfaceGenders viSet1 ≠ mangarayiNs.computeSurfaceGenders viThreeGender

The Dieri vs Mangarayi contrast: same n-heads, different VI → different surface gender counts. This is now DERIVED, not stipulated.

@cite{kramer-2020} §3.3.1 (pp. 60–61) responds to the apparent challenge from "phonological gender assignment."

Empirical pattern (described in §2.3.2, pp. 54–55, citing @cite{newman-2000}): Hausa nonhuman feminines mostly end in -ā, but @cite{newman-2000} p. 209 documents 250+ ā-final masculines (out of ~3000 masculine nouns), partitioned into native exceptions (kadā 'crocodile', ùbā 'father', zàkarā 'rooster'), loanwords, and erstwhile plurals (gidā 'house', ruwā 'water'). The correlation feminine→-ā is unidirectional (@cite{kramer-2020} p. 55): "If a noun has feminine gender, then it likely ends in -ā. However, not every noun that ends in -ā has feminine gender."

Three framings:

• @cite{newman-2000} p. 213 ("overt characterization"): synchronically the {-ā} suffix is a morphological feminine marker (not a phonological rule). Diachronically, feminine nouns acquired -ā via overt characterization (@cite{newman-1979a}).

• @cite{corbett-1991} §3.2.2 (pp. 52–53): synchronic phonological assignment with exceptions ("nouns ending in -aa are feminine"). Diachronic origin in §4.5 (pp. 102–103, citing Newman 1979).

• @cite{kramer-2020} §3.3.1 (pp. 60–61): the -ā suffix "is probably best analyzed as the realization of a feminine gender feature" — morphophonological realization of [+FEM] on n, NOT phonological assignment.

The Newman/Kramer synchronic view is opposed to the Corbett phonological-assignment view; Newman's source grammar favors Kramer's re-analysis.

Hausa Fragment is theory-neutral (carries attestedGender + isNaturalGender, no DM commitment). This section projects those fields onto Set-1 DM categorizers via Hausa.nHead, then formalizes the §3.3.1 diagnostic and encodes the three-way Newman/Corbett/Kramer disagreement at theorem level.

def Phenomena.Gender.Studies.Kramer2020.Hausa.nHead (n : Fragments.Hausa.Gender.Noun) : Morphology.DM.CatHead

DM Set-1 categorizing-head projection from the theory-neutral Fragment fields. The four cells of (attestedGender × isNaturalGender) project to the four Set-1 n-heads (@cite{kramer-2015} Ch. 6). Non-binary surface genders (.neuter, .common, .animate, .inanimate) fall through to .n_plain — irrelevant for Hausa.

UNVERIFIED: Hausa is not classified by @cite{kramer-2015} (it appears only in introductory data examples in Ch. 1). The Set-1 placement extrapolates from @cite{kramer-2020} Table 3 (p. 56).

Equations

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

def Phenomena.Gender.Studies.Kramer2020.Hausa.Predictors.corbettPhonological (n : Fragments.Hausa.Gender.Noun) : Features.SurfaceGender

Naive Corbett-style phonological-assignment rule (@cite{corbett-1991} §3.2.2): nouns ending in -ā are feminine, others are masculine. This is what Kramer's §3.3.1 refutes.

Equations

• Phenomena.Gender.Studies.Kramer2020.Hausa.Predictors.corbettPhonological n = if n.EndsInAa then Features.SurfaceGender.feminine else Features.SurfaceGender.masculine

def Phenomena.Gender.Studies.Kramer2020.Hausa.Predictors.newmanKramerStructural (n : Fragments.Hausa.Gender.Noun) : Features.SurfaceGender

Newman/Kramer structural rule: the noun's surface gender is the morphosyntactically encoded fact (Newman: lexical+overt-char; Kramer: VI realization on n head). At the empirical level, both reduce to the attested agreement-trigger fact.

Equations

• Phenomena.Gender.Studies.Kramer2020.Hausa.Predictors.newmanKramerStructural n = n.attestedGender

theorem Phenomena.Gender.Studies.Kramer2020.hausa_nHead_projection_correct : (Fragments.Hausa.Gender.allNouns.all fun (n : Fragments.Hausa.Gender.Noun) => Hausa.nHead n == match n.attestedGender, n.isNaturalGender with | Features.SurfaceGender.feminine, true => Morphology.DM.CatHead.n_iFem | Features.SurfaceGender.masculine, true => Morphology.DM.CatHead.n_iMasc | Features.SurfaceGender.feminine, false => Morphology.DM.CatHead.n_uFem | Features.SurfaceGender.masculine, false => Morphology.DM.CatHead.n_plain | x, x_1 => Morphology.DM.CatHead.n_plain) = true

Every Hausa Fragment entry projects to the expected Set-1 n-head. decide checks all 12 entries by structural reduction.

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_yarinya : Hausa.nHead Fragments.Hausa.Gender.yarinya = RootClass.femaleReferent.licensedNHead

yārinyā 'girl' projects to natural feminine (i[+FEM]). Parallels spanish_licensing_mujer (§10).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_yaro : Hausa.nHead Fragments.Hausa.Gender.yaro = RootClass.maleReferent.licensedNHead

yārō 'boy' projects to natural masculine (i[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_kaza : Hausa.nHead Fragments.Hausa.Gender.kaza = RootClass.femaleReferent.licensedNHead

kāzā 'hen' projects to natural feminine — Newman lists kāzā paired with zàkarā 'rooster' as a sex-paired entry, satisfying Kramer's "honoris causa" criterion (@cite{kramer-2020} p. 57).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_riga : Hausa.nHead Fragments.Hausa.Gender.riga = RootClass.arbitraryFem.licensedNHead

rīgā 'gown' projects to arbitrary feminine (u[+FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_gida : Hausa.nHead Fragments.Hausa.Gender.gida = RootClass.default.licensedNHead

gidā 'house' projects to default masculine (plain n). @cite{newman-2000} p. 209 erstwhile-plural class (c).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_kada : Hausa.nHead Fragments.Hausa.Gender.kada = RootClass.default.licensedNHead

kadā̀ 'crocodile' projects to default masculine (plain n). @cite{newman-2000} p. 209 native ā-final masculine class (a).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_licensing_uba : Hausa.nHead Fragments.Hausa.Gender.uba = RootClass.maleReferent.licensedNHead

ùbā 'father' projects to natural masculine (i[−FEM]). @cite{newman-2000} p. 209 native ā-final masculine class (a), cited in @cite{kramer-2015} Ch. 1.

theorem Phenomena.Gender.Studies.Kramer2020.hausa_fragment_covers_inventory : (Fragments.Hausa.Gender.allNouns.any fun (x : Fragments.Hausa.Gender.Noun) => Hausa.nHead x == Morphology.DM.CatHead.n_iFem) = true ∧ (Fragments.Hausa.Gender.allNouns.any fun (x : Fragments.Hausa.Gender.Noun) => Hausa.nHead x == Morphology.DM.CatHead.n_iMasc) = true ∧ (Fragments.Hausa.Gender.allNouns.any fun (x : Fragments.Hausa.Gender.Noun) => Hausa.nHead x == Morphology.DM.CatHead.n_uFem) = true ∧ (Fragments.Hausa.Gender.allNouns.any fun (x : Fragments.Hausa.Gender.Noun) => Hausa.nHead x == Morphology.DM.CatHead.n_plain) = true

The Hausa Fragment covers all four Set-1 n-heads via its projection. Parallels fragment_covers_inventory for Spanish.

theorem Phenomena.Gender.Studies.Kramer2020.exists_aa_masculine_noun : ∃ n ∈ Fragments.Hausa.Gender.allNouns, n.EndsInAa ∧ n.attestedGender = Features.SurfaceGender.masculine

§3.3.1 forward refutation (@cite{kramer-2020} ex. 22, p. 55): the naive phonological rule "ends-in--ā ⇒ feminine" is falsified. Witness: kadā̀ 'crocodile' (Kramer's cited example, attributed to @cite{newman-2000} p. 209): ends in -ā but masculine.

theorem Phenomena.Gender.Studies.Kramer2020.exists_feminine_non_aa_noun : ∃ n ∈ Fragments.Hausa.Gender.allNouns, n.attestedGender = Features.SurfaceGender.feminine ∧ ¬n.EndsInAa

§3.3.1 converse, Newman-anchored (@cite{newman-2000} p. 208 footnote [i]): the converse "feminine ⇒ ends-in--ā" is also falsified. Witness: mācè 'woman' — feminine but ends in -è. Newman explicitly flags this as the canonical exception. (Not part of Kramer's argument; @cite{kramer-2020} p. 55 only argues the forward direction. The converse failure is empirically real and well-anchored on Newman.)

theorem Phenomena.Gender.Studies.Kramer2020.uba_masculine_aa : Fragments.Hausa.Gender.uba.EndsInAa ∧ Fragments.Hausa.Gender.uba.attestedGender = Features.SurfaceGender.masculine

ùbā 'father' is a second masculine -ā witness, beyond Kramer's kadā̀. @cite{newman-2000} p. 209 lists ùbā in native masculine class (a); @cite{kramer-2015} Ch. 1 cites it as a Hausa introductory example.

theorem Phenomena.Gender.Studies.Kramer2020.gida_masculine_aa : Fragments.Hausa.Gender.gida.EndsInAa ∧ Fragments.Hausa.Gender.gida.attestedGender = Features.SurfaceGender.masculine

gidā 'house' is a third masculine -ā witness, in Newman's erstwhile-plural class (c) — distinct historical class from kadā/ùbā.

theorem Phenomena.Gender.Studies.Kramer2020.corbett_kramer_diverge_on_kada : Hausa.Predictors.corbettPhonological Fragments.Hausa.Gender.kada ≠ Hausa.Predictors.newmanKramerStructural Fragments.Hausa.Gender.kada

The naive Corbett-style phonological rule and the Newman/Kramer structural rule diverge on Kramer's witness kadā̀: phonological predicts feminine (kadā̀ ends in -ā), structural predicts the actual fact (masculine).

theorem Phenomena.Gender.Studies.Kramer2020.corbett_kramer_divergence_count : (List.filter (fun (n : Fragments.Hausa.Gender.Noun) => Hausa.Predictors.corbettPhonological n != Hausa.Predictors.newmanKramerStructural n) Fragments.Hausa.Gender.allNouns).length = 4

The two rules diverge on EXACTLY four Fragment entries (mācè, gidā, kadā̀, ùbā), agreeing on the other 8. Quantifies the dispute: the structural account differs from naive phonology on 4/12 ≈ 33% of entries — a third of the Fragment load-bears the disagreement.

theorem Phenomena.Gender.Studies.Kramer2020.corbett_kramer_divergent_entries : List.filter (fun (n : Fragments.Hausa.Gender.Noun) => Hausa.Predictors.corbettPhonological n != Hausa.Predictors.newmanKramerStructural n) Fragments.Hausa.Gender.allNouns = [Fragments.Hausa.Gender.mace, Fragments.Hausa.Gender.gida, Fragments.Hausa.Gender.kada, Fragments.Hausa.Gender.uba]

The four divergent entries are exactly mācè (converse direction), gidā / kadā̀ / ùbā (forward direction).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_spanish_same_inventory : hausaNs.nHeads = spanishNs.nHeads

Hausa shares the Set-1 inventory with Spanish and Amharic (the cross-cutting set1_shared theorem at §8 already covers Hausa↔Amharic↔Spanish; this theorem completes Hausa↔Spanish explicitly for downstream convenience).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }]

Hausa satisfies Radical Interpretability on the same Set-1 inventory as Spanish and Amharic (@cite{kramer-2020} §3.3.3).

theorem Phenomena.Gender.Studies.Kramer2020.hausa_ninventory_matches_profile : hausaNs.surfaceGenders = Phenomena.Gender.Studies.Kramer2020.hausa✝.rawGenderCount

Bridge: the Hausa DM n-inventory predicts the same surface gender count as the WALS-style typological profile from Corbett1991.

theorem Phenomena.Gender.Studies.Kramer2020.hausa_surface_genders_consistent : Typology.Gender.GenderCount.two.Contains hausaNs.surfaceGenders

Hausa surface genders fall in the WALS 2-gender bin.

theorem Phenomena.Gender.Studies.Kramer2020.hausa_assignment_consistent : hausaNs.hasArbitraryGender = true ∧ Phenomena.Gender.Studies.Kramer2020.hausa✝.assignment = Typology.Gender.AssignmentSystem.semanticAndFormal

Hausa has u-features → semanticAndFormal assignment, consistent with the Corbett1991/WALS profile.