Poko postlexical tone requires serial, directional evaluation

[McPL26], Phonology 43, e1.

Poko postlexical tone (lexical data in Fragments.Poko.Tone) resists global constraint evaluation: no ranking or weighting of the paper's four faithfulness constraints derives both /nān + rī^H + nā/ ('I ate a pig') and /kāk^H + rī^H/ ('his pig'), while directional Harmonic Serialism ([Lam22d]) with *FLOAT evaluated left-to-right converges on every attested form. All step witnesses are decide-checked (no sorry).

Main results

• parallel_OT_inadequate — the eq. 59 support is ERC-inconsistent (ranking paradox), with W/L patterns derived from candidate violation profiles via ercOfProfiles, not stipulated.
• weighted_HG_inadequate — the paper's weighting contradiction: MAX(H) cannot both exceed and fall below the summed weights of {DEP(link)/H, MAX(M), MAX(link)/M}.
• Fig3.fig3_LR_converged / Fig3.fig3_RL_converged — LR converges to attested [kāk rī dō], RL to the wrong *[kāk rī dó] (fig. 3); Fig3.parallel_optimum_three_way_tie — count-based *FLOAT yields a divergent tie ([Pru09]).
• Eq21–Eq30 — further tableaux (eqs. 21, 22, 24, 27, 30): *FALL repair, *CROWD blocking, *M◁L-forced tautomorphemic docking.

Candidates (eqs. 57, 58)

inductive McPhersonLamont2026.Cand : Type

Winner/loser candidate pairs from [McPL26] eqs. 57 and 58.

• nanWinner : Cand

  (57c) winner of /nān + rī^H + nā/: rī's H docks rightward onto nā.

• nanLoser : Cand

  (57b) loser: the floating H deletes instead.

• kakWinner : Cand

  (58c) winner of /kāk^H + rī^H/: both floating Hs delete.

• kakLoser : Cand

  (58b) unattested MAX(H)-dominant winner: one H docks, one deletes.

@[implicit_reducible]

instance McPhersonLamont2026.instDecidableEqCand : DecidableEq Cand

Equations

• McPhersonLamont2026.instDecidableEqCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Constraints (eq. 7, eq. 59 columns)

def McPhersonLamont2026.maxH : Constraints.Constraint Cand

MAX(H) (eq. 7c): one violation per H tone deleted by GEN.

Equations

• McPhersonLamont2026.maxH McPhersonLamont2026.Cand.nanWinner = 0
• McPhersonLamont2026.maxH McPhersonLamont2026.Cand.nanLoser = 1
• McPhersonLamont2026.maxH McPhersonLamont2026.Cand.kakWinner = 2
• McPhersonLamont2026.maxH McPhersonLamont2026.Cand.kakLoser = 1

def McPhersonLamont2026.depLinkH : Constraints.Constraint Cand

DEP(link)/H (eq. 7a): one violation per inserted H-associated link.

Equations

• McPhersonLamont2026.depLinkH McPhersonLamont2026.Cand.nanWinner = 1
• McPhersonLamont2026.depLinkH McPhersonLamont2026.Cand.nanLoser = 0
• McPhersonLamont2026.depLinkH McPhersonLamont2026.Cand.kakWinner = 0
• McPhersonLamont2026.depLinkH McPhersonLamont2026.Cand.kakLoser = 1

def McPhersonLamont2026.maxM : Constraints.Constraint Cand

MAX(M) (eq. 7c analogue): one violation per M tone deleted.

Equations

• McPhersonLamont2026.maxM McPhersonLamont2026.Cand.nanWinner = 1
• McPhersonLamont2026.maxM McPhersonLamont2026.Cand.nanLoser = 0
• McPhersonLamont2026.maxM McPhersonLamont2026.Cand.kakWinner = 0
• McPhersonLamont2026.maxM McPhersonLamont2026.Cand.kakLoser = 1

def McPhersonLamont2026.maxLinkM : Constraints.Constraint Cand

MAX(link)/M (eq. 7b analogue): one violation per deleted M-tone link.

Equations

• McPhersonLamont2026.maxLinkM McPhersonLamont2026.Cand.nanWinner = 1
• McPhersonLamont2026.maxLinkM McPhersonLamont2026.Cand.nanLoser = 0
• McPhersonLamont2026.maxLinkM McPhersonLamont2026.Cand.kakWinner = 0
• McPhersonLamont2026.maxLinkM McPhersonLamont2026.Cand.kakLoser = 1

def McPhersonLamont2026.ranking : List (Constraints.Constraint Cand)

The eq. 59 columns; *FLOAT factored out per the paper's candidate restriction.

Equations

• McPhersonLamont2026.ranking = [McPhersonLamont2026.maxH, McPhersonLamont2026.depLinkH, McPhersonLamont2026.maxM, McPhersonLamont2026.maxLinkM]

@[reducible, inline]

abbrev McPhersonLamont2026.numConstraints : ℕ

Equations

• McPhersonLamont2026.numConstraints = 4

@[reducible, inline]

abbrev McPhersonLamont2026.maxHIdx : Fin numConstraints

Constraint indices in ranking.

Equations

• McPhersonLamont2026.maxHIdx = 0

@[reducible, inline]

abbrev McPhersonLamont2026.depLinkHIdx : Fin numConstraints

Equations

• McPhersonLamont2026.depLinkHIdx = 1

@[reducible, inline]

abbrev McPhersonLamont2026.maxMIdx : Fin numConstraints

Equations

• McPhersonLamont2026.maxMIdx = 2

@[reducible, inline]

abbrev McPhersonLamont2026.maxLinkMIdx : Fin numConstraints

Equations

• McPhersonLamont2026.maxLinkMIdx = 3

Derived ERCs

def McPhersonLamont2026.ercA : OptimalityTheory.ERC numConstraints

ERC for the /nān + rī^H + nā/ winner-loser pair.

Equations

• McPhersonLamont2026.ercA = McPhersonLamont2026.ercFor✝ McPhersonLamont2026.Cand.nanWinner McPhersonLamont2026.Cand.nanLoser

def McPhersonLamont2026.ercB : OptimalityTheory.ERC numConstraints

ERC for the /kāk^H + rī^H/ winner-loser pair.

Equations

• McPhersonLamont2026.ercB = McPhersonLamont2026.ercFor✝ McPhersonLamont2026.Cand.kakWinner McPhersonLamont2026.Cand.kakLoser

def McPhersonLamont2026.pokoSupport : List (OptimalityTheory.ERC numConstraints)

The ranking-paradox support.

Equations

• McPhersonLamont2026.pokoSupport = [McPhersonLamont2026.ercA, McPhersonLamont2026.ercB]

The ranking paradox (eq. 59)

theorem McPhersonLamont2026.parallel_OT_inadequate : ¬OptimalityTheory.ERCSet.Consistent pokoSupport

Parallel OT cannot model Poko (eq. 59): the derived support is ERC-inconsistent. Structural proof — Equiv.Perm (Fin n)'s Fintype doesn't kernel-reduce under decide.

Weighted HG inadequacy

theorem McPhersonLamont2026.weighted_HG_inadequate : ¬∃ (w : Fin numConstraints → ℚ), w maxHIdx > w depLinkHIdx + w maxMIdx + w maxLinkMIdx ∧ w depLinkHIdx + w maxMIdx + w maxLinkMIdx > w maxHIdx

Weighted HG cannot model Poko: MAX(H) must both exceed and undercut the other three weights' sum (paper p. 32) — no ℚ-weighting satisfies both.

Shared fig. 2 ranking

def McPhersonLamont2026.stdRanking (n : ℕ) : List (Constraints.Constraint Poko.Form)

The fig. 2 ranking (fig. 3 subset); only *FLOAT^→ is directional.

Equations

• McPhersonLamont2026.stdRanking n = Tone.haveTone :: Tone.starFloatBlock n ++ McPhersonLamont2026.rankingTail✝

def McPhersonLamont2026.lrDerivation (input : Poko.Form) : OptimalityTheory.HSDerivation Poko.Form

Left-to-right directional HS over stdRanking — the paper's positive analysis.

Equations

• McPhersonLamont2026.lrDerivation input = { gen := Autosegmental.FloatingForm.gen, ranking := McPhersonLamont2026.stdRanking input.upper.len }

Fig. 3: LR vs RL over /kāk^H + rī^H + dō^H/

def McPhersonLamont2026.Fig3.fig3Input : Poko.Form

Fig. 3 input /kāk^H + rī^H + dō^H/: each M linked, each H floating.

Equations

• McPhersonLamont2026.Fig3.fig3Input = Autosegmental.FloatingForm.ofGraph (Poko.word [Poko.Syll.kak, Poko.Syll.ri, Poko.Syll.do])

def McPhersonLamont2026.Fig3.derivationLR : OptimalityTheory.HSDerivation Poko.Form

Directional-LR derivation (*FLOAT^→).

Equations

• McPhersonLamont2026.Fig3.derivationLR = McPhersonLamont2026.lrDerivation McPhersonLamont2026.Fig3.fig3Input

def McPhersonLamont2026.Fig3.derivationRL : OptimalityTheory.HSDerivation Poko.Form

Mirror under *FLOAT^← (starFloatBlockRev) — the wrong-form counterexample.

Equations

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

def McPhersonLamont2026.Fig3.attestedForm : Poko.Form

The LR final form [kāk rī dō]: all floating Hs deleted (fig. 3 thick line).

Equations

• McPhersonLamont2026.Fig3.attestedForm = ((Autosegmental.FloatingForm.deleteTierElem McPhersonLamont2026.Fig3.fig3Input 1).deleteTierElem 3).deleteTierElem 5

def McPhersonLamont2026.Fig3.starredForm : Poko.Form

The RL final form *[kāk rī dó] (fig. 3; RL evaluation as in the two-stem eq. 61).

Equations

• McPhersonLamont2026.Fig3.starredForm = (((Autosegmental.FloatingForm.deleteTierElem McPhersonLamont2026.Fig3.fig3Input 5).insertLink 3 2).deleteTierElem 1).deleteTierElem 4

Step witnesses

theorem McPhersonLamont2026.Fig3.fig3_LR_step1 : derivationLR.stepOptimum fig3Input = {Autosegmental.FloatingForm.deleteTierElem fig3Input 1}

LR step 1: H-kāk deletes — *TAUTDOCK and *CROWD block its dockings (60b).

theorem McPhersonLamont2026.Fig3.fig3_LR_step2 : derivationLR.stepOptimum (Autosegmental.FloatingForm.deleteTierElem fig3Input 1) = {(Autosegmental.FloatingForm.deleteTierElem fig3Input 1).deleteTierElem 3}

LR step 2: H-rī deletes — *CROWD (right), no-crossing (left), *TAUTDOCK (own).

theorem McPhersonLamont2026.Fig3.fig3_LR_step3 : derivationLR.stepOptimum ((Autosegmental.FloatingForm.deleteTierElem fig3Input 1).deleteTierElem 3) = {((Autosegmental.FloatingForm.deleteTierElem fig3Input 1).deleteTierElem 3).deleteTierElem 5}

LR step 3: H-dō deletes.

theorem McPhersonLamont2026.Fig3.fig3_LR_converged : derivationLR.Converged attestedForm

LR converges on attestedForm.

theorem McPhersonLamont2026.Fig3.fig3_RL_step1 : derivationRL.stepOptimum fig3Input = {Autosegmental.FloatingForm.deleteTierElem fig3Input 5}

RL step 1: the rightmost floating H (H-dō) deletes.

theorem McPhersonLamont2026.Fig3.fig3_RL_step2 : derivationRL.stepOptimum (Autosegmental.FloatingForm.deleteTierElem fig3Input 5) = {(Autosegmental.FloatingForm.deleteTierElem fig3Input 5).insertLink 3 2}

RL step 2 — the wrong-form seed: H-rī docks onto the now-uncrowded dō.

theorem McPhersonLamont2026.Fig3.fig3_RL_step3 : derivationRL.stepOptimum ((Autosegmental.FloatingForm.deleteTierElem fig3Input 5).insertLink 3 2) = {((Autosegmental.FloatingForm.deleteTierElem fig3Input 5).insertLink 3 2).deleteTierElem 1}

RL step 3: H-kāk deletes.

theorem McPhersonLamont2026.Fig3.fig3_RL_step4 : derivationRL.stepOptimum (((Autosegmental.FloatingForm.deleteTierElem fig3Input 5).insertLink 3 2).deleteTierElem 1) = {(((Autosegmental.FloatingForm.deleteTierElem fig3Input 5).insertLink 3 2).deleteTierElem 1).deleteTierElem 4}

RL step 4: *FALL repairs dō's HM contour; MAX(H) ≫ MAX(M) deletes the M.

theorem McPhersonLamont2026.Fig3.fig3_RL_converged : derivationRL.Converged starredForm

RL converges on starredForm.

theorem McPhersonLamont2026.Fig3.fig3_attested_neq_starred : attestedForm ≠ starredForm

The empirical asymmetry: LR and RL converge to distinct surface forms.

Regular HS: the divergent tie (eq. 62)

def McPhersonLamont2026.Fig3.derivationParallel : OptimalityTheory.HSDerivation Poko.Form

Regular-HS derivation: same ranking with count-based starFloatCount for *FLOAT.

Equations

• McPhersonLamont2026.Fig3.derivationParallel = { gen := Autosegmental.FloatingForm.gen, ranking := Tone.haveTone :: Tone.starFloatCount :: McPhersonLamont2026.rankingTail✝ }

theorem McPhersonLamont2026.Fig3.parallel_optimum_three_way_tie : derivationParallel.stepOptimum fig3Input = {Autosegmental.FloatingForm.deleteTierElem fig3Input 1, Autosegmental.FloatingForm.deleteTierElem fig3Input 3, Autosegmental.FloatingForm.deleteTierElem fig3Input 5}

The divergent tie ([Pru09]): the three single-deletion candidates all tie. (The paper's "no tie-breaker whatsoever helps" strengthening stays editorial.)

theorem McPhersonLamont2026.Fig3.parallel_optimum_card_three : (derivationParallel.stepOptimum fig3Input).card = 3

The regular-HS optimum has three elements.

theorem McPhersonLamont2026.Fig3.directional_LR_optimum_card_one : (derivationLR.stepOptimum fig3Input).card = 1

The directional-LR optimum is a singleton.

theorem McPhersonLamont2026.Fig3.only_directional_disambiguates_fig3 : (derivationLR.stepOptimum fig3Input).card < (derivationParallel.stepOptimum fig3Input).card

Headline: regular HS strictly underdetermines the step that directional HS decides.

Eq. (24): LR with *FALL repair

def McPhersonLamont2026.Eq24.eq24Input : Poko.Form

Eq. (24) input /nãn + rī^H + nã/; H-rī is the only floating tone.

Equations

• McPhersonLamont2026.Eq24.eq24Input = Autosegmental.FloatingForm.ofGraph (Poko.word [Poko.Syll.nan, Poko.Syll.ri, Poko.Syll.na])

def McPhersonLamont2026.Eq24.derivationLR : OptimalityTheory.HSDerivation Poko.Form

Directional-LR derivation over stdRanking.

Equations

• McPhersonLamont2026.Eq24.derivationLR = McPhersonLamont2026.lrDerivation McPhersonLamont2026.Eq24.eq24Input

def McPhersonLamont2026.Eq24.attestedForm : Poko.Form

Attested [nãn rī ná]: H-rī docks onto nã, then *FALL repair deletes M-nã.

Equations

• McPhersonLamont2026.Eq24.attestedForm = (Autosegmental.FloatingForm.insertLink McPhersonLamont2026.Eq24.eq24Input 2 2).deleteTierElem 3

theorem McPhersonLamont2026.Eq24.eq24_step1 : derivationLR.stepOptimum eq24Input = {Autosegmental.FloatingForm.insertLink eq24Input 2 2}

Step 1: H-rī docks rightward onto nã (24d).

theorem McPhersonLamont2026.Eq24.eq24_step2 : derivationLR.stepOptimum (Autosegmental.FloatingForm.insertLink eq24Input 2 2) = {(Autosegmental.FloatingForm.insertLink eq24Input 2 2).deleteTierElem 3}

Step 2: *FALL repair — M-nã deletes, MAX(H) ≫ MAX(M) (24g).

theorem McPhersonLamont2026.Eq24.eq24_converged : derivationLR.Converged attestedForm

LR converges on attestedForm.

Eq. (21): phrase-final floating-H deletion

def McPhersonLamont2026.Eq21.eq21Input : Poko.Form

Eq. (21) input /nãn + rī^H/ (phrase-final): no rightward landing site.

Equations

• McPhersonLamont2026.Eq21.eq21Input = Autosegmental.FloatingForm.ofGraph (Poko.word [Poko.Syll.nan, Poko.Syll.ri])

def McPhersonLamont2026.Eq21.derivationLR : OptimalityTheory.HSDerivation Poko.Form

Directional-LR derivation; eq. (20)'s *FLOAT, *TAUTDOCK ≫ MAX(H) is a sub-ranking.

Equations

• McPhersonLamont2026.Eq21.derivationLR = McPhersonLamont2026.lrDerivation McPhersonLamont2026.Eq21.eq21Input

def McPhersonLamont2026.Eq21.attestedForm : Poko.Form

Attested [nãn rī]: the floating H deletes.

Equations

• McPhersonLamont2026.Eq21.attestedForm = Autosegmental.FloatingForm.deleteTierElem McPhersonLamont2026.Eq21.eq21Input 2

theorem McPhersonLamont2026.Eq21.eq21_step1 : derivationLR.stepOptimum eq21Input = {Autosegmental.FloatingForm.deleteTierElem eq21Input 2}

Step 1: H-rī deletes (21b).

theorem McPhersonLamont2026.Eq21.eq21_converged : derivationLR.Converged attestedForm

LR converges on attestedForm (21d).

Eq. (27): *CROWD blocks docking onto an MH stem

def McPhersonLamont2026.Eq27.eq27Input : Poko.Form

Eq. (27) input /kāk^H + kǎ/; kǎ carries a linked MH contour.

Equations

• McPhersonLamont2026.Eq27.eq27Input = Autosegmental.FloatingForm.ofGraph (Poko.word [Poko.Syll.kak, Poko.Syll.ka])

def McPhersonLamont2026.Eq27.derivationLR : OptimalityTheory.HSDerivation Poko.Form

Directional-LR derivation over stdRanking.

Equations

• McPhersonLamont2026.Eq27.derivationLR = McPhersonLamont2026.lrDerivation McPhersonLamont2026.Eq27.eq27Input

def McPhersonLamont2026.Eq27.attestedForm : Poko.Form

Attested [kāk kǎ]: H-kāk deletes; the MH contour survives.

Equations

• McPhersonLamont2026.Eq27.attestedForm = Autosegmental.FloatingForm.deleteTierElem McPhersonLamont2026.Eq27.eq27Input 1

theorem McPhersonLamont2026.Eq27.eq27_step1 : derivationLR.stepOptimum eq27Input = {Autosegmental.FloatingForm.deleteTierElem eq27Input 1}

Step 1: H-kāk deletes — *CROWD blocks docking onto the two-tone kǎ (27b).

theorem McPhersonLamont2026.Eq27.eq27_converged : derivationLR.Converged attestedForm

LR converges on attestedForm (27e).

Eq. (30): *M◁L forces tautomorphemic docking

def McPhersonLamont2026.Eq30.eq30Input : Poko.Form

Eq. (30) input /kāk^H + ìlí/; ìlí carries a linked LH contour (L% omitted).

Equations

• McPhersonLamont2026.Eq30.eq30Input = Autosegmental.FloatingForm.ofGraph (Poko.word [Poko.Syll.kak, Poko.Syll.ili])

def McPhersonLamont2026.Eq30.eq30Ranking : List (Constraints.Constraint Poko.Form)

Eq. (30) ranking: stdRanking plus *M◁L above *TAUTDOCK — the inversion that licenses tautomorphemic docking (30c).

Equations

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

def McPhersonLamont2026.Eq30.derivationLR : OptimalityTheory.HSDerivation Poko.Form

Equations

• McPhersonLamont2026.Eq30.derivationLR = { gen := Autosegmental.FloatingForm.gen, ranking := McPhersonLamont2026.Eq30.eq30Ranking }

def McPhersonLamont2026.Eq30.attestedForm : Poko.Form

Attested [kǎk ìlí]: H-kāk docks onto its own TBU, making an MH contour.

Equations

• McPhersonLamont2026.Eq30.attestedForm = Autosegmental.FloatingForm.insertLink McPhersonLamont2026.Eq30.eq30Input 1 0

theorem McPhersonLamont2026.Eq30.eq30_step1 : derivationLR.stepOptimum eq30Input = {Autosegmental.FloatingForm.insertLink eq30Input 1 0}

Step 1: tautomorphemic dock — deletion would create M◁L tier adjacency (30c).

theorem McPhersonLamont2026.Eq30.eq30_converged : derivationLR.Converged attestedForm

LR converges despite the standing *TAUTDOCK violation (30e).

Eq. (22): HAVETONE drives docking onto a toneless stem

def McPhersonLamont2026.Eq22.eq22Input : Poko.Form

Eq. (22a) input /nãn + rī^H + ne/; ne is toneless.

Equations

• McPhersonLamont2026.Eq22.eq22Input = Autosegmental.FloatingForm.ofGraph (Poko.word [Poko.Syll.nan, Poko.Syll.ri, Poko.Syll.ne])

def McPhersonLamont2026.Eq22.derivationLR : OptimalityTheory.HSDerivation Poko.Form

Directional-LR derivation over stdRanking.

Equations

• McPhersonLamont2026.Eq22.derivationLR = McPhersonLamont2026.lrDerivation McPhersonLamont2026.Eq22.eq22Input

def McPhersonLamont2026.Eq22.attestedForm : Poko.Form

Attested [nãn rī né]: H-rī docks onto toneless ne.

Equations

• McPhersonLamont2026.Eq22.attestedForm = Autosegmental.FloatingForm.insertLink McPhersonLamont2026.Eq22.eq22Input 2 2

theorem McPhersonLamont2026.Eq22.eq22_step1 : derivationLR.stepOptimum eq22Input = {Autosegmental.FloatingForm.insertLink eq22Input 2 2}

Step 1: H-rī docks onto ne — HAVETONE prefers docking over deletion.

theorem McPhersonLamont2026.Eq22.eq22_converged : derivationLR.Converged attestedForm

LR converges on attestedForm.

Deferred: GEN shift and insert-and-associate ops, L% boundary tone, §§3.3–3.4 tableaux

FloatingForm strictly extends the [Rol18] overwrite encoding

def Autosegmental.FloatingForm.ofTBUList {S : Type u_1} (host : List (Tone.TBU S)) (m : Morpheme) : FloatingForm S Tone.TRN

Embed a tonalOverwrite output into FloatingForm: one morpheme m, links (i, i).

Equations

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

theorem Autosegmental.FloatingForm.ofTBUList_linksTo_subsingleton {S : Type u_1} (host : List (Tone.TBU S)) (m : Morpheme) (i : SegIdx) : ((ofTBUList host m).linksTo i).length ≤ 1

Embedded forms carry at most one surface tone per TBU.

theorem Autosegmental.FloatingForm.exists_multi_tone_TBU : ∃ (f : FloatingForm Unit Tone.TRN) (i : SegIdx), 2 ≤ (f.linksTo i).length

A FloatingForm with two surface tones on one TBU — unreachable by ofTBUList.