Documentation

Linglib.Theories.Phonology.Tier

Phonological Tiers #

@cite{goldsmith-1976}

Phonology-specific tier constructors built on Core.Tier. The generic operations (apply, id, byClass, total, monoid-hom laws) live in Core/StringHom.lean; this module only adds the canonical phonological projections that downstream phonology files need.

source
def Phonology.Tier.tonal {S : Type} :
Core.Tier (Autosegmental.GrammaticalTone.TBU S) Autosegmental.RegisterTier.TRN

The canonical tonal tier (@cite{goldsmith-1976}): every TBU projects to its tone. Length-preserving (no erasure) — built via Tier.total.

Equations
Instances For
    source
    theorem Phonology.Tier.apply_tonal {S : Type} (tbus : List (Autosegmental.GrammaticalTone.TBU S)) :
    tonal.apply tbus = List.map Autosegmental.GrammaticalTone.TBU.tone tbus

    The tonal-tier projection equals the historical List.map TBU.tone formulation. Used to ground BasemapCorrespondence.tonalTier.