Matrix-Basemap Correspondence (MxBM-C)

@cite{rolle-2018} @cite{benua-1997}

Matrix-Basemap Correspondence is @cite{rolle-2018}'s central theoretical contribution (Ch 5). It extends Output-Output Correspondence (@cite{benua-1997}) to explain dominant grammatical tone as a special type of faithfulness rather than markedness.

The three problems

Any theory of dominant vs. non-dominant GT must address:

1. Origin problem: where does the grammatical tune come from?
2. Erasure problem: why do the target's underlying tones go unrealized?
3. Scope problem: what determines the domain of the GT operation?

MxBM-C addresses the erasure problem. The origin problem is solved by floating tone representation (the tune is part of the trigger's UR); the scope problem by CoP-scope (CoPScope.lean).

Key insight: dominance as basemap faithfulness

A basemap is an abstract I/O mapping derived from a "deficient projection" of the input: all valued (lexical) tones on the target are stripped, leaving only floating (grammatical) tones. The basemap output shows what the form would look like if the target had no underlying tones.

Dominant GT = faithfulness to the basemap output. The matrix (actual) output must correspond to the basemap output. Since the basemap has no valued tones to preserve, its output is determined entirely by the grammatical tune. The matrix output must match, so the target's underlying tones are forced to go unrealized.

Non-dominant GT = no basemap faithfulness. The matrix output is determined by the default constraint ranking, which may preserve underlying tones.

Connection to tonalOverwrite

tonalOverwrite in GrammaticalTone.lean directly implements the computational result of replacive-dominant GT. Under MxBM-C, this result emerges from basemap faithfulness: tonalOverwrite_basemap_faithful proves that the overwrite function produces the same tonal output as basemap-faithful evaluation.

Connection to Correspondence.lean

Matrix-Basemap Correspondence is the IDENT-OO correspondence relation of @cite{mccarthy-prince-1995} / @cite{benua-1997} specialized to the tonal tier. basemapViolations is defined as Corr.identViol on the (matrix, basemap) edge of a binary correspondence diagram between the two tonal tiers — making the connection true by construction rather than via a separate Hamming-distance implementation.

def Phonology.Autosegmental.BasemapCorrespondence.deficientProjection {S : Type} (host : List (GrammaticalTone.TBU S)) (defaultTone : RegisterTier.TRN) : List (GrammaticalTone.TBU S)

Strip all tones from a host word, replacing them with a default tone. The deficient projection of @cite{rolle-2018} Ch 5: the input with all valued (lexical) tones removed, leaving only the segmental skeleton ready to receive floating (grammatical) tones.

The defaultTone is the tone assigned to "unvalued" TBUs — language-specific (often L in African tone languages).

Equations

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

theorem Phonology.Autosegmental.BasemapCorrespondence.deficientProjection_uniform {S : Type} (host : List (GrammaticalTone.TBU S)) (defaultTone : RegisterTier.TRN) : List.map GrammaticalTone.TBU.tone (deficientProjection host defaultTone) = List.map (fun (x : GrammaticalTone.TBU S) => defaultTone) host

Deficient projection produces uniform tone: every TBU gets the default tone.

def Phonology.Autosegmental.BasemapCorrespondence.basemapOutput {S : Type} [DecidableEq S] [BEq S] [Repr S] (host : List (GrammaticalTone.TBU S)) (spec : GrammaticalTone.Spec) (defaultTone : RegisterTier.TRN) : List (GrammaticalTone.TBU S)

Compute the basemap output: apply the grammatical tune to the deficient projection. This represents what the output would look like if the target had no underlying tones — only the floating tones from the trigger determine the surface pattern.

For replacive-dominant GT with a whole-word melody, the basemap output has the grammatical tune on every TBU.

Equations

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

def Phonology.Autosegmental.BasemapCorrespondence.tonalTier {S : Type} (tbus : List (GrammaticalTone.TBU S)) : List RegisterTier.TRN

Extract the tonal tier from a list of TBUs.

Grounded in the unified Phonology.Tier abstraction (Tier.apply Tier.tonal): an erasing string homomorphism (TBU S)* → TRN* in the Kleisli category of Option. The tonal tier is the total (no-erasure) case @cite{goldsmith-1976}.

Equations

• Phonology.Autosegmental.BasemapCorrespondence.tonalTier tbus = Phonology.Tier.tonal.apply tbus

@[simp]

theorem Phonology.Autosegmental.BasemapCorrespondence.tonalTier_eq_map {S : Type} (tbus : List (GrammaticalTone.TBU S)) : tonalTier tbus = List.map GrammaticalTone.TBU.tone tbus

The tonal tier reduces to List.map TBU.tone (the historical formulation), via Tier.total's length-preservation property.

def Phonology.Autosegmental.BasemapCorrespondence.basemapViolations (tier₁ tier₂ : List RegisterTier.TRN) : ℕ

Matrix-Basemap Correspondence violation count: Hamming distance between the matrix tonal tier and the basemap tonal tier.

Derived from Corr.identViol on the (false, true) edge of the binary parallel-pair correspondence between the two tiers. This structurally identifies MxBM-C as IDENT-OO of @cite{mccarthy-prince-1995} / @cite{benua-1997} specialized to the tonal tier — no separate Hamming implementation, no bridge theorem required.

On unequal-length tiers, the underlying Corr.parallel truncates to the shorter prefix (matching List.zip semantics).

Equations

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

theorem Phonology.Autosegmental.BasemapCorrespondence.basemapViolations_self_eq_zero (t : List RegisterTier.TRN) : basemapViolations t t = 0

Self-comparison has zero basemap violations: a tonal tier is perfectly faithful to itself. Derived from Corr.identity_ident_zero.

theorem Phonology.Autosegmental.BasemapCorrespondence.basemapViolations_eq_zero_imp (t₁ t₂ : List RegisterTier.TRN) (hLen : t₁.length = t₂.length) (hZero : basemapViolations t₁ t₂ = 0) : t₁ = t₂

Zero basemap violations with equal-length tiers implies the tiers are identical. The equal-length hypothesis is necessary because the underlying Corr.parallel truncates to min.

def Phonology.Autosegmental.BasemapCorrespondence.mkBasemapConstraint {C : Type} (basemapTier : List RegisterTier.TRN) (extractTier : C → List RegisterTier.TRN) : Core.Constraint.OT.NamedConstraint C

Wrap basemapViolations as a NamedConstraint for use in OT tableaux and cophonological evaluation.

Given a fixed basemap output (the tonal tier of the basemap-faithful form), this constraint evaluates each candidate by comparing its tonal tier against the basemap. In @cite{rolle-2018}'s analysis, dominant triggers promote this constraint above default markedness in their cophonology's subranking.

extractTier converts a candidate to its tonal tier for comparison. This allows the constraint to work with any candidate type, not just raw List TRN.

Equations

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

theorem Phonology.Autosegmental.BasemapCorrespondence.tonalOverwrite_basemap_faithful {S : Type} [DecidableEq S] [BEq S] [Repr S] (host : List (GrammaticalTone.TBU S)) (t defaultTone : RegisterTier.TRN) : have spec := { name := "", melody := [t], window := GrammaticalTone.ValuationWindow.whole }; tonalTier (GrammaticalTone.tonalOverwrite host spec) = tonalTier (basemapOutput host spec defaultTone)

The central theorem of MxBM-C: for replacive-dominant GT with a whole-word single-tone melody, the matrix output's tonal tier equals the basemap output's tonal tier.

This captures @cite{rolle-2018}'s key insight: dominant GT is not a special deletion rule or markedness constraint, but faithfulness to an abstract basemap. The target's underlying tones go unrealized because the output must match what would happen if those tones were never there.

theorem Phonology.Autosegmental.BasemapCorrespondence.basemapOutput_tone_independent_whole {S : Type} [DecidableEq S] [BEq S] [Repr S] (host₁ host₂ : List (GrammaticalTone.TBU S)) (t defaultTone : RegisterTier.TRN) (hLen : host₁.length = host₂.length) : have spec := { name := "", melody := [t], window := GrammaticalTone.ValuationWindow.whole }; tonalTier (basemapOutput host₁ spec defaultTone) = tonalTier (basemapOutput host₂ spec defaultTone)

The basemap output's tonal tier is independent of the host's underlying tones: for whole-word replacement, two hosts with different lexical tones but identical segmental content produce the same basemap tonal tier.

The formal content of "transparadigmatic uniformity" (@cite{rolle-2018} Ch 5): the basemap abstracts away from the paradigmatic tonal variation of the target.