Slavic Verbalizer [Sto26a]

Stojković (2026) argues the Slavic verbalizer (VBLZ) suffix used in secondary imperfectivisation has a single abstract underlying representation (a defective diphthong) across all Slavic; surface alternation is derived by OT constraint ranking.

Empirical Data

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.

Where the VBLZ precedes the theme vowel /-je-/ in the present, the present stem is the single vowel [u] and the VC alternation is confined to the infinitive stem (before /-a-/). Bulgarian and Macedonian are the exception: having lost the INF/PRS distinction, they have /-a-/ after the VBLZ in both stems, so the VC sequence [uv] surfaces throughout (Table 1).

Candidates

The VBLZ in the pre-vocalic context (before the thematic /-a-/) can surface as one of five candidates, differing in how the unspecified slot of the diphthong is resolved:

Candidate	Vowel	Mechanism
[ov]	[o] = [+back, −high]	epenthesise [+back] and [−high]
[ev]	[e] = [−back, −high]	share [−back] from palatal, epenthesise [−high]
[uv]	[u] = [+back, +high]	epenthesise [+back] and [+high]
[iv]	[i] = [−back, +high]	share [−back] from palatal, epenthesise [+high]
[u]	monophthong	delete the unspecified slot

Constraints

Six constraints, of which two (NOHIATUS, SPECIFY) are undominated and four (*SHARE[−back], DEP[+back], DEP[−high], DEP[+high]) are variable:

• NOHIATUS (markedness): no adjacent vowels
• SPECIFY (markedness): every base node must be fully specified
• *SHARE[−back] (markedness): don't copy [−back] from adjacent segment
• DEP[+back] (faithfulness): don't epenthesise [+back]
• DEP[−high] (faithfulness): don't epenthesise [−high]
• DEP[+high] (faithfulness): don't epenthesise [+high]

Note: DEP[+high] is implicit in Stojković's analysis. Without it, [uv] harmonically bounds [ov] (strictly fewer violations at every constraint), making it impossible for any ranking to select [ov]. The paper derives the same effect from the markedness of [+high] vs [−high]: [−high] is the cross-linguistically unmarked epenthetic height (p. 14), while [+high] epenthesis incurs an implicit faithfulness cost. Making this explicit as DEP[+high] yields the correct factorial typology.

Factorial Typology

[Sto26a]'s own factorial typology (31) ranks three constraints (*SHARE[−back], DEP[+back], DEP[−high]) and derives the three attested patterns — [ov], the context-sensitive [ov][ev], and [uv] — plus a hypothetical [uv][iv] (31f). In pure OT those three constraints leave [uv] harmonically bounding [ov] (§4.2, p. 14), which the paper resolves by the markedness of [−high] epenthesis rather than a constraint. Making that preference explicit as DEP[+high], the 4! = 24 permutations of the four variable constraints here yield four singleton optima — {[ov]}, {[ev]}, {[uv]}, {[iv]} — the first three attested, [iv] unattested ((32): the hypothetical Ukrainian [uv]~[iv] pairs).

Candidates

inductive Stojkovic2026.VBLZCandidate : Type

Candidate surface realisations of the VBLZ, each a resolution of the defective diphthong. This is the typed surface-form inventory used throughout the file (no stringly-typed forms).

• ov : VBLZCandidate

  [ov]: diphthong fissions, slot 1 → [o] via epenthetic [+back, −high].

• ev : VBLZCandidate

  [ev]: diphthong fissions, slot 1 → [e] via shared [−back], epenthetic [−high].

• uv : VBLZCandidate

  [uv]: diphthong fissions, slot 1 → [u] via epenthetic [+back, +high].

• iv : VBLZCandidate

  [iv]: diphthong fissions, slot 1 → [i] via shared [−back], epenthetic [+high].

• uMono : VBLZCandidate

  [u]: monophthong — the unspecified slot is deleted. Before a vowel this yields a hiatus ([u.a], penalised by NOHIATUS); before a consonant (the /-je-/ present) it is the licit single vowel [u].

@[implicit_reducible]

instance Stojkovic2026.instDecidableEqVBLZCandidate : DecidableEq VBLZCandidate

Equations

• Stojkovic2026.instDecidableEqVBLZCandidate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stojkovic2026.instReprVBLZCandidate : Repr VBLZCandidate

Equations

• Stojkovic2026.instReprVBLZCandidate = { reprPrec := Stojkovic2026.instReprVBLZCandidate.repr }

def Stojkovic2026.instReprVBLZCandidate.repr : VBLZCandidate → ℕ → Std.Format

Equations

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

def Stojkovic2026.allCandidates : List VBLZCandidate

All candidates.

Equations

• Stojkovic2026.allCandidates = [Stojkovic2026.VBLZCandidate.ov, Stojkovic2026.VBLZCandidate.ev, Stojkovic2026.VBLZCandidate.uv, Stojkovic2026.VBLZCandidate.iv, Stojkovic2026.VBLZCandidate.uMono]

def Stojkovic2026.fissionCandidates : List VBLZCandidate

The four fission candidates (excluding the monophthong), for factorial typology.

Equations

• Stojkovic2026.fissionCandidates = [Stojkovic2026.VBLZCandidate.ov, Stojkovic2026.VBLZCandidate.ev, Stojkovic2026.VBLZCandidate.uv, Stojkovic2026.VBLZCandidate.iv]

Empirical data

inductive Stojkovic2026.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

@[implicit_reducible]

instance Stojkovic2026.instDecidableEqSlavicLang : DecidableEq SlavicLang

Equations

• Stojkovic2026.instDecidableEqSlavicLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stojkovic2026.instReprSlavicLang : Repr SlavicLang

Equations

• Stojkovic2026.instReprSlavicLang = { reprPrec := Stojkovic2026.instReprSlavicLang.repr }

def Stojkovic2026.instReprSlavicLang.repr : SlavicLang → ℕ → Std.Format

Equations

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

inductive Stojkovic2026.VBLZGroup : Type

The three surface-form groups for the VBLZ in the infinitive stem.

• 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.

@[implicit_reducible]

instance Stojkovic2026.instDecidableEqVBLZGroup : DecidableEq VBLZGroup

Equations

• Stojkovic2026.instDecidableEqVBLZGroup x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Stojkovic2026.instReprVBLZGroup : Repr VBLZGroup

Equations

• Stojkovic2026.instReprVBLZGroup = { reprPrec := Stojkovic2026.instReprVBLZGroup.repr }

def Stojkovic2026.instReprVBLZGroup.repr : VBLZGroup → ℕ → Std.Format

Equations

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

def Stojkovic2026.VBLZGroup.forms : VBLZGroup → List VBLZCandidate

Surface candidates attested in the infinitive stem for each group.

Equations

• Stojkovic2026.VBLZGroup.ovGroup.forms = [Stojkovic2026.VBLZCandidate.ov]
• Stojkovic2026.VBLZGroup.ovEvGroup.forms = [Stojkovic2026.VBLZCandidate.ov, Stojkovic2026.VBLZCandidate.ev]
• Stojkovic2026.VBLZGroup.uvGroup.forms = [Stojkovic2026.VBLZCandidate.uv]

def Stojkovic2026.SlavicLang.vblzGroup : SlavicLang → VBLZGroup

Group membership for each language.

Equations

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

structure Stojkovic2026.VBLZDatum : Type

A VBLZ datum: language, infinitive-stem and present-stem surface candidate.

• lang : SlavicLang
• infStem : VBLZCandidate
• presStem : VBLZCandidate

@[implicit_reducible]

instance Stojkovic2026.instDecidableEqVBLZDatum : DecidableEq VBLZDatum

Equations

• Stojkovic2026.instDecidableEqVBLZDatum = Stojkovic2026.instDecidableEqVBLZDatum.decEq

def Stojkovic2026.instDecidableEqVBLZDatum.decEq (x✝ x✝¹ : VBLZDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Stojkovic2026.instReprVBLZDatum.repr : VBLZDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Stojkovic2026.instReprVBLZDatum : Repr VBLZDatum

Equations

• Stojkovic2026.instReprVBLZDatum = { reprPrec := Stojkovic2026.instReprVBLZDatum.repr }

def Stojkovic2026.polishVBLZ : VBLZDatum

Equations

• Stojkovic2026.polishVBLZ = { lang := Stojkovic2026.SlavicLang.polish, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.czechVBLZ : VBLZDatum

Equations

• Stojkovic2026.czechVBLZ = { lang := Stojkovic2026.SlavicLang.czech, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.slovakVBLZ : VBLZDatum

Equations

• Stojkovic2026.slovakVBLZ = { lang := Stojkovic2026.SlavicLang.slovak, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.upperSorbianVBLZ : VBLZDatum

Equations

• Stojkovic2026.upperSorbianVBLZ = { lang := Stojkovic2026.SlavicLang.upperSorbian, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.lowerSorbianVBLZ : VBLZDatum

Equations

• Stojkovic2026.lowerSorbianVBLZ = { lang := Stojkovic2026.SlavicLang.lowerSorbian, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.russianVBLZ : VBLZDatum

Equations

• Stojkovic2026.russianVBLZ = { lang := Stojkovic2026.SlavicLang.russian, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.bcmsVBLZ : VBLZDatum

Equations

• Stojkovic2026.bcmsVBLZ = { lang := Stojkovic2026.SlavicLang.bcms, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.slovenianVBLZ : VBLZDatum

Equations

• Stojkovic2026.slovenianVBLZ = { lang := Stojkovic2026.SlavicLang.slovenian, infStem := Stojkovic2026.VBLZCandidate.ov, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.ukrainianVBLZ : VBLZDatum

Equations

• Stojkovic2026.ukrainianVBLZ = { lang := Stojkovic2026.SlavicLang.ukrainian, infStem := Stojkovic2026.VBLZCandidate.uv, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.lemkoRusynVBLZ : VBLZDatum

Equations

• Stojkovic2026.lemkoRusynVBLZ = { lang := Stojkovic2026.SlavicLang.lemkoRusyn, infStem := Stojkovic2026.VBLZCandidate.uv, presStem := Stojkovic2026.VBLZCandidate.uMono }

def Stojkovic2026.bulgarianVBLZ : VBLZDatum

Equations

• Stojkovic2026.bulgarianVBLZ = { lang := Stojkovic2026.SlavicLang.bulgarian, infStem := Stojkovic2026.VBLZCandidate.uv, presStem := Stojkovic2026.VBLZCandidate.uv }

def Stojkovic2026.macedonianVBLZ : VBLZDatum

Equations

• Stojkovic2026.macedonianVBLZ = { lang := Stojkovic2026.SlavicLang.macedonian, infStem := Stojkovic2026.VBLZCandidate.uv, presStem := Stojkovic2026.VBLZCandidate.uv }

def Stojkovic2026.allData : List VBLZDatum

Equations

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

theorem Stojkovic2026.allData_length : allData.length = 12

def Stojkovic2026.SlavicLang.HasVCPresent : SlavicLang → Prop

Bulgarian and Macedonian lack the INF/PRS distinction: the VBLZ precedes the theme vowel /-a-/ in both stems, so the VC sequence [uv] surfaces in the present too. All other languages have /-je-/ in the present, where the VBLZ is the single vowel [u] ([Sto26a], Table 1, §4.4).

Equations

• Stojkovic2026.SlavicLang.bulgarian.HasVCPresent = True
• Stojkovic2026.SlavicLang.macedonian.HasVCPresent = True
• x✝.HasVCPresent = False

@[implicit_reducible]

instance Stojkovic2026.instDecidablePredSlavicLangHasVCPresent : DecidablePred SlavicLang.HasVCPresent

Equations

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

theorem Stojkovic2026.presentStem_iff_VCPresent (d : VBLZDatum) : d ∈ allData → (d.lang.HasVCPresent ↔ d.presStem = VBLZCandidate.uv)

The present stem is the single vowel [u] exactly in the languages with a /-je-/ present; Bulgarian and Macedonian surface the VC sequence [uv] throughout — the paper's central cross-Slavic exception ([Sto26a], Table 1, §4.4).

theorem Stojkovic2026.infStem_mem_group_forms (d : VBLZDatum) : d ∈ allData → d.infStem ∈ d.lang.vblzGroup.forms

Each datum's infinitive stem is one of its language's group forms.

Constraints

def Stojkovic2026.noHiatus : Constraints.Constraint VBLZCandidate

NOHIATUS: assign * for adjacent vowels. In the pre-vocalic evaluation the monophthong .uMono realises [u] next to /-a-/, creating the hiatus this constraint penalises.

Equations

• Stojkovic2026.noHiatus = Constraints.Constraint.binary fun (c : Stojkovic2026.VBLZCandidate) => c = Stojkovic2026.VBLZCandidate.uMono

def Stojkovic2026.specify : Constraints.Constraint VBLZCandidate

SPECIFY(•→[F]): assign * for an unspecified base node. Only the fully faithful candidate (not in our candidate set) violates it, so it is vacuously satisfied here; included for faithfulness to the paper's set.

Equations

• Stojkovic2026.specify = Constraints.Constraint.binary fun (x : Stojkovic2026.VBLZCandidate) => False

def Stojkovic2026.noShareBack : Constraints.Constraint VBLZCandidate

*SHARE[−back]: don't copy [−back] from an adjacent palatal. Violated by [ev] and [iv] (both share [−back]).

Equations

• Stojkovic2026.noShareBack = Constraints.Constraint.binary fun (c : Stojkovic2026.VBLZCandidate) => c = Stojkovic2026.VBLZCandidate.ev ∨ c = Stojkovic2026.VBLZCandidate.iv

def Stojkovic2026.depBack : Constraints.Constraint VBLZCandidate

DEP[+back]: don't epenthesise [+back]. Violated by [ov] and [uv].

Equations

• Stojkovic2026.depBack = Constraints.Constraint.binary fun (c : Stojkovic2026.VBLZCandidate) => c = Stojkovic2026.VBLZCandidate.ov ∨ c = Stojkovic2026.VBLZCandidate.uv

def Stojkovic2026.depMinusHigh : Constraints.Constraint VBLZCandidate

DEP[−high]: don't epenthesise [−high]. Violated by [ov] and [ev] (mid vowels).

Equations

• Stojkovic2026.depMinusHigh = Constraints.Constraint.binary fun (c : Stojkovic2026.VBLZCandidate) => c = Stojkovic2026.VBLZCandidate.ov ∨ c = Stojkovic2026.VBLZCandidate.ev

def Stojkovic2026.depHigh : Constraints.Constraint VBLZCandidate

DEP[+high]: don't epenthesise [+high]. Violated by [uv] and [iv] (high vowels).

Implicit in [Sto26a]: without it [uv] harmonically bounds [ov], so no ranking selects [ov]. The paper derives the same effect from the markedness of [+high] vs [−high] (p. 14: "The feature [−high] is cross-linguistically more likely to be unmarked compared to [+high].").

Equations

• Stojkovic2026.depHigh = Constraints.Constraint.binary fun (c : Stojkovic2026.VBLZCandidate) => c = Stojkovic2026.VBLZCandidate.uv ∨ c = Stojkovic2026.VBLZCandidate.iv

def Stojkovic2026.variableConstraints : List (Constraints.Constraint VBLZCandidate)

The four variable constraints (excluding the undominated NOHIATUS and vacuous SPECIFY), permuted in the factorial typology.

Equations

• Stojkovic2026.variableConstraints = [Stojkovic2026.noShareBack, Stojkovic2026.depBack, Stojkovic2026.depMinusHigh, Stojkovic2026.depHigh]

def Stojkovic2026.allConstraints : List (Constraints.Constraint VBLZCandidate)

All six constraints.

Equations

• Stojkovic2026.allConstraints = [Stojkovic2026.noHiatus, Stojkovic2026.specify, Stojkovic2026.noShareBack, Stojkovic2026.depBack, Stojkovic2026.depMinusHigh, Stojkovic2026.depHigh]

Group-specific rankings

def Stojkovic2026.ovRanking : List (Constraints.Constraint VBLZCandidate)

[ov]-group ranking, adapted from [Sto26a] (17). The paper's (17) is NOHIATUS; SPECIFY ≫ *SHARE[−back] ≫ DEP[−high] ≫ DEP[+back] ≫ MAX•, with [ov]≻[uv] following from the markedness of [−high] epenthesis (p. 14) rather than a constraint; we make that preference explicit via DEP[+high], giving *SHARE[−back] ≫ DEP[+high] ≫ DEP[+back] ≫ DEP[−high].

*SHARE[−back] high: sharing [−back] from palatals is banned. DEP[+high] high: [+high] epenthesis is costly, so the unmarked [−high] surfaces → mid [o].

Equations

• Stojkovic2026.ovRanking = [Stojkovic2026.noHiatus, Stojkovic2026.specify, Stojkovic2026.noShareBack, Stojkovic2026.depHigh, Stojkovic2026.depBack, Stojkovic2026.depMinusHigh]

def Stojkovic2026.ovEvRanking : List (Constraints.Constraint VBLZCandidate)

[ov]/[ev]-group ranking, adapted from [Sto26a] (21). The paper's (21) is NOHIATUS; SPECIFY ≫ DEP[+back] ≫ DEP[−high] ≫ *SHARE[−back] ≫ MAX•; with DEP[+high] made explicit: DEP[+back] ≫ DEP[+high] ≫ *SHARE[−back] ≫ DEP[−high].

DEP[+back] high: epenthesising [+back] is banned. After a palatal, sharing [−back] is the only option → [ev]; after a non-palatal, [−high] epenthesis yields [ov] (a separate, non-palatal evaluation — not modelled here).

Equations

• Stojkovic2026.ovEvRanking = [Stojkovic2026.noHiatus, Stojkovic2026.specify, Stojkovic2026.depBack, Stojkovic2026.depHigh, Stojkovic2026.noShareBack, Stojkovic2026.depMinusHigh]

def Stojkovic2026.uvRanking : List (Constraints.Constraint VBLZCandidate)

[uv]-group ranking, adapted from [Sto26a] (29). The paper's (29) is NOHIATUS; SPECIFY ≫ DEP[−high] ≫ *SHARE[−back] ≫ DEP[+back] ≫ MAX•; we keep that order and replace the bottom MAX• with the explicit DEP[+high]: DEP[−high] ≫ *SHARE[−back] ≫ DEP[+back] ≫ DEP[+high].

DEP[−high] high: epenthesising [−high] is banned → [+high] surfaces. *SHARE[−back] above DEP[+back]: epenthesising [+back] is cheaper than sharing [−back] → back vowel [u] surfaces.

Equations

• Stojkovic2026.uvRanking = [Stojkovic2026.noHiatus, Stojkovic2026.specify, Stojkovic2026.depMinusHigh, Stojkovic2026.noShareBack, Stojkovic2026.depBack, Stojkovic2026.depHigh]

Optimality theorems

theorem Stojkovic2026.ov_optimal : (OptimalityTheory.Tableau.ofRanking allCandidates ovRanking ⋯).optimal = {VBLZCandidate.ov}

The [ov]-group ranking selects [ov] as the unique optimum.

theorem Stojkovic2026.ev_optimal : (OptimalityTheory.Tableau.ofRanking allCandidates ovEvRanking ⋯).optimal = {VBLZCandidate.ev}

The [ov]/[ev] ranking selects [ev] in the palatal context. (Non-palatally, [ev] and [iv] are unavailable — no palatal to share [−back] — and [ov] wins; that contextual split is not modelled in this single tableau.)

theorem Stojkovic2026.uv_optimal : (OptimalityTheory.Tableau.ofRanking allCandidates uvRanking ⋯).optimal = {VBLZCandidate.uv}

The [uv]-group ranking selects [uv] as the unique optimum.

Factorial typology

theorem Stojkovic2026.factorial_typology_size : OptimalityTheory.factorialTypologySize fissionCandidates variableConstraints ⋯ = 4

This file's four-constraint factorial typology (the three sharing/epenthesis constraints plus the explicit DEP[+high]) over the four fission candidates produces exactly four distinct optimal sets: {[ov]}, {[ev]}, {[uv]}, {[iv]}. [Sto26a]'s own typology (31) is over three constraints and yields the three attested groups (with [ov][ev] one context-sensitive grammar) plus a hypothetical [uv][iv]; see the module docstring.

theorem Stojkovic2026.factorial_optima_are_singletons : OptimalityTheory.factorialOptima fissionCandidates variableConstraints ⋯ = [{VBLZCandidate.uv}, {VBLZCandidate.iv}, {VBLZCandidate.ov}, {VBLZCandidate.ev}]

The four distinct optima are exactly the four singleton candidate sets.

theorem Stojkovic2026.iv_unattested : {VBLZCandidate.iv} ∈ OptimalityTheory.factorialOptima fissionCandidates variableConstraints ⋯ ∧ ∀ d ∈ allData, VBLZCandidate.iv ∉ d.lang.vblzGroup.forms

[iv] is the unattested optimum: the factorial typology predicts an [iv] grammar ({.iv} is among the optima), yet no attested Slavic language surfaces the [iv] form — every group's inventory is one of [ov]/[ev]/[uv] ([Sto26a], (31f)–(32): the Ukrainian [uv]~[iv] pairs are hypothetical and unattested).

Bridge to empirical data

theorem Stojkovic2026.optimal_forms_attested : VBLZCandidate.ov ∈ VBLZGroup.ovGroup.forms ∧ VBLZCandidate.ev ∈ VBLZGroup.ovEvGroup.forms ∧ VBLZCandidate.ov ∈ VBLZGroup.ovEvGroup.forms ∧ VBLZCandidate.uv ∈ VBLZGroup.uvGroup.forms

The OT-optimal candidate for each group (ov_optimal/ev_optimal/uv_optimal) is among that group's attested forms; [ov] also figures in the [ov]/[ev] group's inventory.