Slavic Verbalizer @cite{stojkovic-2026}

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.

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

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.a]	hiatus	monophthongise, delete 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

The 4! = 24 permutations of the four variable constraints produce exactly 4 distinct optima: {[ov]}, {[ev]}, {[uv]}, {[iv]}. Three correspond to attested groups; {[iv]} is unattested.

inductive Phenomena.Allomorphy.Studies.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

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instDecidableEqSlavicLang : DecidableEq SlavicLang

Equations

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

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqSlavicLang : BEq SlavicLang

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqSlavicLang = { beq := Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqSlavicLang.beq }

def Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqSlavicLang.beq : SlavicLang → SlavicLang → Bool

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqSlavicLang.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Allomorphy.Studies.Stojkovic2026.instReprSlavicLang.repr : SlavicLang → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instReprSlavicLang : Repr SlavicLang

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instReprSlavicLang = { reprPrec := Phenomena.Allomorphy.Studies.Stojkovic2026.instReprSlavicLang.repr }

inductive Phenomena.Allomorphy.Studies.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.

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instDecidableEqVBLZGroup : DecidableEq VBLZGroup

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZGroup.beq : VBLZGroup → VBLZGroup → Bool

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZGroup.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZGroup : BEq VBLZGroup

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZGroup = { beq := Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZGroup.beq }

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZGroup : Repr VBLZGroup

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZGroup = { reprPrec := Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZGroup.repr }

def Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZGroup.repr : VBLZGroup → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZGroup.forms : VBLZGroup → List String

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

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.SlavicLang.vblzGroup : SlavicLang → VBLZGroup

Group membership for each language.

Equations

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

structure Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZDatum : Type

A VBLZ datum: language, infinitive-stem VC, present-stem V.

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

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

Equations

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

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instDecidableEqVBLZDatum : DecidableEq VBLZDatum

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instDecidableEqVBLZDatum = Phenomena.Allomorphy.Studies.Stojkovic2026.instDecidableEqVBLZDatum.decEq

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZDatum : BEq VBLZDatum

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZDatum = { beq := Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZDatum.beq }

def Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZDatum.beq : VBLZDatum → VBLZDatum → Bool

Equations

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

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZDatum : Repr VBLZDatum

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZDatum = { reprPrec := Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZDatum.repr }

def Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZDatum.repr : VBLZDatum → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.polishVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.czechVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.slovakVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.upperSorbianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.lowerSorbianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.russianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.bcmsVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.slovenianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.ukrainianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.lemkoRusynVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.bulgarianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.macedonianVBLZ : VBLZDatum

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.allData : List VBLZDatum

Equations

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

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.allData_length : allData.length = 12

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

The present-stem vowel is universally [u] across all three groups.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.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.

inductive Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate : Type

Candidate surface realisations of the VBLZ before the thematic /-a-/. Each represents a different resolution of the defective diphthong.

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

• uHiatus : VBLZCandidate

  [u.a]: monophthongisation, unspecified slot deleted, hiatus with /-a-/.

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instDecidableEqVBLZCandidate : DecidableEq VBLZCandidate

Equations

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

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZCandidate : BEq VBLZCandidate

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZCandidate = { beq := Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZCandidate.beq }

def Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZCandidate.beq : VBLZCandidate → VBLZCandidate → Bool

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instBEqVBLZCandidate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZCandidate : Repr VBLZCandidate

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZCandidate = { reprPrec := Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZCandidate.repr }

def Phenomena.Allomorphy.Studies.Stojkovic2026.instReprVBLZCandidate.repr : VBLZCandidate → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.allCandidates : List VBLZCandidate

All candidates.

Equations

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

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.allCandidates_nonempty : allCandidates ≠ []

def Phenomena.Allomorphy.Studies.Stojkovic2026.fissionCandidates : List VBLZCandidate

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

Equations

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

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.fissionCandidates_nonempty : fissionCandidates ≠ []

def Phenomena.Allomorphy.Studies.Stojkovic2026.noHiatus : Core.OT.NamedConstraint VBLZCandidate

NOHIATUS: assign * for adjacent vowels.

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.specify : Core.OT.NamedConstraint VBLZCandidate

SPECIFY(•→[F]): assign * for unspecified base node. Only violated by the fully faithful candidate (not in our candidate set), so this constraint is vacuously satisfied. Included for completeness.

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.specify = Theories.Phonology.Constraints.mkMark "SPECIFY" fun (x : Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate) => false

def Phenomena.Allomorphy.Studies.Stojkovic2026.noShareBack : Core.OT.NamedConstraint VBLZCandidate

*SHARE[−back]: don't copy [−back] from an adjacent palatal. Violated by [ev] (shares [−back] for [e]) and [iv] (shares [−back] for [i]).

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.depBack : Core.OT.NamedConstraint VBLZCandidate

DEP[+back]: don't epenthesise [+back] on the unspecified slot. Violated by [ov] and [uv] (both epenthesise [+back] to get a back vowel).

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.depLowHigh : Core.OT.NamedConstraint VBLZCandidate

DEP[−high]: don't epenthesise [−high] on the unspecified slot. Violated by [ov] and [ev] (both epenthesise [−high] to get a mid vowel).

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.depHigh : Core.OT.NamedConstraint VBLZCandidate

DEP[+high]: don't epenthesise [+high] on the unspecified slot. Violated by [uv] and [iv] (both epenthesise [+high] to get a high vowel).

Implicit in Stojković's analysis. Without this constraint, [uv] harmonically bounds [ov], making it impossible for any ranking to select [ov] as optimal. Stojković derives the equivalent 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

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.variableConstraints : List (Core.OT.NamedConstraint VBLZCandidate)

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

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.allConstraints : List (Core.OT.NamedConstraint VBLZCandidate)

All six constraints in one list.

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.ovRanking : List (Core.OT.NamedConstraint VBLZCandidate)

[ov] group ranking (Stojković 2026, (17)): NOHIATUS, SPECIFY ≫ *SHARE[−back] ≫ DEP[+high] ≫ DEP[+back] ≫ DEP[−high]

*SHARE[−back] high: sharing [−back] from palatals is banned. DEP[+high] above DEP[−high]: [+high] epenthesis is costlier than [−high], making [−high] the default → mid vowel [o] surfaces.

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.ovEvRanking : List (Core.OT.NamedConstraint VBLZCandidate)

[ov]/[ev] group ranking (Stojković 2026, (21)): NOHIATUS, SPECIFY ≫ DEP[+back] ≫ DEP[+high] ≫ *SHARE[−back] ≫ DEP[−high]

DEP[+back] high: epenthesising [+back] is banned. After palatals, sharing [−back] is the only option → [ev]. After non-palatals, [−high] epenthesis yields [ov] (in a separate non-palatal evaluation).

Equations

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.uvRanking : List (Core.OT.NamedConstraint VBLZCandidate)

[uv] group ranking (Stojković 2026, (29)): NOHIATUS, SPECIFY ≫ 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

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

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.ov_optimal : (Core.OT.buildTableau allCandidates ovRanking allCandidates_nonempty).optimal = [VBLZCandidate.ov]

The [ov] group ranking selects [ov] as the unique optimal candidate.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.ev_optimal : (Core.OT.buildTableau allCandidates ovEvRanking allCandidates_nonempty).optimal = [VBLZCandidate.ev]

The [ov]/[ev] ranking selects [ev] as optimal in the palatal context. (In the non-palatal context, [ev] and [iv] are unavailable because there is no palatal to share [−back]; [ov] wins trivially.)

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.uv_optimal : (Core.OT.buildTableau allCandidates uvRanking allCandidates_nonempty).optimal = [VBLZCandidate.uv]

The [uv] group ranking selects [uv] as the unique optimal candidate.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.factorial_typology_size : Core.OT.factorialTypologySize fissionCandidates variableConstraints fissionCandidates_nonempty = 4

The factorial typology over the four variable constraints and four fission candidates produces exactly 4 distinct optimal sets.

Three correspond to attested Slavic groups:

• {[ov]}: *SHARE, DEP[+high] ranked high
• {[ev]}: DEP[+back], DEP[+high] ranked high
• {[uv]}: DEP[−high], *SHARE ranked high

The fourth ({[iv]}) is unattested in Slavic.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.factorial_optima_are_singletons : Core.OT.factorialOptima fissionCandidates variableConstraints fissionCandidates_nonempty = [[VBLZCandidate.uv], [VBLZCandidate.iv], [VBLZCandidate.ov], [VBLZCandidate.ev]]

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

def Phenomena.Allomorphy.Studies.Stojkovic2026.ivIsUnattested : Prop

The [iv] pattern (shared [−back] + [+high], giving a front high vowel) is the only unattested pattern among the four predicted by the factorial typology (Stojković 2026, (31f)).

Equations

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

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.iv_pattern_unattested : ivIsUnattested

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.ov_matches_group : VBLZGroup.ovGroup.forms.contains "ov" = true

The [ov] group's OT-predicted form matches the empirical data.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.uv_matches_group : VBLZGroup.uvGroup.forms.contains "uv" = true

The [uv] group's OT-predicted form matches the empirical data.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.ovEv_matches_group : VBLZGroup.ovEvGroup.forms.contains "ev" = true ∧ VBLZGroup.ovEvGroup.forms.contains "ov" = true

The [ov]/[ev] group's OT-predicted forms match the empirical data: [ev] in the palatal context (proved by ev_optimal), [ov] in the non-palatal context (where [ev] is unavailable).

def Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate.surfaceForm : VBLZCandidate → String

The surface form of each candidate.

Equations

• Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate.ov.surfaceForm = "ov"
• Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate.ev.surfaceForm = "ev"
• Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate.uv.surfaceForm = "uv"
• Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate.iv.surfaceForm = "iv"
• Phenomena.Allomorphy.Studies.Stojkovic2026.VBLZCandidate.uHiatus.surfaceForm = "u"

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.ov_surface_correct : VBLZCandidate.ov.surfaceForm = "ov"

The OT-optimal candidate for the [ov] group produces the attested form.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.uv_surface_correct : VBLZCandidate.uv.surfaceForm = "uv"

The OT-optimal candidate for the [uv] group produces the attested form.

theorem Phenomena.Allomorphy.Studies.Stojkovic2026.ev_surface_correct : VBLZCandidate.ev.surfaceForm = "ev"

The OT-optimal candidate for the [ov]/[ev] palatal context produces the attested palatal-conditioned form.