Cophonology theory

A cophonology is a morpheme-specific constraint ranking: in Cophonology Theory ([IZ07]), individual triggers override parts of the default phonological grammar, and the surface form is the optimal candidate under the trigger's ranking rather than the default one. The constraint-merge mechanics are a single apparatus; what varies across the theory family is the trigger:

• per Vocabulary Item ([SJ17]; [Rol18] Ch 4): the inserted VI's R component is the subranking — the subranking argument to cophonologicalEval;
• per ph(r)ase ([SJI20]): a spell-out phase (vP, CP, DP) carries the subranking and activates it over its whole complement at spell-out, deriving cross-word morphologically conditioned effects.

Main definitions

• mergeRanking: place a subranking's constraints above the default ranking, preserving the relative order of the rest.
• cophonologicalEval: OT evaluation under the merged ranking. With an empty subranking it is standard OT evaluation (cophonologicalEval_empty_sub): CPT properly generalizes OT.

Implementation notes

Syntactic reference stays indirect: syntax selects which cophonology fires, but the cophonology itself contains no syntactic vocabulary — [New08]-style cyclic phase phonology without violating modularity.

The substrate implements neither bracket erasure ([Kip82]) nor DM PF discharge ([EN07]) — rival theories of the syntax–phonology interface that [SCD26] §6.2 argues against; it makes the CPT view expressible without forcing it on consumers. The phasal trigger has no formalization yet; Studies/Rolle2018.lean consumes the per-VI one (dominant grammatical tone).

Ranking merge

def OptimalityTheory.Cophonology.mergeRanking {L : Type u_1} {C : Type u_2} [DecidableEq L] (default sub : List (L × Constraint C)) : List (L × Constraint C)

Merge a morpheme-specific subranking with the default ranking: the subranking's constraints first (in the order given), then the default constraints whose labels do not appear in it — the trigger promotes its constraints without disturbing the relative order of the rest.

Equations

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

theorem OptimalityTheory.Cophonology.mergeRanking_empty_sub {L : Type u_1} {C : Type u_2} [DecidableEq L] (default : List (L × Constraint C)) : mergeRanking default [] = default

An empty subranking produces the default ranking unchanged.

Cophonological evaluation

def OptimalityTheory.Cophonology.cophonologicalEval {L : Type u_1} {C : Type u_2} [DecidableEq L] [DecidableEq C] (defaultRanking subranking : List (L × Constraint C)) (candidates : List C) (h : candidates ≠ [] := by decide) : Finset C

Cophonological evaluation takes the optimal candidates under the default ranking merged with the trigger's subranking.

Equations

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

theorem OptimalityTheory.Cophonology.cophonologicalEval_empty_sub {L : Type u_1} {C : Type u_2} [DecidableEq L] [DecidableEq C] (defaultRanking : List (L × Constraint C)) (candidates : List C) (h : candidates ≠ []) : cophonologicalEval defaultRanking [] candidates h = (Tableau.ofRanking candidates (List.map (fun (x : L × Constraint C) => x.2) defaultRanking) h).optimal

With an empty subranking, cophonological evaluation reduces to standard OT evaluation: CPT is a proper generalization of OT.