Syllable Structure

Syllable constituency (onset–nucleus–coda), sonority scale, the Sonority Sequencing Principle, moraic weight, and OT markedness constraints.

Substance-free sonority

The sonority hierarchy is represented as an abstract ordered type (SonorityRank) rather than being defined by articulatory features. Following @cite{berent-2026}, the synchronic grammar operates on the ordering alone — the correlation with phonetic features ([±sonorant], [±approximant], etc.) is a diachronic/evolutionary fact, not a grammatical primitive. The grounding function sonorityOf maps segments to ranks via their features, but the SSP and markedness constraints see only SonorityRank.

Source: @cite{goldsmith-2011} "The Syllable" in The Handbook of Phonological Theory (Ch 6, pp. 164–196). Cross-referenced with Hayes §4.6 and §15.

@cite{goldsmith-2011} @cite{berent-2026}

inductive Phonology.Syllable.SonorityRank : Type

The abstract sonority hierarchy: what the synchronic grammar operates on.

Following @cite{berent-2026}, phonological constraints on syllable structure are substance-free — the grammar sees an ordered set of sonority categories, not the articulatory features that happen to correlate with them. The correlation is diachronic (shaped by cultural evolution and articulatory pressures), but the synchronic computation is algebraic.

Rank	Category
0	Stop
1	Fricative
2	Nasal
3	Liquid
4	Glide
5	Vowel

The 6 levels follow @cite{clements-1990}'s refinement of the basic 5-class hierarchy (splitting obstruents by [±continuant]). See NatClass.parkerSonority for the finer 8-level Parker scale.

• stop : SonorityRank
• fricative : SonorityRank
• nasal : SonorityRank
• liquid : SonorityRank
• glide : SonorityRank
• vowel : SonorityRank

@[implicit_reducible]

instance Phonology.Syllable.instDecidableEqSonorityRank : DecidableEq SonorityRank

Equations

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

def Phonology.Syllable.instReprSonorityRank.repr : SonorityRank → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Syllable.instReprSonorityRank : Repr SonorityRank

Equations

• Phonology.Syllable.instReprSonorityRank = { reprPrec := Phonology.Syllable.instReprSonorityRank.repr }

def Phonology.Syllable.SonorityRank.rank : SonorityRank → ℕ

Numeric rank (0 = least sonorous).

Equations

• Phonology.Syllable.SonorityRank.stop.rank = 0
• Phonology.Syllable.SonorityRank.fricative.rank = 1
• Phonology.Syllable.SonorityRank.nasal.rank = 2
• Phonology.Syllable.SonorityRank.liquid.rank = 3
• Phonology.Syllable.SonorityRank.glide.rank = 4
• Phonology.Syllable.SonorityRank.vowel.rank = 5

theorem Phonology.Syllable.SonorityRank.rank_injective : Function.Injective rank

SonorityRank.rank is injective: distinct ranks map to distinct Nats.

@[implicit_reducible]

instance Phonology.Syllable.SonorityRank.instLinearOrder : LinearOrder SonorityRank

Linear order on sonority ranks, lifted from the numeric ranking. Enables <, ≤, max, min on SonorityRank directly — used by SONCON and other sonority-sensitive constraints. Follows the same pattern as Stratum in Stratal.lean.

Equations

• Phonology.Syllable.SonorityRank.instLinearOrder = LinearOrder.lift' Phonology.Syllable.SonorityRank.rank Phonology.Syllable.SonorityRank.rank_injective

def Phonology.Syllable.sonorityOf (s : Segment) : SonorityRank

Substance-based grounding: classify a segment into the sonority hierarchy by its phonetic features.

Following @cite{hayes-2009}, the hierarchy is decomposed by four features ([±sonorant] > [±approximant] > [±consonantal] > [±syllabic]), with @cite{clements-1990}'s refinement splitting obstruents by [±continuant].

This function bridges phonetic substance and the abstract SonorityRank type. The SSP and other grammatical constraints operate on SonorityRank directly — they do not inspect articulatory features.

Equations

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

structure Phonology.Syllable.Syllable : Type

A syllable: onset, nucleus, coda. The rhyme (nucleus ++ coda) groups naturally in phonological processes.

• onset : List Segment
• nucleus : List Segment
• coda : List Segment

def Phonology.Syllable.Syllable.rhyme (σ : Syllable) : List Segment

The rhyme (rime): nucleus + coda.

Equations

• σ.rhyme = σ.nucleus ++ σ.coda

def Phonology.Syllable.Syllable.segments (σ : Syllable) : List Segment

All segments in linear order.

Equations

• σ.segments = σ.onset ++ σ.nucleus ++ σ.coda

def Phonology.Syllable.Syllable.hasOnset (σ : Syllable) : Bool

Equations

• σ.hasOnset = !σ.onset.isEmpty

def Phonology.Syllable.Syllable.hasCoda (σ : Syllable) : Bool

Equations

• σ.hasCoda = !σ.coda.isEmpty

def Phonology.Syllable.Syllable.isOpen (σ : Syllable) : Bool

Equations

• σ.isOpen = σ.coda.isEmpty

def Phonology.Syllable.Syllable.isClosed (σ : Syllable) : Bool

Equations

• σ.isClosed = !σ.coda.isEmpty

def Phonology.Syllable.monotoneRising : List ℕ → Bool

Is a list of Nats monotonically non-decreasing?

Equations

• Phonology.Syllable.monotoneRising [] = true
• Phonology.Syllable.monotoneRising [head] = true
• Phonology.Syllable.monotoneRising (a :: b :: rest) = (decide (a ≤ b) && Phonology.Syllable.monotoneRising (b :: rest))

def Phonology.Syllable.monotoneFalling : List ℕ → Bool

Is a list of Nats monotonically non-increasing?

Equations

• Phonology.Syllable.monotoneFalling [] = true
• Phonology.Syllable.monotoneFalling [head] = true
• Phonology.Syllable.monotoneFalling (a :: b :: rest) = (decide (a ≥ b) && Phonology.Syllable.monotoneFalling (b :: rest))

def Phonology.Syllable.Syllable.sspOnset (σ : Syllable) : Bool

Does the onset obey SSP? Sonority rises toward the nucleus.

Equations

• σ.sspOnset = Phonology.Syllable.monotoneRising (List.map (fun (s : Phonology.Segment) => (Phonology.Syllable.sonorityOf s).rank) σ.onset)

def Phonology.Syllable.Syllable.sspCoda (σ : Syllable) : Bool

Does the coda obey SSP? Sonority falls from the nucleus.

Equations

• σ.sspCoda = Phonology.Syllable.monotoneFalling (List.map (fun (s : Phonology.Segment) => (Phonology.Syllable.sonorityOf s).rank) σ.coda)

def Phonology.Syllable.Syllable.sspValid (σ : Syllable) : Bool

Full SSP: onset rises, coda falls.

Equations

• σ.sspValid = (σ.sspOnset && σ.sspCoda)

structure Phonology.Syllable.SyllabifiedForm : Type

A syllabified form: a word parsed into syllables.

• syllables : List Syllable

def Phonology.Syllable.SyllabifiedForm.segmentCount (sf : SyllabifiedForm) : ℕ

Total segment count.

Equations

• sf.segmentCount = List.foldl (fun (x1 : ℕ) (x2 : Phonology.Syllable.Syllable) => x1 + x2.segments.length) 0 sf.syllables

def Phonology.Syllable.SyllabifiedForm.allSegments (sf : SyllabifiedForm) : List Segment

All segments in linear order.

Equations

• sf.allSegments = List.flatMap Phonology.Syllable.Syllable.segments sf.syllables

structure Phonology.Syllable.SyllWeight : Type

Syllable weight: the mora count of a syllable.

Instead of a lossy 3-value enum, SyllWeight wraps the actual mora count. The conventional names .light (1μ), .heavy (2μ), .superheavy (3μ) are abbreviations for the common values.

This design ensures the prosodic pipeline is lossless: MoraicSyllable → SyllWeight → PrWd preserves exact mora counts, so bridge theorems between moraic and segmental views are trivial.

• morae : ℕ

  The mora count: 1μ = light (CV), 2μ = heavy (CVV, CVC), 3μ = superheavy (CVVC, CVCC).

def Phonology.Syllable.instDecidableEqSyllWeight.decEq (x✝ x✝¹ : SyllWeight) : Decidable (x✝ = x✝¹)

Equations

• Phonology.Syllable.instDecidableEqSyllWeight.decEq { morae := a } { morae := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phonology.Syllable.instDecidableEqSyllWeight : DecidableEq SyllWeight

Equations

• Phonology.Syllable.instDecidableEqSyllWeight = Phonology.Syllable.instDecidableEqSyllWeight.decEq

def Phonology.Syllable.instReprSyllWeight.repr : SyllWeight → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Syllable.instReprSyllWeight : Repr SyllWeight

Equations

• Phonology.Syllable.instReprSyllWeight = { reprPrec := Phonology.Syllable.instReprSyllWeight.repr }

@[reducible, inline]

abbrev Phonology.Syllable.SyllWeight.light : SyllWeight

Equations

• Phonology.Syllable.SyllWeight.light = { morae := 1 }

@[reducible, inline]

abbrev Phonology.Syllable.SyllWeight.heavy : SyllWeight

Equations

• Phonology.Syllable.SyllWeight.heavy = { morae := 2 }

@[reducible, inline]

abbrev Phonology.Syllable.SyllWeight.superheavy : SyllWeight

Equations

• Phonology.Syllable.SyllWeight.superheavy = { morae := 3 }

def Phonology.Syllable.Syllable.moraCount (σ : Syllable) (codaMoraic : Bool := true) : ℕ

Mora count. codaMoraic = true means coda consonants contribute weight (the "Weight-by-Position" parameter of @cite{hayes-1989}).

Equations

• σ.moraCount codaMoraic = σ.nucleus.length + if codaMoraic = true then σ.coda.length else 0

def Phonology.Syllable.Syllable.weight (σ : Syllable) (codaMoraic : Bool := true) : SyllWeight

Weight from mora count.

Equations

• σ.weight codaMoraic = { morae := σ.moraCount codaMoraic }

def Phonology.Syllable.onsetViolations (sf : SyllabifiedForm) : ℕ

ONSET: every syllable must have an onset. Returns count of onsetless syllables.

Equations

• Phonology.Syllable.onsetViolations sf = (List.filter (fun (σ : Phonology.Syllable.Syllable) => !σ.hasOnset) sf.syllables).length

def Phonology.Syllable.noCodaViolations (sf : SyllabifiedForm) : ℕ

NOCODA: syllables should not have codas. Returns count of syllables with codas.

Equations

• Phonology.Syllable.noCodaViolations sf = (List.filter Phonology.Syllable.Syllable.hasCoda sf.syllables).length

def Phonology.Syllable.complexOnsetViolations (sf : SyllabifiedForm) : ℕ

*COMPLEXONSET: no complex (multi-segment) onsets. Returns count of syllables with onset length > 1.

Equations

• Phonology.Syllable.complexOnsetViolations sf = (List.filter (fun (σ : Phonology.Syllable.Syllable) => decide (σ.onset.length > 1)) sf.syllables).length

def Phonology.Syllable.complexCodaViolations (sf : SyllabifiedForm) : ℕ

*COMPLEXCODA: no complex (multi-segment) codas. Returns count of syllables with coda length > 1.

Equations

• Phonology.Syllable.complexCodaViolations sf = (List.filter (fun (σ : Phonology.Syllable.Syllable) => decide (σ.coda.length > 1)) sf.syllables).length

def Phonology.Syllable.sspViolations (sf : SyllabifiedForm) : ℕ

SSP: every syllable obeys the Sonority Sequencing Principle. Returns count of syllables violating SSP.

Equations

• Phonology.Syllable.sspViolations sf = (List.filter (fun (σ : Phonology.Syllable.Syllable) => !σ.sspValid) sf.syllables).length

theorem Phonology.Syllable.monotoneRising_singleton (n : ℕ) : monotoneRising [n] = true

theorem Phonology.Syllable.monotoneFalling_singleton (n : ℕ) : monotoneFalling [n] = true

theorem Phonology.Syllable.cv_is_light (σ : Syllable) (h1 : σ.nucleus.length = 1) (h2 : σ.coda = []) : σ.weight = SyllWeight.light

theorem Phonology.Syllable.cvc_is_heavy (σ : Syllable) (h1 : σ.nucleus.length = 1) (h2 : σ.coda.length = 1) : σ.weight = SyllWeight.heavy