Akinbo and Fwangwar (2026): Iconicity and expressiveness of grammatical tones targeting ideophones in Mwaghavul

Mwaghavul derives verbs from ideophones by a segmentally null verbaliser with two lexically selected allomorphs, whose only exponents are the tunes M and M-H. A singular verb bears M on every syllable, or M on every nonfinal syllable and H on the final one. A pluractional verb doubles the ideophone and bears M on every syllable of the reduplicant and H on every syllable of the base, so corresponding syllables never agree in tone, an iconic disharmony. The derived verbs occur wherever underived verbs do and stay expressive, against the claimed inverse relation between grammatical integration and expressiveness. The paper classifies the verbaliser as replacive-dominant grammatical tone and derives its realisation in Optimality Theory from constraints anchoring the verbaliser's tones to the edges of roots.

The printed verbs fit replacive dominance and no other dominance type, so the magnitude iconicity the ideophones carry in their lexical tones is lost in their verbs. The three tableaux, built from the dataset's ideophones under one constraint set, select the printed verbs exactly under the rankings with R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Hᵥ and MAX-Tone below both M anchors. Two dominations the paper states, L-ANCH-Mᵥ ≫ R-ANCH-Mᵥ and L-ANCH-Hᵥ ≫ MAX-Tone, are not needed.

Main statements

• fits_iff: replacive dominance is the only dominance type that derives every printed verb.
• selectsWinners_iff: the rankings under which the tableaux select the printed verbs.
• exists_selectsWinners_rAnchorM_lAnchorM: neither L-ANCH-Mᵥ ≫ R-ANCH-Mᵥ nor L-ANCH-Hᵥ ≫ MAX-Tone is needed.

Implementation notes

• An input writes a root's lexical tones as the paper does, one tone for each run of identical tones, linked to every syllable of its run.
• The hosts of the verbaliser's tones are the roots, the morphemes sponsoring the syllables, since the verbaliser has no segments.

TODO

• INTEGRITY-Mᵥ forbids an output with two correspondents of the verbaliser's M, and only the copying candidate of the first tableau violates it. A Candidate shares its input's tiers, so neither is represented. The copying candidate's printed row is harmonically bounded by the winner's, so leaving it out changes no optimum and no ranking condition.

References

• [AF26]
• [Rol18]
• [Fin09b]
• [McCP95]
• [DA17]
• [DT20]

The verbaliser as replacive-dominant grammatical tone

inductive AkinboFwangwar2026.Verbalizer : Type

The two lexically selected allomorphs of the verbaliser, VBZ₁ with the tune M and VBZ₂ with the tune M-H.

• m : Verbalizer
• mh : Verbalizer

@[instance_reducible]

instance AkinboFwangwar2026.instDecidableEqVerbalizer : DecidableEq Verbalizer

Equations

• AkinboFwangwar2026.instDecidableEqVerbalizer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AkinboFwangwar2026.instReprVerbalizer.repr : Verbalizer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AkinboFwangwar2026.instReprVerbalizer : Repr Verbalizer

Equations

• AkinboFwangwar2026.instReprVerbalizer = { reprPrec := AkinboFwangwar2026.instReprVerbalizer.repr }

def AkinboFwangwar2026.Verbalizer.tune : Verbalizer → Tone.Tune

The tune of a verbaliser on a single host: M spreading over every syllable, or M-H anchored at the right edge.

Equations

• AkinboFwangwar2026.Verbalizer.m.tune = { melody := [Tone.TRN.M], anchor := Edge.left }
• AkinboFwangwar2026.Verbalizer.mh.tune = { melody := [Tone.TRN.M, Tone.TRN.H], anchor := Edge.right }

def AkinboFwangwar2026.verbalizer (i : Mwaghavul.Ideophone) : Option Verbalizer

The verbaliser an ideophone selects, read off its singular verb: VBZ₁ when the verb is level M.

Equations

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

def AkinboFwangwar2026.singular (d : Tone.Dominance) (v : Verbalizer) (i : Mwaghavul.Ideophone) : List Tone.TRN

The singular verb of a trigger of dominance type d with verbaliser v: the tune applied to the ideophone's syllables.

Equations

• AkinboFwangwar2026.singular d v i = List.map Tone.TBU.tone (d.apply v.tune i.syllables)

def AkinboFwangwar2026.pluractional (d : Tone.Dominance) (i : Mwaghavul.Ideophone) : List Tone.TRN

The pluractional verb of a trigger of dominance type d: VBZ₂ on the doubled ideophone, each of its tones on its own root, M on the reduplicant and H on the base.

Equations

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

theorem AkinboFwangwar2026.fits_iff (d : Tone.Dominance) : (∀ i ∈ Mwaghavul.ideophones, i.verb = Option.map (fun (x : Verbalizer) => singular d x i) (verbalizer i) ∧ i.pluractional = pluractional d i) ↔ d = Tone.Dominance.replacive

The printed verbs fit replacive dominance and no other type of [Rol18]'s typology: the singular verb is the selected verbaliser's tune applied to the ideophone, and the pluractional verb VBZ₂ on the doubled ideophone.

theorem AkinboFwangwar2026.magnitude_overwritten : List.map Tone.TBU.seg Mwaghavul.wulash.syllables = List.map Tone.TBU.seg Mwaghavul.wulashSmall.syllables ∧ Mwaghavul.wulash.tones ≠ Mwaghavul.wulashSmall.tones ∧ Mwaghavul.wulash.verb = Mwaghavul.wulashSmall.verb ∧ Mwaghavul.wulash.pluractional = Mwaghavul.wulashSmall.pluractional

The verbaliser overwrites the magnitude iconicity of lexical tone: wùlàʃ ‘wide open’ and wúláʃ ‘wide open of small thing’ differ only in tone and have the same verbs.

The descriptive generalisations

theorem AkinboFwangwar2026.verb_melodies (i : Mwaghavul.Ideophone) : i ∈ Mwaghavul.ideophones → ∀ v ∈ i.verb, v = List.map (fun (x : Tone.TRN) => Tone.TRN.M) i.tones ∨ v = List.map (fun (x : Tone.TRN) => Tone.TRN.M) i.tones.dropLast ++ [Tone.TRN.H]

Every singular verb has M on every syllable, or M on every nonfinal syllable and H on the final one.

theorem AkinboFwangwar2026.verbalizer_lexical : Mwaghavul.wulash.tones = Mwaghavul.bishol.tones ∧ verbalizer Mwaghavul.wulash = some Verbalizer.m ∧ verbalizer Mwaghavul.bishol = some Verbalizer.mh

Which melody a singular verb has is lexical: wùlàʃ ‘wide open’ and bɨ̀ʃɔ̀l ‘shabbily dressed’ have the same tones and select different verbalisers.

theorem AkinboFwangwar2026.pluractional_eq (i : Mwaghavul.Ideophone) : i ∈ Mwaghavul.ideophones → i.pluractional = List.map (fun (x : Tone.TRN) => Tone.TRN.M) i.tones ++ List.map (fun (x : Tone.TRN) => Tone.TRN.H) i.tones

Every pluractional verb has M on every syllable of the reduplicant and H on every syllable of the base, whichever melody its singular verb has.

theorem AkinboFwangwar2026.pluractional_disharmonic (i : Mwaghavul.Ideophone) : i ∈ Mwaghavul.ideophones → List.Forall₂ (fun (x1 x2 : Tone.TRN) => x1 ≠ x2) (List.take i.tones.length i.pluractional) (List.drop i.tones.length i.pluractional)

Corresponding syllables of a pluractional verb's reduplicant and base never agree in tone, the disharmony that depicts distinguishable identity.

Inputs and constraints

inductive AkinboFwangwar2026.Morpheme : Type

The morphemes of a derived verb: the ideophonic root, doubled into a reduplicant and a base in a pluractional verb, and the verbaliser.

• root : Morpheme
• red : Morpheme
• base : Morpheme
• vbz : Morpheme

@[instance_reducible]

instance AkinboFwangwar2026.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• AkinboFwangwar2026.instDecidableEqMorpheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AkinboFwangwar2026.instReprMorpheme : Repr Morpheme

Equations

• AkinboFwangwar2026.instReprMorpheme = { reprPrec := AkinboFwangwar2026.instReprMorpheme.repr }

def AkinboFwangwar2026.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev AkinboFwangwar2026.Form : Type

A form with syllable TBUs, tones, and the sponsoring morphemes.

Equations

• AkinboFwangwar2026.Form = Autosegmental.Form Mwaghavul.Syl Tone.TRN AkinboFwangwar2026.Morpheme

def AkinboFwangwar2026.rootInput (m : Morpheme) (i : Mwaghavul.Ideophone) : Form

The input of an ideophone as the root m: one lexical tone for each run of identical tones, linked to every syllable of its run.

Equations

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

def AkinboFwangwar2026.Verbalizer.input (v : Verbalizer) : Form

The input of a verbaliser: its tones, floating.

Equations

• v.input = Autosegmental.Form.melody AkinboFwangwar2026.Morpheme.vbz v.tune.melody [] ∅

inductive AkinboFwangwar2026.Con : Type

The constraints of the analysis: LEFT-ANCHOR and RIGHT-ANCHOR for the verbaliser's M and H ((22)), and MAX-Tone ((23)).

• lAnchorM : Con
• rAnchorH : Con
• rAnchorM : Con
• lAnchorH : Con
• maxTone : Con

@[instance_reducible]

instance AkinboFwangwar2026.instDecidableEqCon : DecidableEq Con

Equations

• AkinboFwangwar2026.instDecidableEqCon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AkinboFwangwar2026.instFintypeCon : Fintype Con

Equations

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

@[instance_reducible]

instance AkinboFwangwar2026.instReprCon : Repr Con

Equations

• AkinboFwangwar2026.instReprCon = { reprPrec := AkinboFwangwar2026.instReprCon.repr }

def AkinboFwangwar2026.instReprCon.repr : Con → ℕ → Std.Format

Equations

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

def AkinboFwangwar2026.roots (u : Form) : List Morpheme

The roots of a form, the morphemes sponsoring its syllables.

Equations

• AkinboFwangwar2026.roots u = (List.map Autosegmental.Sponsored.morpheme u.lower).dedup

def AkinboFwangwar2026.BearsTone {u : Form} (c : Autosegmental.Candidate u) (t : Tone.TRN) (i : Fin u.lower.length) : Prop

Syllable i bears the verbaliser's tone t.

Equations

• AkinboFwangwar2026.BearsTone c t i = ∃ k ∈ c.linksTo i, u.upper[k].value = t ∧ u.upper[k].morpheme = AkinboFwangwar2026.Morpheme.vbz

@[instance_reducible]

instance AkinboFwangwar2026.instDecidableBearsTone {u : Form} (c : Autosegmental.Candidate u) (t : Tone.TRN) (i : Fin u.lower.length) : Decidable (BearsTone c t i)

Equations

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

def AkinboFwangwar2026.anchor {u : Form} (e : Edge) (t : Tone.TRN) : OptimalityTheory.Constraint (Autosegmental.Candidate u)

LEFT-ANCHOR-Tᵥ and RIGHT-ANCHOR-Tᵥ ([Fin09b]): the verbaliser's t corresponds to the edge e of a root. One violation for each syllable between a root's edge and the nearest syllable bearing t, on the root where they are fewest, and one for every syllable when no root bears t.

Equations

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

def AkinboFwangwar2026.con {u : Form} : OptimalityTheory.ConstraintSet (Autosegmental.Candidate u) Con

The constraint set, MAX-Tone counting the deleted tones.

Equations

• AkinboFwangwar2026.con AkinboFwangwar2026.Con.lAnchorM = AkinboFwangwar2026.anchor Edge.left Tone.TRN.M
• AkinboFwangwar2026.con AkinboFwangwar2026.Con.rAnchorH = AkinboFwangwar2026.anchor Edge.right Tone.TRN.H
• AkinboFwangwar2026.con AkinboFwangwar2026.Con.rAnchorM = AkinboFwangwar2026.anchor Edge.right Tone.TRN.M
• AkinboFwangwar2026.con AkinboFwangwar2026.Con.lAnchorH = AkinboFwangwar2026.anchor Edge.left Tone.TRN.H
• AkinboFwangwar2026.con AkinboFwangwar2026.Con.maxTone = fun (c : Autosegmental.Candidate u) => c.deleted.card

def AkinboFwangwar2026.surface {u : Form} (c : Autosegmental.Candidate u) : List Tone.TRN

The tones on the syllables of a candidate, left to right.

Equations

• AkinboFwangwar2026.surface c = List.flatMap c.tierValues (List.finRange u.lower.length)

The M verbaliser and an unreduplicated ideophone

def AkinboFwangwar2026.Tableau24.input : Form

wùlàʃ ‘wide open’ with VBZ₁: one lexical L linked to both syllables, the verbaliser's M floating.

Equations

• AkinboFwangwar2026.Tableau24.input = AkinboFwangwar2026.rootInput AkinboFwangwar2026.Morpheme.root Mwaghavul.wulash * AkinboFwangwar2026.Verbalizer.m.input

instance AkinboFwangwar2026.Tableau24.instNeZeroNatLengthSponsoredTRNMorphemeUpperSylInput : NeZero input.upper.length

instance AkinboFwangwar2026.Tableau24.instNeZeroNatLengthSponsoredSylMorphemeLowerTRNInput : NeZero input.lower.length

def AkinboFwangwar2026.Tableau24.cand : Autosegmental.Candidate input

The faithful candidate.

Equations

• AkinboFwangwar2026.Tableau24.cand = Autosegmental.Candidate.input AkinboFwangwar2026.Tableau24.input

def AkinboFwangwar2026.Tableau24.candA : Autosegmental.Candidate input

The candidates (24a)–(24e): (wùlàʃ)₁ M₂, (wùlàʃ)₁, (wù)₁(lāʃ)₂, (wū)₂(làʃ)₁, and (wūlāʃ)₂.

Equations

• AkinboFwangwar2026.Tableau24.candA = AkinboFwangwar2026.Tableau24.cand

def AkinboFwangwar2026.Tableau24.candB : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau24.candB = AkinboFwangwar2026.Tableau24.cand.deleteTierElem 1

def AkinboFwangwar2026.Tableau24.candC : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau24.candC = (AkinboFwangwar2026.Tableau24.cand.deleteLink 0 1).insertLink 1 1

def AkinboFwangwar2026.Tableau24.candD : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau24.candD = (AkinboFwangwar2026.Tableau24.cand.deleteLink 0 0).insertLink 1 0

def AkinboFwangwar2026.Tableau24.candE : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau24.candE = ((AkinboFwangwar2026.Tableau24.cand.deleteTierElem 0).insertLink 1 0).insertLink 1 1

def AkinboFwangwar2026.Tableau24.candidates : List (Autosegmental.Candidate input)

Equations

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

theorem AkinboFwangwar2026.Tableau24.optimal_iff (r : OptimalityTheory.Ranking Con 5) : (OptimalityTheory.Tableau.ofPerm con r candidates optimal_iff._proof_1).optimal = {candE} ↔ r.Dominates Con.lAnchorM Con.maxTone ∧ r.Dominates Con.rAnchorM Con.maxTone

The tableau selects the spreading of M exactly when MAX-Tone is below both M anchors. It does not rank L-ANCH-Mᵥ against R-ANCH-Mᵥ, which the paper reads off it.

The M-H verbaliser and an unreduplicated ideophone

def AkinboFwangwar2026.Tableau25.input : Form

háŋláɣáp ‘light-weighted’ with VBZ₂.

Equations

• AkinboFwangwar2026.Tableau25.input = AkinboFwangwar2026.rootInput AkinboFwangwar2026.Morpheme.root Mwaghavul.hanlaghap * AkinboFwangwar2026.Verbalizer.mh.input

instance AkinboFwangwar2026.Tableau25.instNeZeroNatLengthSponsoredTRNMorphemeUpperSylInput : NeZero input.upper.length

instance AkinboFwangwar2026.Tableau25.instNeZeroNatLengthSponsoredSylMorphemeLowerTRNInput : NeZero input.lower.length

def AkinboFwangwar2026.Tableau25.cand : Autosegmental.Candidate input

The faithful candidate.

Equations

• AkinboFwangwar2026.Tableau25.cand = Autosegmental.Candidate.input AkinboFwangwar2026.Tableau25.input

def AkinboFwangwar2026.Tableau25.candA : Autosegmental.Candidate input

The candidates (25a)–(25g): (háŋláɣáp)₁, (hāŋlā)₂(ɣáp)₁, (háŋláɣáp)₃, (hāŋlāɣāp)₂, (hāŋlā)₂(ɣáp)₃, (hāŋ)₂(láɣáp)₃, and (hāŋ)₂(lá)₁(ɣáp)₃.

Equations

• AkinboFwangwar2026.Tableau25.candA = (AkinboFwangwar2026.Tableau25.cand.deleteTierElem 1).deleteTierElem 2

def AkinboFwangwar2026.Tableau25.candB : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau25.candB = ((((AkinboFwangwar2026.Tableau25.cand.deleteLink 0 0).deleteLink 0 1).insertLink 1 0).insertLink 1 1).deleteTierElem 2

def AkinboFwangwar2026.Tableau25.candC : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau25.candC = ((((AkinboFwangwar2026.Tableau25.cand.deleteTierElem 0).deleteTierElem 1).insertLink 2 0).insertLink 2 1).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candD : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau25.candD = ((((AkinboFwangwar2026.Tableau25.cand.deleteTierElem 0).deleteTierElem 2).insertLink 1 0).insertLink 1 1).insertLink 1 2

def AkinboFwangwar2026.Tableau25.candE : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau25.candE = (((AkinboFwangwar2026.Tableau25.cand.deleteTierElem 0).insertLink 1 0).insertLink 1 1).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candF : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau25.candF = (((AkinboFwangwar2026.Tableau25.cand.deleteTierElem 0).insertLink 1 0).insertLink 2 1).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candG : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau25.candG = (((AkinboFwangwar2026.Tableau25.cand.deleteLink 0 0).deleteLink 0 2).insertLink 1 0).insertLink 2 2

def AkinboFwangwar2026.Tableau25.candidates : List (Autosegmental.Candidate input)

Equations

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

theorem AkinboFwangwar2026.Tableau25.optimal_iff (r : OptimalityTheory.Ranking Con 5) : (OptimalityTheory.Tableau.ofPerm con r candidates optimal_iff._proof_1).optimal = {candE} ↔ r.Dominates Con.rAnchorH Con.rAnchorM ∧ r.Dominates Con.rAnchorM Con.lAnchorH ∧ r.Dominates Con.rAnchorM Con.maxTone

The tableau selects M then H exactly under R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Hᵥ and R-ANCH-Mᵥ ≫ MAX-Tone. It does not rank L-ANCH-Mᵥ against R-ANCH-Mᵥ either.

The M-H verbaliser and a reduplicated ideophone

def AkinboFwangwar2026.Tableau26.input : Form

jàlpàt ‘hanging loose’ doubled into a reduplicant and a base, each with its own lexical L, with VBZ₂.

Equations

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

instance AkinboFwangwar2026.Tableau26.instNeZeroNatLengthSponsoredTRNMorphemeUpperSylInput : NeZero input.upper.length

instance AkinboFwangwar2026.Tableau26.instNeZeroNatLengthSponsoredSylMorphemeLowerTRNInput : NeZero input.lower.length

def AkinboFwangwar2026.Tableau26.cand : Autosegmental.Candidate input

The faithful candidate.

Equations

• AkinboFwangwar2026.Tableau26.cand = Autosegmental.Candidate.input AkinboFwangwar2026.Tableau26.input

def AkinboFwangwar2026.Tableau26.candA : Autosegmental.Candidate input

The candidates (26a)–(26g): (jàlpàt)₁(jàlpàt)₂, (jàl)₁(pāt)₃(jàl)₂(pát)₄, (jāl)₃(pàt)₁(jàl)₄(pàt)₂, (jālpāt)₃(jálpát)₄, (jāl)₃(pát)₄(jàlpàt)₂, (jālpāt jāl)₃(pát)₄, and (jāl)₃(pàt jàl)₁(pát)₄.

Equations

• AkinboFwangwar2026.Tableau26.candA = AkinboFwangwar2026.Tableau26.cand

def AkinboFwangwar2026.Tableau26.candB : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau26.candB = (((AkinboFwangwar2026.Tableau26.cand.deleteLink 0 1).insertLink 2 1).deleteLink 1 3).insertLink 3 3

def AkinboFwangwar2026.Tableau26.candC : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau26.candC = (((AkinboFwangwar2026.Tableau26.cand.deleteLink 0 0).insertLink 2 0).deleteLink 1 2).insertLink 3 2

def AkinboFwangwar2026.Tableau26.candD : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau26.candD = (((((AkinboFwangwar2026.Tableau26.cand.deleteTierElem 0).deleteTierElem 1).insertLink 2 0).insertLink 2 1).insertLink 3 2).insertLink 3 3

def AkinboFwangwar2026.Tableau26.candE : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau26.candE = ((AkinboFwangwar2026.Tableau26.cand.deleteTierElem 0).insertLink 2 0).insertLink 3 1

def AkinboFwangwar2026.Tableau26.candF : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau26.candF = (((((AkinboFwangwar2026.Tableau26.cand.deleteTierElem 0).deleteTierElem 1).insertLink 2 0).insertLink 2 1).insertLink 2 2).insertLink 3 3

def AkinboFwangwar2026.Tableau26.candG : Autosegmental.Candidate input

Equations

• AkinboFwangwar2026.Tableau26.candG = ((((AkinboFwangwar2026.Tableau26.cand.deleteLink 0 0).deleteTierElem 1).insertLink 2 0).insertLink 0 2).insertLink 3 3

def AkinboFwangwar2026.Tableau26.candidates : List (Autosegmental.Candidate input)

Equations

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

theorem AkinboFwangwar2026.Tableau26.optimal_iff (r : OptimalityTheory.Ranking Con 5) : (OptimalityTheory.Tableau.ofPerm con r candidates optimal_iff._proof_1).optimal = {candD} ↔ (r.Dominates Con.lAnchorM Con.maxTone ∨ r.Dominates Con.lAnchorH Con.maxTone) ∧ (r.Dominates Con.rAnchorH Con.maxTone ∨ r.Dominates Con.rAnchorM Con.maxTone) ∧ (r.Dominates Con.rAnchorM Con.maxTone ∨ r.Dominates Con.lAnchorH Con.maxTone)

The tableau ranks no two constraints on its own: it selects M on the reduplicant and H on the base exactly when MAX-Tone is below a left anchor, a right anchor, and one of R-ANCH-Mᵥ and L-ANCH-Hᵥ.

The ranking

def AkinboFwangwar2026.SelectsWinners (r : OptimalityTheory.Ranking Con 5) : Prop

A ranking selects the printed verbs: the spreading of M over the root in the first tableau, M then H in the second, and M on the reduplicant with H on the base in the third.

Equations

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

theorem AkinboFwangwar2026.selectsWinners_iff (r : OptimalityTheory.Ranking Con 5) : SelectsWinners r ↔ r.Dominates Con.rAnchorH Con.rAnchorM ∧ r.Dominates Con.rAnchorM Con.lAnchorH ∧ r.Dominates Con.rAnchorM Con.maxTone ∧ r.Dominates Con.lAnchorM Con.maxTone

The tableaux select the printed verbs exactly under the rankings with R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Hᵥ and MAX-Tone below both M anchors.

theorem AkinboFwangwar2026.exists_selectsWinners_rAnchorM_lAnchorM : ∃ (r : OptimalityTheory.Ranking Con 5), SelectsWinners r ∧ r.Dominates Con.rAnchorM Con.lAnchorM ∧ r.Dominates Con.maxTone Con.lAnchorH

Neither L-ANCH-Mᵥ ≫ R-ANCH-Mᵥ nor L-ANCH-Hᵥ ≫ MAX-Tone, both of which the paper states, is needed: the ranking R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Mᵥ ≫ MAX-Tone ≫ L-ANCH-Hᵥ reverses both and selects the printed verbs.

theorem AkinboFwangwar2026.selectsWinners_of_dominates {r : OptimalityTheory.Ranking Con 5} (h₁ : r.Dominates Con.lAnchorM Con.rAnchorM) (h₂ : r.Dominates Con.rAnchorH Con.rAnchorM) (h₃ : r.Dominates Con.rAnchorM Con.lAnchorH) (h₄ : r.Dominates Con.lAnchorH Con.maxTone) : SelectsWinners r

The paper's ranking, L-ANCH-Mᵥ and R-ANCH-Hᵥ ≫ R-ANCH-Mᵥ ≫ L-ANCH-Hᵥ ≫ MAX-Tone, selects the printed verbs.

theorem AkinboFwangwar2026.surface_winners : some (surface Tableau24.candE) = Mwaghavul.wulash.verb ∧ some (surface Tableau25.candE) = Mwaghavul.hanlaghap.verb ∧ surface Tableau26.candD = Mwaghavul.jalpat.pluractional

The winners surface as the printed verbs wūlāʃ, hāŋlāɣáp, and jālpāt-jálpát.

Morphosyntactic integration

theorem AkinboFwangwar2026.derived_verbs_integrated (row : Datum) : row ∈ Examples.all → row.feature? "verb" = some "underived" → ∃ row' ∈ Examples.all, row'.feature? "verb" = some "derived" ∧ row'.feature? "construction" = row.feature? "construction"

Every construction attested with the underived verb of (11) is attested with the derived verb of (12): tense, focus, serial verbs, negation.