Russian Negation Fragment

@cite{miestamo-2005} @cite{haspelmath-2013} @cite{dryer-haspelmath-2013}

Russian expresses standard negation with the preverbal particle не (ne). Negation is symmetric: adding не introduces no structural changes — no finiteness change, no TAM restrictions, no paradigmatic gaps.

Negative concord (Ch 115)

Russian has obligatory negative concord (WALS: co-occur):

• Никто не пришёл 'Nobody NEG came' = 'Nobody came'
• Ничего не видел 'Nothing NEG saw' = '(I) saw nothing'

N-words of the ни- series always co-occur with predicate negation не. The lexical-reactive side — никто, ничего, никогда, кто-либо, etc. — lives in Fragments/Russian/PolarityItems.lean per the operator/lexical- reactive split documented in Core/Lexical/NegMarker.lean. The NegConcordExample data below illustrates the marker's NC behavior at the sentence level, which is operator-side typology consumed by Phenomena/Negation/Studies/Miestamo2005.lean.

def Fragments.Slavic.Russian.Negation.ne : Typology.Negation.NegMarkerEntry

не — Russian's standard preverbal negation particle. A free word, syntactically immediately preverbal.

Equations

• Fragments.Slavic.Russian.Negation.ne = { form := "не", morphemeType := Typology.Negation.NegMorphemeType.particle, position := Typology.Negation.NegMarkerPosition.preverbal }

def Fragments.Slavic.Russian.Negation.negationSystem : Typology.Negation.NegationSystem

The Russian negation system: a single preverbal particle. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.Slavic.Russian.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "rus" [Fragments.Slavic.Russian.Negation.ne]

structure Fragments.Slavic.Russian.Negation.NegExample : Type

A Russian negation example.

• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String
• tenseLabel : String

def Fragments.Slavic.Russian.Negation.instReprNegExample.repr : NegExample → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Slavic.Russian.Negation.instReprNegExample : Repr NegExample

Equations

• Fragments.Slavic.Russian.Negation.instReprNegExample = { reprPrec := Fragments.Slavic.Russian.Negation.instReprNegExample.repr }

@[implicit_reducible]

instance Fragments.Slavic.Russian.Negation.instBEqNegExample : BEq NegExample

Equations

• Fragments.Slavic.Russian.Negation.instBEqNegExample = { beq := Fragments.Slavic.Russian.Negation.instBEqNegExample.beq }

def Fragments.Slavic.Russian.Negation.instBEqNegExample.beq : NegExample → NegExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Slavic.Russian.Negation.instBEqNegExample.beq x✝¹ x✝ = false

def Fragments.Slavic.Russian.Negation.present : NegExample

Present tense.

Equations

• Fragments.Slavic.Russian.Negation.present = { affirmative := "Он ест", negative := "Он не ест", glossAff := "3SG eat.PRS", glossNeg := "3SG NEG eat.PRS", tenseLabel := "present" }

def Fragments.Slavic.Russian.Negation.past : NegExample

Past tense.

Equations

• Fragments.Slavic.Russian.Negation.past = { affirmative := "Он ел", negative := "Он не ел", glossAff := "3SG eat.PST.M", glossNeg := "3SG NEG eat.PST.M", tenseLabel := "past" }

def Fragments.Slavic.Russian.Negation.future : NegExample

Future (periphrastic).

Equations

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

def Fragments.Slavic.Russian.Negation.imperative : NegExample

Imperative.

Equations

• Fragments.Slavic.Russian.Negation.imperative = { affirmative := "Ешь!", negative := "Не ешь!", glossAff := "eat.IMP.2SG", glossNeg := "NEG eat.IMP.2SG", tenseLabel := "imperative" }

def Fragments.Slavic.Russian.Negation.allExamples : List NegExample

Equations

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

structure Fragments.Slavic.Russian.Negation.NegConcordExample : Type

A negative concord example.

• sentence : String
• translation : String
• nword : String
• nwordGloss : String

def Fragments.Slavic.Russian.Negation.instReprNegConcordExample.repr : NegConcordExample → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Slavic.Russian.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

• Fragments.Slavic.Russian.Negation.instReprNegConcordExample = { reprPrec := Fragments.Slavic.Russian.Negation.instReprNegConcordExample.repr }

def Fragments.Slavic.Russian.Negation.instBEqNegConcordExample.beq : NegConcordExample → NegConcordExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Slavic.Russian.Negation.instBEqNegConcordExample.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.Slavic.Russian.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

• Fragments.Slavic.Russian.Negation.instBEqNegConcordExample = { beq := Fragments.Slavic.Russian.Negation.instBEqNegConcordExample.beq }

def Fragments.Slavic.Russian.Negation.nikto : NegConcordExample

Никто не пришёл — obligatory negative concord.

Equations

• Fragments.Slavic.Russian.Negation.nikto = { sentence := "Никто не пришёл", translation := "Nobody came", nword := "никто", nwordGloss := "nobody" }

def Fragments.Slavic.Russian.Negation.nichego : NegConcordExample

Ничего не видел — obligatory negative concord.

Equations

• Fragments.Slavic.Russian.Negation.nichego = { sentence := "Ничего не видел", translation := "(I) saw nothing", nword := "ничего", nwordGloss := "nothing.GEN" }

def Fragments.Slavic.Russian.Negation.nikogda : NegConcordExample

Никогда не приходил — obligatory negative concord.

Equations

• Fragments.Slavic.Russian.Negation.nikogda = { sentence := "Никогда не приходил", translation := "(He) never came", nword := "никогда", nwordGloss := "never" }

def Fragments.Slavic.Russian.Negation.allConcordExamples : List NegConcordExample

Equations

• Fragments.Slavic.Russian.Negation.allConcordExamples = [Fragments.Slavic.Russian.Negation.nikto, Fragments.Slavic.Russian.Negation.nichego, Fragments.Slavic.Russian.Negation.nikogda]

Verification

theorem Fragments.Slavic.Russian.Negation.ne_form : ne.form = "не"

theorem Fragments.Slavic.Russian.Negation.all_examples_count : allExamples.length = 4

theorem Fragments.Slavic.Russian.Negation.all_negative_contain_ne : (allExamples.all fun (e : NegExample) => Fragments.Slavic.Russian.Negation.hasSubstr✝ e.negative "не" || Fragments.Slavic.Russian.Negation.hasSubstr✝ e.negative "Не") = true

All negative examples contain не (or sentence-initial Не).

theorem Fragments.Slavic.Russian.Negation.all_concord_contain_ne : (allConcordExamples.all fun (e : NegConcordExample) => Fragments.Slavic.Russian.Negation.hasSubstr✝ e.sentence "не") = true

All negative concord examples contain не alongside the n-word.

theorem Fragments.Slavic.Russian.Negation.all_nwords_ni_prefix : (allConcordExamples.all fun (e : NegConcordExample) => e.nword.startsWith "ни") = true

All n-words begin with ни-.

def Fragments.Slavic.Russian.Negation.negationProfile : Typology.Negation.NegationProfile

Russian negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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