Gender — feature decompositions of the labels

[Smi15] [Smi21] [Kra15] [AA25] [Ham19]

Rival feature analyses of gender values. None is baked into Gender.System — the carrier is analysis-neutral, and each scheme here is a presentation a study can adopt or refute.

• The split-feature architecture ([Smi15]; book version [Smi21]): a grammatical feature has two halves — uF legible to morphology, iF legible to semantics — which "in general match up" but "can be distinct or one can be missing altogether". SplitFeature V encodes this for any value vocabulary. [Kra15]'s interpretability classification falls out as the special cases (IsNatural, IsArbitrary), and hybrid values (IsHybrid — [Smi21]'s mismatch zoo: committee-type collectives for number, Russian profession nouns for gender, Hebrew be'alim, Chichewa heroes) are exactly what the special cases cannot represent.
• Kramer's gender calculus ([Kra15]): valued gender features are signed binary dimensions (Signed over Dimension — FEM, ANIM, and [Ada24]'s MASC), whose surface labels underdetermine them (Signed.surface_femNeg_eq_mascPos). The interpretability-annotated FEM slice is KramerN = {plain, i[±FEM], u[±FEM]}. Natural and arbitrary gender differ only in interpretability and receive the same exponence at PF (KramerN.exponence), which yields the calculus's signature limit, here a theorem (KramerN.card_image_exponence_le_three): no inventory of gender-relevant ns distinguishes more than three agreement classes — Kramer's own argument that >3-gender systems need per-class identity features, i.e. a language-particular carrier (Gender.System).

Implementation notes

• SplitFeature is φ-generic (its motivating mismatch, committee uF:SG × iF:PL, is a number value): it lives here until a second feature module consumes it, then hoists to a shared file.
• The bivalent [±feminine, ±neuter] presentation ([Sau03]): Gender.Features, a ContainmentPairLike label scheme for sex-based three-gender systems — one edge of the φ-feature iso-web (phiKernelEquiv, Studies/Harbour2016.lean), parallel to Person.Features and Number.Features. Its no_fourth_gender is a claim about this scheme, not about gender writ large (Fula has 20 controller genders).
• [Ham19] rejects both interpretability schemes (masculine = bare GENDER node, no masculine feature; natural/arbitrary derived at LF, not represented) — a single-paper analysis, so it belongs in Studies/Hammerly2019.lean, stated over the same Gender.System carriers as its rivals.

The split-feature architecture

structure Gender.SplitFeature (V : Type u_1) : Type u_1

A feature split into a morphology-legible half uF and a semantics-legible half iF ([Smi15]). The halves usually match, but may differ (hybrid values) or be singly absent.

• uF : Option V

  The half legible to morphology (agreement, exponence).

• iF : Option V

  The half legible to semantics (interpretation).

def Gender.instDecidableEqSplitFeature.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : SplitFeature V✝) : Decidable (x✝ = x✝¹)

Equations

• Gender.instDecidableEqSplitFeature.decEq { uF := a, iF := a_1 } { uF := b, iF := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Gender.instDecidableEqSplitFeature {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (SplitFeature V✝)

Equations

• Gender.instDecidableEqSplitFeature = Gender.instDecidableEqSplitFeature.decEq

@[instance_reducible]

instance Gender.instReprSplitFeature {V✝ : Type u_1} [Repr V✝] : Repr (SplitFeature V✝)

Equations

• Gender.instReprSplitFeature = { reprPrec := Gender.instReprSplitFeature.repr }

def Gender.instReprSplitFeature.repr {V✝ : Type u_1} [Repr V✝] : SplitFeature V✝ → ℕ → Std.Format

Equations

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

def Gender.SplitFeature.IsNatural {V : Type u_1} (s : SplitFeature V) : Prop

Natural (conceptual) value: both halves present and matched — [Kra15]'s interpretable gender in split-feature terms.

Equations

• s.IsNatural = ∃ (v : V), s.uF = some v ∧ s.iF = some v

def Gender.SplitFeature.IsArbitrary {V : Type u_1} (s : SplitFeature V) : Prop

Arbitrary value: morphological half only — [Kra15]'s uninterpretable gender in split-feature terms.

Equations

• s.IsArbitrary = ((∃ (v : V), s.uF = some v) ∧ s.iF = none)

def Gender.SplitFeature.IsSemanticOnly {V : Type u_1} (s : SplitFeature V) : Prop

Semantic-only value: interpreted but morphologically inert (the half [Smi15] allows to go missing on the uF side).

Equations

• s.IsSemanticOnly = (s.uF = none ∧ ∃ (v : V), s.iF = some v)

def Gender.SplitFeature.IsHybrid {V : Type u_1} (s : SplitFeature V) : Prop

Hybrid value: both halves present and mismatched — committee-type nouns ([Smi15]); unrepresentable in an interpretability classification of single feature tokens.

Equations

• s.IsHybrid = ∃ (u : V) (i : V), s.uF = some u ∧ s.iF = some i ∧ u ≠ i

def Gender.SplitFeature.IsAbsent {V : Type u_1} (s : SplitFeature V) : Prop

Featureless: both halves absent.

Equations

• s.IsAbsent = (s.uF = none ∧ s.iF = none)

theorem Gender.SplitFeature.classify {V : Type u_1} (s : SplitFeature V) : s.IsNatural ∨ s.IsHybrid ∨ s.IsArbitrary ∨ s.IsSemanticOnly ∨ s.IsAbsent

The five cases are exhaustive: every split feature is natural, hybrid, arbitrary, semantic-only, or absent.

theorem Gender.SplitFeature.IsHybrid.not_isNatural {V : Type u_1} {s : SplitFeature V} (h : s.IsHybrid) : ¬s.IsNatural

A hybrid value is not natural: the mismatch is real.

The bivalent presentation: [±feminine, ±neuter]

[Sau03]'s decomposition of sex-based gender: [±feminine] (feminine and neuter are [+feminine]) and [±neuter] (only neuter is [+neuter]), with the containment [+neuter] → [+feminine]: neuter is the most specified gender (like singular for number, 1st for person) and masculine the least. The three well-formed combinations are the three genders of a sex-based system; the scheme parallels person [±author] ⊂ [±participant] and number [±atomic] ⊂ [±minimal] — all three are ContainmentPairLike presentations of the same skeleton (Features/ContainmentPair.lean).

structure Gender.Features : Type

Bivalent gender features: [±feminine, ±neuter] ([Sau03]).

The three well-formed combinations yield the three sex-based genders: neuter [+feminine, +neuter], feminine [+feminine, −neuter], masculine [−feminine, −neuter].

• isFeminine : Bool

  [+feminine]: referent triggers feminine (or neuter) agreement.

• isNeuter : Bool

  [+neuter]: referent triggers neuter agreement.

@[instance_reducible]

instance Gender.instDecidableEqFeatures : DecidableEq Features

Equations

• Gender.instDecidableEqFeatures = Gender.instDecidableEqFeatures.decEq

def Gender.instDecidableEqFeatures.decEq (x✝ x✝¹ : Features) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Gender.instReprFeatures : Repr Features

Equations

• Gender.instReprFeatures = { reprPrec := Gender.instReprFeatures.repr }

def Gender.instReprFeatures.repr : Features → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gender.instFintypeFeatures : Fintype Features

Equations

• Gender.instFintypeFeatures = Fintype.ofEquiv ((_ : Bool) × Bool) Gender.Features.proxyTypeEquiv

def Gender.neuterF : Features

Neuter features: [+feminine, +neuter].

Equations

• Gender.neuterF = { isFeminine := true, isNeuter := true }

def Gender.feminineF : Features

Feminine features: [+feminine, −neuter].

Equations

• Gender.feminineF = { isFeminine := true, isNeuter := false }

def Gender.masculineF : Features

Masculine features: [−feminine, −neuter].

Equations

• Gender.masculineF = { isFeminine := false, isNeuter := false }

def Gender.featuresEquiv : Features ≃ Features.ContainmentPair

The [±feminine, ±neuter] decomposition is carrier-equivalent to the containment pair: outer = feminine, inner = neuter — one edge of the φ-feature iso-web (phiKernelEquiv, Studies/Harbour2016.lean).

Equations

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

@[instance_reducible]

instance Gender.instContainmentPairLikeFeatures : Features.ContainmentPairLike Features

Equations

• Gender.instContainmentPairLikeFeatures = Features.ContainmentPairLike.ofEquiv Gender.featuresEquiv

@[simp]

theorem Gender.neuter_is_maximal : Features.ContainmentPairLike.toPair neuterF = Features.ContainmentPair.maximal

The three canonical gender values land on the three well-formed cells.

@[simp]

theorem Gender.feminine_is_intermediate : Features.ContainmentPairLike.toPair feminineF = Features.ContainmentPair.intermediate

@[simp]

theorem Gender.masculine_is_minimal : Features.ContainmentPairLike.toPair masculineF = Features.ContainmentPair.minimal

@[reducible, inline]

abbrev Gender.Features.WellFormed (gf : Features) : Prop

Well-formedness: [+neuter] → [+feminine] — neuter entails feminine in the feature geometry, inherited from ContainmentPair.WellFormed.

Equations

• gf.WellFormed = Features.ContainmentPairLike.WellFormed gf

theorem Gender.no_fourth_gender (a b c d : Features) : a.WellFormed → b.WellFormed → c.WellFormed → d.WellFormed → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

No 4-way distinction within this scheme (inherited from ContainmentPairLike.no_four_way) — a claim about the sex-based bivalent presentation, not about gender systems writ large.

@[simp]

theorem Gender.neuter_wellFormed : neuterF.WellFormed

@[simp]

theorem Gender.feminine_wellFormed : feminineF.WellFormed

@[simp]

theorem Gender.masculine_wellFormed : masculineF.WellFormed

theorem Gender.illFormed_only : ¬{ isFeminine := false, isNeuter := true }.WellFormed

The filtered combination [−feminine, +neuter] is the only one that violates containment.

theorem Gender.card_wellFormed : Fintype.card { gf : Features // gf.WellFormed } = 3

Exactly 3 well-formed feature combinations (= 3 genders) — the carrier count of the containment chain (ContainmentPair.card_wellFormed).

theorem Gender.neuter_implies_feminine (f : Features) : f.WellFormed → f.isNeuter = true → f.isFeminine = true

Containment: [+neuter] → [+feminine] for all well-formed features.

def Gender.Features.toGender : Features → Option Gender

Map gender features to the comparative labels.

Equations

• { isFeminine := true, isNeuter := true }.toGender = some Gender.neuter
• { isFeminine := true, isNeuter := false }.toGender = some Gender.feminine
• { isFeminine := false, isNeuter := false }.toGender = some Gender.masculine
• { isFeminine := false, isNeuter := true }.toGender = none

def Gender.Features.fromGender : Gender → Option Features

Map comparative labels to gender features (partial — only sex-based labels have feature equivalents).

Equations

• Gender.Features.fromGender Gender.neuter = some Gender.neuterF
• Gender.Features.fromGender Gender.feminine = some Gender.feminineF
• Gender.Features.fromGender Gender.masculine = some Gender.masculineF
• Gender.Features.fromGender x✝ = none

theorem Gender.roundtrip_fromGender_toGender : ([neuterF, feminineF, masculineF].all fun (f : Features) => f.toGender.bind Features.fromGender == some f) = true

Round-trip: fromGender ∘ toGender = some for all well-formed features.

Dimensions and signed features

Kramer's calculus ranges over language-particular binary dimensions: [±FEM] (Amharic, Spanish, Maa), [±ANIM] (Lealao Chinantec, Algonquian, Teop), and [Ada24]'s [±MASC] (Jarawara). A signed dimension is a valued gender feature, and its surface is the comparative label of the chosen pole. KramerN below is the interpretability-annotated FEM slice.

inductive Gender.Dimension : Type

A binary gender dimension: the contrast a language's gender features are drawn over ([Kra15]; [Ada24] for MASC).

• fem : Dimension
• masc : Dimension
• anim : Dimension

@[instance_reducible]

instance Gender.instDecidableEqDimension : DecidableEq Dimension

Equations

• Gender.instDecidableEqDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gender.instReprDimension : Repr Dimension

Equations

• Gender.instReprDimension = { reprPrec := Gender.instReprDimension.repr }

def Gender.instReprDimension.repr : Dimension → ℕ → Std.Format

Equations

• Gender.instReprDimension.repr Gender.Dimension.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Dimension.fem")).group prec✝
• Gender.instReprDimension.repr Gender.Dimension.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Dimension.masc")).group prec✝
• Gender.instReprDimension.repr Gender.Dimension.anim prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Dimension.anim")).group prec✝

@[instance_reducible]

instance Gender.instFintypeDimension : Fintype Dimension

Equations

• Gender.instFintypeDimension = { elems := { val := ↑Gender.Dimension.enumList, nodup := Gender.Dimension.enumList_nodup }, complete := Gender.instFintypeDimension._proof_1 }

inductive Gender.Pole : Type

The sign of a valued binary feature. Neither sign is inherently marked: which one a language's arbitrary gender carries is the Set 1 vs Set 2 parameter ([Kra15] Ch 6).

• pos : Pole
• neg : Pole

@[instance_reducible]

instance Gender.instDecidableEqPole : DecidableEq Pole

Equations

• Gender.instDecidableEqPole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gender.instReprPole : Repr Pole

Equations

• Gender.instReprPole = { reprPrec := Gender.instReprPole.repr }

def Gender.instReprPole.repr : Pole → ℕ → Std.Format

Equations

• Gender.instReprPole.repr Gender.Pole.pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Pole.pos")).group prec✝
• Gender.instReprPole.repr Gender.Pole.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.Pole.neg")).group prec✝

@[instance_reducible]

instance Gender.instFintypePole : Fintype Pole

Equations

• Gender.instFintypePole = { elems := { val := ↑Gender.Pole.enumList, nodup := Gender.Pole.enumList_nodup }, complete := Gender.instFintypePole._proof_1 }

def Gender.Dimension.positive : Dimension → Gender

The comparative label at a dimension's positive pole.

Equations

• Gender.Dimension.fem.positive = Gender.feminine
• Gender.Dimension.masc.positive = Gender.masculine
• Gender.Dimension.anim.positive = Gender.animate

def Gender.Dimension.negative : Dimension → Gender

The comparative label at a dimension's negative pole.

Equations

• Gender.Dimension.fem.negative = Gender.masculine
• Gender.Dimension.masc.negative = Gender.feminine
• Gender.Dimension.anim.negative = Gender.inanimate

structure Gender.Signed : Type

A valued gender feature: a dimension with a sign — [+FEM], [−FEM], [+ANIM], and so on.

• dim : Dimension
• pole : Pole

def Gender.instDecidableEqSigned.decEq (x✝ x✝¹ : Signed) : Decidable (x✝ = x✝¹)

Equations

• Gender.instDecidableEqSigned.decEq { dim := a, pole := a_1 } { dim := b, pole := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Gender.instDecidableEqSigned : DecidableEq Signed

Equations

• Gender.instDecidableEqSigned = Gender.instDecidableEqSigned.decEq

def Gender.instReprSigned.repr : Signed → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gender.instReprSigned : Repr Signed

Equations

• Gender.instReprSigned = { reprPrec := Gender.instReprSigned.repr }

@[instance_reducible]

instance Gender.instFintypeSigned : Fintype Signed

Equations

• Gender.instFintypeSigned = Fintype.ofEquiv ((_ : Gender.Dimension) × Gender.Pole) Gender.Signed.proxyTypeEquiv

def Gender.Signed.surface (v : Signed) : Gender

The comparative label a valued feature denotes: the pole its sign picks.

Equations

• v.surface = match v.pole with | Gender.Pole.pos => v.dim.positive | Gender.Pole.neg => v.dim.negative

theorem Gender.Signed.surface_femNeg_eq_mascPos : { dim := Dimension.fem, pole := Pole.neg }.surface = { dim := Dimension.masc, pole := Pole.pos }.surface

Surface labels underdetermine features: Maa's [−FEM] and Jarawara's [+MASC] both surface masculine ([Kra15] §6.3 vs [Ada24] §3.2) — drawing the featural distinction is what the dimension inventory is for.

def Gender.Signed.toNat : Signed → ℕ

The canonical numbering of the six valued features — the encoding consumers with numeral gender slots (the Minimalist φ-interface) use.

Equations

• { dim := Gender.Dimension.fem, pole := Gender.Pole.pos }.toNat = 0
• { dim := Gender.Dimension.fem, pole := Gender.Pole.neg }.toNat = 1
• { dim := Gender.Dimension.masc, pole := Gender.Pole.pos }.toNat = 2
• { dim := Gender.Dimension.masc, pole := Gender.Pole.neg }.toNat = 3
• { dim := Gender.Dimension.anim, pole := Gender.Pole.pos }.toNat = 4
• { dim := Gender.Dimension.anim, pole := Gender.Pole.neg }.toNat = 5

theorem Gender.Signed.toNat_injective : Function.Injective toNat

The numbering is faithful.

Kramer's gender calculus and its three-gender bound

inductive Gender.KramerN : Type

A gender-relevant nominalizing head in [Kra15]'s calculus: plain n, or n bearing an interpretable or uninterpretable [±FEM].

• plain : KramerN

  n with no gender features (Romanian default-gender nouns).

• iFem : KramerN

  n i[+FEM]: interpretable feminine (natural gender).

• iMasc : KramerN

  n i[−FEM]: interpretable masculine (natural gender).

• uFem : KramerN

  n u[+FEM]: uninterpretable feminine (arbitrary gender).

• uMasc : KramerN

  n u[−FEM]: uninterpretable masculine (arbitrary gender).

@[instance_reducible]

instance Gender.instDecidableEqKramerN : DecidableEq KramerN

Equations

• Gender.instDecidableEqKramerN x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Gender.instReprKramerN : Repr KramerN

Equations

• Gender.instReprKramerN = { reprPrec := Gender.instReprKramerN.repr }

def Gender.instReprKramerN.repr : KramerN → ℕ → Std.Format

Equations

• Gender.instReprKramerN.repr Gender.KramerN.plain prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.KramerN.plain")).group prec✝
• Gender.instReprKramerN.repr Gender.KramerN.iFem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.KramerN.iFem")).group prec✝
• Gender.instReprKramerN.repr Gender.KramerN.iMasc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.KramerN.iMasc")).group prec✝
• Gender.instReprKramerN.repr Gender.KramerN.uFem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.KramerN.uFem")).group prec✝
• Gender.instReprKramerN.repr Gender.KramerN.uMasc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Gender.KramerN.uMasc")).group prec✝

@[instance_reducible]

instance Gender.instFintypeKramerN : Fintype KramerN

Equations

• Gender.instFintypeKramerN = { elems := { val := ↑Gender.KramerN.enumList, nodup := Gender.KramerN.enumList_nodup }, complete := Gender.instFintypeKramerN._proof_1 }

def Gender.KramerN.exponence : KramerN → Option Bool

What agreement exponence sees: the feature value, not its interpretability — natural and arbitrary gender receive the same Vocabulary Item ([Kra15]). none = no gender features.

Equations

• Gender.KramerN.plain.exponence = none
• Gender.KramerN.iFem.exponence = some true
• Gender.KramerN.uFem.exponence = some true
• Gender.KramerN.iMasc.exponence = some false
• Gender.KramerN.uMasc.exponence = some false

def Gender.KramerN.toSplitFeature : KramerN → SplitFeature Bool

Each Kramer head reads as a split feature: interpretable heads value both halves, uninterpretable heads only the morphological half.

Equations

• Gender.KramerN.plain.toSplitFeature = { uF := none, iF := none }
• Gender.KramerN.iFem.toSplitFeature = { uF := some true, iF := some true }
• Gender.KramerN.iMasc.toSplitFeature = { uF := some false, iF := some false }
• Gender.KramerN.uFem.toSplitFeature = { uF := some true, iF := none }
• Gender.KramerN.uMasc.toSplitFeature = { uF := some false, iF := none }

theorem Gender.KramerN.toSplitFeature_not_isHybrid (n : KramerN) : ¬n.toSplitFeature.IsHybrid

The calculus generates no hybrids: every Kramer head is natural, arbitrary, or absent in split-feature terms — the representational gap [Smi15]'s architecture closes.

theorem Gender.KramerN.card_image_exponence_le_three (inv : Finset KramerN) : (Finset.image exponence inv).card ≤ 3

[Kra15]'s three-gender bound, as a theorem: any inventory of gender-relevant ns distinguishes at most three agreement classes ([+FEM], [−FEM], bare). More than three genders therefore requires machinery beyond the calculus — per-class identity features, i.e. a language-particular Gender.System carrier.