Zompì 2023: *ABA in multidimensional paradigms, Max/Dep Eval

[Zom23]

Exponent selection as ranked violable faithfulness: per-dimension Max and Dep constraints ([Wol08], after [McCP95]) under strict-domination Eval ([PS93]). An exponent may be both underspecified and overspecified for its context, each departure penalized but neither fatal — the midpoint between DM's Underspecification and nanosyntax's Overspecification ([Sta09a]).

Contexts are the cumulative case × number decompositions (the dissertation's (163)): NOM ∅ ⊂ ACC {κ_dep} ⊂ DAT {κ_dep, κ_dat} on one dimension ([SMX+19], [Cah09]), SG ∅ ⊂ PL {#pl} on the other — realized here over ChristopoulosZompi2023.K, with specs carried by the same rule type the Subset-Principle study runs on. What changes is only the competition.

Main results:

• mem_eval_iff / mem_eval_iff_lexMins — the strict-domination Eval cut cascade is exactly lexicographic minimization: an Eval survivor is a LexMinProblem.lexMins optimum (the shared core OptimalityTheory.Tableau aliases), so this Max/Dep competition and phonological OT are one engine.
• eastFrisian_pattern / malayalam_pattern — the two minimally compliant Russian-doll patterns of §4.1.3: East Frisian 3M (h-äi, z-äi; h-um, h-ör) puts ABA on ⟨NOM.SG, NOM.PL, ACC.PL⟩ with AAA on ⟨NOM.SG, ACC.SG, ACC.PL⟩; Malayalam 1EX (ñān, ñaŋŋaḷ; enne, ñaŋŋaḷe) the reverse — same two candidate specifications, opposite rankings of the Dep pair and of the Max pair.
• checkerboard_excluded — the system's novel exclusion: over every ranking of the four relativized constraints and every two-candidate vocabulary on the paradigm's feature space, a candidate winning NOM.SG and ACC.PL also wins ACC.SG or NOM.PL (kernel-checked exhaustively); checkerboard_excluded_general states the vocabulary-general claim (the dissertation's W/T/L leftmost-column argument), left as a sorry TODO.
• unidimensional_ABA_excluded — *ABA down the singular case column survives the move to violable constraints, over every ranking (§4.1.4).
• depTop_eq_subsetPrinciple — [Wol08]'s mimicry, connecting the two engines: with global Dep outranking global Max, whenever some candidate is subset-applicable, unique Max/Dep winners are exactly the Subset-Principle-with-feature-counting winners of ChristopoulosZompi2023.pattern ([Hal97]'s counting formulation). The dual corner (Max ≫ Dep) is nanosyntax's least-specified non-underspecified choice.

inductive Zompi2023.Dim : Type

The inflectional dimensions the constraints are relativized to.

• kase : Dim
• num : Dim
• gen : Dim

@[implicit_reducible]

instance Zompi2023.instDecidableEqDim : DecidableEq Dim

Equations

• Zompi2023.instDecidableEqDim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Zompi2023.instReprDim.repr : Dim → ℕ → Std.Format

Equations

• Zompi2023.instReprDim.repr Zompi2023.Dim.kase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zompi2023.Dim.kase")).group prec✝
• Zompi2023.instReprDim.repr Zompi2023.Dim.num prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zompi2023.Dim.num")).group prec✝
• Zompi2023.instReprDim.repr Zompi2023.Dim.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zompi2023.Dim.gen")).group prec✝

@[implicit_reducible]

instance Zompi2023.instReprDim : Repr Dim

Equations

• Zompi2023.instReprDim = { reprPrec := Zompi2023.instReprDim.repr }

def Zompi2023.dimOf : ChristopoulosZompi2023.K → Dim

Which dimension each feature of ChristopoulosZompi2023.K belongs to.

Equations

• Zompi2023.dimOf ChristopoulosZompi2023.K.k0 = Zompi2023.Dim.kase
• Zompi2023.dimOf ChristopoulosZompi2023.K.k1 = Zompi2023.Dim.kase
• Zompi2023.dimOf ChristopoulosZompi2023.K.k2 = Zompi2023.Dim.kase
• Zompi2023.dimOf ChristopoulosZompi2023.K.k3 = Zompi2023.Dim.kase
• Zompi2023.dimOf ChristopoulosZompi2023.K.s0 = Zompi2023.Dim.num
• Zompi2023.dimOf ChristopoulosZompi2023.K.p0 = Zompi2023.Dim.num
• Zompi2023.dimOf ChristopoulosZompi2023.K.m0 = Zompi2023.Dim.gen
• Zompi2023.dimOf ChristopoulosZompi2023.K.f0 = Zompi2023.Dim.gen

structure Zompi2023.ZCell : Type

A case-number cell.

• case : ChristopoulosZompi2023.Case3
• num : ChristopoulosZompi2023.LNum

def Zompi2023.instDecidableEqZCell.decEq (x✝ x✝¹ : ZCell) : Decidable (x✝ = x✝¹)

Equations

• Zompi2023.instDecidableEqZCell.decEq { case := a, num := a_1 } { case := b, num := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Zompi2023.instDecidableEqZCell : DecidableEq ZCell

Equations

• Zompi2023.instDecidableEqZCell = Zompi2023.instDecidableEqZCell.decEq

@[implicit_reducible]

instance Zompi2023.instFintypeZCell : Fintype ZCell

Equations

• Zompi2023.instFintypeZCell = Fintype.ofEquiv ((_ : ChristopoulosZompi2023.Case3) × ChristopoulosZompi2023.LNum) Zompi2023.ZCell.proxyTypeEquiv

def Zompi2023.instReprZCell.repr : ZCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Zompi2023.instReprZCell : Repr ZCell

Equations

• Zompi2023.instReprZCell = { reprPrec := Zompi2023.instReprZCell.repr }

def Zompi2023.zdecomp (c : ZCell) : Finset ChristopoulosZompi2023.K

The cumulative two-dimensional decomposition ((163)): SCC-style case (NOM ∅ ⊂ ACC {k₁} ⊂ DAT {k₁,k₂}) crossed with cumulative number (SG ∅ ⊂ PL {p₀}).

Equations

• Zompi2023.zdecomp c = ChristopoulosZompi2023.scc c.case ∪ match c.num with | ChristopoulosZompi2023.LNum.sg => ∅ | ChristopoulosZompi2023.LNum.pl => {ChristopoulosZompi2023.K.p0}

@[reducible, inline]

abbrev Zompi2023.Cand (F : Type u_2) : Type u_2

A candidate: the Subset-Principle study's rule carrier, re-read as an OT candidate — the spec may now be unfaithful to the context in both directions.

Equations

• Zompi2023.Cand F = Morphology.Decomposition.Rule Zompi2023.ZCell Zompi2023.zdecomp F

inductive Zompi2023.Con : Type

The constraint inventory: Max/Dep relativized to a dimension ((162)), plus the unrelativized globals of (161) used for the corner rankings.

• maxD (d : Dim) : Con
• depD (d : Dim) : Con
• maxG : Con
• depG : Con

@[implicit_reducible]

instance Zompi2023.instDecidableEqCon : DecidableEq Con

Equations

• Zompi2023.instDecidableEqCon = Zompi2023.instDecidableEqCon.decEq

def Zompi2023.instDecidableEqCon.decEq (x✝ x✝¹ : Con) : Decidable (x✝ = x✝¹)

Equations

• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.maxD a) (Zompi2023.Con.maxD b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.maxD d) (Zompi2023.Con.depD d_1) = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.maxD d) Zompi2023.Con.maxG = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.maxD d) Zompi2023.Con.depG = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.depD d) (Zompi2023.Con.maxD d_1) = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.depD a) (Zompi2023.Con.depD b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.depD d) Zompi2023.Con.maxG = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq (Zompi2023.Con.depD d) Zompi2023.Con.depG = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.maxG (Zompi2023.Con.maxD d) = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.maxG (Zompi2023.Con.depD d) = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.maxG Zompi2023.Con.maxG = isTrue ⋯
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.maxG Zompi2023.Con.depG = isFalse Zompi2023.instDecidableEqCon.decEq._proof_13
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.depG (Zompi2023.Con.maxD d) = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.depG (Zompi2023.Con.depD d) = isFalse ⋯
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.depG Zompi2023.Con.maxG = isFalse Zompi2023.instDecidableEqCon.decEq._proof_16
• Zompi2023.instDecidableEqCon.decEq Zompi2023.Con.depG Zompi2023.Con.depG = isTrue ⋯

@[implicit_reducible]

instance Zompi2023.instReprCon : Repr Con

Equations

• Zompi2023.instReprCon = { reprPrec := Zompi2023.instReprCon.repr }

def Zompi2023.instReprCon.repr : Con → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Zompi2023.instReprCon.repr Zompi2023.Con.maxG prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zompi2023.Con.maxG")).group prec✝
• Zompi2023.instReprCon.repr Zompi2023.Con.depG prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zompi2023.Con.depG")).group prec✝

def Zompi2023.viol {F : Type u_1} : Con → ZCell → Cand F → ℕ

Violation counts: Max-type stars for expected features the spec lacks, Dep-type stars for spurious features the spec adds, counted on one dimension or globally.

Equations

• Zompi2023.viol (Zompi2023.Con.maxD d) x✝¹ x✝ = {k ∈ Zompi2023.zdecomp x✝¹ \ x✝.feats | Zompi2023.dimOf k = d}.card
• Zompi2023.viol (Zompi2023.Con.depD d) x✝¹ x✝ = {k ∈ x✝.feats \ Zompi2023.zdecomp x✝¹ | Zompi2023.dimOf k = d}.card
• Zompi2023.viol Zompi2023.Con.maxG x✝¹ x✝ = (Zompi2023.zdecomp x✝¹ \ x✝.feats).card
• Zompi2023.viol Zompi2023.Con.depG x✝¹ x✝ = (x✝.feats \ Zompi2023.zdecomp x✝¹).card

def Zompi2023.cut {F : Type u_1} (c : ZCell) (cands : List (Cand F)) (C : Con) : List (Cand F)

One Eval cut: keep the candidates with fewest violations of C.

Equations

• Zompi2023.cut c cands C = match (List.map (Zompi2023.viol C c) cands).min? with | none => cands | some m => List.filter (fun (r : Zompi2023.Cand F) => decide (Zompi2023.viol C c r = m)) cands

def Zompi2023.eval {F : Type u_1} (rk : List Con) (v : List (Cand F)) (c : ZCell) : List (Cand F)

Strict-domination Eval: successive cuts down the ranking, top constraint first.

Equations

• Zompi2023.eval rk v c = List.foldl (Zompi2023.cut c) v rk

def Zompi2023.Wins {F : Type u_1} (rk : List Con) (v : List (Cand F)) (c : ZCell) (r : Cand F) : Prop

r is the unique survivor of Eval at c.

Equations

• Zompi2023.Wins rk v c r = (Zompi2023.eval rk v c = [r])

@[implicit_reducible]

instance Zompi2023.instDecidableWinsOfDecidableEq {F : Type u_1} [DecidableEq F] {rk : List Con} {v : List (Cand F)} {c : ZCell} {r : Cand F} : Decidable (Wins rk v c r)

Equations

• Zompi2023.instDecidableWinsOfDecidableEq = Zompi2023.instDecidableWinsOfDecidableEq._aux_1

The shared lexicographic-minimization core

eval is the strict-domination filter cascade; the phonology OT engine is lexicographic arg-min over a fixed-length violation profile. Its foundation is Core.Optimization.Evaluation.LexMinProblem — a finite candidate set scored by a Lex (Fin n → ℕ) profile, exposing the winner set LexMinProblem.lexMins; OptimalityTheory.Tableau is a definitional alias for it (Tableau := LexMinProblem, Tableau.optimal := lexMins). eval and this engine are one object, not two parallel engines: mem_eval_iff characterizes an Eval survivor as a lexicographic minimizer of the ranked violation vector, and mem_eval_iff_lexMins reads that off the LexMinProblem whose candidates are v and whose profile is that vector. So morphological Max/Dep Eval and phonological OT provably share the same lexicographic core.

def Zompi2023.rankedViols {F : Type u_1} (rk : List Con) (c : ZCell) (r : Cand F) : List ℕ

The candidate's violation vector at a cell, ordered by the ranking — the List ℕ reading of the OT ViolationProfile.

Equations

• Zompi2023.rankedViols rk c r = List.map (fun (C : Zompi2023.Con) => Zompi2023.viol C c r) rk

@[simp]

theorem Zompi2023.rankedViols_nil {F : Type u_1} (c : ZCell) (r : Cand F) : rankedViols [] c r = []

@[simp]

theorem Zompi2023.rankedViols_cons {F : Type u_1} (C : Con) (rk : List Con) (c : ZCell) (r : Cand F) : rankedViols (C :: rk) c r = viol C c r :: rankedViols rk c r

theorem Zompi2023.mem_cut_iff {F : Type u_1} {C : Con} {c : ZCell} {v : List (Cand F)} {r : Cand F} : r ∈ cut c v C ↔ r ∈ v ∧ ∀ s ∈ v, viol C c r ≤ viol C c s

A candidate survives one Eval cut iff it minimises that constraint over the field: the cut keeps exactly the constraint's arg-min.

theorem Zompi2023.mem_eval_iff {F : Type u_1} {rk : List Con} {v : List (Cand F)} {c : ZCell} {r : Cand F} : r ∈ eval rk v c ↔ r ∈ v ∧ ∀ s ∈ v, Core.Optimization.Evaluation.LexLE (rankedViols rk c r) (rankedViols rk c s)

Eval is lexicographic minimization. A candidate survives the whole cut cascade iff its ranked violation vector is lexicographically ≤ every rival's: the strict-domination cut sequence computes exactly the lex-min set.

theorem Zompi2023.rankedViols_eq_ofFn {F : Type u_1} (rk : List Con) (c : ZCell) (r : Cand F) : rankedViols rk c r = List.ofFn fun (i : Fin rk.length) => viol (rk.get i) c r

The ranked violation vector is the fixed-length OT profile spelled out as a list.

def Zompi2023.zTableau {F : Type u_1} [DecidableEq F] (rk : List Con) (v : List (Cand F)) (c : ZCell) (hv : v ≠ []) : Core.Optimization.Evaluation.LexMinProblem (Cand F) rk.length

The Eval competition as a LexMinProblem — the engine OptimalityTheory.Tableau aliases: candidate set v, profile the ranked violation vector (rank position i reading the i-th constraint as a violation count via lexFinNatOf). This is a phonological OT tableau with morphological Max/Dep constraints.

Equations

• Zompi2023.zTableau rk v c hv = { candidates := v.toFinset, profile := Core.Optimization.Evaluation.lexFinNatOf fun (i : Fin rk.length) => Zompi2023.viol (rk.get i) c, nonempty := ⋯ }

theorem Zompi2023.mem_eval_iff_lexMins {F : Type u_1} [DecidableEq F] {rk : List Con} {v : List (Cand F)} {c : ZCell} {r : Cand F} (hv : v ≠ []) : r ∈ eval rk v c ↔ r ∈ (zTableau rk v c hv).lexMins

Eval and OT are one engine. An Eval survivor is exactly a lex-minimizer of the OT tableau zTableau: the morphological Max/Dep competition is a phonological OT tableau (LexMinProblem) over the shared lexicographic-minimization core.

def Zompi2023.rankings : List (List Con)

The 24 rankings of the four dimension-relativized constraints of the case-number paradigm, enumerated (kernel-reducible, unlike List.permutations).

Equations

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

def Zompi2023.featSpace : Finset ChristopoulosZompi2023.K

The candidate feature space of the case-number paradigm.

Equations

• Zompi2023.featSpace = {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.k2, ChristopoulosZompi2023.K.p0}

def Zompi2023.specSpace : List (Finset ChristopoulosZompi2023.K)

The possible context specifications ((163)): feature-structural entailments hold inside specs too — κ_dat only alongside κ_dep. The dissertation makes this well-formedness an entry condition on candidates and flags it as crucial for unidimensional *ABA.

Equations

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

The two minimally compliant patterns (§4.1.3)

def Zompi2023.eastFrisian : List (Cand String)

East Frisian 3M candidates ((165)): z- specified for plural, h- for accusative.

Equations

• Zompi2023.eastFrisian = [{ feats := {ChristopoulosZompi2023.K.p0}, exponent := "z" }, { feats := {ChristopoulosZompi2023.K.k1}, exponent := "h" }]

theorem Zompi2023.eastFrisian_pattern : Wins [Con.depD Dim.num, Con.depD Dim.kase, Con.maxD Dim.kase, Con.maxD Dim.num] eastFrisian { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.k1}, exponent := "h" } ∧ Wins [Con.depD Dim.num, Con.depD Dim.kase, Con.maxD Dim.kase, Con.maxD Dim.num] eastFrisian { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.pl } { feats := {ChristopoulosZompi2023.K.p0}, exponent := "z" } ∧ Wins [Con.depD Dim.num, Con.depD Dim.kase, Con.maxD Dim.kase, Con.maxD Dim.num] eastFrisian { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.k1}, exponent := "h" } ∧ Wins [Con.depD Dim.num, Con.depD Dim.kase, Con.maxD Dim.kase, Con.maxD Dim.num] eastFrisian { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.pl } { feats := {ChristopoulosZompi2023.K.k1}, exponent := "h" }

East Frisian ((164), (166)): ranking Dep(#) ≫ Dep(K) and Max(K) ≫ Max(#) yields h- in NOM.SG, ACC.SG, ACC.PL and z- in NOM.PL — ABA along ⟨NOM.SG, NOM.PL, ACC.PL⟩, AAA along ⟨NOM.SG, ACC.SG, ACC.PL⟩.

def Zompi2023.malayalam : List (Cand String)

Malayalam 1EX candidates ((168)): same two specifications, exponents ñan- and enn-.

Equations

• Zompi2023.malayalam = [{ feats := {ChristopoulosZompi2023.K.p0}, exponent := "ñan" }, { feats := {ChristopoulosZompi2023.K.k1}, exponent := "enn" }]

theorem Zompi2023.malayalam_pattern : Wins [Con.depD Dim.kase, Con.depD Dim.num, Con.maxD Dim.num, Con.maxD Dim.kase] malayalam { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.p0}, exponent := "ñan" } ∧ Wins [Con.depD Dim.kase, Con.depD Dim.num, Con.maxD Dim.num, Con.maxD Dim.kase] malayalam { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.pl } { feats := {ChristopoulosZompi2023.K.p0}, exponent := "ñan" } ∧ Wins [Con.depD Dim.kase, Con.depD Dim.num, Con.maxD Dim.num, Con.maxD Dim.kase] malayalam { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.k1}, exponent := "enn" } ∧ Wins [Con.depD Dim.kase, Con.depD Dim.num, Con.maxD Dim.num, Con.maxD Dim.kase] malayalam { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.pl } { feats := {ChristopoulosZompi2023.K.p0}, exponent := "ñan" }

Malayalam ((167), (169)): swapping both relative rankings — Dep(K) ≫ Dep(#), Max(#) ≫ Max(K) — reverses both diagonals: ñan- in NOM.SG, NOM.PL, ACC.PL and enn- in ACC.SG.

The checkerboard exclusion

theorem Zompi2023.checkerboard_excluded (rk : List Con) : rk ∈ rankings → ∀ fa ∈ featSpace.powerset, ∀ fb ∈ featSpace.powerset, Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.sg } { feats := fa, exponent := ChristopoulosZompi2023.Ex.A } → Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.pl } { feats := fa, exponent := ChristopoulosZompi2023.Ex.A } → Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.sg } { feats := fa, exponent := ChristopoulosZompi2023.Ex.A } ∨ Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.pl } { feats := fa, exponent := ChristopoulosZompi2023.Ex.A }

The novel multidimensional generalization, exhaustively: over all 24 rankings and all two-candidate vocabularies on the paradigm's feature space, a candidate that uniquely wins both NOM.SG and ACC.PL also uniquely wins ACC.SG or NOM.PL — the non-compliant "checkerboard" is ungenerable while either Russian-doll ABA remains available (eastFrisian_pattern, malayalam_pattern).

theorem Zompi2023.checkerboard_excluded_general {F : Type u_1} {rk : List Con} {v : List (Cand F)} {a : Cand F} (hperm : rk.Perm [Con.maxD Dim.kase, Con.maxD Dim.num, Con.depD Dim.kase, Con.depD Dim.num]) (hns : Wins rk v { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.sg } a) (hap : Wins rk v { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.pl } a) : Wins rk v { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.sg } a ∨ Wins rk v { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.pl } a

The vocabulary-general checkerboard exclusion, for any candidate list and any ranking of the four relativized constraints.

TODO: the shared-core mem_eval_iff reduces Wins to strict lexicographic domination of the ranked violation vector (eval rk v c = [a] iff a's vector lex-dominates every rival's, strictly since a tying rival would also survive). On that footing the dissertation's argument ((170) and §4.1.4's continuation) runs: (i) dimension-relativized counts factor through the dimension slice of the context (viol (maxD d)/viol (depD d) at ⟨κ,ν⟩ depend only on the d-part of zdecomp), so each constraint's field-level W/T/L verdict at NOM.SG and ACC.PL transfers to the cell sharing its dimension; (ii) Wins at a cell is equivalent to the leftmost non-tie column of the ranking (over the original field, cascade-eliminations included) being a strict win; (iii) a three-way case analysis on the relative rank of the leftmost strict-win columns at NOM.SG and ACC.PL then forces a strict win at ACC.SG or NOM.PL. Step (ii) — the column-scan characterization of the filter cascade — is the load-bearing lemma still to be formalized.

theorem Zompi2023.unidimensional_ABA_excluded (rk : List Con) : rk ∈ rankings → ∀ fa ∈ specSpace, ∀ fb ∈ specSpace, Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.sg } { feats := fa, exponent := ChristopoulosZompi2023.Ex.A } → Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.dat, num := ChristopoulosZompi2023.LNum.sg } { feats := fa, exponent := ChristopoulosZompi2023.Ex.A } → ¬Wins rk [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.sg } { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }

Unidimensional *ABA survives the move to violable constraints (§4.1.4): down the singular case column, no ranking and no two-candidate vocabulary of well-formed specs lets one candidate win NOM and DAT while the other takes ACC.

theorem Zompi2023.illformed_spec_breaks_unidimensional_ABA : Wins [Con.maxD Dim.kase, Con.depD Dim.kase, Con.maxD Dim.num, Con.depD Dim.num] [{ feats := {ChristopoulosZompi2023.K.k2}, exponent := ChristopoulosZompi2023.Ex.A }, { feats := {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.p0}, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.nom, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.k2}, exponent := ChristopoulosZompi2023.Ex.A } ∧ Wins [Con.maxD Dim.kase, Con.depD Dim.kase, Con.maxD Dim.num, Con.depD Dim.num] [{ feats := {ChristopoulosZompi2023.K.k2}, exponent := ChristopoulosZompi2023.Ex.A }, { feats := {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.p0}, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.acc, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.p0}, exponent := ChristopoulosZompi2023.Ex.B } ∧ Wins [Con.maxD Dim.kase, Con.depD Dim.kase, Con.maxD Dim.num, Con.depD Dim.num] [{ feats := {ChristopoulosZompi2023.K.k2}, exponent := ChristopoulosZompi2023.Ex.A }, { feats := {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.p0}, exponent := ChristopoulosZompi2023.Ex.B }] { case := ChristopoulosZompi2023.Case3.dat, num := ChristopoulosZompi2023.LNum.sg } { feats := {ChristopoulosZompi2023.K.k2}, exponent := ChristopoulosZompi2023.Ex.A }

The well-formedness entry condition is necessary, not merely convenient: admit the entailment-violating spec {κ_dat} (κ_dat without κ_dep) and case-column ABA becomes derivable — {κ_dat} takes NOM and DAT while {κ_dep, #pl} takes ACC under Max(K) ≫ Dep(K) ≫ Max(#) ≫ Dep(#). The dissertation asserts the assumption "will play a crucial role in allowing the current theory to derive unidimensional *ABA"; this witness confirms the system cannot do without it.

The corner rankings: Wolf's mimicry

theorem Zompi2023.depTop_eq_subsetPrinciple (fa : Finset ChristopoulosZompi2023.K) : fa ∈ featSpace.powerset → ∀ fb ∈ featSpace.powerset, ∀ (c : ZCell), ∀ r ∈ [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }], fa ⊆ zdecomp c ∨ fb ⊆ zdecomp c → Wins [Con.depG, Con.maxG] [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] c r → Morphology.Decomposition.pattern [{ feats := fa, exponent := ChristopoulosZompi2023.Ex.A }, { feats := fb, exponent := ChristopoulosZompi2023.Ex.B }] c = some r.exponent

Dep ≫ Max is the Subset Principle with feature counting ([Wol08] on [Hal97]; the dissertation's §4.1.1): whenever some candidate is subset-applicable, the unique winner under the global corner ranking is exactly what ChristopoulosZompi2023.pattern — the Elsewhere engine the companion study runs — selects. Inviolable-Max is the dual, nanosyntax's least-specified non-underspecified choice ([Sta09a]).