Prosodic Word (PrWd)

@cite{selkirk-1984}

The prosodic word (PrWd, ω) is the prosodic constituent immediately above the foot in the prosodic hierarchy:

σ < f < **ω** < φ < ι

PrWd is the domain for a cluster of phonological processes:

• Stress assignment and metrical parsing
• Vowel harmony (progressive harmony in Telugu)
• Minimal word constraints (bimoraic minimum)
• Obligatory hiatus resolution (within PrWd; optional across PrWd)

Morphosyntax-Prosody Mapping

Not all morphological elements are PrWd-internal. The mapping from morphosyntactic structure to prosodic structure determines which elements fall within the PrWd and which form their own domain:

Morphological status	PrWd membership	Example (Telugu)
Root	Internal	samudr-
Derivational suffix	Internal	(not shown)
Inflectional suffix	Internal	-am, -ni, -ki
Agreement suffix	Internal	-ni (1SG), -vi (2SG)
Postposition	External	-lō, -tō, -gurinci

This boundary is diagnosed by vowel harmony scope, minimal word effects, and obligatory vs optional hiatus resolution (@cite{aitha-2026} §3.2).

Connection to Linglib

Features.Prosody defines the prosodic hierarchy levels (σ, f, ω, φ, ι) and intonational structure. This module provides the internal structure of the prosodic word: syllable constituency, weight profiles, minimal word constraints, and the morphosyntax-prosody mapping that determines PrWd boundaries.

structure Phonology.ProsodicWord.MorphStatus : Type

Morphological status of an element relative to the prosodic word, decomposed into orthogonal Boolean axes rather than a flat enumeration of named cases. The previous inductive design with cases root | derivational | ... | clitic conflated three independent dimensions and made it impossible to add new combinations (e.g., a "free" vs. "bound" N2 in a Japanese compound, which is the moderator in @cite{breiss-katsuda-kawahara-2026}) without doubling the case enumeration.

The three axes:

• prWdInternal — is this element parsed inside the prosodic word with the stem? Empirically diagnosed by vowel-harmony scope, minimal-word effects, and hiatus-resolution obligation (@cite{aitha-2026} §3.2).
• free — can this element stand alone as a wordform? Roots and free morphemes are true; bound roots, inflectional suffixes, and most clitics are false. The Breiss N2 free-vs-bound distinction lives on this axis.
• affixal — is this element morphologically bound to a stem (vs. a separate lexical word)? Roots are false; affixes, clitics, and bound morphemes are true.

Named constructors below recover the old enum cases.

• prWdInternal : Bool
• free : Bool
• affixal : Bool

def Phonology.ProsodicWord.instDecidableEqMorphStatus.decEq (x✝ x✝¹ : MorphStatus) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phonology.ProsodicWord.instDecidableEqMorphStatus : DecidableEq MorphStatus

Equations

• Phonology.ProsodicWord.instDecidableEqMorphStatus = Phonology.ProsodicWord.instDecidableEqMorphStatus.decEq

def Phonology.ProsodicWord.instReprMorphStatus.repr : MorphStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.ProsodicWord.instReprMorphStatus : Repr MorphStatus

Equations

• Phonology.ProsodicWord.instReprMorphStatus = { reprPrec := Phonology.ProsodicWord.instReprMorphStatus.repr }

def Phonology.ProsodicWord.MorphStatus.root : MorphStatus

Root morpheme: PrWd-internal, free-standing, not affixal.

Equations

• Phonology.ProsodicWord.MorphStatus.root = { prWdInternal := true, free := true, affixal := false }

def Phonology.ProsodicWord.MorphStatus.derivational : MorphStatus

Derivational affix: PrWd-internal with the stem, bound, affixal.

Equations

• Phonology.ProsodicWord.MorphStatus.derivational = { prWdInternal := true, free := false, affixal := true }

def Phonology.ProsodicWord.MorphStatus.inflectional : MorphStatus

Inflectional affix (case, number, tense): PrWd-internal, bound.

Equations

• Phonology.ProsodicWord.MorphStatus.inflectional = { prWdInternal := true, free := false, affixal := true }

def Phonology.ProsodicWord.MorphStatus.agreement : MorphStatus

Agreement marker: PrWd-internal (crucially, for Telugu nominal predicative agreement; @cite{aitha-2026} §3.1).

Equations

• Phonology.ProsodicWord.MorphStatus.agreement = { prWdInternal := true, free := false, affixal := true }

def Phonology.ProsodicWord.MorphStatus.postposition : MorphStatus

Postposition: forms a separate PrWd. Evidence: not subject to progressive vowel harmony, obeys minimal word constraint independently, hiatus resolution across boundary is optional (@cite{aitha-2026} §3.2). Free-standing in many languages.

Equations

• Phonology.ProsodicWord.MorphStatus.postposition = { prWdInternal := false, free := true, affixal := false }

def Phonology.ProsodicWord.MorphStatus.clitic : MorphStatus

Clitic: PrWd-external boundary element; phonologically bound but syntactically not an affix.

Equations

• Phonology.ProsodicWord.MorphStatus.clitic = { prWdInternal := false, free := false, affixal := true }

def Phonology.ProsodicWord.MorphStatus.boundStem : MorphStatus

Bound free-standing morpheme that occurs only inside compounds — e.g., the "bound" N2 in Japanese compound nominals. PrWd-internal, not free, not strictly affixal (it's a stem-class member, just one that never surfaces alone).

Equations

• Phonology.ProsodicWord.MorphStatus.boundStem = { prWdInternal := true, free := false, affixal := false }

def Phonology.ProsodicWord.MorphStatus.isPrWdInternal (s : MorphStatus) : Bool

Is this morphological element parsed inside the PrWd with the stem? Direct projection of the prWdInternal axis.

Equations

• s.isPrWdInternal = s.prWdInternal

structure Phonology.ProsodicWord.PrWd : Type

A prosodic word: a sequence of syllables (by weight) that forms a single domain for stress assignment and phonological processes.

The syllables field gives the weight profile in linear order. For example, Telugu samudram 'ocean' has profile [L, L, H] (sa.mu.dram).

• syllables : List Syllable.SyllWeight

@[implicit_reducible]

instance Phonology.ProsodicWord.instDecidableEqPrWd : DecidableEq PrWd

Equations

• Phonology.ProsodicWord.instDecidableEqPrWd = Phonology.ProsodicWord.instDecidableEqPrWd.decEq

def Phonology.ProsodicWord.instDecidableEqPrWd.decEq (x✝ x✝¹ : PrWd) : Decidable (x✝ = x✝¹)

Equations

• Phonology.ProsodicWord.instDecidableEqPrWd.decEq { syllables := a } { syllables := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Phonology.ProsodicWord.instReprPrWd.repr : PrWd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.ProsodicWord.instReprPrWd : Repr PrWd

Equations

• Phonology.ProsodicWord.instReprPrWd = { reprPrec := Phonology.ProsodicWord.instReprPrWd.repr }

def Phonology.ProsodicWord.PrWd.moraCount (w : PrWd) : ℕ

Total mora count of a prosodic word.

Equations

• w.moraCount = List.foldl (fun (x1 : ℕ) (x2 : Phonology.Syllable.SyllWeight) => x1 + x2.morae) 0 w.syllables

def Phonology.ProsodicWord.PrWd.syllableCount (w : PrWd) : ℕ

Number of syllables.

Equations

• w.syllableCount = w.syllables.length

def Phonology.ProsodicWord.PrWd.satisfiesMinWord (w : PrWd) (minMorae : ℕ := 2) : Bool

Does a prosodic word satisfy the minimal word constraint?

@cite{mccarthy-prince-1993}: the smallest prosodic word must contain at least one foot, which requires at least two morae (for moraic trochee languages) or two syllables (for syllabic trochee languages).

Telugu requires a bimoraic minimum (@cite{aitha-2026} §3.2): the shortest standalone words are informal 2SG imperatives like rā 'come' (CVV = 2μ) and pō 'go' (CVV = 2μ). No word consists of a single light syllable.

Equations

• w.satisfiesMinWord minMorae = decide (w.moraCount ≥ minMorae)

structure Phonology.ProsodicWord.MorphElement : Type

A morphological element with its prosodic properties. Used to determine how it interacts with the stem's PrWd.

• form : String

  Surface form (for documentation).

• status : MorphStatus

  Morphological status (determines PrWd membership).

• initialWeight : Syllable.SyllWeight

  Weight of the initial syllable. Relevant for the Telugu weak alternation: the long form is triggered when a light initial syllable follows within the PrWd (@cite{aitha-2026} §3.2).

@[implicit_reducible]

instance Phonology.ProsodicWord.instDecidableEqMorphElement : DecidableEq MorphElement

Equations

• Phonology.ProsodicWord.instDecidableEqMorphElement = Phonology.ProsodicWord.instDecidableEqMorphElement.decEq

def Phonology.ProsodicWord.instDecidableEqMorphElement.decEq (x✝ x✝¹ : MorphElement) : Decidable (x✝ = x✝¹)

Equations

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

def Phonology.ProsodicWord.instReprMorphElement.repr : MorphElement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.ProsodicWord.instReprMorphElement : Repr MorphElement

Equations

• Phonology.ProsodicWord.instReprMorphElement = { reprPrec := Phonology.ProsodicWord.instReprMorphElement.repr }

def Phonology.ProsodicWord.MorphElement.triggersLongForm (m : MorphElement) : Bool

Does this element trigger the long stem form in Telugu weak nouns?

The long form (-āni) surfaces when the element is:

1. PrWd-internal (inflectional suffix or agreement marker), AND
2. Its initial syllable is light (CV = 1μ)

Postpositions never trigger the long form, even if they begin with a light syllable (e.g., -gurinci 'about', -eduru 'in front of'), because they are PrWd-external.

Equations

• m.triggersLongForm = (m.status.isPrWdInternal && m.initialWeight == Phonology.Syllable.SyllWeight.light)

inductive Phonology.ProsodicWord.HiatusObligation : Type

Hiatus resolution obligation: within a PrWd, hiatus resolution is obligatory; across PrWd boundaries, it is optional.

@cite{aitha-2026} §3.2: Telugu koṭṭu 'to hit' + -āli 'OBLIG' → koṭṭāli (obligatory deletion of /u/ word-internally), but kukka eduru 'in front of the dog' allows optional retention.

• obligatory : HiatusObligation
• optional : HiatusObligation

@[implicit_reducible]

instance Phonology.ProsodicWord.instDecidableEqHiatusObligation : DecidableEq HiatusObligation

Equations

• Phonology.ProsodicWord.instDecidableEqHiatusObligation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.ProsodicWord.instReprHiatusObligation : Repr HiatusObligation

Equations

• Phonology.ProsodicWord.instReprHiatusObligation = { reprPrec := Phonology.ProsodicWord.instReprHiatusObligation.repr }

def Phonology.ProsodicWord.instReprHiatusObligation.repr : HiatusObligation → ℕ → Std.Format

Equations

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

def Phonology.ProsodicWord.hiatusObligation (following : MorphStatus) : HiatusObligation

Determine hiatus resolution obligation from the morphological status of the following element.

Equations

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

theorem Phonology.ProsodicWord.root_is_internal : MorphStatus.root.isPrWdInternal = true

theorem Phonology.ProsodicWord.infl_is_internal : MorphStatus.inflectional.isPrWdInternal = true

theorem Phonology.ProsodicWord.agr_is_internal : MorphStatus.agreement.isPrWdInternal = true

theorem Phonology.ProsodicWord.postp_is_external : MorphStatus.postposition.isPrWdInternal = false

theorem Phonology.ProsodicWord.heavy_satisfies_min : { syllables := [Syllable.SyllWeight.heavy] }.satisfiesMinWord = true

A single heavy syllable (CVV or CVC) = 2μ: satisfies bimoraic min.

theorem Phonology.ProsodicWord.light_violates_min : { syllables := [Syllable.SyllWeight.light] }.satisfiesMinWord = false

A single light syllable (CV) = 1μ: violates bimoraic min.

theorem Phonology.ProsodicWord.ll_satisfies_min : { syllables := [Syllable.SyllWeight.light, Syllable.SyllWeight.light] }.satisfiesMinWord = true

Two light syllables (CV.CV) = 2μ: satisfies bimoraic min.

theorem Phonology.ProsodicWord.lo_satisfies_min : { syllables := [Syllable.SyllWeight.heavy] }.satisfiesMinWord = true

-lō 'in' (CVV = 2μ): satisfies min word as a separate PrWd.

theorem Phonology.ProsodicWord.kinda_satisfies_min : { syllables := [Syllable.SyllWeight.heavy, Syllable.SyllWeight.light] }.satisfiesMinWord = true

-kinda 'below' (CVC.CV = 3μ): satisfies min word.

theorem Phonology.ProsodicWord.infl_hiatus_obligatory : hiatusObligation MorphStatus.inflectional = HiatusObligation.obligatory

theorem Phonology.ProsodicWord.postp_hiatus_optional : hiatusObligation MorphStatus.postposition = HiatusObligation.optional

theorem Phonology.ProsodicWord.acc_ni_triggers_long : { form := "-ni", status := MorphStatus.inflectional, initialWeight := Syllable.SyllWeight.light }.triggersLongForm = true

ACC -ni: PrWd-internal, light → triggers long form.

theorem Phonology.ProsodicWord.dat_ki_triggers_long : { form := "-ki", status := MorphStatus.inflectional, initialWeight := Syllable.SyllWeight.light }.triggersLongForm = true

DAT -ki: PrWd-internal, light → triggers long form.

theorem Phonology.ProsodicWord.agr_1sg_triggers_long : { form := "-ni", status := MorphStatus.agreement, initialWeight := Syllable.SyllWeight.light }.triggersLongForm = true

1SG -ni: PrWd-internal (agreement), light → triggers long form.

theorem Phonology.ProsodicWord.postp_lo_no_long : { form := "-lō", status := MorphStatus.postposition, initialWeight := Syllable.SyllWeight.heavy }.triggersLongForm = false

P -lō 'in': PrWd-external → does NOT trigger long form.

theorem Phonology.ProsodicWord.postp_gurinci_no_long : { form := "-gurinci", status := MorphStatus.postposition, initialWeight := Syllable.SyllWeight.light }.triggersLongForm = false

P -gurinci 'about': PrWd-external → does NOT trigger long form, even though its initial syllable gu- is light.