Mwaghavul Phonological Fragment

@cite{akinbo-fwangwar-2026} @cite{fwangwar-2018}

Mwaghavul (ISO 639-3: sur, Glottocode: mwag1236) is an A3 West Chadic (Afro-Asiatic) language spoken by more than 700,000 people in Plateau State, Nigeria (@cite{crozier-blench-1992}).

Tone system

Mwaghavul contrasts three level tones — high (H), mid (M), and low (L) — plus an LH rising contour. The tone-bearing unit (TBU) is the syllable. All tonal co-occurrences on bisyllabic roots are attested except M-LH (@cite{akinbo-fwangwar-2026} Table 3).

Ideophones

Mwaghavul has a rich inventory of ideophones — "an open class of marked words that depict sensory imagery" (@cite{dingemanse-2019}:16). Ideophones share the same grammatical classes as nonideophonic words (nouns, verbs, adjectives, adverbs) and occur in comparable morphosyntactic environments.

Verbalisation

All tonally derived verbs in Mwaghavul have ideophonic bases. The verb formation is morphophonologically marked through one of two lexically determined tonal alternations triggered by segmentally null verbalisers:

1. M verbaliser (VBZ₁): overwrites every TBU with M
2. M-H verbaliser (VBZ₂): overwrites nonfinal TBUs with M, final with H

The M-H melody is attested only in derived verbs — no underived verb has this pattern. Data from @cite{akinbo-fwangwar-2026} and @cite{fwangwar-2018}.

def Fragments.Mwaghavul.wordProsodicType : Phonology.Autosegmental.RegisterTier.WordProsodicType

Mwaghavul is a three-level tone language with syllable TBUs.

Equations

• Fragments.Mwaghavul.wordProsodicType = Phonology.Autosegmental.RegisterTier.WordProsodicType.toneBased

def Fragments.Mwaghavul.tbuKind : Phonology.Autosegmental.RegisterTier.TBUKind

Equations

• Fragments.Mwaghavul.tbuKind = Phonology.Autosegmental.RegisterTier.TBUKind.syllable

inductive Fragments.Mwaghavul.VerbalizerChoice : Type

The two lexically specific suppletive allomorphs of the verbaliser morpheme (@cite{akinbo-fwangwar-2026} (17)).

• m : VerbalizerChoice
• mh : VerbalizerChoice

@[implicit_reducible]

instance Fragments.Mwaghavul.instDecidableEqVerbalizerChoice : DecidableEq VerbalizerChoice

Equations

• Fragments.Mwaghavul.instDecidableEqVerbalizerChoice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mwaghavul.instReprVerbalizerChoice : Repr VerbalizerChoice

Equations

• Fragments.Mwaghavul.instReprVerbalizerChoice = { reprPrec := Fragments.Mwaghavul.instReprVerbalizerChoice.repr }

def Fragments.Mwaghavul.instReprVerbalizerChoice.repr : VerbalizerChoice → ℕ → Std.Format

Equations

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

def Fragments.Mwaghavul.verbM : Phonology.Autosegmental.GrammaticalTone.Spec

The M-tone verbaliser (VBZ₁): targets only unreduplicated ideophones. Overwrites every TBU of the host with M.

Equations

• Fragments.Mwaghavul.verbM = { name := "VBZ₁", melody := [Phonology.Autosegmental.RegisterTier.TRN.M], window := Phonology.Autosegmental.GrammaticalTone.ValuationWindow.whole }

def Fragments.Mwaghavul.verbMH : Phonology.Autosegmental.GrammaticalTone.Spec

The M-H verbaliser (VBZ₂): targets both unreduplicated and reduplicated ideophones. Nonfinal TBUs get M, final gets H.

Equations

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

structure Fragments.Mwaghavul.Ideophone : Type

An ideophone entry: base form, gloss, lexical tones, and which verbaliser it selects. Tone pattern is listed left-to-right matching syllable order.

Whether an ideophone undergoes M or M-H alternation is lexically determined and not predictable from syllable structure or tone (@cite{akinbo-fwangwar-2026} §3.1).

• form : String
• gloss : String
• tones : List Phonology.Autosegmental.RegisterTier.TRN
• verbType : VerbalizerChoice

def Fragments.Mwaghavul.instReprIdeophone.repr : Ideophone → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Mwaghavul.instReprIdeophone : Repr Ideophone

Equations

• Fragments.Mwaghavul.instReprIdeophone = { reprPrec := Fragments.Mwaghavul.instReprIdeophone.repr }

def Fragments.Mwaghavul.Ideophone.nSyl (i : Ideophone) : ℕ

Number of syllables, derived from the tone list.

Equations

• i.nSyl = i.tones.length

def Fragments.Mwaghavul.zut : Ideophone

Equations

• Fragments.Mwaghavul.zut = { form := "zùt", gloss := "how solid substance ejects", tones := [Phonology.Autosegmental.RegisterTier.TRN.L], verbType := Fragments.Mwaghavul.VerbalizerChoice.m }

def Fragments.Mwaghavul.diis : Ideophone

Equations

• Fragments.Mwaghavul.diis = { form := "dìːs", gloss := "blood sucking", tones := [Phonology.Autosegmental.RegisterTier.TRN.L], verbType := Fragments.Mwaghavul.VerbalizerChoice.m }

def Fragments.Mwaghavul.kwaaj : Ideophone

Equations

• Fragments.Mwaghavul.kwaaj = { form := "kwàj", gloss := "bubbling hot water", tones := [Phonology.Autosegmental.RegisterTier.TRN.L], verbType := Fragments.Mwaghavul.VerbalizerChoice.m }

def Fragments.Mwaghavul.vjaar : Ideophone

Equations

• Fragments.Mwaghavul.vjaar = { form := "vjàr", gloss := "pouring of urine", tones := [Phonology.Autosegmental.RegisterTier.TRN.L], verbType := Fragments.Mwaghavul.VerbalizerChoice.m }

def Fragments.Mwaghavul.shweer : Ideophone

Equations

• Fragments.Mwaghavul.shweer = { form := "ʃwèr", gloss := "how water falls", tones := [Phonology.Autosegmental.RegisterTier.TRN.L], verbType := Fragments.Mwaghavul.VerbalizerChoice.m }

def Fragments.Mwaghavul.wuulash : Ideophone

Equations

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

def Fragments.Mwaghavul.fooyoop : Ideophone

Equations

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

def Fragments.Mwaghavul.vjayaap : Ideophone

Equations

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

def Fragments.Mwaghavul.bishool : Ideophone

Equations

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

def Fragments.Mwaghavul.kitiif : Ideophone

Equations

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

def Fragments.Mwaghavul.kodzoong : Ideophone

Equations

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

def Fragments.Mwaghavul.kitfor : Ideophone

Equations

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

def Fragments.Mwaghavul.korjong : Ideophone

Equations

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

def Fragments.Mwaghavul.mondos : Ideophone

Equations

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

def Fragments.Mwaghavul.vwaplas : Ideophone

Equations

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

def Fragments.Mwaghavul.jalpat : Ideophone

Equations

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

def Fragments.Mwaghavul.hanlayap : Ideophone

Equations

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

def Fragments.Mwaghavul.hamhoyof : Ideophone

Equations

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

structure Fragments.Mwaghavul.Syl : Type

A toned Mwaghavul syllable.

• ipa : String

def Fragments.Mwaghavul.instDecidableEqSyl.decEq (x✝ x✝¹ : Syl) : Decidable (x✝ = x✝¹)

Equations

• Fragments.Mwaghavul.instDecidableEqSyl.decEq { ipa := a } { ipa := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mwaghavul.instDecidableEqSyl : DecidableEq Syl

Equations

• Fragments.Mwaghavul.instDecidableEqSyl = Fragments.Mwaghavul.instDecidableEqSyl.decEq

def Fragments.Mwaghavul.instReprSyl.repr : Syl → ℕ → Std.Format

Equations

• Fragments.Mwaghavul.instReprSyl.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "ipa" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.ipa)).group) " }"

@[implicit_reducible]

instance Fragments.Mwaghavul.instReprSyl : Repr Syl

Equations

• Fragments.Mwaghavul.instReprSyl = { reprPrec := Fragments.Mwaghavul.instReprSyl.repr }

@[reducible, inline]

abbrev Fragments.Mwaghavul.TSyl : Type

Convenience: a toned Mwaghavul syllable.

Equations

• Fragments.Mwaghavul.TSyl = Phonology.Autosegmental.GrammaticalTone.TBU Fragments.Mwaghavul.Syl

def Fragments.Mwaghavul.mkTSyl (ipa : String) (t : Phonology.Autosegmental.RegisterTier.TRN) : TSyl

Build a toned syllable from IPA and tone.

Equations

• Fragments.Mwaghavul.mkTSyl ipa t = { seg := { ipa := ipa }, tone := t }

def Fragments.Mwaghavul.deriveVerb (base : Ideophone) : List Phonology.Autosegmental.RegisterTier.TRN

Derive a verb from an ideophone using its verbaliser spec. Returns the output tonal pattern.

Equations

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

theorem Fragments.Mwaghavul.wuulash_verb : deriveVerb wuulash = [Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.M]

theorem Fragments.Mwaghavul.diis_verb : deriveVerb diis = [Phonology.Autosegmental.RegisterTier.TRN.M]

theorem Fragments.Mwaghavul.bishool_verb : deriveVerb bishool = [Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.H]

theorem Fragments.Mwaghavul.hanlayap_verb : deriveVerb hanlayap = [Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.H]

theorem Fragments.Mwaghavul.kitiif_verb : deriveVerb kitiif = [Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.H]

theorem Fragments.Mwaghavul.jalpat_verb : deriveVerb jalpat = [Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.H]

theorem Fragments.Mwaghavul.m_verb_uniform (i : Ideophone) (h : i.verbType = VerbalizerChoice.m) : deriveVerb i = List.map (fun (x : Phonology.Autosegmental.RegisterTier.TRN) => Phonology.Autosegmental.RegisterTier.TRN.M) i.tones

All M-tone derived verbs produce uniform M across all TBUs (13a).

theorem Fragments.Mwaghavul.mh_verb_bisyllabic_pattern (i : Ideophone) (h : i.verbType = VerbalizerChoice.mh) (h2 : i.tones.length = 2) : deriveVerb i = [Phonology.Autosegmental.RegisterTier.TRN.M, Phonology.Autosegmental.RegisterTier.TRN.H]

M-H derived verbs have M on nonfinal TBUs and H on the final TBU. Verified on bisyllabic bases.