Dominant Cophonology ↔ Tonal Overwrite Agreement

@cite{rolle-2018}

This file proves the general agreement between the two parallel formalisms for dominant grammatical tone in @cite{rolle-2018}:

1. Direct: tonalOverwrite — a functional operation replacing tones
2. Constraint-based: cophonologicalEval — OT evaluation under a morpheme-specific subranking that promotes MxBM-C (basemap faithfulness)

The key insight is that when MxBM-C is the top-ranked constraint (via cophonological subranking), OT evaluation necessarily selects basemap-faithful candidates — which are exactly the tonalOverwrite outputs. The per-tableau agreement theorems in study files (e.g., AkinboFwangwar2026.t24_winner_agrees_with_deriveVerb) are instances of this general result.

Proof structure

optimal_zero_first (OT.lean)
   "if any candidate has 0 violations on the top constraint,
    every optimal candidate does too"
         ↓
dominant_coph_selects_basemap_faithful
   "when MxBM-C is in the subranking, every optimal candidate
    has extractTier c = basemapTier"
         ↓
dominant_coph_agrees_with_tonalOverwrite
   "every optimal candidate under the dominant cophonology agrees
    with tonalOverwrite — the two formalisms are equivalent"

theorem Phonology.Autosegmental.DominantCophAgreement.dominant_coph_selects_basemap_faithful {C : Type} [DecidableEq C] (basemapTier : List RegisterTier.TRN) (extractTier : C → List RegisterTier.TRN) (defaultRanking : List (Core.Constraint.OT.NamedConstraint C)) (candidates : List C) (h : candidates ≠ []) (hLen : ∀ c ∈ candidates, (extractTier c).length = basemapTier.length) (hFaithful : ∃ c ∈ candidates, extractTier c = basemapTier) : have mxbmc := BasemapCorrespondence.mkBasemapConstraint basemapTier extractTier; ∀ c ∈ CophonologyTheory.cophonologicalEval defaultRanking [mxbmc] candidates h, extractTier c = basemapTier

The general agreement theorem: when MxBM-C (basemap faithfulness) is in the cophonological subranking, every OT-optimal candidate is basemap-faithful — its tonal tier exactly matches the basemap output.

This is the mathematical core of @cite{rolle-2018} Ch 5: dominant GT is not a special rule but a consequence of promoting a faithfulness constraint. The constraint forces the matrix output to correspond to the basemap output, which is independent of the target's underlying tones (basemapOutput_tone_independent_whole).

theorem Phonology.Autosegmental.DominantCophAgreement.dominant_coph_agrees_with_tonalOverwrite {S C : Type} [DecidableEq S] [BEq S] [Repr S] [DecidableEq C] (host : List (GrammaticalTone.TBU S)) (t defaultTone : RegisterTier.TRN) (extractTier : C → List RegisterTier.TRN) (defaultRanking : List (Core.Constraint.OT.NamedConstraint C)) (candidates : List C) (h : candidates ≠ []) (hLen : ∀ c ∈ candidates, (extractTier c).length = (BasemapCorrespondence.tonalTier (BasemapCorrespondence.basemapOutput host { name := "", melody := [t], window := GrammaticalTone.ValuationWindow.whole } defaultTone)).length) (hFaithful : ∃ c ∈ candidates, extractTier c = BasemapCorrespondence.tonalTier (BasemapCorrespondence.basemapOutput host { name := "", melody := [t], window := GrammaticalTone.ValuationWindow.whole } defaultTone)) : have spec := { name := "", melody := [t], window := GrammaticalTone.ValuationWindow.whole }; have baseTier := BasemapCorrespondence.tonalTier (BasemapCorrespondence.basemapOutput host spec defaultTone); have mxbmc := BasemapCorrespondence.mkBasemapConstraint baseTier extractTier; ∀ c ∈ CophonologyTheory.cophonologicalEval defaultRanking [mxbmc] candidates h, extractTier c = BasemapCorrespondence.tonalTier (GrammaticalTone.tonalOverwrite host spec)

Dominant cophonology agrees with tonalOverwrite: for whole-word single-tone replacement, OT evaluation under the dominant cophonology selects candidates whose tonal tier matches the direct tonalOverwrite operation.

This connects the two formalisms of dominant GT:

1. Direct (tonalOverwrite): replaces all tones with the melody
2. Constraint-based (cophonologicalEval with MxBM-C): selects candidates faithful to the basemap output

The connection goes through tonalOverwrite_basemap_faithful: the tonalOverwrite output equals the basemap output, and dominant_coph_selects_basemap_faithful ensures the OT evaluation selects exactly the basemap-faithful candidates.