McPherson and Lamont (2026): Poko Postlexical Tone Requires Serial, Directional Evaluation

This file formalizes the argument of [McPL26] that Poko postlexical 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': the ranking argument is an inconsistent set of elementary ranking conditions derived from the candidates' violation profiles (parallel_OT_inadequate), and the weighting argument a contradiction in which one constraint's weight must both exceed and fall below a sum of others (weighted_HG_inadequate). Directional Harmonic Serialism after [Lam22d], with the constraint against floating tones evaluated left to right, converges on every attested form, whereas right-to-left evaluation converges on the wrong form and a count-based constraint yields a divergent tie ([Pru09]); the further tableaux show the repair of falling contours, the blocking of crowding, and forced tautomorphemic docking. Every step witness is decided.

Implementation notes

The lexical data live in Fragments.Poko.Tone; the tableaux, rankings, and serial derivations are the substrate's harmonic-serialism and tableau apparatus.

References

• [McPL26]
• [Lam22d]
• [Pru09]

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

  In the (57b) loser, the floating H deletes instead.

• kakWinner : Cand

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

• kakLoser : Cand

  In the unattested MAX(H)-dominant winner (58b), one H docks and one deletes.

@[instance_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 : OptimalityTheory.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 : OptimalityTheory.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 : OptimalityTheory.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 : OptimalityTheory.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 (OptimalityTheory.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.ercFor (winner loser : Cand) : OptimalityTheory.ERC (Fin numConstraints)

ERC of a winner/loser pair via ercOfProfiles ([Pri02]).

Equations

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

def McPhersonLamont2026.ercA : OptimalityTheory.ERC (Fin 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 (Fin 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 : Finset (OptimalityTheory.ERC (Fin numConstraints))

The ranking-paradox support.

Equations

• McPhersonLamont2026.pokoSupport = {McPhersonLamont2026.ercA, McPhersonLamont2026.ercB}

The ranking paradox (eq. 59)

theorem McPhersonLamont2026.parallel_OT_inadequate : ¬(OptimalityTheory.ERC.linearExtensions pokoSupport).Nonempty

Parallel OT cannot model Poko (eq. 59): the derived support is ERC-inconsistent, since no ranking of the four constraints satisfies both of its ERCs.

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, since MAX(H) must both exceed and undercut the other three weights' sum (paper p. 32) and no ℚ-weighting satisfies both.

Shared fig. 2 ranking

def McPhersonLamont2026.rankingTail {u : Poko.Form} : List (OptimalityTheory.Constraint (Autosegmental.Candidate u))

Non-float tail of the fig. 2 ranking, in (60) column order.

Equations

• McPhersonLamont2026.rankingTail = [Tone.starCrowd, Tone.starTautDock, Tone.maxTone Tone.TRN.H, Tone.starFall, Tone.depLinkTone Tone.TRN.H, Tone.maxTone Tone.TRN.M, Tone.maxLinkTone Tone.TRN.M]

def McPhersonLamont2026.stdRanking {u : Poko.Form} : List (OptimalityTheory.Constraint (Autosegmental.Candidate u))

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

Equations

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

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

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

Equations

• McPhersonLamont2026.lrDerivation input = { gen := Autosegmental.Candidate.gen, ranking := McPhersonLamont2026.stdRanking }

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 = Poko.word [Poko.Syll.kak, Poko.Syll.ri, Poko.Syll.do]

instance McPhersonLamont2026.Fig3.instNeZeroNatLengthSponsoredTRNMorphUpperSyllFig3Input : NeZero fig3Input.upper.length

instance McPhersonLamont2026.Fig3.instNeZeroNatLengthSponsoredSyllMorphLowerTRNFig3Input : NeZero fig3Input.lower.length

def McPhersonLamont2026.Fig3.fig3 : Autosegmental.Candidate fig3Input

The faithful candidate of the input.

Equations

• McPhersonLamont2026.Fig3.fig3 = Autosegmental.Candidate.input McPhersonLamont2026.Fig3.fig3Input

def McPhersonLamont2026.Fig3.derivationLR : OptimalityTheory.HSDerivation (Autosegmental.Candidate fig3Input)

Directional-LR derivation (*FLOAT^→).

Equations

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

def McPhersonLamont2026.Fig3.derivationRL : OptimalityTheory.HSDerivation (Autosegmental.Candidate fig3Input)

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

Equations

• McPhersonLamont2026.Fig3.derivationRL = { gen := Autosegmental.Candidate.gen, ranking := Tone.haveTone :: Tone.starFloatBlockRev ++ McPhersonLamont2026.rankingTail }

def McPhersonLamont2026.Fig3.attestedForm : Autosegmental.Candidate fig3Input

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

Equations

• McPhersonLamont2026.Fig3.attestedForm = ((McPhersonLamont2026.Fig3.fig3.deleteTierElem 1).deleteTierElem 3).deleteTierElem 5

def McPhersonLamont2026.Fig3.starredForm : Autosegmental.Candidate fig3Input

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

Equations

• McPhersonLamont2026.Fig3.starredForm = (((McPhersonLamont2026.Fig3.fig3.deleteTierElem 5).insertLink 3 2).deleteTierElem 1).deleteTierElem 4

Step witnesses

theorem McPhersonLamont2026.Fig3.fig3_LR_step1 : derivationLR.stepOptimum fig3 = {fig3.deleteTierElem 1}

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

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

In LR step 2, H-rī deletes, blocked by *CROWD (right), no-crossing (left) and *TAUTDOCK (own).

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

In 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 fig3 = {fig3.deleteTierElem 5}

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

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

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

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

In RL step 3, H-kāk deletes.

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

In RL step 4, *FALL repairs dō's HM contour and 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

LR and RL converge to distinct surface forms.

Regular HS: the divergent tie (eq. 62)

def McPhersonLamont2026.Fig3.derivationParallel : OptimalityTheory.HSDerivation (Autosegmental.Candidate fig3Input)

The regular-HS derivation uses the same ranking with the count-based starFloatCount for *FLOAT.

Equations

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

theorem McPhersonLamont2026.Fig3.parallel_optimum_three_way_tie : derivationParallel.stepOptimum fig3 = {fig3.deleteTierElem 1, fig3.deleteTierElem 3, fig3.deleteTierElem 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 fig3).card = 3

The regular-HS optimum has three elements.

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

The directional-LR optimum is a singleton.

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

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 = Poko.word [Poko.Syll.nan, Poko.Syll.ri, Poko.Syll.na]

instance McPhersonLamont2026.Eq24.instNeZeroNatLengthSponsoredTRNMorphUpperSyllEq24Input : NeZero eq24Input.upper.length

instance McPhersonLamont2026.Eq24.instNeZeroNatLengthSponsoredSyllMorphLowerTRNEq24Input : NeZero eq24Input.lower.length

def McPhersonLamont2026.Eq24.eq24 : Autosegmental.Candidate eq24Input

The faithful candidate of the input.

Equations

• McPhersonLamont2026.Eq24.eq24 = Autosegmental.Candidate.input McPhersonLamont2026.Eq24.eq24Input

def McPhersonLamont2026.Eq24.derivationLR : OptimalityTheory.HSDerivation (Autosegmental.Candidate eq24Input)

Directional-LR derivation over stdRanking.

Equations

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

def McPhersonLamont2026.Eq24.attestedForm : Autosegmental.Candidate eq24Input

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

Equations

• McPhersonLamont2026.Eq24.attestedForm = (McPhersonLamont2026.Eq24.eq24.insertLink 2 2).deleteTierElem 3

theorem McPhersonLamont2026.Eq24.eq24_step1 : derivationLR.stepOptimum eq24 = {eq24.insertLink 2 2}

In step 1, H-rī docks rightward onto nã (24d).

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

In step 2, *FALL repairs the contour by deleting M-nã, as 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 = Poko.word [Poko.Syll.nan, Poko.Syll.ri]

instance McPhersonLamont2026.Eq21.instNeZeroNatLengthSponsoredTRNMorphUpperSyllEq21Input : NeZero eq21Input.upper.length

instance McPhersonLamont2026.Eq21.instNeZeroNatLengthSponsoredSyllMorphLowerTRNEq21Input : NeZero eq21Input.lower.length

def McPhersonLamont2026.Eq21.eq21 : Autosegmental.Candidate eq21Input

The faithful candidate of the input.

Equations

• McPhersonLamont2026.Eq21.eq21 = Autosegmental.Candidate.input McPhersonLamont2026.Eq21.eq21Input

def McPhersonLamont2026.Eq21.derivationLR : OptimalityTheory.HSDerivation (Autosegmental.Candidate eq21Input)

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 : Autosegmental.Candidate eq21Input

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

Equations

• McPhersonLamont2026.Eq21.attestedForm = McPhersonLamont2026.Eq21.eq21.deleteTierElem 2

theorem McPhersonLamont2026.Eq21.eq21_step1 : derivationLR.stepOptimum eq21 = {eq21.deleteTierElem 2}

In 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 = Poko.word [Poko.Syll.kak, Poko.Syll.ka]

instance McPhersonLamont2026.Eq27.instNeZeroNatLengthSponsoredTRNMorphUpperSyllEq27Input : NeZero eq27Input.upper.length

instance McPhersonLamont2026.Eq27.instNeZeroNatLengthSponsoredSyllMorphLowerTRNEq27Input : NeZero eq27Input.lower.length

def McPhersonLamont2026.Eq27.eq27 : Autosegmental.Candidate eq27Input

The faithful candidate of the input.

Equations

• McPhersonLamont2026.Eq27.eq27 = Autosegmental.Candidate.input McPhersonLamont2026.Eq27.eq27Input

def McPhersonLamont2026.Eq27.derivationLR : OptimalityTheory.HSDerivation (Autosegmental.Candidate eq27Input)

Directional-LR derivation over stdRanking.

Equations

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

def McPhersonLamont2026.Eq27.attestedForm : Autosegmental.Candidate eq27Input

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

Equations

• McPhersonLamont2026.Eq27.attestedForm = McPhersonLamont2026.Eq27.eq27.deleteTierElem 1

theorem McPhersonLamont2026.Eq27.eq27_step1 : derivationLR.stepOptimum eq27 = {eq27.deleteTierElem 1}

In step 1, H-kāk deletes, since *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 = Poko.word [Poko.Syll.kak, Poko.Syll.ili]

instance McPhersonLamont2026.Eq30.instNeZeroNatLengthSponsoredTRNMorphUpperSyllEq30Input : NeZero eq30Input.upper.length

instance McPhersonLamont2026.Eq30.instNeZeroNatLengthSponsoredSyllMorphLowerTRNEq30Input : NeZero eq30Input.lower.length

def McPhersonLamont2026.Eq30.eq30 : Autosegmental.Candidate eq30Input

The faithful candidate of the input.

Equations

• McPhersonLamont2026.Eq30.eq30 = Autosegmental.Candidate.input McPhersonLamont2026.Eq30.eq30Input

def McPhersonLamont2026.Eq30.eq30Ranking : List (OptimalityTheory.Constraint (Autosegmental.Candidate eq30Input))

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 (Autosegmental.Candidate eq30Input)

Equations

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

def McPhersonLamont2026.Eq30.attestedForm : Autosegmental.Candidate eq30Input

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

Equations

• McPhersonLamont2026.Eq30.attestedForm = McPhersonLamont2026.Eq30.eq30.insertLink 1 0

theorem McPhersonLamont2026.Eq30.eq30_step1 : derivationLR.stepOptimum eq30 = {eq30.insertLink 1 0}

In step 1, the tone docks tautomorphemically, since 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 = Poko.word [Poko.Syll.nan, Poko.Syll.ri, Poko.Syll.ne]

instance McPhersonLamont2026.Eq22.instNeZeroNatLengthSponsoredTRNMorphUpperSyllEq22Input : NeZero eq22Input.upper.length

instance McPhersonLamont2026.Eq22.instNeZeroNatLengthSponsoredSyllMorphLowerTRNEq22Input : NeZero eq22Input.lower.length

def McPhersonLamont2026.Eq22.eq22 : Autosegmental.Candidate eq22Input

The faithful candidate of the input.

Equations

• McPhersonLamont2026.Eq22.eq22 = Autosegmental.Candidate.input McPhersonLamont2026.Eq22.eq22Input

def McPhersonLamont2026.Eq22.derivationLR : OptimalityTheory.HSDerivation (Autosegmental.Candidate eq22Input)

Directional-LR derivation over stdRanking.

Equations

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

def McPhersonLamont2026.Eq22.attestedForm : Autosegmental.Candidate eq22Input

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

Equations

• McPhersonLamont2026.Eq22.attestedForm = McPhersonLamont2026.Eq22.eq22.insertLink 2 2

theorem McPhersonLamont2026.Eq22.eq22_step1 : derivationLR.stepOptimum eq22 = {eq22.insertLink 2 2}

In step 1, H-rī docks onto ne, as 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

Candidate strictly extends the [Rol18] overwrite encoding

def Autosegmental.Form.ofTBUList {S : Type u_1} (host : List (Tone.TBU S)) (m : Morphology.Morph) : Form S Tone.TRN Morphology.Morph

Embed a Tone.overwrite output as a form with one morpheme m and links (i, i).

Equations

• Autosegmental.Form.ofTBUList host m = Autosegmental.Form.melody m (List.map Tone.TBU.tone host) (List.map Tone.TBU.seg host) (List.map (fun (i : ℕ) => (i, i)) (List.range host.length)).toFinset

theorem Autosegmental.Form.ofTBUList_linksTo_subsingleton {S : Type u_1} (host : List (Tone.TBU S)) (m : Morphology.Morph) (i : Fin (ofTBUList host m).lower.length) : ((Candidate.input (ofTBUList host m)).linksTo i).length ≤ 1

The faithful candidate of an embedded form carries at most one surface tone per TBU.

theorem Autosegmental.Candidate.exists_multi_tone_TBU : ∃ (u : Form Unit Tone.TRN Morphology.Morph) (c : Candidate u) (i : Fin u.lower.length), 2 ≤ (c.linksTo i).length

A candidate with two surface tones on one TBU, which no faithful candidate of an ofTBUList form has.