Marco & Rasin (2026): Optimal Paradigms — A Challenge from JTA

@cite{marco-rasin-2026} @cite{mccarthy-2005}

Formalizes the argument that Optimal Paradigms (OP) cannot simultaneously predict the distribution of schwa in verbs, nouns, and adjectives in Judeo-Tripolitanian Arabic (JTA). The core paradox:

• Verbs: schwa always between C₂ and C₃ (CCəC), regardless of sonority
• Adjectives: same as verbs — CCəC regardless of sonority
• Nouns: sonority-sensitive — CəCC when C₂ > C₃, CCəC otherwise

Adjectives share phonological behavior with verbs but paradigm structure with nouns (only V-initial suffixes). OP predicts phonological behavior should track paradigm structure, so it wrongly predicts adjectives should behave like nouns.

Modeling note

In OP, candidates are whole paradigms where each member independently chooses a stem shape. Markedness constraints (*CCC, *ə]σ) determine the shapes of suffixed members: C-initial suffixed forms must be CCəC (to avoid tri-consonantal clusters), V-initial suffixed forms must be CəCC (to avoid schwa in an open syllable). Only the suffix-less bare form is free — its shape is determined by OP-MAX-V (paradigm uniformity).

For verbs, we enumerate the 4 candidates from tableau (10) in the paper. For adjectives, we enumerate all 2³ = 8 possible paradigms exhaustively. The main result (adj_always_initial) proves that the uniform CəCC paradigm has 0 violations on all four constraints and thus wins under every ranking — contradicting the attested CCəC pattern.

The paper considers two scenarios for adjectives: with a paradigm (tableau (19)) and without (tableau (20)). Both fail — op_wrong_adjectives covers (19) and op_wrong_adj_bare covers (20), formalizing the paper's argument that OP fails "regardless of what constitutes a paradigm."

inductive MarcoRasin2026.SchwaPos : Type

The two possible schwa positions in a tri-consonantal stem C₁C₂C₃. medial = CCəC (schwa between C₂ and C₃); initial = CəCC (schwa between C₁ and C₂).

• medial : SchwaPos
• initial : SchwaPos

@[implicit_reducible]

instance MarcoRasin2026.instDecidableEqSchwaPos : DecidableEq SchwaPos

Equations

• MarcoRasin2026.instDecidableEqSchwaPos x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance MarcoRasin2026.instReprSchwaPos : Repr SchwaPos

Equations

• MarcoRasin2026.instReprSchwaPos = { reprPrec := MarcoRasin2026.instReprSchwaPos.repr }

def MarcoRasin2026.instReprSchwaPos.repr : SchwaPos → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MarcoRasin2026.instBEqSchwaPos : BEq SchwaPos

Equations

• MarcoRasin2026.instBEqSchwaPos = { beq := MarcoRasin2026.instBEqSchwaPos.beq }

def MarcoRasin2026.instBEqSchwaPos.beq : SchwaPos → SchwaPos → Bool

Equations

• MarcoRasin2026.instBEqSchwaPos.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance MarcoRasin2026.instInhabitedSchwaPos : Inhabited SchwaPos

Equations

• MarcoRasin2026.instInhabitedSchwaPos = { default := MarcoRasin2026.instInhabitedSchwaPos.default }

def MarcoRasin2026.instInhabitedSchwaPos.default : SchwaPos

Equations

• MarcoRasin2026.instInhabitedSchwaPos.default = MarcoRasin2026.SchwaPos.medial

inductive MarcoRasin2026.SuffixOnset : Type

Suffix onset type, determining the phonological environment.

• cInit : SuffixOnset
• vInit : SuffixOnset
• bare : SuffixOnset

@[implicit_reducible]

instance MarcoRasin2026.instDecidableEqSuffixOnset : DecidableEq SuffixOnset

Equations

• MarcoRasin2026.instDecidableEqSuffixOnset x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance MarcoRasin2026.instReprSuffixOnset : Repr SuffixOnset

Equations

• MarcoRasin2026.instReprSuffixOnset = { reprPrec := MarcoRasin2026.instReprSuffixOnset.repr }

def MarcoRasin2026.instReprSuffixOnset.repr : SuffixOnset → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MarcoRasin2026.instBEqSuffixOnset : BEq SuffixOnset

Equations

• MarcoRasin2026.instBEqSuffixOnset = { beq := MarcoRasin2026.instBEqSuffixOnset.beq }

def MarcoRasin2026.instBEqSuffixOnset.beq : SuffixOnset → SuffixOnset → Bool

Equations

• MarcoRasin2026.instBEqSuffixOnset.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure MarcoRasin2026.JTAForm : Type

A single paradigm member: schwa position + suffix type.

• schwa : SchwaPos
• suffix : SuffixOnset

@[implicit_reducible]

instance MarcoRasin2026.instDecidableEqJTAForm : DecidableEq JTAForm

Equations

• MarcoRasin2026.instDecidableEqJTAForm = MarcoRasin2026.instDecidableEqJTAForm.decEq

def MarcoRasin2026.instDecidableEqJTAForm.decEq (x✝ x✝¹ : JTAForm) : Decidable (x✝ = x✝¹)

Equations

• MarcoRasin2026.instDecidableEqJTAForm.decEq { schwa := a, suffix := a_1 } { schwa := b, suffix := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def MarcoRasin2026.instReprJTAForm.repr : JTAForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance MarcoRasin2026.instReprJTAForm : Repr JTAForm

Equations

• MarcoRasin2026.instReprJTAForm = { reprPrec := MarcoRasin2026.instReprJTAForm.repr }

@[implicit_reducible]

instance MarcoRasin2026.instBEqJTAForm : BEq JTAForm

Equations

• MarcoRasin2026.instBEqJTAForm = { beq := MarcoRasin2026.instBEqJTAForm.beq }

def MarcoRasin2026.instBEqJTAForm.beq : JTAForm → JTAForm → Bool

Equations

• MarcoRasin2026.instBEqJTAForm.beq { schwa := a, suffix := a_1 } { schwa := b, suffix := b_1 } = (a == b && a_1 == b_1)
• MarcoRasin2026.instBEqJTAForm.beq x✝¹ x✝ = false

def MarcoRasin2026.starCCC : Core.Constraint.OT.NamedConstraint (List JTAForm)

*CCC: assign * for every sequence of three consonants. Violated by CəCC (initial) stems before C-initial suffixes: C₁əC₂C₃ + C → C₂C₃C = tri-consonantal cluster.

Equations

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

def MarcoRasin2026.starSchwaOpen : Core.Constraint.OT.NamedConstraint (List JTAForm)

*ə]σ: assign * for every schwa in an open syllable. Violated by CCəC (medial) stems before V-initial suffixes: C₁C₂ə.C₃V → schwa in open syllable.

Equations

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

def MarcoRasin2026.sonCon (c2 c3 : Phonology.Syllable.SonorityRank) : Core.Constraint.OT.NamedConstraint (List JTAForm)

SONCON: assign * for a CCəC (medial) form when C₂ > C₃ in sonority. Parametrized over the sonority ranks of C₂ and C₃, using the LinearOrder SonorityRank instance from Syllable.Defs.

Equations

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

def MarcoRasin2026.opMaxV : Core.Constraint.OT.NamedConstraint (List JTAForm)

OP-MAX-V: assign * for each ordered pair of paradigm members with different schwa positions. Each positional mismatch = 1 violation. For n₁ medial and n₂ initial members: n₁·n₂ + n₂·n₁ = 2·n₁·n₂ total violations (matching @cite{mccarthy-2005}'s counting).

Equations

• MarcoRasin2026.opMaxV = Phonology.ParadigmUniformity.mkOPMaxV fun (f1 f2 : MarcoRasin2026.JTAForm) => if (f1.schwa != f2.schwa) = true then 1 else 0

def MarcoRasin2026.vSuf : List SuffixOnset

JTA verbal suffixes: bare + 4 C-initial + 2 V-initial = 7 members.

Equations

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

def MarcoRasin2026.mkP (shapes : List SchwaPos) (suffixes : List SuffixOnset) : List JTAForm

Helper: build a paradigm from a list of schwa positions and suffix list.

Equations

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

def MarcoRasin2026.vA : List JTAForm

(10a) ☞ Bare=medial: 5 medial, 2 initial. OP-MAX-V = 20.

Equations

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

def MarcoRasin2026.vB : List JTAForm

(10b) Bare=initial: 4 medial, 3 initial. OP-MAX-V = 24.

Equations

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

def MarcoRasin2026.vC : List JTAForm

(10c) Uniform medial: *ə]σ violated twice.

Equations

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

def MarcoRasin2026.vD : List JTAForm

(10d) Uniform initial: *CCC violated four times.

Equations

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

def MarcoRasin2026.verbCands : List (List JTAForm)

Equations

• MarcoRasin2026.verbCands = [MarcoRasin2026.vA, MarcoRasin2026.vB, MarcoRasin2026.vC, MarcoRasin2026.vD]

theorem MarcoRasin2026.verbCands_ne : verbCands ≠ []

def MarcoRasin2026.nM : List JTAForm

Nouns: bare singular only (1 member).

Equations

• MarcoRasin2026.nM = MarcoRasin2026.mkP [MarcoRasin2026.SchwaPos.medial] [MarcoRasin2026.SuffixOnset.bare]

def MarcoRasin2026.nI : List JTAForm

Equations

• MarcoRasin2026.nI = MarcoRasin2026.mkP [MarcoRasin2026.SchwaPos.initial] [MarcoRasin2026.SuffixOnset.bare]

def MarcoRasin2026.nounCands : List (List JTAForm)

Equations

• MarcoRasin2026.nounCands = [MarcoRasin2026.nM, MarcoRasin2026.nI]

theorem MarcoRasin2026.nounCands_ne : nounCands ≠ []

def MarcoRasin2026.aSuf : List SuffixOnset

Adjective suffixes: bare (MSG) + 2 V-initial (-a FSG, -in PL).

Equations

• MarcoRasin2026.aSuf = [MarcoRasin2026.SuffixOnset.bare, MarcoRasin2026.SuffixOnset.vInit, MarcoRasin2026.SuffixOnset.vInit]

def MarcoRasin2026.adjCands : List (List JTAForm)

All 2³ = 8 possible adjective paradigms. Exhaustive enumeration ensures the negative result holds for ALL candidates, not just selected ones.

Equations

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

theorem MarcoRasin2026.adjCands_ne : adjCands ≠ []

def MarcoRasin2026.adjAttested : List JTAForm

The attested adjective paradigm: bare=medial, V-init=initial.

Equations

• MarcoRasin2026.adjAttested = MarcoRasin2026.mkP [MarcoRasin2026.SchwaPos.medial, MarcoRasin2026.SchwaPos.initial, MarcoRasin2026.SchwaPos.initial] MarcoRasin2026.aSuf

def MarcoRasin2026.adjOPpred : List JTAForm

The OP-predicted paradigm: uniform initial.

Equations

• MarcoRasin2026.adjOPpred = MarcoRasin2026.mkP [MarcoRasin2026.SchwaPos.initial, MarcoRasin2026.SchwaPos.initial, MarcoRasin2026.SchwaPos.initial] MarcoRasin2026.aSuf

def MarcoRasin2026.mccarthyRanking : List (Core.Constraint.OT.NamedConstraint (List JTAForm))

McCarthy's ranking: *ə]σ, *CCC ≫ OP-MAX-V ≫ SONCON (for C₂ > C₃).

Equations

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

theorem MarcoRasin2026.op_correct_verbs : (Core.Constraint.OT.mkTableau verbCands mccarthyRanking verbCands_ne).optimal = {vA}

OP correctly selects the attested verbal paradigm (10a): bare=medial. Majority Rules in action — the bare form aligns with the C-initial majority (5 medial vs 2 initial members).

theorem MarcoRasin2026.op_correct_nouns : (Core.Constraint.OT.mkTableau nounCands mccarthyRanking nounCands_ne).optimal = {nI}

OP correctly selects CəCC for nouns (when C₂ > C₃). Single-member paradigm, so OP-MAX-V is vacuous; SONCON decides.

theorem MarcoRasin2026.op_wrong_adjectives : (Core.Constraint.OT.mkTableau adjCands mccarthyRanking adjCands_ne).optimal = {adjOPpred}

OP wrongly selects uniform-initial for adjectives (tableau (19)). Adjectives have only V-initial suffixes (like nouns), so OP-MAX-V cannot force medial schwa in the bare form. SONCON then favors initial.

theorem MarcoRasin2026.op_fails_adjectives : (Core.Constraint.OT.mkTableau adjCands mccarthyRanking adjCands_ne).optimal ≠ {adjAttested}

The attested adjective paradigm (bare=CCəC) is NOT selected by OP.

def MarcoRasin2026.opConstraints : List (Core.Constraint.OT.NamedConstraint (List JTAForm))

The four constraints used in McCarthy's OP analysis.

Equations

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

theorem MarcoRasin2026.adjOPpred_zero_viols (con : Core.Constraint.OT.NamedConstraint (List JTAForm)) : con ∈ opConstraints → con.eval adjOPpred = 0

The uniform-initial adjective paradigm has zero violations on all four OP constraints. This is the structural reason it wins under every ranking — not a coincidence of McCarthy's particular ranking.

• *ə]σ: 0 — initial schwa (CəCC) is never in an open syllable
• *CCC: 0 — no C-initial suffixes in the adjective paradigm
• OP-MAX-V: 0 — uniform paradigm, no positional mismatches
• SONCON: 0 — no medial (CCəC) forms to violate sonority

A candidate with profile [0,0,...,0] is the minimum of any lexicographic order on Nat-valued profiles (ViolationProfile.zero_le), so permuting the ranking cannot change the outcome.

theorem MarcoRasin2026.adjOPpred_always_optimal (ranking : List (Core.Constraint.OT.NamedConstraint (List JTAForm))) : ranking ∈ Core.Constraint.OT.permutations opConstraints → adjOPpred ∈ (Core.Constraint.OT.mkTableau adjCands ranking adjCands_ne).optimal

theorem MarcoRasin2026.adj_always_initial (ranking : List (Core.Constraint.OT.NamedConstraint (List JTAForm))) : ranking ∈ Core.Constraint.OT.permutations opConstraints → (Core.Constraint.OT.mkTableau adjCands ranking adjCands_ne).optimal = {adjOPpred}

Main result. No ranking of the four OP constraints selects the attested adjective paradigm (bare=CCəC).

The uniform-initial paradigm has zero violations on all four constraints (adjOPpred_zero_viols), making it the lexicographic minimum under any permutation (adjOPpred_always_optimal). Moreover, it is the unique winner — no other candidate also has a zero profile (verified by decide).

Since [0,0,0,0] is the lexicographic minimum regardless of constraint permutation, uniform-initial wins under every ranking. The attested paradigm (bare=medial, V-init=initial) always loses because it incurs OP-MAX-V and SONCON violations.

This formalizes @cite{marco-rasin-2026}'s central challenge: OP cannot derive category-distinct phonological behavior when two categories share paradigm structure but differ phonologically.

theorem MarcoRasin2026.op_wrong_adj_bare : (Core.Constraint.OT.mkTableau nounCands mccarthyRanking nounCands_ne).optimal = {nI}

If adjectives have no inflectional paradigm (single bare form, like nouns), SONCON wrongly favors CəCC (initial). This is tableau (20) in the paper: the single-member adjective case. Combined with op_wrong_adjectives (tableau (19)), this shows OP fails regardless of what constitutes a paradigm for JTA adjectives.

theorem MarcoRasin2026.op_wrong_adj_bare_not_attested : (Core.Constraint.OT.mkTableau nounCands mccarthyRanking nounCands_ne).optimal ≠ {nM}

The attested adjective form (CCəC = medial) is NOT selected when adjectives are treated as having no paradigm.

inductive MarcoRasin2026.MorphCat : Type

Morphosyntactic category, used for category-indexed constraints.

• verb : MorphCat
• adj : MorphCat
• noun : MorphCat

@[implicit_reducible]

instance MarcoRasin2026.instDecidableEqMorphCat : DecidableEq MorphCat

Equations

• MarcoRasin2026.instDecidableEqMorphCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance MarcoRasin2026.instReprMorphCat : Repr MorphCat

Equations

• MarcoRasin2026.instReprMorphCat = { reprPrec := MarcoRasin2026.instReprMorphCat.repr }

def MarcoRasin2026.instReprMorphCat.repr : MorphCat → ℕ → Std.Format

Equations

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

def MarcoRasin2026.instBEqMorphCat.beq : MorphCat → MorphCat → Bool

Equations

• MarcoRasin2026.instBEqMorphCat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance MarcoRasin2026.instBEqMorphCat : BEq MorphCat

Equations

• MarcoRasin2026.instBEqMorphCat = { beq := MarcoRasin2026.instBEqMorphCat.beq }

def MarcoRasin2026.templateMedial (cat : MorphCat) : Core.Constraint.OT.NamedConstraint (List JTAForm)

{CCəC}_{Verb, Adj}: template constraint applying to verbs and adjectives but not nouns. Penalizes initial (CəCC) forms in verbs and adjectives. Directly references morphosyntactic categories, violating the TCNP (@cite{bobaljik-2008}).

Equations

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

def MarcoRasin2026.templateRanking (cat : MorphCat) : List (Core.Constraint.OT.NamedConstraint (List JTAForm))

Category-specific ranking: {CCəC}_{V,A} ≫ SONCON.

Equations

• MarcoRasin2026.templateRanking cat = [MarcoRasin2026.templateMedial cat, MarcoRasin2026.sonCon Phonology.Syllable.SonorityRank.liquid Phonology.Syllable.SonorityRank.stop]

def MarcoRasin2026.verbUnifM : List JTAForm

Template correctly selects medial (CCəC) for verbs. (Using uniform candidates since template forces all members to medial.)

Equations

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

def MarcoRasin2026.verbUnifI : List JTAForm

Equations

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

def MarcoRasin2026.verbTemplateCands : List (List JTAForm)

Equations

• MarcoRasin2026.verbTemplateCands = [MarcoRasin2026.verbUnifM, MarcoRasin2026.verbUnifI]

theorem MarcoRasin2026.verbTemplateCands_ne : verbTemplateCands ≠ []

theorem MarcoRasin2026.template_correct_verbs : (Core.Constraint.OT.mkTableau verbTemplateCands (templateRanking MorphCat.verb) verbTemplateCands_ne).optimal = {verbUnifM}

theorem MarcoRasin2026.template_correct_nouns : (Core.Constraint.OT.mkTableau nounCands (templateRanking MorphCat.noun) nounCands_ne).optimal = {nI}

Template correctly selects initial (CəCC) for nouns (template inactive).

def MarcoRasin2026.adjTemplateCands : List (List JTAForm)

Template correctly selects the attested adjective paradigm — the case where OP fails. The template forces medial (CCəC) for both verb and adjective categories, overriding SONCON.

Equations

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

theorem MarcoRasin2026.adjTemplateCands_ne : adjTemplateCands ≠ []

theorem MarcoRasin2026.template_correct_adjectives : (Core.Constraint.OT.mkTableau adjTemplateCands (templateRanking MorphCat.adj) adjTemplateCands_ne).optimal = {mkP [SchwaPos.medial, SchwaPos.medial, SchwaPos.medial] aSuf}

Each unique-winner tableau lifts to a generic ConstraintSystem via tableauSystem. For McCarthy's OP ranking this exposes the correct predictions for verbs and nouns, and the wrong prediction for adjectives — the empirical content of @cite{marco-rasin-2026}'s argument.

noncomputable def MarcoRasin2026.verbSystem : Core.Constraint.ConstraintSystem (List JTAForm) (Core.Constraint.LexProfile ℕ 4)

Verbal paradigm under McCarthy's OP ranking.

Equations

• MarcoRasin2026.verbSystem = Core.Constraint.tableauSystem (Core.Constraint.OT.mkTableau MarcoRasin2026.verbCands MarcoRasin2026.mccarthyRanking MarcoRasin2026.verbCands_ne)

theorem MarcoRasin2026.verbSystem_predict_vA : verbSystem.predict vA = 1

OP correctly predicts the attested bare-medial verbal paradigm (10a).

noncomputable def MarcoRasin2026.nounSystem : Core.Constraint.ConstraintSystem (List JTAForm) (Core.Constraint.LexProfile ℕ 4)

Nominal paradigm under McCarthy's OP ranking.

Equations

• MarcoRasin2026.nounSystem = Core.Constraint.tableauSystem (Core.Constraint.OT.mkTableau MarcoRasin2026.nounCands MarcoRasin2026.mccarthyRanking MarcoRasin2026.nounCands_ne)

theorem MarcoRasin2026.nounSystem_predict_nI : nounSystem.predict nI = 1

OP correctly predicts CəCC for nouns when C₂ > C₃.

noncomputable def MarcoRasin2026.adjSystem : Core.Constraint.ConstraintSystem (List JTAForm) (Core.Constraint.LexProfile ℕ 4)

Adjectival paradigm under McCarthy's OP ranking. The probability-1 prediction here is the wrong uniform-initial paradigm — the formal content of @cite{marco-rasin-2026}'s challenge.

Equations

• MarcoRasin2026.adjSystem = Core.Constraint.tableauSystem (Core.Constraint.OT.mkTableau MarcoRasin2026.adjCands MarcoRasin2026.mccarthyRanking MarcoRasin2026.adjCands_ne)

theorem MarcoRasin2026.adjSystem_predict_OPpred : adjSystem.predict adjOPpred = 1

OP wrongly assigns probability 1 to the uniform-initial adjective paradigm. The attested CCəC pattern receives probability 0 — the formal sharpening of "OP fails for adjectives."

theorem MarcoRasin2026.adjSystem_predict_attested_zero : adjSystem.predict adjAttested = 0

Loser side: the attested adjective paradigm gets probability 0.

noncomputable def MarcoRasin2026.verbTemplateSystem : Core.Constraint.ConstraintSystem (List JTAForm) (Core.Constraint.LexProfile ℕ 2)

Verbal paradigm under the category-specific template ranking.

Equations

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

theorem MarcoRasin2026.verbTemplateSystem_predict_unifM : verbTemplateSystem.predict verbUnifM = 1

noncomputable def MarcoRasin2026.adjTemplateSystem : Core.Constraint.ConstraintSystem (List JTAForm) (Core.Constraint.LexProfile ℕ 2)

Adjectival paradigm under the category-specific template ranking — now correctly predicting the attested medial pattern with probability 1.

Equations

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

theorem MarcoRasin2026.adjTemplateSystem_predict_medial : adjTemplateSystem.predict (mkP [SchwaPos.medial, SchwaPos.medial, SchwaPos.medial] aSuf) = 1