Akinbo & Fwangwar (2026): Grammatical tones targeting ideophones

[AF26]

Akinbo, S. K. & Fwangwar, T. R. (2026). Iconicity and expressiveness of grammatical tones targeting ideophones in Mwaghavul. Natural Language & Linguistic Theory 44:21.

Empirical claims

1. Grammatical tone targets ideophones. Mwaghavul derives verbs from ideophones via two segmentally null verbalisers with M and M-H tonal melodies as their sole exponents.

2. Anchor + INTEGRITY OT analysis (paper §4.3, eq. 22). The tonal alternations are accounted for by morpheme-specific correspondence constraints ([Fin09b]): LEFT-ANCHOR-Tᵥ, RIGHT-ANCHOR-Tᵥ, INTEGRITY-Tᵥ, and MAX-Tone.

3. Iconic Phonological Disharmony. In pluractional verbs, the M-H verbaliser realises M on every TBU of the reduplicant and H on every TBU of the base. This disharmony iconically marks "distinguishable identity" ([DT20]).

4. Expressiveness survives integration. Derived ideophonic verbs retain expressive properties (affective meaning, nondisplaceability, ineffability) despite full morphosyntactic integration ([Pot07]-style secondary meanings), challenging the inverse correlation predicted by [DA17].

Substrate

The OT analysis is built on Autosegmental.FloatingForm Syl TRN (Goldsmith-style autosegmental representation; built originally for [McPL26]). Each ulTier entry is one autosegment; surfaceLinks records associations between tier and TBUs. This represents spreading (one autosegment, multi-linked) and copying (multiple autosegments) as distinct objects — load-bearing for the INTEGRITY-Mᵥ constraint that rules out the copying variant of Tableau 24's optimum (paper p. 26 eq. 22c).

Constraint primitives come from Phonology/Tone/Constraints.lean, with Mwaghavul-specific anchor combinators defined in §2 below.

Section structure

• §1 Substrate setup (morpheme IDs, tone/segment helpers)
• §2 Constraints over MwaghavulForm — anchor + INTEGRITY + MAX-Tone, with per-root variants for the pluractional tableau
• §3 Tableau 24 — M verbaliser + wùlàʃ (INTEGRITY rules out copying)
• §4 Tableau 25 — M-H verbaliser + háŋláyáp
• §5 Tableau 26 — pluractional jàlpàt with per-root anchoring
• §6 Classification under [Rol18] — replacive-dominant GT
• §7 Empirical generalisations
• §8 Connection to Distributed Morphology categorisers
• §9 Expressiveness preservation

@[reducible, inline]

abbrev AkinboFwangwar2026.MwaghavulForm : Type

The Mwaghavul-instantiated autosegmental form.

Equations

• AkinboFwangwar2026.MwaghavulForm = Autosegmental.FloatingForm Mwaghavul.Syl Tone.TRN

def AkinboFwangwar2026.rootMorph : Morphology.WordStructure.Morpheme

The ideophone root (wùlàʃ in Tableau 24, háŋláyáp in Tableau 25). Both single-root tableaux share this morpheme.

Equations

• AkinboFwangwar2026.rootMorph = { form := "root" }

def AkinboFwangwar2026.vbzMorph : Morphology.WordStructure.Morpheme

The verbaliser. The M-tone verbaliser (Tableau 24) and the M-H verbaliser (Tableaux 25/26) share this morpheme — they're suppletive allomorphs of the same verbaliser per paper p. 20 eq. (17).

Equations

• AkinboFwangwar2026.vbzMorph = { form := "vbz" }

def AkinboFwangwar2026.rootRedMorph : Morphology.WordStructure.Morpheme

The reduplicant root in pluractional Tableau 26.

Equations

• AkinboFwangwar2026.rootRedMorph = { form := "root-red" }

def AkinboFwangwar2026.rootBaseMorph : Morphology.WordStructure.Morpheme

The base root in pluractional Tableau 26.

Equations

• AkinboFwangwar2026.rootBaseMorph = { form := "root-base" }

def AkinboFwangwar2026.rootSeg (s : Mwaghavul.Syl) : Autosegmental.SegSpec Mwaghavul.Syl

Wrap a Mwaghavul syllable as a TBU of the (single) ideophone root.

Equations

• AkinboFwangwar2026.rootSeg s = { seg := s, morpheme := AkinboFwangwar2026.rootMorph }

def AkinboFwangwar2026.redSeg (s : Mwaghavul.Syl) : Autosegmental.SegSpec Mwaghavul.Syl

Wrap a syllable as a TBU of the reduplicant (Tableau 26).

Equations

• AkinboFwangwar2026.redSeg s = { seg := s, morpheme := AkinboFwangwar2026.rootRedMorph }

def AkinboFwangwar2026.baseSeg (s : Mwaghavul.Syl) : Autosegmental.SegSpec Mwaghavul.Syl

Wrap a syllable as a TBU of the base (Tableau 26).

Equations

• AkinboFwangwar2026.baseSeg s = { seg := s, morpheme := AkinboFwangwar2026.rootBaseMorph }

def AkinboFwangwar2026.rootL : Autosegmental.TierSpec Tone.TRN

L tone of the (single) ideophone root.

Equations

• AkinboFwangwar2026.rootL = { value := Tone.TRN.L, morpheme := AkinboFwangwar2026.rootMorph }

def AkinboFwangwar2026.vbzM : Autosegmental.TierSpec Tone.TRN

M tone of the verbaliser.

Equations

• AkinboFwangwar2026.vbzM = { value := Tone.TRN.M, morpheme := AkinboFwangwar2026.vbzMorph }

def AkinboFwangwar2026.vbzH : Autosegmental.TierSpec Tone.TRN

H tone of the verbaliser.

Equations

• AkinboFwangwar2026.vbzH = { value := Tone.TRN.H, morpheme := AkinboFwangwar2026.vbzMorph }

def AkinboFwangwar2026.lRed : Autosegmental.TierSpec Tone.TRN

L tone of the reduplicant root (Tableau 26).

Equations

• AkinboFwangwar2026.lRed = { value := Tone.TRN.L, morpheme := AkinboFwangwar2026.rootRedMorph }

def AkinboFwangwar2026.lBase : Autosegmental.TierSpec Tone.TRN

L tone of the base root (Tableau 26).

Equations

• AkinboFwangwar2026.lBase = { value := Tone.TRN.L, morpheme := AkinboFwangwar2026.rootBaseMorph }

Anchor + INTEGRITY + MAX-Tone constraints. Anchor constraints come in two flavours: - Single-root (lAnchToneC/rAnchToneC): scope over all TBUs. Correct for Tableaux 24/25 with one root morpheme. - Per-root, summed across roots (lAnchToneCAcross / rAnchToneCAcross): scope to each root morpheme separately, sum violations; if no root hosts the gram tone, every TBU of every targeted root counts (paper p. 28). Required for Tableau 26's two-root pluractional.

def AkinboFwangwar2026.isGramTbu (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (f : MwaghavulForm) (i : Autosegmental.SegIdx) : Bool

Does TBU i bear a tone of value t from morpheme m?

Equations

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

def AkinboFwangwar2026.lAnchTone (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : ℕ

L-ANCHOR-t-from-m: number of TBUs (in tier order) before the leftmost gram-t-from-m TBU. If no such TBU exists, every TBU counts (full TBU count).

Equations

• AkinboFwangwar2026.lAnchTone t m f = match List.findIdx? (AkinboFwangwar2026.isGramTbu t m f) (List.range f.lower.len) with | some i => i | none => f.lower.len

def AkinboFwangwar2026.rAnchTone (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : ℕ

R-ANCHOR-t-from-m: counted from the right edge.

Equations

• AkinboFwangwar2026.rAnchTone t m f = match List.findIdx? (AkinboFwangwar2026.isGramTbu t m f) (List.range f.lower.len).reverse with | some i => i | none => f.lower.len

def AkinboFwangwar2026.maxToneAuto (f : MwaghavulForm) : ℕ

MAX-Tone (per autosegment): count of deleted ulTier entries. Matches paper p. 26 per-autosegment counting.

Equations

• AkinboFwangwar2026.maxToneAuto f = Autosegmental.FloatingForm.countUpper f (Autosegmental.FloatingForm.IsDeleted f)

def AkinboFwangwar2026.lAnchToneC (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) : Constraints.Constraint MwaghavulForm

L-ANCHOR-Mᵥ as a Constraint.

Equations

• AkinboFwangwar2026.lAnchToneC t m = AkinboFwangwar2026.lAnchTone t m

def AkinboFwangwar2026.rAnchToneC (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) : Constraints.Constraint MwaghavulForm

R-ANCHOR-Mᵥ as a Constraint.

Equations

• AkinboFwangwar2026.rAnchToneC t m = AkinboFwangwar2026.rAnchTone t m

def AkinboFwangwar2026.maxToneC : Constraints.Constraint MwaghavulForm

MAX-Tone as a Constraint.

Equations

• AkinboFwangwar2026.maxToneC = AkinboFwangwar2026.maxToneAuto

def AkinboFwangwar2026.integMv : Constraints.Constraint MwaghavulForm

INTEGRITY-Mᵥ for the verbaliser (canonical case).

Equations

• AkinboFwangwar2026.integMv = Tone.integrityTone AkinboFwangwar2026.vbzMorph Tone.TRN.M

def AkinboFwangwar2026.lAnchMv : Constraints.Constraint MwaghavulForm

L-ANCHOR-Mᵥ for the verbaliser.

Equations

• AkinboFwangwar2026.lAnchMv = AkinboFwangwar2026.lAnchToneC Tone.TRN.M AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.rAnchMv : Constraints.Constraint MwaghavulForm

R-ANCHOR-Mᵥ for the verbaliser.

Equations

• AkinboFwangwar2026.rAnchMv = AkinboFwangwar2026.rAnchToneC Tone.TRN.M AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.lAnchHv : Constraints.Constraint MwaghavulForm

L-ANCHOR-Hᵥ for the verbaliser (paper p. 25 fn: H-tone version of eq. 22 has the same conditions).

Equations

• AkinboFwangwar2026.lAnchHv = AkinboFwangwar2026.lAnchToneC Tone.TRN.H AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.rAnchHv : Constraints.Constraint MwaghavulForm

R-ANCHOR-Hᵥ for the verbaliser.

Equations

• AkinboFwangwar2026.rAnchHv = AkinboFwangwar2026.rAnchToneC Tone.TRN.H AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.isRealisedOnRoot (t : Tone.TRN) (m rm : Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : Bool

A gram-t-from-m tone is realised on root rm iff some TBU of rm bears one.

Equations

• AkinboFwangwar2026.isRealisedOnRoot t m rm f = (Autosegmental.FloatingForm.segsOfMorpheme f rm).any (AkinboFwangwar2026.isGramTbu t m f)

def AkinboFwangwar2026.lAnchTonePerRoot (t : Tone.TRN) (m rm : Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : ℕ

L-ANCHOR scoped to root rm. 0 if t-from-m not realised on rm (per paper p. 28: "no violation to the other root morpheme"); else count TBUs of rm before the leftmost gram-t TBU of rm.

Equations

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

def AkinboFwangwar2026.rAnchTonePerRoot (t : Tone.TRN) (m rm : Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : ℕ

R-ANCHOR scoped to root rm.

Equations

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

def AkinboFwangwar2026.lAnchToneAcrossRoots (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (rms : List Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : ℕ

L-ANCHOR summed across a list of root morphemes. If the gram tone is not realised on ANY of the roots, paper p. 28 assigns one violation per TBU of every targeted root (not 0).

Equations

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

def AkinboFwangwar2026.rAnchToneAcrossRoots (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (rms : List Morphology.WordStructure.Morpheme) (f : MwaghavulForm) : ℕ

R-ANCHOR summed across a list of root morphemes.

Equations

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

def AkinboFwangwar2026.lAnchToneCAcross (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (rms : List Morphology.WordStructure.Morpheme) : Constraints.Constraint MwaghavulForm

L-ANCHOR-t-from-m-across-roots as a Constraint.

Equations

• AkinboFwangwar2026.lAnchToneCAcross t m rms = AkinboFwangwar2026.lAnchToneAcrossRoots t m rms

def AkinboFwangwar2026.rAnchToneCAcross (t : Tone.TRN) (m : Morphology.WordStructure.Morpheme) (rms : List Morphology.WordStructure.Morpheme) : Constraints.Constraint MwaghavulForm

R-ANCHOR across roots as a Constraint.

Equations

• AkinboFwangwar2026.rAnchToneCAcross t m rms = AkinboFwangwar2026.rAnchToneAcrossRoots t m rms

Paper Tableau 24 (p. 26): (wùlàʃ)₁ + Mᵥ. Six candidates including the copying variant (24f) that the paper rules out via INTEGRITY-Mᵥ.

Encoding: ONE lex L autosegment multi-linked to both TBUs of the
bisyllabic root (Goldsmith 1976 convention; paper notation
`(wùlàʃ)₁` confirms a single morpheme-internal melody). 

def AkinboFwangwar2026.Tableau24.input : MwaghavulForm

Faithful input: ulTier = [L_root (multi-linked), M_vbz (floating)].

Equations

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

def AkinboFwangwar2026.Tableau24.candA : MwaghavulForm

(24a) (wùlàʃ)₁ M₂: M still floating; L unchanged.

Equations

• AkinboFwangwar2026.Tableau24.candA = AkinboFwangwar2026.Tableau24.input

def AkinboFwangwar2026.Tableau24.candB : MwaghavulForm

(24b) (wùlàʃ)₁: M deleted; L unchanged.

Equations

• AkinboFwangwar2026.Tableau24.candB = Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau24.input 1

def AkinboFwangwar2026.Tableau24.candC : MwaghavulForm

(24c) (wù)₁(làʃ)₂: L on σ0 only; M docked on σ1 only.

Equations

• AkinboFwangwar2026.Tableau24.candC = (Autosegmental.FloatingForm.deleteLink AkinboFwangwar2026.Tableau24.input 0 1).insertLink 1 1

def AkinboFwangwar2026.Tableau24.candD : MwaghavulForm

(24d) (wū)₂(làʃ)₁: M on σ0 only; L on σ1 only.

Equations

• AkinboFwangwar2026.Tableau24.candD = (Autosegmental.FloatingForm.deleteLink AkinboFwangwar2026.Tableau24.input 0 0).insertLink 1 0

def AkinboFwangwar2026.Tableau24.candE : MwaghavulForm

(24e) ☞ (wūlāʃ)₂ SPREADING: M multi-linked to both TBUs; L deleted. ONE M autosegment, two surface links.

Equations

• AkinboFwangwar2026.Tableau24.candE = ((Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau24.input 0).insertLink 1 0).insertLink 1 1

def AkinboFwangwar2026.Tableau24.candF : MwaghavulForm

(24f) (wū)₂(lāʃ)₂ COPYING: TWO separate M autosegments, each linked to one TBU. L deleted. Differs from (24a-e) in ulTier — the autosegmental representation has an extra M autosegment. INTEGRITY-Mᵥ fatally penalises this copying.

Equations

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

def AkinboFwangwar2026.Tableau24.candidates : List MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau24.candidates_ne : candidates ≠ []

def AkinboFwangwar2026.Tableau24.ranking : List (Constraints.Constraint MwaghavulForm)

Ranking from paper §4.3 + p. 26: INTEG-Mᵥ ≫ L-ANCH-Mᵥ ≫ R-ANCH-Mᵥ ≫ MAX-Tone.

Equations

• AkinboFwangwar2026.Tableau24.ranking = [AkinboFwangwar2026.integMv, AkinboFwangwar2026.lAnchMv, AkinboFwangwar2026.rAnchMv, AkinboFwangwar2026.maxToneC]

def AkinboFwangwar2026.Tableau24.tableau : OptimalityTheory.Tableau MwaghavulForm ranking.length

Equations

• AkinboFwangwar2026.Tableau24.tableau = OptimalityTheory.Tableau.ofRanking AkinboFwangwar2026.Tableau24.candidates AkinboFwangwar2026.Tableau24.ranking AkinboFwangwar2026.Tableau24.candidates_ne

theorem AkinboFwangwar2026.Tableau24.candA_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candA) ranking = [0, 2, 2, 0]

(24a) profile [INTEG-Mᵥ, L-ANCH-Mᵥ, R-ANCH-Mᵥ, MAX-T] = [0, 2, 2, 0]: M floating, both anchors fail (no gram-M TBU), no deletions.

theorem AkinboFwangwar2026.Tableau24.candB_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candB) ranking = [0, 2, 2, 1]

(24b) profile [0, 2, 2, 1]: M deleted, anchors fail, MAX-T fires.

theorem AkinboFwangwar2026.Tableau24.candC_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candC) ranking = [0, 1, 0, 0]

(24c) profile [0, 1, 0, 0]: M on σ1; L-ANCH = 1 (M not at left).

theorem AkinboFwangwar2026.Tableau24.candD_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candD) ranking = [0, 0, 1, 0]

(24d) profile [0, 0, 1, 0]: M on σ0; R-ANCH = 1 (M not at right).

theorem AkinboFwangwar2026.Tableau24.candE_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candE) ranking = [0, 0, 0, 1]

(24e) ☞ profile [0, 0, 0, 1]: M multi-linked, anchors satisfied; INTEG = 0 (1 alive vbz M); MAX-T = 1 (L deleted). The unique optimum.

theorem AkinboFwangwar2026.Tableau24.candF_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candF) ranking = [1, 0, 0, 1]

(24f) profile [1, 0, 0, 1]: TWO M autosegments → INTEG = 1 (fatal under the ranking, even though anchors and MAX-T tie with (24e)).

theorem AkinboFwangwar2026.Tableau24.optimal : tableau.optimal = {candE}

Headline: (24e) is the unique optimum under INTEG-Mᵥ ≫ L-ANCH-Mᵥ ≫ R-ANCH-Mᵥ ≫ MAX-Tone. The copying variant (24f) is ruled out by INTEGRITY; (24a-d) lose on anchors.

Paper Tableau 25 (p. 27): (háŋláyáp)₁ + M₂H₃ᵥ. Seven candidates; no INTEGRITY column (no copying variant arises). Encoding: ONE lex H autosegment multi-linked to all 3 TBUs (Goldsmith convention).

def AkinboFwangwar2026.Tableau25.input : MwaghavulForm

Faithful input: ulTier = [H_root (multi-linked), M_vbz, H_vbz].

Equations

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

def AkinboFwangwar2026.Tableau25.candA : MwaghavulForm

(25a) (háŋláyáp)₁: lex H linked; both vbz tones deleted.

Equations

• AkinboFwangwar2026.Tableau25.candA = (Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau25.input 1).deleteTierElem 2

def AkinboFwangwar2026.Tableau25.candB : MwaghavulForm

(25b) (hāŋlā)₂(yáp)₁: M on σ0-σ1; lex H on σ2; vbz H deleted.

Equations

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

def AkinboFwangwar2026.Tableau25.candC : MwaghavulForm

(25c) (háŋláyáp)₃: vbz H multi-linked to all TBUs; vbz M and lex H deleted.

Equations

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

def AkinboFwangwar2026.Tableau25.candD : MwaghavulForm

(25d) (hāŋlāyāp)₂: vbz M multi-linked to all TBUs; vbz H and lex H deleted.

Equations

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

def AkinboFwangwar2026.Tableau25.candE : MwaghavulForm

(25e) ☞ (hāŋlā)₂(yáp)₃: vbz M on σ0-σ1; vbz H on σ2; lex H deleted. The winner.

Equations

• AkinboFwangwar2026.Tableau25.candE = (((Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau25.input 0).insertLink 1 0).insertLink 1 1).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candF : MwaghavulForm

(25f) (hāŋ)₂(láyáp)₃: vbz M on σ0; vbz H on σ1-σ2; lex H deleted.

Equations

• AkinboFwangwar2026.Tableau25.candF = (((Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau25.input 0).insertLink 1 0).insertLink 2 1).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candG : MwaghavulForm

(25g) (hāŋ)₂(lá)₁(yáp)₃: vbz M on σ0; lex H on σ1; vbz H on σ2. Lex H NOT deleted.

Equations

• AkinboFwangwar2026.Tableau25.candG = (((Autosegmental.FloatingForm.deleteLink AkinboFwangwar2026.Tableau25.input 0 0).deleteLink 0 2).insertLink 1 0).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candidates : List MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau25.candidates_ne : candidates ≠ []

def AkinboFwangwar2026.Tableau25.ranking : List (Constraints.Constraint MwaghavulForm)

Ranking from paper Tableau 25 (p. 27): L-ANCH-Mᵥ ≫ R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Hᵥ ≫ MAX-Tone.

Equations

• AkinboFwangwar2026.Tableau25.ranking = [AkinboFwangwar2026.lAnchMv, AkinboFwangwar2026.rAnchHv, AkinboFwangwar2026.rAnchMv, AkinboFwangwar2026.lAnchHv, AkinboFwangwar2026.maxToneC]

def AkinboFwangwar2026.Tableau25.tableau : OptimalityTheory.Tableau MwaghavulForm ranking.length

Equations

• AkinboFwangwar2026.Tableau25.tableau = OptimalityTheory.Tableau.ofRanking AkinboFwangwar2026.Tableau25.candidates AkinboFwangwar2026.Tableau25.ranking AkinboFwangwar2026.Tableau25.candidates_ne

theorem AkinboFwangwar2026.Tableau25.candA_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candA) ranking = [3, 3, 3, 3, 2]

(25a) profile [3, 3, 3, 3, 2]: no verbaliser realised.

theorem AkinboFwangwar2026.Tableau25.candB_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candB) ranking = [0, 3, 1, 3, 1]

(25b) profile [0, 3, 1, 3, 1]: vbz M docked left; vbz H deleted.

theorem AkinboFwangwar2026.Tableau25.candC_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candC) ranking = [3, 0, 3, 0, 2]

(25c) profile [3, 0, 3, 0, 2]: vbz H spreading; vbz M deleted.

theorem AkinboFwangwar2026.Tableau25.candD_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candD) ranking = [0, 3, 0, 3, 2]

(25d) profile [0, 3, 0, 3, 2]: vbz M spreading; vbz H deleted.

theorem AkinboFwangwar2026.Tableau25.candE_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candE) ranking = [0, 0, 1, 2, 1]

(25e) ☞ profile [0, 0, 1, 2, 1]: M on σ0-σ1; H on σ2; lex H deleted. Winner.

theorem AkinboFwangwar2026.Tableau25.candF_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candF) ranking = [0, 0, 2, 1, 1]

(25f) profile [0, 0, 2, 1, 1].

theorem AkinboFwangwar2026.Tableau25.candG_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candG) ranking = [0, 0, 2, 2, 0]

(25g) profile [0, 0, 2, 2, 0]: lex H NOT deleted (still on σ1).

theorem AkinboFwangwar2026.Tableau25.optimal : tableau.optimal = {candE}

Headline: (25e) is the unique optimum. (25a-d) lose on the top-tier anchors; (25f-g) tie with (25e) on top constraints but lose on R-ANCH-Mᵥ.

Paper Tableau 26 (p. 28): (jàlpàt)₁ + (jàlpàt)₂ + M₃H₄ᵥ. Two root morphemes (reduplicant + base), each with /LL/ lexical melody (one L autosegment multi-linked to its 2 TBUs). The M-H verbaliser realises M on RED's TBUs and H on BASE's TBUs.

Per-root anchoring (paper p. 28): if vbz M is realised on one root,
the other root contributes no violation. If unrealised on both,
every TBU of every targeted root counts. The
`lAnchToneCAcross`/`rAnchToneCAcross` constraints in §2 implement
this. 

def AkinboFwangwar2026.Tableau26.input : MwaghavulForm

Faithful input: ulTier = [L_RED (multi-linked), L_BASE (multi-linked), M_vbz, H_vbz]. Each lex L is multi-linked to its own root's 2 TBUs.

Equations

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

def AkinboFwangwar2026.Tableau26.lAnchMv26 : Constraints.Constraint MwaghavulForm

Per-root anchor instantiations for the two-root pluractional.

Equations

• AkinboFwangwar2026.Tableau26.lAnchMv26 = AkinboFwangwar2026.lAnchToneCAcross Tone.TRN.M AkinboFwangwar2026.vbzMorph [AkinboFwangwar2026.rootRedMorph, AkinboFwangwar2026.rootBaseMorph]

def AkinboFwangwar2026.Tableau26.rAnchHv26 : Constraints.Constraint MwaghavulForm

Equations

• AkinboFwangwar2026.Tableau26.rAnchHv26 = AkinboFwangwar2026.rAnchToneCAcross Tone.TRN.H AkinboFwangwar2026.vbzMorph [AkinboFwangwar2026.rootRedMorph, AkinboFwangwar2026.rootBaseMorph]

def AkinboFwangwar2026.Tableau26.rAnchMv26 : Constraints.Constraint MwaghavulForm

Equations

• AkinboFwangwar2026.Tableau26.rAnchMv26 = AkinboFwangwar2026.rAnchToneCAcross Tone.TRN.M AkinboFwangwar2026.vbzMorph [AkinboFwangwar2026.rootRedMorph, AkinboFwangwar2026.rootBaseMorph]

def AkinboFwangwar2026.Tableau26.lAnchHv26 : Constraints.Constraint MwaghavulForm

Equations

• AkinboFwangwar2026.Tableau26.lAnchHv26 = AkinboFwangwar2026.lAnchToneCAcross Tone.TRN.H AkinboFwangwar2026.vbzMorph [AkinboFwangwar2026.rootRedMorph, AkinboFwangwar2026.rootBaseMorph]

def AkinboFwangwar2026.Tableau26.candA : MwaghavulForm

(26a): both vbz tones deleted; both lex Ls survive.

Equations

• AkinboFwangwar2026.Tableau26.candA = (Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau26.input 2).deleteTierElem 3

def AkinboFwangwar2026.Tableau26.candB : MwaghavulForm

(26b): vbz M on σ1 (rightmost of RED); vbz H on σ3 (rightmost of BASE); lex Ls survive on σ0 and σ2 respectively.

Equations

• AkinboFwangwar2026.Tableau26.candB = (((Autosegmental.FloatingForm.deleteLink AkinboFwangwar2026.Tableau26.input 0 1).insertLink 2 1).deleteLink 1 3).insertLink 3 3

def AkinboFwangwar2026.Tableau26.candC : MwaghavulForm

(26c): vbz M on σ0 (leftmost of RED); vbz H on σ2 (leftmost of BASE); lex Ls survive on σ1 and σ3.

Equations

• AkinboFwangwar2026.Tableau26.candC = (((Autosegmental.FloatingForm.deleteLink AkinboFwangwar2026.Tableau26.input 0 0).insertLink 2 0).deleteLink 1 2).insertLink 3 2

def AkinboFwangwar2026.Tableau26.candD : MwaghavulForm

(26d) ☞: M spreading on RED (both σ0, σ1); H spreading on BASE (both σ2, σ3); both lex Ls deleted. The winner — iconic M-on-RED

• H-on-BASE pattern.

Equations

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

def AkinboFwangwar2026.Tableau26.candE : MwaghavulForm

(26e): vbz M on σ0; vbz H on σ1 (both within RED); lex L of BASE survives multi-linked. Lex L of RED deleted.

Equations

• AkinboFwangwar2026.Tableau26.candE = ((Autosegmental.FloatingForm.deleteTierElem AkinboFwangwar2026.Tableau26.input 0).insertLink 2 0).insertLink 3 1

def AkinboFwangwar2026.Tableau26.candF : MwaghavulForm

(26f): vbz M spreading on RED + σ2 (first BASE TBU); vbz H on σ3.

Equations

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

def AkinboFwangwar2026.Tableau26.candG : MwaghavulForm

(26g): vbz M on σ0 (RED) + σ2 (BASE); lex L of RED on σ1; vbz H on σ3.

Equations

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

def AkinboFwangwar2026.Tableau26.candidates : List MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau26.candidates_ne : candidates ≠ []

def AkinboFwangwar2026.Tableau26.ranking : List (Constraints.Constraint MwaghavulForm)

Ranking, same shape as Tableau 25 but with per-root anchors: L-ANCH-Mᵥ ≫ R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Hᵥ ≫ MAX-Tone.

Equations

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

def AkinboFwangwar2026.Tableau26.tableau : OptimalityTheory.Tableau MwaghavulForm ranking.length

Equations

• AkinboFwangwar2026.Tableau26.tableau = OptimalityTheory.Tableau.ofRanking AkinboFwangwar2026.Tableau26.candidates AkinboFwangwar2026.Tableau26.ranking AkinboFwangwar2026.Tableau26.candidates_ne

theorem AkinboFwangwar2026.Tableau26.candD_profile : List.map (fun (c : Constraints.Constraint MwaghavulForm) => c candD) ranking = [0, 0, 0, 0, 2]

(26d) profile [0, 0, 0, 0, 2]: perfect realisation — vbz M on every TBU of RED, vbz H on every TBU of BASE. Both lex Ls deleted (MAX-T = 2).

theorem AkinboFwangwar2026.Tableau26.optimal : tableau.optimal = {candD}

Headline: (26d) is the unique optimum — the iconic M-on-RED + H-on-BASE disharmony pattern.

The Mwaghavul verbalisers are classified under [Rol18]'s grammatical-tone framework as replacive-dominant GT (Def 1): automatic replacement of the underlying tone within the valuation window of the target-host. Verbalisers are word-level + independent prosodic exponence (segmentally null — tone is the sole exponent).

def AkinboFwangwar2026.verbM_GT : Tone.GTSpec

M-tone verbaliser (VBZ₁) classified under Rolle 2018: replacive-dominant, word-level, independent.

Equations

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

def AkinboFwangwar2026.verbMH_GT : Tone.GTSpec

M-H verbaliser (VBZ₂).

Equations

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

theorem AkinboFwangwar2026.verbalizers_are_dominant : verbM_GT.dominance.IsDominant ∧ verbMH_GT.dominance.IsDominant

Both verbalisers are dominant: they neutralise the target's lexical tonal contrast.

theorem AkinboFwangwar2026.verbalizers_prosodic_dominant : verbM_GT.dominance.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant ∧ verbMH_GT.dominance.toProsodicDominance = Features.Prosody.ProsodicDominance.dominant

Mwaghavul verbalisers classify as dominant at the abstract prosodic level.

theorem AkinboFwangwar2026.verbalizer_asymmetry_holds : { triggerIsDependent := Rolle2018.CoPPosition.spec.isDependent, targetIsHead := !Rolle2018.CoPPosition.head.isDependent }.holds = true

The verbaliser-to-root relationship satisfies the dominant GT asymmetry, derived from CoP-scope: verbaliser is in Spec (dependent), root is in Head. Spec scopes over Head, so the asymmetry holds.

theorem AkinboFwangwar2026.verbM_GT_toSpec_eq : verbM_GT.toSpec = Mwaghavul.verbM

VBZ₁'s GTSpec.toSpec recovers the Spec used by deriveVerb.

theorem AkinboFwangwar2026.verbMH_GT_toSpec_eq : verbMH_GT.toSpec = Mwaghavul.verbMH

VBZ₂'s GTSpec.toSpec recovers the Spec used by deriveVerb.

Cross-verb generalisations about the Mwaghavul ideophone-to-verb derivation (paper §3, summarised in eq. (13)). These are properties of the data, decidable from the Ideophone records in Fragments/Mwaghavul/Basic.lean.

theorem AkinboFwangwar2026.mh_only_from_mh_verbalizer (i : Mwaghavul.Ideophone) : i ∈ [Mwaghavul.bishool, Mwaghavul.kitiif, Mwaghavul.kodzoong, Mwaghavul.kitfor, Mwaghavul.korjong, Mwaghavul.mondos, Mwaghavul.vwaplas, Mwaghavul.jalpat, Mwaghavul.hanlayap, Mwaghavul.hamhoyof] → i.verbType = Mwaghavul.VerbalizerChoice.mh

The M-H tonal melody is attested only in derived verbs (paper eq. 13e). No underived Mwaghavul verb has M-H. We test against the concrete ideophone data.

theorem AkinboFwangwar2026.m_verbs_all_uniform (i : Mwaghavul.Ideophone) : i ∈ [Mwaghavul.zut, Mwaghavul.diis, Mwaghavul.kwaaj, Mwaghavul.vjaar, Mwaghavul.shweer, Mwaghavul.wuulash, Mwaghavul.fooyoop, Mwaghavul.vjayaap] → Mwaghavul.deriveVerb i = List.map (fun (x : Tone.TRN) => Tone.TRN.M) i.tones

All M-tone ideophones produce uniform M output.

theorem AkinboFwangwar2026.pluractional_uses_mh : Mwaghavul.jalpat.verbType = Mwaghavul.VerbalizerChoice.mh ∧ Mwaghavul.hanlayap.verbType = Mwaghavul.VerbalizerChoice.mh

Pluractional verbs always use M-H (paper eq. 13f).

theorem AkinboFwangwar2026.mwaghavul_is_tonal_hyman : Hyman2006.isTonalUnderHyman Mwaghavul.wordProsodicType = true

Mwaghavul satisfies [Hym06]'s tonal-language definition (3): "an indication of pitch enters into the lexical realisation of at least some morphemes."

The segmentally null verbalisers that trigger the tonal alternations are instances of the verbal categoriser v in Distributed Morphology ([Mar97], [Har14b]). The ideophonic base (noun, adjective, or adverb) is recategorised as a verb through merger with v, whose sole phonological exponent is a tonal melody.

def AkinboFwangwar2026.verbalizerCat : Morphology.DM.CatHead

The verbaliser produces verbal category.

Equations

• AkinboFwangwar2026.verbalizerCat = Morphology.DM.CatHead.v_plain

theorem AkinboFwangwar2026.verbalizer_is_verbal : verbalizerCat.cat = Morphology.DM.Categorizer.v

theorem AkinboFwangwar2026.denominal_ideophone_verb : Morphology.DM.Recategorization.denominal.source = Morphology.DM.Categorizer.n ∧ Morphology.DM.Recategorization.denominal.target = Morphology.DM.Categorizer.v

Denominal verb derivation (n → v): Recategorization.denominal.

theorem AkinboFwangwar2026.deadjectival_ideophone_verb : Morphology.DM.Recategorization.deadjectival.source = Morphology.DM.Categorizer.a ∧ Morphology.DM.Recategorization.deadjectival.target = Morphology.DM.Categorizer.v

Deadjectival verb derivation (a → v).

[AF26] §4.2 argues that derived ideophonic verbs retain [Pot07]-style expressive properties despite morphosyntactic integration: affective meaning, nondisplaceability, descriptive ineffability, context-dependence. This challenges [DA17]'s prediction of inverse correlation between integration and expressiveness.

def AkinboFwangwar2026.ideophoneVerbProperties : Pragmatics.Expressives.SecondaryMeaningProperties

Derived ideophonic verbs exhibit all canonical expressive properties: independent, nondisplaceable, perspective-dependent, descriptively ineffable, immediate, repeatable, no perspective shift, no discourse antecedent required.

Equations

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

General dominant-cophonology ↔ overwrite agreement ([Rol18])

The per-tableau agreement theorems in the Tableau24/25/26 sections above are instances of a general result: the two parallel formalisms for dominant grammatical tone in [Rol18] — direct tonalOverwrite and constraint-based cophonologicalEval under a subranking promoting MxBM-C (basemap faithfulness) — coincide. When MxBM-C is top-ranked, OT evaluation necessarily selects basemap-faithful candidates, which are exactly the tonalOverwrite outputs. The proof chain goes through optimal_zero_first (OT substrate): a candidate with 0 violations on the top constraint forces every optimal candidate to 0.

theorem AkinboFwangwar2026.dominant_coph_selects_basemap_faithful {L C : Type} [DecidableEq L] [DecidableEq C] (basemapTier : List Tone.TRN) (extractTier : C → List Tone.TRN) (l : L) (defaultRanking : List (L × Constraints.Constraint C)) (candidates : List C) (h : candidates ≠ []) (hLen : ∀ c ∈ candidates, (extractTier c).length = basemapTier.length) (hFaithful : ∃ c ∈ candidates, extractTier c = basemapTier) : have mxbmc := Rolle2018.mkBasemapConstraint basemapTier extractTier; ∀ c ∈ OptimalityTheory.Cophonology.cophonologicalEval defaultRanking [(l, 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 [Rol18] 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 AkinboFwangwar2026.dominant_coph_agrees_with_tonalOverwrite {S L C : Type} [DecidableEq S] [BEq S] [Repr S] [DecidableEq L] [DecidableEq C] (host : List (Tone.TBU S)) (t defaultTone : Tone.TRN) (extractTier : C → List Tone.TRN) (l : L) (defaultRanking : List (L × Constraints.Constraint C)) (candidates : List C) (h : candidates ≠ []) (hLen : ∀ c ∈ candidates, (extractTier c).length = (Rolle2018.tonalTier (Rolle2018.basemapOutput host { name := "", melody := [t], window := Tone.ValuationWindow.whole } defaultTone)).length) (hFaithful : ∃ c ∈ candidates, extractTier c = Rolle2018.tonalTier (Rolle2018.basemapOutput host { name := "", melody := [t], window := Tone.ValuationWindow.whole } defaultTone)) : have spec := { name := "", melody := [t], window := Tone.ValuationWindow.whole }; have baseTier := Rolle2018.tonalTier (Rolle2018.basemapOutput host spec defaultTone); have mxbmc := Rolle2018.mkBasemapConstraint baseTier extractTier; ∀ c ∈ OptimalityTheory.Cophonology.cophonologicalEval defaultRanking [(l, mxbmc)] candidates h, extractTier c = Rolle2018.tonalTier (Tone.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. 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.