Tonal Constraints — Generic Constructors over FloatingForm

@cite{wolf-2007} @cite{cahill-2004} @cite{mcpherson-lamont-2026}

OT/HS constraint constructors over the FloatingForm S autosegmental representation (Theories/Phonology/Autosegmental/Floating.lean). Generic over the segment type S.

All constraints are DirectionalConstraints:

• Genuinely directional (e.g., *FLOAT^→) emit indicator vectors with positions in tier order.
• Parallel-by-nature emit singletons [count] (per EvalMode.le_singleton's singleton-degeneracy guarantee).

Constraint inventory (paper, eqs. 5, 7, 15-17, 23)

• starFloat ← paper eq. 16 (*FLOAT, directional)
• starTautDock ← paper eq. 15 (*TAUTDOCK, after @cite{wolf-2007})
• starCrowd threshold ← paper eq. 5 (*CROWD, after @cite{cahill-2004})
• starFall ← paper eq. 23 (*FALL, falling-contour ban)
• maxTone t ← paper eq. 7c (MAX(T))
• depLinkTone t ← paper eq. 7a (DEP(link)/T)
• maxLinkTone t ← paper eq. 7b (MAX(link)/T)
• haveTone ← paper eq. 17 (HAVETONE)

Faithfulness against the underlying form

Faithfulness constraints (maxTone, maxLinkTone, depLinkTone) compare surface state to the immutable underlying state stored in FloatingForm. This is what makes the @cite{mcpherson-lamont-2026} fig. 3 multi-step asymmetry visible: without underlying-form tracking, faithfulness can't fire and the LR-vs-RL distinction collapses.

def Phonology.Tone.IsInsertedLink {S : Type} (f : Autosegmental.FloatingForm S) (l : Autosegmental.Link) : Prop

The link (k, i) was inserted by GEN (in surface but not in underlying).

Equations

• Phonology.Tone.IsInsertedLink f l = (l ∈ f.surfaceLinks ∧ l ∉ f.ulLinks)

@[implicit_reducible]

instance Phonology.Tone.instDecidableIsInsertedLink {S : Type} (f : Autosegmental.FloatingForm S) (l : Autosegmental.Link) : Decidable (IsInsertedLink f l)

Equations

• Phonology.Tone.instDecidableIsInsertedLink f l = Phonology.Tone.instDecidableIsInsertedLink._aux_1 f l

def Phonology.Tone.IsDeletedLink {S : Type} (f : Autosegmental.FloatingForm S) (l : Autosegmental.Link) : Prop

The link (k, i) was deleted by GEN (in underlying but not in surface).

Equations

• Phonology.Tone.IsDeletedLink f l = (l ∈ f.ulLinks ∧ l ∉ f.surfaceLinks)

@[implicit_reducible]

instance Phonology.Tone.instDecidableIsDeletedLink {S : Type} (f : Autosegmental.FloatingForm S) (l : Autosegmental.Link) : Decidable (IsDeletedLink f l)

Equations

• Phonology.Tone.instDecidableIsDeletedLink f l = Phonology.Tone.instDecidableIsDeletedLink._aux_1 f l

def Phonology.Tone.ToneHasValue {S : Type} (f : Autosegmental.FloatingForm S) (k : Autosegmental.ToneIdx) (t : Autosegmental.RegisterTier.TRN) : Prop

The tone at index k has value t.

Equations

• Phonology.Tone.ToneHasValue f k t = (Option.map Phonology.Autosegmental.ToneSpec.tone f.ulTones[k]? = some t)

@[implicit_reducible]

instance Phonology.Tone.instDecidableToneHasValue {S : Type} (f : Autosegmental.FloatingForm S) (k : Autosegmental.ToneIdx) (t : Autosegmental.RegisterTier.TRN) : Decidable (ToneHasValue f k t)

Equations

• Phonology.Tone.instDecidableToneHasValue f k t = Phonology.Tone.instDecidableToneHasValue._aux_1 f k t

def Phonology.Tone.starFloat {S : Type} : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

*FLOAT (paper, eq. 16): one violation per tone not associated to a syllable. Directional: emits the indicator vector floatIndicator, with one entry per underlying tone position recording whether that tone is currently floating.

Equations

• Phonology.Tone.starFloat = { name := "*FLOAT", family := Core.Constraint.OT.ConstraintFamily.markedness, eval := Phonology.Autosegmental.FloatingForm.floatIndicator }

def Phonology.Tone.starFloatCount {S : Type} : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

*FLOAT (count): count-based variant of *FLOAT that emits the total floating-tone count as a singleton vector. Used in regular (non-directional) HS where positions don't matter — only the cardinality of the floating set.

Distinct from starFloat (which emits the position-aware indicator vector). The two coincide when there is at most one floating tone but diverge as the floating set grows: count-based comparison cannot distinguish "delete leftmost" from "delete rightmost" since both reduce the count by 1. This is @cite{mcpherson-lamont-2026}'s eq. (62) "divergent ties" claim — regular HS with starFloatCount cannot disambiguate /kāk^H + rī^H + dō^H/ step 1.

Architectural note: the substrate's EvalMode.le .parallel and EvalMode.le (.directional .leftToRight) both use the same LexLE on the violation vector. The parallel-vs-directional distinction therefore lives in the constraint (count vs indicator), not the EVAL mode flag. The flag remains useful for documenting intent and for the right-to-left case (which uses LexLE on the reversed vector).

Equations

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

def Phonology.Tone.starTautDock {S : Type} : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

*TAUTDOCK (paper, eq. 15, after @cite{wolf-2007}): one violation per GEN-inserted tautomorphic surface link.

Equations

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

def Phonology.Tone.ToneInMorpheme {S : Type} (f : Autosegmental.FloatingForm S) (k : Autosegmental.ToneIdx) (m : Autosegmental.MorphemeId) : Prop

The tone at index k belongs to morpheme m.

Equations

• Phonology.Tone.ToneInMorpheme f k m = (Option.map Phonology.Autosegmental.ToneSpec.morpheme f.ulTones[k]? = some m)

@[implicit_reducible]

instance Phonology.Tone.instDecidableToneInMorpheme {S : Type} (f : Autosegmental.FloatingForm S) (k : Autosegmental.ToneIdx) (m : Autosegmental.MorphemeId) : Decidable (ToneInMorpheme f k m)

Equations

• Phonology.Tone.instDecidableToneInMorpheme f k m = Phonology.Tone.instDecidableToneInMorpheme._aux_1 f k m

def Phonology.Tone.SegInMorpheme {S : Type} (f : Autosegmental.FloatingForm S) (i : Autosegmental.SegIdx) (m : Autosegmental.MorphemeId) : Prop

The TBU at index i belongs to morpheme m.

Equations

• Phonology.Tone.SegInMorpheme f i m = (Option.map Phonology.Autosegmental.SegSpec.morpheme f.segs[i]? = some m)

@[implicit_reducible]

instance Phonology.Tone.instDecidableSegInMorpheme {S : Type} (f : Autosegmental.FloatingForm S) (i : Autosegmental.SegIdx) (m : Autosegmental.MorphemeId) : Decidable (SegInMorpheme f i m)

Equations

• Phonology.Tone.instDecidableSegInMorpheme f i m = Phonology.Tone.instDecidableSegInMorpheme._aux_1 f i m

def Phonology.Tone.tonesForMorpheme {S : Type} (f : Autosegmental.FloatingForm S) (m : Autosegmental.MorphemeId) : Finset Autosegmental.ToneIdx

The set of tone indices counting toward morpheme m's tonal mass: surviving underlying tones of m, plus tones surface-linked to TBUs of m.

Equations

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

def Phonology.Tone.starCrowd {S : Type} (threshold : ℕ := 2) : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

*CROWD (paper, eq. 5, after @cite{cahill-2004}): one violation per morpheme associated with more than threshold tones. Default threshold = 2 matches the paper.

Counting includes surviving underlying tones of the morpheme PLUS surface tones from other morphemes docked onto this morpheme's TBUs. This is how the paper (p. 32) blocks rightward docking onto /rī^H/: rī already has 2 tones (M + own H), so an external H docking would make 3.

Equations

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

def Phonology.Tone.IsFallingPair (t1 t2 : Autosegmental.RegisterTier.TRN) : Prop

A tone pair (t1, t2) (in tier order) is falling iff it is HM, HL, or ML (paper, eq. 23). TRN's H, M, L are not constructors (they're defs), so we use equality rather than pattern matching.

Equations

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

@[implicit_reducible]

instance Phonology.Tone.instDecidableIsFallingPair (t1 t2 : Autosegmental.RegisterTier.TRN) : Decidable (IsFallingPair t1 t2)

Equations

• Phonology.Tone.instDecidableIsFallingPair t1 t2 = Phonology.Tone.instDecidableIsFallingPair._aux_1 t1 t2

def Phonology.Tone.HasFall : List Autosegmental.RegisterTier.TRN → Prop

A tone sequence contains a falling adjacent pair. Recursive Prop predicate; the explicit decidability instance below carries the recursion through.

Equations

• Phonology.Tone.HasFall [] = False
• Phonology.Tone.HasFall [head] = False
• Phonology.Tone.HasFall (t1 :: t2 :: rest) = (Phonology.Tone.IsFallingPair t1 t2 ∨ Phonology.Tone.HasFall (t2 :: rest))

@[implicit_reducible]

instance Phonology.Tone.decidableHasFall (ts : List Autosegmental.RegisterTier.TRN) : Decidable (HasFall ts)

Equations

• Phonology.Tone.decidableHasFall [] = isFalse not_false
• Phonology.Tone.decidableHasFall [head] = isFalse not_false
• Phonology.Tone.decidableHasFall (t1 :: t2 :: rest) = Phonology.Tone.decidableHasFall._aux_1 t1 t2 rest (Phonology.Tone.decidableHasFall (t2 :: rest))

def Phonology.Tone.starFall {S : Type} : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

*FALL (paper, eq. 23): one violation per syllable associated with a falling contour (HM, HL, ML).

A TBU is checked by extracting its surface-linked tones in tier order (via toneSequence) and scanning for falling adjacent pairs. Uses List.range + countP rather than Finset.range + filter

• card so kernel decide reduces.

Equations

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

def Phonology.Tone.starMlessL {S : Type} : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

*M<L (paper, eq. 29): one violation per M tone that immediately precedes an L tone on the tonal tier. The "tier" is the sequence of surviving (non-deleted) underlying tones in ulTones order; deletions skip positions, so adjacency is measured over the alive subsequence.

Motivates @cite{mcpherson-lamont-2026}'s account of why floating H tones can dock leftward tautomorphically before L (eq. 30): without *M<L ≫ *TAUTDOCK, an underlying /M H L/ sequence would prefer H deletion, but that yields a surface ML adjacency which *M<L penalises. Tautomorphic docking of H breaks the ML adjacency, creating an MH contour rather than M-L.

Equations

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

def Phonology.Tone.haveTone {S : Type} : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

HAVETONE (paper, eq. 17): one violation per syllable not associated to any tone.

Equations

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

def Phonology.Tone.maxTone {S : Type} (t : Autosegmental.RegisterTier.TRN) : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

MAX(T) (paper, eq. 7c): one violation per underlying tone of value t deleted by GEN.

Equations

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

def Phonology.Tone.depLinkTone {S : Type} (t : Autosegmental.RegisterTier.TRN) : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

DEP(link)/T (paper, eq. 7a): one violation per surface link inserted by GEN whose linked tone has value t.

Equations

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

def Phonology.Tone.maxLinkTone {S : Type} (t : Autosegmental.RegisterTier.TRN) : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

MAX(link)/T (paper, eq. 7b): one violation per underlying link of value t deleted by GEN.

Equations

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

def Phonology.Tone.integrityTone {S : Type} (m : Autosegmental.MorphemeId) (t : Autosegmental.RegisterTier.TRN) : Core.Constraint.OT.DirectionalConstraint (Autosegmental.FloatingForm S)

INTEGRITY (paper, @cite{mccarthy-prince-1995}; @cite{akinbo-fwangwar-2026} eq. 22c): no input tone has multiple output correspondents. In our autosegmental encoding, an "output correspondent of an input tone" is an alive ulTones entry sharing the input tone's value AND morpheme. SPREADING (one alive ulTones entry, multi-linked) → 0 violations. COPYING (multiple alive ulTones entries with same value+morpheme) → (count - 1) violations.

Parameterised by the morpheme m and tone value t whose copies are being counted (typically the verbaliser's M or H). The paper's INTEGRITY-Mᵥ is integrityTone vbzMorph .M.

Equations

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