Russian Noun Gender

[Wad20] [Cor91] [Kra20] [Kra15]

Russian has three surface genders: masculine, feminine, neuter. Gender is partly determined by the referent's biological sex (semantic core) and partly by morphological declension class.

Theory-neutral data layer

The Fragment carries empirical fields per entry:

• attestedGender : Gender — the agreement-trigger fact (verified against [Wad20]). Three values for Russian: masculine, feminine, neuter.
• isNaturalGender : Bool — whether the gender comes from the referent's biological sex.
• declClass : Option DeclClass — Russian-specific morphological classification ([Wad20]). Optional because semantic-core nouns get their gender from the referent, not morphology.

These fields suffice to project entries to [Kra15] Ch. 7's 5-n DM analysis (projection in Studies/Kramer2020.lean); they also support [Cor91]'s controller-target classification directly.

Hybrid nouns

vrač 'doctor' triggers feminine agreement on some targets (verb, predicate adjective) when the referent is female, while retaining masculine morphology ([Wad20], e.g. "Врач обязана..." with fem.-agreeing predicate; [Cor91]). The Fragment encodes vrač's morphological gender (masculine, derived from Class I); the hybrid agreement story lives in Studies/Kramer2020.lean §7 via the existing russianVrac : HybridNoun struct.

Per-entry verification

Entries explicitly named in [Kra15]: otec, put', vrač. All others are extrapolations from Kramer's framework, anchored on [Wad20]'s declension and gender treatment + [Cor91]'s canonical 5-language sample. kost' (Class III feminine) verified at Wade ≈ noun-declension tables; put' (Class III masculine, sole exception) verified at Wade §6397; znamja (-мя neuter) is the textbook Class III neuter group.

inductive Russian.Gender.DeclClass : Type

Russian declension classes. Gender correlates with class but neither fully determines the other ([Cor91]; [Kra20] §2.3.2).

• I : DeclClass
• II : DeclClass
• III : DeclClass
• IV : DeclClass

@[implicit_reducible]

instance Russian.Gender.instDecidableEqDeclClass : DecidableEq DeclClass

Equations

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

def Russian.Gender.instReprDeclClass.repr : DeclClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Russian.Gender.instReprDeclClass : Repr DeclClass

Equations

• Russian.Gender.instReprDeclClass = { reprPrec := Russian.Gender.instReprDeclClass.repr }

structure Russian.Gender.RussianNoun : Type

A Russian noun. Empirical agreement-gender + natural-gender + optional declension class. No commitment to any specific theoretical framework — Kramer's DM categorizing head, Corbett's controller-target are projections in Studies/.

• form : String
• gloss : String
• attestedGender : Gender

  Empirical agreement-trigger fact ([Wad20]).

• isNaturalGender : Bool

  True iff the gender comes from biological sex of the referent. For vrač 'doctor' (hybrid) the morphological gender is encoded here as masculine; the hybrid female-referent agreement lives in Studies/Kramer2020.lean §7.

• declClass : Option DeclClass

  Optional declension class. Semantic-core nouns may omit since their gender is determined by the referent.

@[implicit_reducible]

instance Russian.Gender.instDecidableEqRussianNoun : DecidableEq RussianNoun

Equations

• Russian.Gender.instDecidableEqRussianNoun = Russian.Gender.instDecidableEqRussianNoun.decEq

def Russian.Gender.instDecidableEqRussianNoun.decEq (x✝ x✝¹ : RussianNoun) : Decidable (x✝ = x✝¹)

Equations

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

def Russian.Gender.instReprRussianNoun.repr : RussianNoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Russian.Gender.instReprRussianNoun : Repr RussianNoun

Equations

• Russian.Gender.instReprRussianNoun = { reprPrec := Russian.Gender.instReprRussianNoun.repr }

@[reducible, inline]

abbrev Russian.Gender.RussianNoun.gender (n : RussianNoun) : Gender

Equations

• n.gender = n.attestedGender

def Russian.Gender.otec : RussianNoun

Equations

• Russian.Gender.otec = { form := "otec", gloss := "father", attestedGender := Gender.masculine, isNaturalGender := true }

def Russian.Gender.mat' : RussianNoun

Equations

• Russian.Gender.mat' = { form := "mat'", gloss := "mother", attestedGender := Gender.feminine, isNaturalGender := true }

def Russian.Gender.brat : RussianNoun

Equations

• Russian.Gender.brat = { form := "brat", gloss := "brother", attestedGender := Gender.masculine, isNaturalGender := true }

def Russian.Gender.sestra : RussianNoun

Equations

• Russian.Gender.sestra = { form := "sestra", gloss := "sister", attestedGender := Gender.feminine, isNaturalGender := true }

def Russian.Gender.byk : RussianNoun

Equations

• Russian.Gender.byk = { form := "byk", gloss := "bull", attestedGender := Gender.masculine, isNaturalGender := true }

def Russian.Gender.korova : RussianNoun

Equations

• Russian.Gender.korova = { form := "korova", gloss := "cow", attestedGender := Gender.feminine, isNaturalGender := true }

def Russian.Gender.zakon : RussianNoun

Equations

• Russian.Gender.zakon = { form := "zakon", gloss := "law", attestedGender := Gender.masculine, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.I }

def Russian.Gender.škola : RussianNoun

Equations

• Russian.Gender.škola = { form := "škola", gloss := "school", attestedGender := Gender.feminine, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.II }

def Russian.Gender.kost' : RussianNoun

Equations

• Russian.Gender.kost' = { form := "kost'", gloss := "bone", attestedGender := Gender.feminine, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.III }

def Russian.Gender.vino : RussianNoun

Equations

• Russian.Gender.vino = { form := "vino", gloss := "wine", attestedGender := Gender.neuter, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.IV }

def Russian.Gender.znamja : RussianNoun

znamja 'banner': Class III but neuter, not feminine (the -мя neuter group; [Cor91]; [Kra20] ex. 19a).

Equations

• Russian.Gender.znamja = { form := "znamja", gloss := "banner", attestedGender := Gender.neuter, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.III }

def Russian.Gender.put' : RussianNoun

put' 'way': the only masculine noun in Class III ([Wad20] §6397: "путь is qualified by masculine adjectives"; [Cor91]; [Kra20] ex. 19b).

Equations

• Russian.Gender.put' = { form := "put'", gloss := "way", attestedGender := Gender.masculine, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.III }

def Russian.Gender.vrač : RussianNoun

vrač 'doctor': morphologically masculine (Class I), but triggers feminine agreement on some targets when the referent is female (verified at [Wad20] "Врач обязана…" with feminine-agreeing predicate). The Fragment encodes morphological gender; the hybrid behavior is captured in Studies/Kramer2020.lean §7.

Equations

• Russian.Gender.vrač = { form := "vrač", gloss := "doctor", attestedGender := Gender.masculine, isNaturalGender := false, declClass := some Russian.Gender.DeclClass.I }

def Russian.Gender.semanticCoreNouns : List RussianNoun

Equations

• Russian.Gender.semanticCoreNouns = [Russian.Gender.otec, Russian.Gender.mat', Russian.Gender.brat, Russian.Gender.sestra, Russian.Gender.byk, Russian.Gender.korova]

def Russian.Gender.remainderNouns : List RussianNoun

Equations

• Russian.Gender.remainderNouns = [Russian.Gender.zakon, Russian.Gender.škola, Russian.Gender.kost', Russian.Gender.vino, Russian.Gender.znamja, Russian.Gender.put']

def Russian.Gender.allNouns : List RussianNoun

Equations

• Russian.Gender.allNouns = Russian.Gender.semanticCoreNouns ++ Russian.Gender.remainderNouns ++ [Russian.Gender.vrač]

theorem Russian.Gender.declClass_ne_gender : znamja.declClass = kost'.declClass ∧ znamja.attestedGender ≠ kost'.attestedGender

Declension class does not determine gender: znamja and kost' share Class III but differ in surface gender (the Class III counter-correlation [Cor91] highlights). Stated directly over attestedGender (no DM intermediary).

inductive Russian.Gender.Value : Type

Russian's three controller genders — the carrier of its Gender.System ([Cor91]; [Kra15] ch. 7).

• masc : Value
• fem : Value
• neut : Value

@[implicit_reducible]

instance Russian.Gender.instDecidableEqValue : DecidableEq Value

Equations

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

def Russian.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Russian.Gender.instReprValue.repr Russian.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Russian.Gender.Value.masc")).group prec✝
• Russian.Gender.instReprValue.repr Russian.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Russian.Gender.Value.fem")).group prec✝
• Russian.Gender.instReprValue.repr Russian.Gender.Value.neut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Russian.Gender.Value.neut")).group prec✝

@[implicit_reducible]

instance Russian.Gender.instReprValue : Repr Value

Equations

• Russian.Gender.instReprValue = { reprPrec := Russian.Gender.instReprValue.repr }

@[implicit_reducible]

instance Russian.Gender.instFintypeValue : Fintype Value

Equations

• Russian.Gender.instFintypeValue = { elems := { val := ↑Russian.Gender.Value.enumList, nodup := Russian.Gender.Value.enumList_nodup }, complete := Russian.Gender.instFintypeValue._proof_1 }

inductive Russian.Gender.PastConcord : Type

Past-tense verbal concord exponents: -∅ / -a / -o ([Wad20]). Evidence type for Gender.Faithful.

• zero : PastConcord
• a : PastConcord
• o : PastConcord

@[implicit_reducible]

instance Russian.Gender.instDecidableEqPastConcord : DecidableEq PastConcord

Equations

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

@[implicit_reducible]

instance Russian.Gender.instReprPastConcord : Repr PastConcord

Equations

• Russian.Gender.instReprPastConcord = { reprPrec := Russian.Gender.instReprPastConcord.repr }

def Russian.Gender.instReprPastConcord.repr : PastConcord → ℕ → Std.Format

Equations

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

def Russian.Gender.Value.pastConcord : Value → PastConcord

Per-gender past-tense concord.

Equations

• Russian.Gender.Value.masc.pastConcord = Russian.Gender.PastConcord.zero
• Russian.Gender.Value.fem.pastConcord = Russian.Gender.PastConcord.a
• Russian.Gender.Value.neut.pastConcord = Russian.Gender.PastConcord.o

def Russian.Gender.system : Gender.System Value

The Russian gender system over its own carrier: full comparative labelling; neuter is the morphosyntactic default (plain-n roots like vino surface neuter — [Kra15]'s ch. 7 derivation, exercised at Kramer2020.russian_licensing_vino).

Equations

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

def Russian.Gender.Value.ofLabel : Gender → Value

Comparative label → controller gender (ingestion).

Equations

• Russian.Gender.Value.ofLabel Gender.feminine = Russian.Gender.Value.fem
• Russian.Gender.Value.ofLabel Gender.neuter = Russian.Gender.Value.neut
• Russian.Gender.Value.ofLabel x✝ = Russian.Gender.Value.masc

def Russian.Gender.RussianNoun.controllerGender (n : RussianNoun) : Value

Controller gender of a noun, from the attested agreement fact. For the hybrid vrač this is the morphological masculine; the female-referent agreement alternation lives in Studies/Kramer2020.lean §7.

Equations

• n.controllerGender = Russian.Gender.Value.ofLabel n.attestedGender

def Russian.Gender.assigned : Gender.System.Assigned RussianNoun Value

The assigned system: every noun gets its controller gender.

Equations

• Russian.Gender.assigned = { toSystem := Russian.Gender.system, assign := Russian.Gender.RussianNoun.controllerGender }

theorem Russian.Gender.faithful_pastConcord : Gender.Faithful fun (g : Value) (x : Unit) => g.pastConcord

The carrier is faithful to the past-tense concord evidence: -∅ / -a / -o distinguishes all three genders on a single target. [Cor91]'s genders-are-agreement-classes criterion, discharged via Gender.Faithful.

theorem Russian.Gender.system_label_assign (n : RussianNoun) : n ∈ allNouns → system.label n.controllerGender = some n.attestedGender

Label ∘ assign recovers the attested gender across the inventory.

theorem Russian.Gender.assigned_semanticCore : assigned.SemanticCore {n : RussianNoun | n.isNaturalGender = true} fun (x : RussianNoun) => x.attestedGender

[Kra15]'s (7ii) / [Dah00]'s generalization instantiated: on the natural-gender core, assignment factors through the attested gender (= referent sex on that core). The hybrid vrač and the declension-class remainder are outside the core.