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 Phenomena.Tone.Studies.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

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

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instDecidableEqWordProsodicProfile : DecidableEq WordProsodicProfile

Equations

• Phenomena.Tone.Studies.Hyman2006.instDecidableEqWordProsodicProfile = Phenomena.Tone.Studies.Hyman2006.instDecidableEqWordProsodicProfile.decEq

instance Phenomena.Tone.Studies.Hyman2006.instBEqWordProsodicProfile : BEq WordProsodicProfile

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqWordProsodicProfile = { beq := Phenomena.Tone.Studies.Hyman2006.instBEqWordProsodicProfile.beq }

def Phenomena.Tone.Studies.Hyman2006.instBEqWordProsodicProfile.beq : WordProsodicProfile → WordProsodicProfile → Bool

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqWordProsodicProfile.beq { hasTone := a, hasStressAccent := a_1 } { hasTone := b, hasStressAccent := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Tone.Studies.Hyman2006.instBEqWordProsodicProfile.beq x✝¹ x✝ = false

def Phenomena.Tone.Studies.Hyman2006.instReprWordProsodicProfile.repr : WordProsodicProfile → Nat → Std.Format

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instReprWordProsodicProfile : Repr WordProsodicProfile

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprWordProsodicProfile = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprWordProsodicProfile.repr }

inductive Phenomena.Tone.Studies.Hyman2006.ProsodicQuadrant : Type

The four cells of Table I.

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

instance Phenomena.Tone.Studies.Hyman2006.instDecidableEqProsodicQuadrant : DecidableEq ProsodicQuadrant

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instBEqProsodicQuadrant : BEq ProsodicQuadrant

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqProsodicQuadrant = { beq := Phenomena.Tone.Studies.Hyman2006.instBEqProsodicQuadrant.beq }

def Phenomena.Tone.Studies.Hyman2006.instBEqProsodicQuadrant.beq : ProsodicQuadrant → ProsodicQuadrant → Bool

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqProsodicQuadrant.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Tone.Studies.Hyman2006.instReprProsodicQuadrant : Repr ProsodicQuadrant

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprProsodicQuadrant = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprProsodicQuadrant.repr }

def Phenomena.Tone.Studies.Hyman2006.instReprProsodicQuadrant.repr : ProsodicQuadrant → Nat → Std.Format

Equations

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

def Phenomena.Tone.Studies.Hyman2006.WordProsodicProfile.quadrant (p : WordProsodicProfile) : ProsodicQuadrant

Equations

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

structure Phenomena.Tone.Studies.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.

instance Phenomena.Tone.Studies.Hyman2006.instDecidableEqStressAccentCriteria : DecidableEq StressAccentCriteria

Equations

• Phenomena.Tone.Studies.Hyman2006.instDecidableEqStressAccentCriteria = Phenomena.Tone.Studies.Hyman2006.instDecidableEqStressAccentCriteria.decEq

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

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instBEqStressAccentCriteria : BEq StressAccentCriteria

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqStressAccentCriteria = { beq := Phenomena.Tone.Studies.Hyman2006.instBEqStressAccentCriteria.beq }

def Phenomena.Tone.Studies.Hyman2006.instBEqStressAccentCriteria.beq : StressAccentCriteria → StressAccentCriteria → Bool

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqStressAccentCriteria.beq { obligatoriness := a, culminativity := a_1 } { obligatoriness := b, culminativity := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Tone.Studies.Hyman2006.instBEqStressAccentCriteria.beq x✝¹ x✝ = false

def Phenomena.Tone.Studies.Hyman2006.instReprStressAccentCriteria.repr : StressAccentCriteria → Nat → Std.Format

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instReprStressAccentCriteria : Repr StressAccentCriteria

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprStressAccentCriteria = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprStressAccentCriteria.repr }

def Phenomena.Tone.Studies.Hyman2006.StressAccentCriteria.isPrototypicalSA (c : StressAccentCriteria) : Bool

A system satisfying both criteria is a prototypical SA system.

Equations

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

def Phenomena.Tone.Studies.Hyman2006.StressAccentCriteria.satisfiesOblHead (c : StressAccentCriteria) : Bool

OBLHEAD requires both obligatoriness and syllable-targeting.

Equations

• c.satisfiesOblHead = c.obligatoriness

structure Phenomena.Tone.Studies.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).

instance Phenomena.Tone.Studies.Hyman2006.instDecidableEqClusteringProperties : DecidableEq ClusteringProperties

Equations

• Phenomena.Tone.Studies.Hyman2006.instDecidableEqClusteringProperties = Phenomena.Tone.Studies.Hyman2006.instDecidableEqClusteringProperties.decEq

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

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instBEqClusteringProperties : BEq ClusteringProperties

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqClusteringProperties = { beq := Phenomena.Tone.Studies.Hyman2006.instBEqClusteringProperties.beq }

def Phenomena.Tone.Studies.Hyman2006.instBEqClusteringProperties.beq : ClusteringProperties → ClusteringProperties → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Tone.Studies.Hyman2006.instBEqClusteringProperties.beq x✝¹ x✝ = false

instance Phenomena.Tone.Studies.Hyman2006.instReprClusteringProperties : Repr ClusteringProperties

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprClusteringProperties = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprClusteringProperties.repr }

def Phenomena.Tone.Studies.Hyman2006.instReprClusteringProperties.repr : ClusteringProperties → Nat → Std.Format

Equations

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

def Phenomena.Tone.Studies.Hyman2006.prototypicalSACluster : ClusteringProperties

Prototypical SA systems exhibit all four clustering properties.

Equations

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

structure Phenomena.Tone.Studies.Hyman2006.TypologyEntry : Type

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

• name : String
• profile : WordProsodicProfile

instance Phenomena.Tone.Studies.Hyman2006.instReprTypologyEntry : Repr TypologyEntry

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprTypologyEntry = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprTypologyEntry.repr }

def Phenomena.Tone.Studies.Hyman2006.instReprTypologyEntry.repr : TypologyEntry → Nat → Std.Format

Equations

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

def Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.Hyman2006.RestrictedHToneEntry : Type

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

• name : String
• criteria : StressAccentCriteria

def Phenomena.Tone.Studies.Hyman2006.instReprRestrictedHToneEntry.repr : RestrictedHToneEntry → Nat → Std.Format

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instReprRestrictedHToneEntry : Repr RestrictedHToneEntry

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprRestrictedHToneEntry = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprRestrictedHToneEntry.repr }

def Phenomena.Tone.Studies.Hyman2006.tableII : List RestrictedHToneEntry

Table II entries.

Equations

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

theorem Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.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. ∅).

instance Phenomena.Tone.Studies.Hyman2006.instDecidableEqPALikeProperty : DecidableEq PALikeProperty

Equations

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

instance Phenomena.Tone.Studies.Hyman2006.instBEqPALikeProperty : BEq PALikeProperty

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqPALikeProperty = { beq := Phenomena.Tone.Studies.Hyman2006.instBEqPALikeProperty.beq }

def Phenomena.Tone.Studies.Hyman2006.instBEqPALikeProperty.beq : PALikeProperty → PALikeProperty → Bool

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqPALikeProperty.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Tone.Studies.Hyman2006.instReprPALikeProperty : Repr PALikeProperty

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprPALikeProperty = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprPALikeProperty.repr }

def Phenomena.Tone.Studies.Hyman2006.instReprPALikeProperty.repr : PALikeProperty → Nat → Std.Format

Equations

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

def Phenomena.Tone.Studies.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

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

def Phenomena.Tone.Studies.Hyman2006.somali : WordProsodicProfile

Equations

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

def Phenomena.Tone.Studies.Hyman2006.westernBasque : WordProsodicProfile

Equations

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

theorem Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.Hyman2006.wals13AToHasTone (t : Phonology.ToneSystem) : Bool

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

Equations

• Phenomena.Tone.Studies.Hyman2006.wals13AToHasTone Phenomena.Phonology.ToneSystem.none = false
• Phenomena.Tone.Studies.Hyman2006.wals13AToHasTone Phenomena.Phonology.ToneSystem.simple = true
• Phenomena.Tone.Studies.Hyman2006.wals13AToHasTone Phenomena.Phonology.ToneSystem.complex = true

def Phenomena.Tone.Studies.Hyman2006.wals14AToHasStress : 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

• Phenomena.Tone.Studies.Hyman2006.wals14AToHasStress x✝ = true

def Phenomena.Tone.Studies.Hyman2006.profileFromPhon (p : Phonology.PhonProfile) : WordProsodicProfile

Derive a partial word-prosodic profile from WALS data.

The stress dimension is only available when the language has a WALS F14A entry. Languages absent from F14A may or may not have stress — their profiles require independent evidence.

Equations

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

theorem Phenomena.Tone.Studies.Hyman2006.english_stress_only : (profileFromPhon Phonology.english).quadrant = ProsodicQuadrant.stressOnly

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

theorem Phenomena.Tone.Studies.Hyman2006.finnish_stress_only : (profileFromPhon Phonology.finnish).quadrant = ProsodicQuadrant.stressOnly

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

theorem Phenomena.Tone.Studies.Hyman2006.yoruba_tone_only : (profileFromPhon Phonology.yoruba).quadrant = ProsodicQuadrant.toneOnly

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

theorem Phenomena.Tone.Studies.Hyman2006.japanese_tone_only : (profileFromPhon Phonology.japanese).quadrant = ProsodicQuadrant.toneOnly

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

theorem Phenomena.Tone.Studies.Hyman2006.mandarin_tone_and_stress : (profileFromPhon Phonology.mandarin).quadrant = ProsodicQuadrant.toneAndStress

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

theorem Phenomena.Tone.Studies.Hyman2006.zulu_tone_and_stress : (profileFromPhon Phonology.zulu).quadrant = ProsodicQuadrant.toneAndStress

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

theorem Phenomena.Tone.Studies.Hyman2006.wals_covers_three_quadrants : have profiles := [Phonology.english, Phonology.german, Phonology.finnish, Phonology.turkish, Phonology.russian, Phonology.french, Phonology.spanish, Phonology.japanese, Phonology.mandarin, Phonology.hindi, Phonology.georgian, Phonology.hungarian, Phonology.swahili, Phonology.yoruba, Phonology.maori, Phonology.zulu]; (profiles.any fun (p : Phonology.PhonProfile) => (profileFromPhon p).quadrant == ProsodicQuadrant.toneAndStress) = true ∧ (profiles.any fun (p : Phonology.PhonProfile) => (profileFromPhon p).quadrant == ProsodicQuadrant.toneOnly) = true ∧ (profiles.any fun (p : Phonology.PhonProfile) => (profileFromPhon 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 Phenomena.Tone.Studies.Hyman2006.french_wals_mismatch : (profileFromPhon Phonology.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 profileFromPhon 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 Phenomena.Tone.Studies.Hyman2006.isTonalUnderHyman (wpt : Theories.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

• Phenomena.Tone.Studies.Hyman2006.isTonalUnderHyman Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType.toneBased = true
• Phenomena.Tone.Studies.Hyman2006.isTonalUnderHyman Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType.registerBased = true
• Phenomena.Tone.Studies.Hyman2006.isTonalUnderHyman Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType.mixed = true
• Phenomena.Tone.Studies.Hyman2006.isTonalUnderHyman Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType.stressAccent = false

theorem Phenomena.Tone.Studies.Hyman2006.register_based_is_tonal : isTonalUnderHyman Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType.registerBased = true

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

theorem Phenomena.Tone.Studies.Hyman2006.stress_accent_is_not_tonal : isTonalUnderHyman Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType.stressAccent = false

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

theorem Phenomena.Tone.Studies.Hyman2006.all_wpt_classified (wpt : Theories.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 Phenomena.Tone.Studies.Hyman2006.wals_coarser_than_lionnet : wals13AToHasTone Phonology.ToneSystem.simple = true ∧ wals13AToHasTone Phonology.ToneSystem.complex = true ∧ wals13AToHasTone 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 Phenomena.Tone.Studies.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

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

theorem Phenomena.Tone.Studies.Hyman2006.drubea_tone_only : drubea.quadrant = ProsodicQuadrant.toneOnly

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

theorem Phenomena.Tone.Studies.Hyman2006.drubea_same_quadrant_as_yoruba : drubea.quadrant = (profileFromPhon Phonology.yoruba).quadrant

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

theorem Phenomena.Tone.Studies.Hyman2006.drubea_no_stress : drubea.hasStressAccent = false

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

inductive Phenomena.Tone.Studies.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

instance Phenomena.Tone.Studies.Hyman2006.instDecidableEqCulminativityDomain : DecidableEq CulminativityDomain

Equations

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

def Phenomena.Tone.Studies.Hyman2006.instBEqCulminativityDomain.beq : CulminativityDomain → CulminativityDomain → Bool

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqCulminativityDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Tone.Studies.Hyman2006.instBEqCulminativityDomain : BEq CulminativityDomain

Equations

• Phenomena.Tone.Studies.Hyman2006.instBEqCulminativityDomain = { beq := Phenomena.Tone.Studies.Hyman2006.instBEqCulminativityDomain.beq }

instance Phenomena.Tone.Studies.Hyman2006.instReprCulminativityDomain : Repr CulminativityDomain

Equations

• Phenomena.Tone.Studies.Hyman2006.instReprCulminativityDomain = { reprPrec := Phenomena.Tone.Studies.Hyman2006.instReprCulminativityDomain.repr }

def Phenomena.Tone.Studies.Hyman2006.instReprCulminativityDomain.repr : CulminativityDomain → Nat → Std.Format

Equations

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

theorem Phenomena.Tone.Studies.Hyman2006.culminativity_parallel_but_distinct : CulminativityDomain.stressPerWord ≠ CulminativityDomain.registerPerStem

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

def Phenomena.Tone.Studies.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

• Phenomena.Tone.Studies.Hyman2006.isOblHeadSystem p = p.hasStressAccent

theorem Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.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 Phenomena.Tone.Studies.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.