Slavic Verbalizer (VBLZ) — Empirical Data @cite{stojkovic-2026}

Theory-neutral empirical data for the Slavic verbalizer suffix used in secondary imperfectivisation. Stojković (2026) documents a three-way surface alternation across Slavic:

Group	INF stem VC	Languages
[ov] group	[ov]	Polish, Czech, Slovak, U/L Sorbian,...
[ov]/[ev]	[ov]∼[ev]	BCMS, Slovenian, Russian,...
[uv] group	[uv]	Ukrainian, Lemko Rusyn, Bulgarian, Maced.

All groups share the present-stem vowel [u] (before /-je-/). The variation is confined to the infinitive stem (before /-a-/).

inductive Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang : Type

Representative Slavic languages exhibiting secondary imperfectivisation.

• russian : SlavicLang
• polish : SlavicLang
• czech : SlavicLang
• upperSorbian : SlavicLang
• bcms : SlavicLang
• slovenian : SlavicLang
• slovak : SlavicLang
• lowerSorbian : SlavicLang
• ukrainian : SlavicLang
• lemkoRusyn : SlavicLang
• bulgarian : SlavicLang
• macedonian : SlavicLang

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqSlavicLang : DecidableEq SlavicLang

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqSlavicLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqSlavicLang.beq : SlavicLang → SlavicLang → Bool

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqSlavicLang.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqSlavicLang : BEq SlavicLang

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqSlavicLang = { beq := Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqSlavicLang.beq }

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprSlavicLang : Repr SlavicLang

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprSlavicLang = { reprPrec := Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprSlavicLang.repr }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprSlavicLang.repr : SlavicLang → Nat → Std.Format

Equations

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

inductive Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup : Type

The three surface-form groups for the VBLZ in the infinitive stem. Stojković (2026), Table 3.

• ovGroup : VBLZGroup

  Always [ov], regardless of preceding consonant.

• ovEvGroup : VBLZGroup

  [ov] after non-palatals, [ev] after palatals.

• uvGroup : VBLZGroup

  Always [uv], regardless of preceding consonant.

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqVBLZGroup : DecidableEq VBLZGroup

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqVBLZGroup x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZGroup : BEq VBLZGroup

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZGroup = { beq := Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZGroup.beq }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZGroup.beq : VBLZGroup → VBLZGroup → Bool

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZGroup.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZGroup.repr : VBLZGroup → Nat → Std.Format

Equations

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

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZGroup : Repr VBLZGroup

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZGroup = { reprPrec := Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZGroup.repr }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.forms : VBLZGroup → List String

Surface VC forms attested in the infinitive stem for each group.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovGroup.forms = ["ov"]
• Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovEvGroup.forms = ["ov", "ev"]
• Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.uvGroup.forms = ["uv"]

def Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.vblzGroup : SlavicLang → VBLZGroup

Group membership for each language.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.polish.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.czech.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.slovak.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.upperSorbian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.lowerSorbian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.russian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovEvGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.bcms.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovEvGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.slovenian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.ovEvGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.ukrainian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.uvGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.lemkoRusyn.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.uvGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.bulgarian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.uvGroup
• Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.macedonian.vblzGroup = Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZGroup.uvGroup

structure Phenomena.Allomorphy.SlavicVerbalizer.Data.VBLZDatum : Type

A VBLZ datum: language, infinitive-stem VC, present-stem V. The present stem V is the vowel that surfaces before the present-tense suffix /-je-/; the infinitive stem VC is before /-a-/ (thematic).

• lang : SlavicLang
• infStem : String
• presStem : String

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqVBLZDatum.decEq (x✝ x✝¹ : VBLZDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqVBLZDatum : DecidableEq VBLZDatum

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqVBLZDatum = Phenomena.Allomorphy.SlavicVerbalizer.Data.instDecidableEqVBLZDatum.decEq

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZDatum : BEq VBLZDatum

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZDatum = { beq := Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZDatum.beq }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZDatum.beq : VBLZDatum → VBLZDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Allomorphy.SlavicVerbalizer.Data.instBEqVBLZDatum.beq x✝¹ x✝ = false

def Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZDatum.repr : VBLZDatum → Nat → Std.Format

Equations

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

instance Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZDatum : Repr VBLZDatum

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZDatum = { reprPrec := Phenomena.Allomorphy.SlavicVerbalizer.Data.instReprVBLZDatum.repr }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.polishVBLZ : VBLZDatum

Polish: kup-ov-a-ć / kup-uj-e 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.polishVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.polish, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.czechVBLZ : VBLZDatum

Czech: kup-ov-a-t / kup-uj-e 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.czechVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.czech, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.slovakVBLZ : VBLZDatum

Slovak: kup-ov-a-ť / kup-uj-e 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.slovakVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.slovak, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.upperSorbianVBLZ : VBLZDatum

Upper Sorbian: kup-ov-a-ć / kup-uj-e 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.upperSorbianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.upperSorbian, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.lowerSorbianVBLZ : VBLZDatum

Lower Sorbian: kup-ov-a-ś / kup-uj-o 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.lowerSorbianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.lowerSorbian, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.russianVBLZ : VBLZDatum

Russian: kup-ov-a-t' / kup-uj-et 'buy' (non-palatal base). After palatals: torg-ev-a-t' / torg-uj-et 'trade'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.russianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.russian, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.bcmsVBLZ : VBLZDatum

BCMS: kup-ov-a-ti / kup-uj-e 'buy' (non-palatal). After palatals: poštov-ev-a-ti (palatal assimilation).

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.bcmsVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.bcms, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.slovenianVBLZ : VBLZDatum

Slovenian: kup-ov-a-ti / kup-uj-e 'buy' (non-palatal). After palatals: dež-ev-a-ti 'rain'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.slovenianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.slovenian, infStem := "ov", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.ukrainianVBLZ : VBLZDatum

Ukrainian: kup-uv-a-ty / kup-uj-e 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.ukrainianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.ukrainian, infStem := "uv", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.lemkoRusynVBLZ : VBLZDatum

Lemko Rusyn: ris-uv-a-ty / ris-uj-e 'draw'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.lemkoRusynVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.lemkoRusyn, infStem := "uv", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.bulgarianVBLZ : VBLZDatum

Bulgarian: kup-uv-a-m / kup-uv-a-m 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.bulgarianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.bulgarian, infStem := "uv", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.macedonianVBLZ : VBLZDatum

Macedonian: kup-uv-a / kup-uv-a 'buy'.

Equations

• Phenomena.Allomorphy.SlavicVerbalizer.Data.macedonianVBLZ = { lang := Phenomena.Allomorphy.SlavicVerbalizer.Data.SlavicLang.macedonian, infStem := "uv", presStem := "u" }

def Phenomena.Allomorphy.SlavicVerbalizer.Data.allData : List VBLZDatum

All VBLZ data points.

Equations

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

theorem Phenomena.Allomorphy.SlavicVerbalizer.Data.allData_length : allData.length = 12

theorem Phenomena.Allomorphy.SlavicVerbalizer.Data.presentStemUniversal : (allData.all fun (d : VBLZDatum) => d.presStem == "u") = true

The present-stem vowel is universally [u] across all three groups (before the present-tense suffix /-je-/). This uniformity is the starting point of Stojković's analysis: the variation is confined to the infinitive stem.

theorem Phenomena.Allomorphy.SlavicVerbalizer.Data.infStem_matches_group : (allData.all fun (d : VBLZDatum) => d.lang.vblzGroup.forms.contains d.infStem) = true

Each datum's infinitive stem is consistent with its language's group.