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 (PhrasalCophonology) 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.
• PhrasalCophonology: the phasal trigger — a phase-head predicate bundled with its subranking; selectCophonology picks the first match from a registry, the elsewhere ordering of [SJI20].

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. Consuming studies: Studies/AkinboFwangwar2026.lean (per-VI, dominant grammatical tone) and Studies/SandeClemDabkowski2026.lean (phasal, Guébie discontinuous harmony).

Ranking merge

def OptimalityTheory.Cophonology.mergeRanking {L : Type u_1} {C : Type u_2} [DecidableEq L] (default sub : List (L × Constraints.Constraint C)) : List (L × Constraints.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 × Constraints.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 × Constraints.Constraint C)) (candidates : List C) (h : candidates ≠ [] := by decide) : Finset C

Evaluate a candidate set under a cophonology: merge the trigger's subranking with the default ranking, then take the optimal candidates. The core of CPT — the same candidate set can yield different winners depending on which subranking is active. A dominant grammatical-tone trigger, for instance, promotes a basemap-faithfulness constraint above the default markedness constraints, forcing the output to match the basemap rather than preserve the target's underlying tones ([Rol18] Ch 5).

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 × Constraints.Constraint C)) (candidates : List C) (h : candidates ≠ []) : cophonologicalEval defaultRanking [] candidates h = (Tableau.ofRanking candidates (List.map (fun (x : L × Constraints.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.

Cophonologies by ph(r)ase

@[reducible, inline]

abbrev OptimalityTheory.Cophonology.PhrasalCophonology (L : Type u_3) (C : Type u_4) : Type (max u_4 u_3)

A cophonology triggered by spell-out of a particular kind of phase ([SJI20]): a Minimalist.Phase.Trigger whose payload is the constraint subranking promoted within the matched phase. Per [SCD26], the vP phase carries the ATR-harmony cophonology (the selector matches v heads) and the DP phase the definite-marker phonology (the selector matches definite D heads). Selection from a registry is Minimalist.Phase.selectTrigger (first-match, the elsewhere ordering).

Equations

• OptimalityTheory.Cophonology.PhrasalCophonology L C = Minimalist.Phase.Trigger (List (L × Constraints.Constraint C))