Zompì (2023): *ABA in Multidimensional Paradigms

This file formalizes the Max/Dep account of exponent selection in [Zom23]. An exponent's context specification may be both underspecified and overspecified for the cell it realizes; each departure is penalized by a violable faithfulness constraint, Max for expected features the specification lacks and Dep for spurious features it adds ([Wol08], after [McCP95]), relativized to the paradigm's dimensions, and the winner is selected by strict-domination evaluation ([PS93]). Cells are the cumulative case and number decompositions of ChristopoulosZompi2023, with candidates carried by the same rule type as that study's Subset Principle, so that only the competition changes.

Evaluation is lexicographic minimization of the ranked violation vector (mem_eval_iff), the engine of OptimalityTheory.Tableau (mem_eval_iff_optimal). On it, the two minimally compliant patterns of the case-number paradigm are derived from opposite rankings of the same two candidate specifications, East Frisian with ABA down the nominative column and Malayalam with ABA down the plural row (eastFrisian_pattern, malayalam_pattern); the checkerboard pattern, in which one exponent takes the nominative singular and the accusative plural but neither of the other two cells, is excluded over every ranking and every two-candidate vocabulary (checkerboard_excluded); unidimensional *ABA down the singular case column survives the move to violable constraints (unidimensional_ABA_excluded), and only because specifications respect the feature entailments (illformed_spec_breaks_unidimensional_ABA); and with Dep outranking Max the system is the Subset Principle with feature counting ([Wol08], [Hal97a]) whenever some candidate is subset-applicable (depTop_eq_subsetPrinciple).

Implementation notes

• Rankings of the four dimension-relativized constraints are enumerated rather than generated by List.permutations, which does not reduce in the kernel.
• The exhaustive theorems range over two-candidate vocabularies on the paradigm's feature space; the dissertation's argument is vocabulary-general.

TODO

• The vocabulary-general checkerboard exclusion, by the dissertation's argument that each dimension-relativized constraint's verdict at a cell transfers to the cell sharing that dimension, so that the leftmost decisive column at the nominative singular or the accusative plural decides one of the other two cells.

References

• [Zom23]
• [Wol08]
• [McCP95]
• [PS93]
• [Hal97a]
• [Sta09a]
• [SMX+19]
• [Cah09]

inductive Zompi2023.Dim : Type

The inflectional dimensions the constraints are relativized to.

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

@[instance_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✝

@[instance_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 ⋯

@[instance_reducible]

instance Zompi2023.instDecidableEqZCell : DecidableEq ZCell

Equations

• Zompi2023.instDecidableEqZCell = Zompi2023.instDecidableEqZCell.decEq

@[instance_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.

@[instance_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

@[instance_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 ⋯

@[instance_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])

@[instance_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, OptimalityTheory.Tableau, a finite candidate set scored by a Lex (Fin n → ℕ) profile with the winner set Tableau.optimal. 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_optimal reads that off the tableau 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, 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 ≠ []) : OptimalityTheory.Tableau (Cand F) rk.length

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

Equations

• Zompi2023.zTableau rk v c hv = { candidates := v.toFinset, profile := fun (r : Zompi2023.Cand F) => toLex fun (i : Fin rk.length) => Zompi2023.viol (rk.get i) c r, nonempty := ⋯ }

theorem Zompi2023.mem_eval_iff_optimal {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).optimal

Eval and OT are one engine. An Eval survivor is exactly a winner of the OT tableau zTableau: the morphological Max/Dep competition is a phonological OT tableau over the shared lexicographic order.

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.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 [Hal97a]; 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]).