Akinbo & Fwangwar (2026): Grammatical tones targeting ideophones

@cite{akinbo-fwangwar-2026}

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 (@cite{finley-2009}): 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" (@cite{dingemanse-thompson-2020}).

4. Expressiveness survives integration. Derived ideophonic verbs retain expressive properties (affective meaning, nondisplaceability, ineffability) despite full morphosyntactic integration (@cite{potts-2005}-style secondary meanings), challenging the inverse correlation predicted by @cite{dingemanse-akita-2017}.

Substrate

The OT analysis is built on Phonology.Autosegmental.FloatingForm Syl (Goldsmith-style autosegmental representation; built originally for @cite{mcpherson-lamont-2026}). Each ulTones 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 Theories/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 @cite{rolle-2018} — 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 = Phonology.Autosegmental.FloatingForm Fragments.Mwaghavul.Syl

def AkinboFwangwar2026.rootMorph : Phonology.Autosegmental.MorphemeId

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

Equations

• AkinboFwangwar2026.rootMorph = 0

def AkinboFwangwar2026.vbzMorph : Phonology.Autosegmental.MorphemeId

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

Equations

• AkinboFwangwar2026.vbzMorph = 1

def AkinboFwangwar2026.rootRedMorph : Phonology.Autosegmental.MorphemeId

Morpheme ID for the reduplicant root in pluractional Tableau 26.

Equations

• AkinboFwangwar2026.rootRedMorph = 2

def AkinboFwangwar2026.rootBaseMorph : Phonology.Autosegmental.MorphemeId

Morpheme ID for the base root in pluractional Tableau 26.

Equations

• AkinboFwangwar2026.rootBaseMorph = 3

def AkinboFwangwar2026.rootSeg (s : Fragments.Mwaghavul.Syl) : Phonology.Autosegmental.SegSpec Fragments.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 : Fragments.Mwaghavul.Syl) : Phonology.Autosegmental.SegSpec Fragments.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 : Fragments.Mwaghavul.Syl) : Phonology.Autosegmental.SegSpec Fragments.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 : Phonology.Autosegmental.ToneSpec

L tone of the (single) ideophone root.

Equations

• AkinboFwangwar2026.rootL = { tone := Phonology.Autosegmental.RegisterTier.TRN.L, morpheme := AkinboFwangwar2026.rootMorph }

def AkinboFwangwar2026.vbzM : Phonology.Autosegmental.ToneSpec

M tone of the verbaliser.

Equations

• AkinboFwangwar2026.vbzM = { tone := Phonology.Autosegmental.RegisterTier.TRN.M, morpheme := AkinboFwangwar2026.vbzMorph }

def AkinboFwangwar2026.vbzH : Phonology.Autosegmental.ToneSpec

H tone of the verbaliser.

Equations

• AkinboFwangwar2026.vbzH = { tone := Phonology.Autosegmental.RegisterTier.TRN.H, morpheme := AkinboFwangwar2026.vbzMorph }

def AkinboFwangwar2026.lRed : Phonology.Autosegmental.ToneSpec

L tone of the reduplicant root (Tableau 26).

Equations

• AkinboFwangwar2026.lRed = { tone := Phonology.Autosegmental.RegisterTier.TRN.L, morpheme := AkinboFwangwar2026.rootRedMorph }

def AkinboFwangwar2026.lBase : Phonology.Autosegmental.ToneSpec

L tone of the base root (Tableau 26).

Equations

• AkinboFwangwar2026.lBase = { tone := Phonology.Autosegmental.RegisterTier.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 : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (f : MwaghavulForm) (i : Phonology.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 : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (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.segs.length) with | some i => i | none => f.segs.length

def AkinboFwangwar2026.rAnchTone (t : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (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.segs.length).reverse with | some i => i | none => f.segs.length

def AkinboFwangwar2026.maxToneAuto (f : MwaghavulForm) : ℕ

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

Equations

• AkinboFwangwar2026.maxToneAuto f = List.countP (fun (k : Phonology.Autosegmental.ToneIdx) => decide (Phonology.Autosegmental.FloatingForm.IsDeleted f k)) (List.range f.ulTones.length)

def AkinboFwangwar2026.lAnchToneC (t : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

L-ANCHOR-Mᵥ as a DirectionalConstraint.

Equations

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

def AkinboFwangwar2026.rAnchToneC (t : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

R-ANCHOR-Mᵥ as a DirectionalConstraint.

Equations

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

def AkinboFwangwar2026.maxToneC : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

MAX-Tone as a DirectionalConstraint.

Equations

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

def AkinboFwangwar2026.integMv : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

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

Equations

• AkinboFwangwar2026.integMv = Phonology.Tone.integrityTone AkinboFwangwar2026.vbzMorph Phonology.Autosegmental.RegisterTier.TRN.M

def AkinboFwangwar2026.lAnchMv : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

L-ANCHOR-Mᵥ for the verbaliser.

Equations

• AkinboFwangwar2026.lAnchMv = AkinboFwangwar2026.lAnchToneC Phonology.Autosegmental.RegisterTier.TRN.M AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.rAnchMv : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

R-ANCHOR-Mᵥ for the verbaliser.

Equations

• AkinboFwangwar2026.rAnchMv = AkinboFwangwar2026.rAnchToneC Phonology.Autosegmental.RegisterTier.TRN.M AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.lAnchHv : Core.Constraint.OT.DirectionalConstraint 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 Phonology.Autosegmental.RegisterTier.TRN.H AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.rAnchHv : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

R-ANCHOR-Hᵥ for the verbaliser.

Equations

• AkinboFwangwar2026.rAnchHv = AkinboFwangwar2026.rAnchToneC Phonology.Autosegmental.RegisterTier.TRN.H AkinboFwangwar2026.vbzMorph

def AkinboFwangwar2026.isRealisedOnRoot (t : Phonology.Autosegmental.RegisterTier.TRN) (m rm : Phonology.Autosegmental.MorphemeId) (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 = (Phonology.Autosegmental.FloatingForm.segsOfMorpheme f rm).any (AkinboFwangwar2026.isGramTbu t m f)

def AkinboFwangwar2026.lAnchTonePerRoot (t : Phonology.Autosegmental.RegisterTier.TRN) (m rm : Phonology.Autosegmental.MorphemeId) (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 : Phonology.Autosegmental.RegisterTier.TRN) (m rm : Phonology.Autosegmental.MorphemeId) (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 : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (rms : List Phonology.Autosegmental.MorphemeId) (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 : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (rms : List Phonology.Autosegmental.MorphemeId) (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 : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (rms : List Phonology.Autosegmental.MorphemeId) : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

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

Equations

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

def AkinboFwangwar2026.rAnchToneCAcross (t : Phonology.Autosegmental.RegisterTier.TRN) (m : Phonology.Autosegmental.MorphemeId) (rms : List Phonology.Autosegmental.MorphemeId) : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

R-ANCHOR across roots as a DirectionalConstraint.

Equations

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

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: ulTones = [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 = Phonology.Autosegmental.FloatingForm.deleteTone 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 = (Phonology.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 = (Phonology.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 = ((Phonology.Autosegmental.FloatingForm.deleteTone 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 ulTones — 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 : Finset MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau24.nonempty : candidates.Nonempty

def AkinboFwangwar2026.Tableau24.ranking : List (Core.Constraint.OT.DirectionalConstraint 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 : Core.Constraint.OT.DirectionalTableau MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau24.candA_profile : List.map (fun (c : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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: ulTones = [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 = (Phonology.Autosegmental.FloatingForm.deleteTone AkinboFwangwar2026.Tableau25.input 1).deleteTone 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 = (((Phonology.Autosegmental.FloatingForm.deleteTone 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 = (((Phonology.Autosegmental.FloatingForm.deleteTone 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 = (((Phonology.Autosegmental.FloatingForm.deleteLink AkinboFwangwar2026.Tableau25.input 0 0).deleteLink 0 2).insertLink 1 0).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candidates : Finset MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau25.nonempty : candidates.Nonempty

def AkinboFwangwar2026.Tableau25.ranking : List (Core.Constraint.OT.DirectionalConstraint 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 : Core.Constraint.OT.DirectionalTableau MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau25.candA_profile : List.map (fun (c : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval candF) ranking = [[0], [0], [2], [1], [1]]

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

theorem AkinboFwangwar2026.Tableau25.candG_profile : List.map (fun (c : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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: ulTones = [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 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

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

Equations

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

def AkinboFwangwar2026.Tableau26.rAnchHv26 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

Equations

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

def AkinboFwangwar2026.Tableau26.rAnchMv26 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

Equations

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

def AkinboFwangwar2026.Tableau26.lAnchHv26 : Core.Constraint.OT.DirectionalConstraint MwaghavulForm

Equations

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

def AkinboFwangwar2026.Tableau26.candA : MwaghavulForm

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

Equations

• AkinboFwangwar2026.Tableau26.candA = (Phonology.Autosegmental.FloatingForm.deleteTone AkinboFwangwar2026.Tableau26.input 2).deleteTone 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 = (((Phonology.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 = (((Phonology.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 = ((Phonology.Autosegmental.FloatingForm.deleteTone 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 : Finset MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau26.nonempty : candidates.Nonempty

def AkinboFwangwar2026.Tableau26.ranking : List (Core.Constraint.OT.DirectionalConstraint 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 : Core.Constraint.OT.DirectionalTableau MwaghavulForm

Equations

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

theorem AkinboFwangwar2026.Tableau26.candD_profile : List.map (fun (c : Core.Constraint.OT.DirectionalConstraint MwaghavulForm) => c.eval 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 @cite{rolle-2018}'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 : Phonology.Autosegmental.GrammaticalTone.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 : Phonology.Autosegmental.GrammaticalTone.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 := Phonology.Autosegmental.CoPScope.CoPPosition.spec.isDependent, targetIsHead := !Phonology.Autosegmental.CoPScope.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 = Fragments.Mwaghavul.verbM

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

theorem AkinboFwangwar2026.verbMH_GT_toSpec_eq : verbMH_GT.toSpec = Fragments.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 : Fragments.Mwaghavul.Ideophone) : i ∈ [Fragments.Mwaghavul.bishool, Fragments.Mwaghavul.kitiif, Fragments.Mwaghavul.kodzoong, Fragments.Mwaghavul.kitfor, Fragments.Mwaghavul.korjong, Fragments.Mwaghavul.mondos, Fragments.Mwaghavul.vwaplas, Fragments.Mwaghavul.jalpat, Fragments.Mwaghavul.hanlayap, Fragments.Mwaghavul.hamhoyof] → i.verbType = Fragments.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 : Fragments.Mwaghavul.Ideophone) : i ∈ [Fragments.Mwaghavul.zut, Fragments.Mwaghavul.diis, Fragments.Mwaghavul.kwaaj, Fragments.Mwaghavul.vjaar, Fragments.Mwaghavul.shweer, Fragments.Mwaghavul.wuulash, Fragments.Mwaghavul.fooyoop, Fragments.Mwaghavul.vjayaap] → Fragments.Mwaghavul.deriveVerb i = List.map (fun (x : Phonology.Autosegmental.RegisterTier.TRN) => Phonology.Autosegmental.RegisterTier.TRN.M) i.tones

All M-tone ideophones produce uniform M output.

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

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

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

Mwaghavul satisfies @cite{hyman-2006}'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 (@cite{marantz-1997}, @cite{harley-2014}). 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).

@cite{akinbo-fwangwar-2026} §4.2 argues that derived ideophonic verbs retain @cite{potts-2005}-style expressive properties despite morphosyntactic integration: affective meaning, nondisplaceability, descriptive ineffability, context-dependence. This challenges @cite{dingemanse-akita-2017}'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.