Hyman 2006: Word-prosodic typology

@cite{hyman-2006}

Hyman, L. M. (2006). Word-prosodic typology. Phonology 23, 225--257.

Core claims formalized

1. Two prototypes, not three: The highest-level typological cut distinguishes two prototypical word-prosodic systems — tone (T) and stress accent (SA) — not three. Pitch accent (PA) is not a coherent third type but a "pick and choose" combination of properties from both prototypes.

2. Definition of tone (def. 3): "A language with tone is one in which an indication of pitch enters into the lexical realisation of at least some morphemes." Tone is featural and paradigmatic.

3. Definition of stress accent (def. 5): "A language with stress accent is one in which there is an indication of word-level metrical structure" meeting two criteria: (a) OBLIGATORINESS — every lexical word has at least one primary stress; (b) CULMINATIVITY — every lexical word has at most one primary stress. OBLHEAD is the more important criterion.

4. 2×2 typology (Table I): Since T and SA are independent properties, languages may have both (+T+SA), either (+T−SA, −T+SA), or neither (−T−SA).

5. Non-definitional properties: Additional properties cluster with but do not define the SA prototype: privativity, subordination, demarcation, rhythmicity.

6. Table II: Restricted H-tone systems independently attest all four combinations of obligatoriness × culminativity, showing these are orthogonal.

7. OBLHEAD as the deepest cut: The most significant typological cut is between systems satisfying OBLHEAD and those that do not.

Connection to @cite{lionnet-2025}

Hyman's tone prototype encompasses all systems where pitch enters lexical realization. @cite{lionnet-2025} shows this category splits further into tone-based (paradigmatic H/L: Yoruba, Mandarin) and register-based (syntagmatic downstep: Drubea, Numèè). This enrichment is orthogonal to Hyman's SA dimension.

structure Hyman2006.WordProsodicProfile : Type

Hyman's two independent binary word-prosodic properties.

A language's word-prosodic profile is characterized by two independent Boolean dimensions, not a single categorical type. This is the key insight: T and SA can freely co-occur (Table I).

• hasTone : Bool
• hasStressAccent : Bool

@[implicit_reducible]

instance Hyman2006.instDecidableEqWordProsodicProfile : DecidableEq WordProsodicProfile

Equations

• Hyman2006.instDecidableEqWordProsodicProfile = Hyman2006.instDecidableEqWordProsodicProfile.decEq

def Hyman2006.instDecidableEqWordProsodicProfile.decEq (x✝ x✝¹ : WordProsodicProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Hyman2006.instReprWordProsodicProfile.repr : WordProsodicProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hyman2006.instReprWordProsodicProfile : Repr WordProsodicProfile

Equations

• Hyman2006.instReprWordProsodicProfile = { reprPrec := Hyman2006.instReprWordProsodicProfile.repr }

inductive Hyman2006.ProsodicQuadrant : Type

The four cells of Table I.

• toneAndStress : ProsodicQuadrant
• toneOnly : ProsodicQuadrant
• stressOnly : ProsodicQuadrant
• neither : ProsodicQuadrant

@[implicit_reducible]

instance Hyman2006.instDecidableEqProsodicQuadrant : DecidableEq ProsodicQuadrant

Equations

• Hyman2006.instDecidableEqProsodicQuadrant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hyman2006.instReprProsodicQuadrant.repr : ProsodicQuadrant → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hyman2006.instReprProsodicQuadrant : Repr ProsodicQuadrant

Equations

• Hyman2006.instReprProsodicQuadrant = { reprPrec := Hyman2006.instReprProsodicQuadrant.repr }

def Hyman2006.WordProsodicProfile.quadrant (p : WordProsodicProfile) : ProsodicQuadrant

Equations

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

structure Hyman2006.StressAccentCriteria : Type

The two central definitional criteria for stress accent (def. 5).

OBLIGATORINESS is more important: it is "an absolute universal — definitional — of a SA system" (p. 232). Culminativity may be violated in some alleged PA systems.

• obligatoriness : Bool

  (5a) Every lexical word has at least one syllable with primary stress.

• culminativity : Bool

  (5b) Every lexical word has at most one syllable with primary stress.

@[implicit_reducible]

instance Hyman2006.instDecidableEqStressAccentCriteria : DecidableEq StressAccentCriteria

Equations

• Hyman2006.instDecidableEqStressAccentCriteria = Hyman2006.instDecidableEqStressAccentCriteria.decEq

def Hyman2006.instDecidableEqStressAccentCriteria.decEq (x✝ x✝¹ : StressAccentCriteria) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Hyman2006.instReprStressAccentCriteria : Repr StressAccentCriteria

Equations

• Hyman2006.instReprStressAccentCriteria = { reprPrec := Hyman2006.instReprStressAccentCriteria.repr }

def Hyman2006.instReprStressAccentCriteria.repr : StressAccentCriteria → ℕ → Std.Format

Equations

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

def Hyman2006.StressAccentCriteria.isPrototypicalSA (c : StressAccentCriteria) : Bool

A system satisfying both criteria is a prototypical SA system.

Equations

• c.isPrototypicalSA = (c.obligatoriness && c.culminativity)

def Hyman2006.StressAccentCriteria.satisfiesOblHead (c : StressAccentCriteria) : Bool

OBLHEAD requires both obligatoriness and syllable-targeting.

Equations

• c.satisfiesOblHead = c.obligatoriness

structure Hyman2006.ClusteringProperties : Type

Additional properties that cluster with the SA and T prototypes but are not definitional.

SA-clustering properties include privativity, subordination, demarcation, and rhythmicity. T-clustering properties include being paradigmatic and identifying TBU tones.

• privativity : Bool

  Privativity: stress is present vs. absent, not graded (p. 234).

• subordination : Bool

  Subordination: one stress may be subordinated to another (p. 234).

• demarcation : Bool

  Demarcation: stress fixed on initial/final/etc. signals word boundary (p. 234).

• rhythmicity : Bool

  Rhythmicity: echo-stresses occur on every other syllable (p. 234).

@[implicit_reducible]

instance Hyman2006.instDecidableEqClusteringProperties : DecidableEq ClusteringProperties

Equations

• Hyman2006.instDecidableEqClusteringProperties = Hyman2006.instDecidableEqClusteringProperties.decEq

def Hyman2006.instDecidableEqClusteringProperties.decEq (x✝ x✝¹ : ClusteringProperties) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Hyman2006.instReprClusteringProperties : Repr ClusteringProperties

Equations

• Hyman2006.instReprClusteringProperties = { reprPrec := Hyman2006.instReprClusteringProperties.repr }

def Hyman2006.instReprClusteringProperties.repr : ClusteringProperties → ℕ → Std.Format

Equations

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

def Hyman2006.prototypicalSACluster : ClusteringProperties

Prototypical SA systems exhibit all four clustering properties.

Equations

• Hyman2006.prototypicalSACluster = { privativity := true, subordination := true, demarcation := true, rhythmicity := true }

structure Hyman2006.TypologyEntry : Type

Language entry for the 2×2 typology (Table I, p. 237).

• name : String
• profile : WordProsodicProfile

@[implicit_reducible]

instance Hyman2006.instReprTypologyEntry : Repr TypologyEntry

Equations

• Hyman2006.instReprTypologyEntry = { reprPrec := Hyman2006.instReprTypologyEntry.repr }

def Hyman2006.instReprTypologyEntry.repr : TypologyEntry → ℕ → Std.Format

Equations

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

def Hyman2006.tableI : List TypologyEntry

Table I entries: representative languages for each quadrant.

Equations

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

theorem Hyman2006.all_quadrants_attested : (tableI.any fun (e : TypologyEntry) => e.profile.quadrant == ProsodicQuadrant.toneAndStress) = true ∧ (tableI.any fun (e : TypologyEntry) => e.profile.quadrant == ProsodicQuadrant.toneOnly) = true ∧ (tableI.any fun (e : TypologyEntry) => e.profile.quadrant == ProsodicQuadrant.stressOnly) = true ∧ (tableI.any fun (e : TypologyEntry) => e.profile.quadrant == ProsodicQuadrant.neither) = true

All four quadrants are attested in Table I.

structure Hyman2006.RestrictedHToneEntry : Type

Table II (p. 245): restricted H-tone systems attest all four combinations of obligatoriness and culminativity.

• name : String
• criteria : StressAccentCriteria

@[implicit_reducible]

instance Hyman2006.instReprRestrictedHToneEntry : Repr RestrictedHToneEntry

Equations

• Hyman2006.instReprRestrictedHToneEntry = { reprPrec := Hyman2006.instReprRestrictedHToneEntry.repr }

def Hyman2006.instReprRestrictedHToneEntry.repr : RestrictedHToneEntry → ℕ → Std.Format

Equations

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

def Hyman2006.tableII : List RestrictedHToneEntry

Table II entries.

Equations

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

theorem Hyman2006.all_oblig_culm_combos : (tableII.any fun (e : RestrictedHToneEntry) => e.criteria.obligatoriness && e.criteria.culminativity) = true ∧ (tableII.any fun (e : RestrictedHToneEntry) => e.criteria.obligatoriness && !e.criteria.culminativity) = true ∧ (tableII.any fun (e : RestrictedHToneEntry) => !e.criteria.obligatoriness && e.criteria.culminativity) = true ∧ (tableII.any fun (e : RestrictedHToneEntry) => !e.criteria.obligatoriness && !e.criteria.culminativity) = true

All four combinations of obligatoriness × culminativity are attested.

theorem Hyman2006.only_kinga_prototypical_sa : (List.filter (fun (e : RestrictedHToneEntry) => e.criteria.isPrototypicalSA) tableII).length = 1

Only Kinga satisfies both definitional criteria for SA.

inductive Hyman2006.PALikeProperty : Type

"PA-like" properties (13): three distinct things that have been called pitch accent. These do not cohere into a single prototype.

• abstractDifferent : PALikeProperty

  (13a) Underlying prosody abstractly different from surface realisations.

• combinesToneAndStress : PALikeProperty

  (13b) System combines tone and stress.

• restrictedTone : PALikeProperty

  (13c) Restricted, sparse, or privative tone (e.g., /H/ vs. ∅).

@[implicit_reducible]

instance Hyman2006.instDecidableEqPALikeProperty : DecidableEq PALikeProperty

Equations

• Hyman2006.instDecidableEqPALikeProperty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hyman2006.instReprPALikeProperty : Repr PALikeProperty

Equations

• Hyman2006.instReprPALikeProperty = { reprPrec := Hyman2006.instReprPALikeProperty.repr }

def Hyman2006.instReprPALikeProperty.repr : PALikeProperty → ℕ → Std.Format

Equations

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

def Hyman2006.tokyoJapanese : WordProsodicProfile

Hyman's key argument: languages called "PA" freely pick and choose between these properties. No single definition of PA can be given that parallels the definitions for T (3) and SA (5).

The claim is that PA reduces to T (since pitch enters lexical realization), with additional SA-like properties possibly co-occurring. Hyman reclassifies Tokyo Japanese, Somali, and Western Basque as [+T, −SA] — i.e., tonal.

Equations

• Hyman2006.tokyoJapanese = { hasTone := true, hasStressAccent := false }

def Hyman2006.somali : WordProsodicProfile

Equations

• Hyman2006.somali = { hasTone := true, hasStressAccent := false }

def Hyman2006.westernBasque : WordProsodicProfile

Equations

• Hyman2006.westernBasque = { hasTone := true, hasStressAccent := false }

theorem Hyman2006.pa_languages_are_tonal : tokyoJapanese.quadrant = ProsodicQuadrant.toneOnly ∧ somali.quadrant = ProsodicQuadrant.toneOnly ∧ westernBasque.quadrant = ProsodicQuadrant.toneOnly

All three classic "PA" languages are reclassified as +T, −SA.

def Hyman2006.wals13AToHasTone (t : Typology.Phonology.ToneSystem) : Bool

WALS F13A maps onto Hyman's binary tone dimension: noTones → −T; simpleToneSystem/complexToneSystem → +T.

Equations

• Hyman2006.wals13AToHasTone Typology.Phonology.ToneSystem.none = false
• Hyman2006.wals13AToHasTone Typology.Phonology.ToneSystem.simple = true
• Hyman2006.wals13AToHasTone Typology.Phonology.ToneSystem.complex = true

def Hyman2006.wals14AToHasStress : Typology.Phonology.StressLocation → Bool

WALS F14A maps onto Hyman's binary stress dimension: noFixed (free stress) → +SA; fixed locations → +SA; absence from WALS survey → indeterminate.

Note: WALS F14A only classifies fixed stress location. Free stress languages (English, Russian) appear as noFixed, which still indicates +SA. The −SA case (Bella Coola, French) is not directly captured by WALS F14A.

Equations

• Hyman2006.wals14AToHasStress x✝ = true

def Hyman2006.wpProfile (t : Typology.Phonology.ToneSystem) (s : Option Typology.Phonology.StressLocation) : WordProsodicProfile

Construct a WordProsodicProfile directly from WALS F13A tone + optional F14A stress coding. Replaces a former PhonProfile → WordProsodicProfile indirection where PhonProfile carried 14 fields Hyman2006 never read. The 16 language defs below construct their WordProsodicProfile values via this helper, keeping the WALS-encoding visible at the call site.

Equations

• Hyman2006.wpProfile t (some sloc) = { hasTone := Hyman2006.wals13AToHasTone t, hasStressAccent := Hyman2006.wals14AToHasStress sloc }
• Hyman2006.wpProfile t none = { hasTone := Hyman2006.wals13AToHasTone t, hasStressAccent := false }

Per-language sample (16 languages from a former Phenomena/Phonology/Typology.lean PhonProfile block). Each wpProfile argument pair is the language's WALS F13A coding (Hyman's +T/−T) and WALS F14A coding (Hyman's +SA/−SA). The none stress cases correspond to "WALS F14A does not survey this language" — NOT "language has no stress" — see french_wals_mismatch for an example of why this distinction matters.

def Hyman2006.english : WordProsodicProfile

Equations

• Hyman2006.english = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.noFixed)

def Hyman2006.german : WordProsodicProfile

Equations

• Hyman2006.german = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.noFixed)

def Hyman2006.finnish : WordProsodicProfile

Equations

• Hyman2006.finnish = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.initial)

def Hyman2006.turkish : WordProsodicProfile

Equations

• Hyman2006.turkish = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.ultimate)

def Hyman2006.russian : WordProsodicProfile

Equations

• Hyman2006.russian = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.noFixed)

def Hyman2006.french : WordProsodicProfile

Equations

• Hyman2006.french = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.noFixed)

def Hyman2006.spanish : WordProsodicProfile

Equations

• Hyman2006.spanish = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.penultimate)

def Hyman2006.japanese : WordProsodicProfile

Equations

• Hyman2006.japanese = Hyman2006.wpProfile Typology.Phonology.ToneSystem.simple none

def Hyman2006.mandarin : WordProsodicProfile

Equations

• Hyman2006.mandarin = Hyman2006.wpProfile Typology.Phonology.ToneSystem.complex (some Typology.Phonology.StressLocation.noFixed)

def Hyman2006.hindi : WordProsodicProfile

Equations

• Hyman2006.hindi = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.noFixed)

def Hyman2006.georgian : WordProsodicProfile

Equations

• Hyman2006.georgian = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.initial)

def Hyman2006.hungarian : WordProsodicProfile

Equations

• Hyman2006.hungarian = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.initial)

def Hyman2006.swahili : WordProsodicProfile

Equations

• Hyman2006.swahili = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.penultimate)

def Hyman2006.yoruba : WordProsodicProfile

Equations

• Hyman2006.yoruba = Hyman2006.wpProfile Typology.Phonology.ToneSystem.complex none

def Hyman2006.maori : WordProsodicProfile

Equations

• Hyman2006.maori = Hyman2006.wpProfile Typology.Phonology.ToneSystem.none (some Typology.Phonology.StressLocation.initial)

def Hyman2006.zulu : WordProsodicProfile

Equations

• Hyman2006.zulu = Hyman2006.wpProfile Typology.Phonology.ToneSystem.simple (some Typology.Phonology.StressLocation.penultimate)

theorem Hyman2006.english_stress_only : english.quadrant = ProsodicQuadrant.stressOnly

English: −tone (WALS none), +stress (WALS noFixed = free stress).

theorem Hyman2006.finnish_stress_only : finnish.quadrant = ProsodicQuadrant.stressOnly

Finnish: −tone, +stress (WALS initial = fixed stress).

theorem Hyman2006.yoruba_tone_only : yoruba.quadrant = ProsodicQuadrant.toneOnly

Yoruba: +tone (WALS complex), −stress (absent from WALS F14A).

theorem Hyman2006.japanese_tone_only : japanese.quadrant = ProsodicQuadrant.toneOnly

Japanese: +tone (WALS simple), −stress (absent from WALS F14A).

theorem Hyman2006.mandarin_tone_and_stress : mandarin.quadrant = ProsodicQuadrant.toneAndStress

Mandarin: +tone (WALS complex), +stress (WALS noFixed).

theorem Hyman2006.zulu_tone_and_stress : zulu.quadrant = ProsodicQuadrant.toneAndStress

Zulu: +tone (WALS simple), +stress (WALS penultimate).

theorem Hyman2006.wals_covers_three_quadrants : have profiles := [english, german, finnish, turkish, russian, french, spanish, japanese, mandarin, hindi, georgian, hungarian, swahili, yoruba, maori, zulu]; (profiles.any fun (p : WordProsodicProfile) => p.quadrant == ProsodicQuadrant.toneAndStress) = true ∧ (profiles.any fun (p : WordProsodicProfile) => p.quadrant == ProsodicQuadrant.toneOnly) = true ∧ (profiles.any fun (p : WordProsodicProfile) => p.quadrant == ProsodicQuadrant.stressOnly) = true

Three of the four quadrants are attested among the 16 PhonProfile languages. The −T−SA quadrant is NOT attested because WALS F14A encodes stress location but not stress absence: languages like French appear as noFixed (= free stress = +SA), even though Hyman classifies French as −SA.

This demonstrates the inherent limitation of deriving Hyman's framework from WALS data alone.

theorem Hyman2006.french_wals_mismatch : french.quadrant = ProsodicQuadrant.stressOnly ∧ ((List.filter (fun (e : TypologyEntry) => e.name == "French") tableI).all fun (e : TypologyEntry) => e.profile.quadrant == ProsodicQuadrant.neither) = true

French is classified as −T−SA in Hyman's Table I, but WALS F14A records it with noFixed stress (= free stress), which our profileFromWPSample maps to +SA. This mismatch arises because WALS F14A does not distinguish "free word stress" (English) from "no word stress" (French — stress is phrase-final, not word-level).

This is not a bug in the formalization but a documented limitation of the WALS→Hyman bridge. The −SA classification requires language-specific analysis beyond WALS data.

def Hyman2006.isTonalUnderHyman (wpt : Phonology.Autosegmental.RegisterTier.WordProsodicType) : Bool

Whether a WordProsodicType counts as tonal under Hyman's definition (3): "an indication of pitch enters into the lexical realisation of at least some morphemes."

@cite{lionnet-2025} enriches Hyman's tone prototype by splitting it into tone-based (paradigmatic H/L) and register-based (syntagmatic h/l). Both sub-types satisfy definition (3).

Equations

• Hyman2006.isTonalUnderHyman Phonology.Autosegmental.RegisterTier.WordProsodicType.toneBased = true
• Hyman2006.isTonalUnderHyman Phonology.Autosegmental.RegisterTier.WordProsodicType.registerBased = true
• Hyman2006.isTonalUnderHyman Phonology.Autosegmental.RegisterTier.WordProsodicType.mixed = true
• Hyman2006.isTonalUnderHyman Phonology.Autosegmental.RegisterTier.WordProsodicType.stressAccent = false

theorem Hyman2006.register_based_is_tonal : isTonalUnderHyman Phonology.Autosegmental.RegisterTier.WordProsodicType.registerBased = true

Both tone-based and register-based systems count as +tone under Hyman's definition (3).

theorem Hyman2006.stress_accent_is_not_tonal : isTonalUnderHyman Phonology.Autosegmental.RegisterTier.WordProsodicType.stressAccent = false

Stress accent systems are −tone under Hyman's definition.

theorem Hyman2006.all_wpt_classified (wpt : Phonology.Autosegmental.RegisterTier.WordProsodicType) : isTonalUnderHyman wpt = true ∨ isTonalUnderHyman wpt = false

All four WordProsodicType values from @cite{lionnet-2025} map consistently to Hyman's binary +/−tone.

theorem Hyman2006.wals_coarser_than_lionnet : wals13AToHasTone Typology.Phonology.ToneSystem.simple = true ∧ wals13AToHasTone Typology.Phonology.ToneSystem.complex = true ∧ wals13AToHasTone Typology.Phonology.ToneSystem.none = false

The WALS 3-way tone classification (F13A) does not capture the tone-based vs. register-based distinction. Both Yoruba (tone-based) and Drubea (register-based) would be classified as "simple" or "complex" in WALS, losing the syntagmatic vs. paradigmatic distinction that @cite{lionnet-2025} identifies.

def Hyman2006.drubea : WordProsodicProfile

Drubea's word-prosodic profile under Hyman's framework: +T, −SA.

+T: register features (downstep) enter lexical realization — the minimal pairs in @cite{lionnet-2025} ex. 4 demonstrate this directly. −SA: no obligatory metrical head; the prosodic system is purely register-based with no stress accent.

This places Drubea in the same quadrant as Yoruba, Igbo, and the reclassified "PA" languages (Tokyo Japanese, Somali).

Equations

• Hyman2006.drubea = { hasTone := true, hasStressAccent := false }

theorem Hyman2006.drubea_tone_only : drubea.quadrant = ProsodicQuadrant.toneOnly

Drubea is in the +T−SA quadrant (tone only).

theorem Hyman2006.drubea_same_quadrant_as_yoruba : drubea.quadrant = yoruba.quadrant

Drubea's profile is consistent with Yoruba's (both +T, −SA from different sub-types of tone).

theorem Hyman2006.drubea_no_stress : drubea.hasStressAccent = false

Drubea lacks stress accent — it is not an OBLHEAD system.

inductive Hyman2006.CulminativityDomain : Type

Hyman's stress culminativity (5b) and Drubea's register culminativity (@cite{lionnet-2025}) share the name but apply to different domains:

• Stress culminativity (Hyman): at most one primary stress per word. Definitional for SA systems. Violated in some alleged PA systems (Creek, Seneca — Table II).
• Register culminativity (Lionnet): at most one l feature per native stem. A distributional constraint on register features, not a metrical property.

Both are "at most one X per domain" constraints, but the X differs (metrical prominence vs. register feature) and the domain differs (word vs. stem).

• stressPerWord : CulminativityDomain
• registerPerStem : CulminativityDomain

@[implicit_reducible]

instance Hyman2006.instDecidableEqCulminativityDomain : DecidableEq CulminativityDomain

Equations

• Hyman2006.instDecidableEqCulminativityDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hyman2006.instReprCulminativityDomain.repr : CulminativityDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hyman2006.instReprCulminativityDomain : Repr CulminativityDomain

Equations

• Hyman2006.instReprCulminativityDomain = { reprPrec := Hyman2006.instReprCulminativityDomain.repr }

theorem Hyman2006.culminativity_parallel_but_distinct : CulminativityDomain.stressPerWord ≠ CulminativityDomain.registerPerStem

The two culminativity constraints are formally parallel but apply to different phonological objects.

theorem Hyman2006.culminativity_orthogonal_to_dominance : CulminativityDomain.stressPerWord ≠ CulminativityDomain.registerPerStem → True

Culminativity (distributional: at most one X per domain) is orthogonal to prosodic dominance (Features.Prosody.ProsodicDominance, interactional: does a morpheme override the prosodic specification of its base?).

A system can be culminative — at most one accent per prosodic word — while having both dominant and recessive morphemes. Japanese exemplifies this: pitch accent is culminative (one accent per AP), yet deaccenting suffixes like -teki are dominant while -si 'Mr.' is recessive (@cite{kawahara-2015}).

def Hyman2006.isOblHeadSystem (p : WordProsodicProfile) : Bool

Hyman's final proposal (§7): the most significant typological cut is OBLHEAD — whether every word obligatorily has a metrical head.

OBLHEAD = OBLIGATORINESS: every lexical word has at least one syllable marked for the highest degree of metrical prominence. This is the unique defining property of SA systems.

Systems satisfying OBLHEAD are SA (possibly with co-occurring T). Systems not satisfying OBLHEAD include tone-only systems and −T−SA systems (e.g., Bella Coola, which lacks syllables and therefore cannot have OBLHEAD).

Equations

• Hyman2006.isOblHeadSystem p = p.hasStressAccent

theorem Hyman2006.oblhead_separates : isOblHeadSystem { hasTone := true, hasStressAccent := true } = true ∧ isOblHeadSystem { hasTone := false, hasStressAccent := true } = true ∧ isOblHeadSystem { hasTone := true, hasStressAccent := false } = false ∧ isOblHeadSystem { hasTone := false, hasStressAccent := false } = false

OBLHEAD separates SA (±T) from non-SA systems.

theorem Hyman2006.oblhead_partitions_tableI : (List.filter (fun (e : TypologyEntry) => isOblHeadSystem e.profile) tableI).length = 10 ∧ (List.filter (fun (e : TypologyEntry) => !isOblHeadSystem e.profile) tableI).length = 8

OBLHEAD partitions Table I: languages with +SA are OBLHEAD systems, regardless of whether they also have tone.

theorem Hyman2006.no_stress_implies_no_oblhead : (tableI.all fun (e : TypologyEntry) => e.profile.hasStressAccent || !isOblHeadSystem e.profile) = true

Every Table I language with −SA also has −OBLHEAD.