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

Core.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.

inductive Theories.Phonology.ProsodicWord.MorphStatus : Type

The morphological status of an element relative to the prosodic word. Determines whether the element is parsed inside the PrWd with the stem or forms a separate prosodic domain.

• root : MorphStatus

  Root morpheme: always PrWd-internal.

• derivational : MorphStatus

  Derivational affix: PrWd-internal with the stem.

• inflectional : MorphStatus

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

• agreement : MorphStatus

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

• 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).

• clitic : MorphStatus

  Clitic: may be PrWd-internal or -external depending on the language and the specific clitic.

instance Theories.Phonology.ProsodicWord.instDecidableEqMorphStatus : DecidableEq MorphStatus

Equations

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

instance Theories.Phonology.ProsodicWord.instBEqMorphStatus : BEq MorphStatus

Equations

• Theories.Phonology.ProsodicWord.instBEqMorphStatus = { beq := Theories.Phonology.ProsodicWord.instBEqMorphStatus.beq }

def Theories.Phonology.ProsodicWord.instBEqMorphStatus.beq : MorphStatus → MorphStatus → Bool

Equations

• Theories.Phonology.ProsodicWord.instBEqMorphStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.ProsodicWord.instReprMorphStatus : Repr MorphStatus

Equations

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

def Theories.Phonology.ProsodicWord.instReprMorphStatus.repr : MorphStatus → Nat → Std.Format

Equations

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

def Theories.Phonology.ProsodicWord.MorphStatus.isPrWdInternal : MorphStatus → Bool

Is this morphological element parsed inside the PrWd with the stem?

The boundary between PrWd-internal and PrWd-external elements is empirically diagnosed by:

1. Vowel harmony: progressive harmony in Telugu affects only PrWd-internal suffixes, not postpositions
2. Minimal word constraint: postpositions independently satisfy the bimoraic minimum; inflectional suffixes do not
3. Hiatus resolution: obligatory within PrWd, optional across PrWd boundaries

Equations

• Theories.Phonology.ProsodicWord.MorphStatus.root.isPrWdInternal = true
• Theories.Phonology.ProsodicWord.MorphStatus.derivational.isPrWdInternal = true
• Theories.Phonology.ProsodicWord.MorphStatus.inflectional.isPrWdInternal = true
• Theories.Phonology.ProsodicWord.MorphStatus.agreement.isPrWdInternal = true
• Theories.Phonology.ProsodicWord.MorphStatus.postposition.isPrWdInternal = false
• Theories.Phonology.ProsodicWord.MorphStatus.clitic.isPrWdInternal = false

structure Theories.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

instance Theories.Phonology.ProsodicWord.instDecidableEqPrWd : DecidableEq PrWd

Equations

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

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

Equations

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

def Theories.Phonology.ProsodicWord.instBEqPrWd.beq : PrWd → PrWd → Bool

Equations

• Theories.Phonology.ProsodicWord.instBEqPrWd.beq { syllables := a } { syllables := b } = (a == b)
• Theories.Phonology.ProsodicWord.instBEqPrWd.beq x✝¹ x✝ = false

instance Theories.Phonology.ProsodicWord.instBEqPrWd : BEq PrWd

Equations

• Theories.Phonology.ProsodicWord.instBEqPrWd = { beq := Theories.Phonology.ProsodicWord.instBEqPrWd.beq }

def Theories.Phonology.ProsodicWord.instReprPrWd.repr : PrWd → Nat → Std.Format

Equations

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

instance Theories.Phonology.ProsodicWord.instReprPrWd : Repr PrWd

Equations

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

def Theories.Phonology.ProsodicWord.PrWd.moraCount (w : PrWd) : Nat

Total mora count of a prosodic word.

Equations

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

def Theories.Phonology.ProsodicWord.PrWd.syllableCount (w : PrWd) : Nat

Number of syllables.

Equations

• w.syllableCount = w.syllables.length

def Theories.Phonology.ProsodicWord.PrWd.satisfiesMinWord (w : PrWd) (minMorae : Nat := 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 Theories.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).

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

Equations

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

instance Theories.Phonology.ProsodicWord.instDecidableEqMorphElement : DecidableEq MorphElement

Equations

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

instance Theories.Phonology.ProsodicWord.instBEqMorphElement : BEq MorphElement

Equations

• Theories.Phonology.ProsodicWord.instBEqMorphElement = { beq := Theories.Phonology.ProsodicWord.instBEqMorphElement.beq }

def Theories.Phonology.ProsodicWord.instBEqMorphElement.beq : MorphElement → MorphElement → Bool

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.ProsodicWord.instBEqMorphElement.beq x✝¹ x✝ = false

instance Theories.Phonology.ProsodicWord.instReprMorphElement : Repr MorphElement

Equations

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

def Theories.Phonology.ProsodicWord.instReprMorphElement.repr : MorphElement → Nat → Std.Format

Equations

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

def Theories.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 == Theories.Phonology.Syllable.SyllWeight.light)

inductive Theories.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

instance Theories.Phonology.ProsodicWord.instDecidableEqHiatusObligation : DecidableEq HiatusObligation

Equations

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

instance Theories.Phonology.ProsodicWord.instBEqHiatusObligation : BEq HiatusObligation

Equations

• Theories.Phonology.ProsodicWord.instBEqHiatusObligation = { beq := Theories.Phonology.ProsodicWord.instBEqHiatusObligation.beq }

def Theories.Phonology.ProsodicWord.instBEqHiatusObligation.beq : HiatusObligation → HiatusObligation → Bool

Equations

• Theories.Phonology.ProsodicWord.instBEqHiatusObligation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Theories.Phonology.ProsodicWord.instReprHiatusObligation.repr : HiatusObligation → Nat → Std.Format

Equations

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

instance Theories.Phonology.ProsodicWord.instReprHiatusObligation : Repr HiatusObligation

Equations

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

def Theories.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 Theories.Phonology.ProsodicWord.root_is_internal : MorphStatus.root.isPrWdInternal = true

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Theories.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 Theories.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 Theories.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 Theories.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 Theories.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.