Register Tier Theory

@cite{snider-1999} @cite{snider-2020}

Register features as independent phonological primitives, following Snider's (1999, 2020) Register Tier Theory. Register features are syntagmatic: they effect a pitch shift relative to the preceding context, unlike paradigmatic tone features which specify absolute pitch targets within a register.

Geometry of tone (Snider 2020)

    h / l     Register tier
    H / L     Tonal tier
      ○       Tonal root node (TRN)
      |
     TBU      Tone-bearing unit

The TRN bundles register and tone features. In register-only systems like Drubea and Numèè (@cite{lionnet-2025}), the tonal tier is absent and the system is fully described by register features alone.

Key distinction

• Tone-based systems: tonal contrasts defined paradigmatically (H is higher than L in the same context)
• Register-based systems: tonal contrasts defined syntagmatically (a downstepped unit is lower than the preceding unit)

This distinction enriches @cite{hyman-2006}'s word-prosodic typology.

inductive Theories.Phonology.Autosegmental.RegisterTier.RegisterFeature : Type

Register features (@cite{snider-1999}, @cite{snider-2020}).

Syntagmatically defined: each feature effects a register shift relative to the preceding register setting.

• h: raise register (upstep) — higher than preceding
• l: lower register (downstep) — lower than preceding

• h : RegisterFeature
• l : RegisterFeature

instance Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqRegisterFeature : DecidableEq RegisterFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqRegisterFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Phonology.Autosegmental.RegisterTier.instBEqRegisterFeature : BEq RegisterFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqRegisterFeature = { beq := Theories.Phonology.Autosegmental.RegisterTier.instBEqRegisterFeature.beq }

def Theories.Phonology.Autosegmental.RegisterTier.instBEqRegisterFeature.beq : RegisterFeature → RegisterFeature → Bool

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqRegisterFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.Autosegmental.RegisterTier.instReprRegisterFeature : Repr RegisterFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprRegisterFeature = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprRegisterFeature.repr }

def Theories.Phonology.Autosegmental.RegisterTier.instReprRegisterFeature.repr : RegisterFeature → Nat → Std.Format

Equations

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

def Theories.Phonology.Autosegmental.RegisterTier.instInhabitedRegisterFeature.default : RegisterFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instInhabitedRegisterFeature.default = Theories.Phonology.Autosegmental.RegisterTier.RegisterFeature.h

instance Theories.Phonology.Autosegmental.RegisterTier.instInhabitedRegisterFeature : Inhabited RegisterFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instInhabitedRegisterFeature = { default := Theories.Phonology.Autosegmental.RegisterTier.instInhabitedRegisterFeature.default }

inductive Theories.Phonology.Autosegmental.RegisterTier.ToneFeature : Type

Tone features (@cite{yip-1980}, @cite{clements-1981}).

Paradigmatically defined: specify a pitch target within the current register setting.

• H: high pitch target (upper half of register)
• L: low pitch target (lower half of register)

• H : ToneFeature
• L : ToneFeature

instance Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqToneFeature : DecidableEq ToneFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqToneFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Phonology.Autosegmental.RegisterTier.instBEqToneFeature.beq : ToneFeature → ToneFeature → Bool

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqToneFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.Autosegmental.RegisterTier.instBEqToneFeature : BEq ToneFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqToneFeature = { beq := Theories.Phonology.Autosegmental.RegisterTier.instBEqToneFeature.beq }

def Theories.Phonology.Autosegmental.RegisterTier.instReprToneFeature.repr : ToneFeature → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instReprToneFeature : Repr ToneFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprToneFeature = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprToneFeature.repr }

def Theories.Phonology.Autosegmental.RegisterTier.instInhabitedToneFeature.default : ToneFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instInhabitedToneFeature.default = Theories.Phonology.Autosegmental.RegisterTier.ToneFeature.H

instance Theories.Phonology.Autosegmental.RegisterTier.instInhabitedToneFeature : Inhabited ToneFeature

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instInhabitedToneFeature = { default := Theories.Phonology.Autosegmental.RegisterTier.instInhabitedToneFeature.default }

structure Theories.Phonology.Autosegmental.RegisterTier.TonalRootNode : Type

Tonal root node (TRN): bundles register and tone features into a single prosodic specification (@cite{snider-2020}: 23).

Standard tones decompose as register + tone:

• High = Hh (high tone, raised register)
• Low = Ll (low tone, lowered register)
• Mid = Lh or Hl
• Downstepped High = Hl

Register-only systems (Drubea/Numèè) use tone = none.

• register : Option RegisterFeature
• tone : Option ToneFeature

instance Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqTonalRootNode : DecidableEq TonalRootNode

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqTonalRootNode = Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqTonalRootNode.decEq

def Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqTonalRootNode.decEq (x✝ x✝¹ : TonalRootNode) : Decidable (x✝ = x✝¹)

Equations

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

def Theories.Phonology.Autosegmental.RegisterTier.instBEqTonalRootNode.beq : TonalRootNode → TonalRootNode → Bool

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqTonalRootNode.beq { register := a, tone := a_1 } { register := b, tone := b_1 } = (a == b && a_1 == b_1)
• Theories.Phonology.Autosegmental.RegisterTier.instBEqTonalRootNode.beq x✝¹ x✝ = false

instance Theories.Phonology.Autosegmental.RegisterTier.instBEqTonalRootNode : BEq TonalRootNode

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqTonalRootNode = { beq := Theories.Phonology.Autosegmental.RegisterTier.instBEqTonalRootNode.beq }

def Theories.Phonology.Autosegmental.RegisterTier.instReprTonalRootNode.repr : TonalRootNode → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instReprTonalRootNode : Repr TonalRootNode

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprTonalRootNode = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprTonalRootNode.repr }

inductive Theories.Phonology.Autosegmental.RegisterTier.TBUKind : Type

The prosodic domain that carries register/tone specifications.

In most tone languages this is the syllable; in Drubea and Numèè it is the mora (@cite{lionnet-2025} §4.2).

• mora : TBUKind
• syllable : TBUKind

instance Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqTBUKind : DecidableEq TBUKind

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqTBUKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Theories.Phonology.Autosegmental.RegisterTier.instBEqTBUKind : BEq TBUKind

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqTBUKind = { beq := Theories.Phonology.Autosegmental.RegisterTier.instBEqTBUKind.beq }

def Theories.Phonology.Autosegmental.RegisterTier.instBEqTBUKind.beq : TBUKind → TBUKind → Bool

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqTBUKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Theories.Phonology.Autosegmental.RegisterTier.instReprTBUKind.repr : TBUKind → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instReprTBUKind : Repr TBUKind

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprTBUKind = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprTBUKind.repr }

@[reducible, inline]

abbrev Theories.Phonology.Autosegmental.RegisterTier.RegisterSpec : Type

Register specification on a single register-bearing unit (RBU). none = registerless (prosodically unspecified).

Equations

• Theories.Phonology.Autosegmental.RegisterTier.RegisterSpec = Option Theories.Phonology.Autosegmental.RegisterTier.RegisterFeature

def Theories.Phonology.Autosegmental.RegisterTier.realizePitch : Nat → List RegisterSpec → List Nat

Realize a sequence of register specifications as pitch levels.

Models terracing: starting from a baseline pitch level, each l lowers by one step and each h raises by one step. Registerless units maintain the current level.

This captures the staircase-descent seen in utterances with multiple downsteps (@cite{lionnet-2025}: ex. 11, 12, Figure 7).

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Autosegmental.RegisterTier.realizePitch x✝ [] = []
• Theories.Phonology.Autosegmental.RegisterTier.realizePitch x✝ (none :: rest) = x✝ :: Theories.Phonology.Autosegmental.RegisterTier.realizePitch x✝ rest

def Theories.Phonology.Autosegmental.RegisterTier.uttInitialNeutralize : List RegisterSpec → List RegisterSpec

Utterance-initial neutralization: an l feature on the first RBU is not phonetically realized (no preceding register to contrast with), but remains phonologically active (@cite{lionnet-2025} §3.5, §4.5).

Equations

• Theories.Phonology.Autosegmental.RegisterTier.uttInitialNeutralize (some Theories.Phonology.Autosegmental.RegisterTier.RegisterFeature.l :: rest) = none :: rest
• Theories.Phonology.Autosegmental.RegisterTier.uttInitialNeutralize x✝ = x✝

def Theories.Phonology.Autosegmental.RegisterTier.isCulminative (specs : List RegisterSpec) : Bool

Culminativity: a stem contains at most one l feature.

This constraint holds for all native Drubea and Numèè stems (@cite{lionnet-2025} §3.10, Table 2).

Equations

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

def Theories.Phonology.Autosegmental.RegisterTier.hEpenthesis : List RegisterSpec → List RegisterSpec

Pre-downstep h-epenthesis (@cite{lionnet-2025} §4.4): insert an h feature on the registerless RBU immediately before a downstep.

This raises the pitch of the preceding syllable, reinforcing the downward contrast. The operation is postlexical and optional.

This models the abrupt raising pattern (the most common case). For the gradual pattern where raising extends over multiple registerless RBUs, see hEpenthesisSpread.

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Autosegmental.RegisterTier.hEpenthesis [] = []
• Theories.Phonology.Autosegmental.RegisterTier.hEpenthesis [x_1] = [x_1]
• Theories.Phonology.Autosegmental.RegisterTier.hEpenthesis (x_1 :: rest) = x_1 :: Theories.Phonology.Autosegmental.RegisterTier.hEpenthesis rest

def Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread (specs : List RegisterSpec) : List RegisterSpec

Spreading h-epenthesis: raise ALL registerless RBUs in the sequence preceding a downstep, not just the immediately preceding one.

This models the spreading pattern described in @cite{lionnet-2025} §3.2 (ex. 16), where pitch raising "extends through a sequence of registerless syllables" before a downstep.

Equations

• Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread specs = Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread.mark specs

def Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread.mark : List RegisterSpec → List RegisterSpec

Equations

• One or more equations did not get rendered due to their size.
• Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread.mark [] = []
• Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread.mark (x_1 :: rest) = x_1 :: Theories.Phonology.Autosegmental.RegisterTier.hEpenthesisSpread.mark rest

inductive Theories.Phonology.Autosegmental.RegisterTier.WordProsodicType : Type

Word-prosodic system types (@cite{hyman-2006}, enriched by @cite{lionnet-2025} §6.2).

Hyman (2006) defines two prototypical systems: tone and stress accent. Lionnet (2025) shows that tone systems split into tone-based (paradigmatic) and register-based (syntagmatic).

• toneBased : WordProsodicType
• registerBased : WordProsodicType
• stressAccent : WordProsodicType
• mixed : WordProsodicType

instance Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqWordProsodicType : DecidableEq WordProsodicType

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqWordProsodicType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Phonology.Autosegmental.RegisterTier.instBEqWordProsodicType.beq : WordProsodicType → WordProsodicType → Bool

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqWordProsodicType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Theories.Phonology.Autosegmental.RegisterTier.instBEqWordProsodicType : BEq WordProsodicType

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqWordProsodicType = { beq := Theories.Phonology.Autosegmental.RegisterTier.instBEqWordProsodicType.beq }

def Theories.Phonology.Autosegmental.RegisterTier.instReprWordProsodicType.repr : WordProsodicType → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instReprWordProsodicType : Repr WordProsodicType

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprWordProsodicType = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprWordProsodicType.repr }

structure Theories.Phonology.Autosegmental.RegisterTier.DownstepProperties : Type

Core definitional properties of downstep, following @cite{leben-2018} as refined by @cite{lionnet-2025} §6.1.

Properties (a–c) are definitional; (d–f) are cross-linguistic tendencies that need not hold in every system.

• affectsDomain : Bool

  (a) Affects the entire prosodic domain, not just a single tone.

• changesRegister : Bool

  (b) Changes the register for what follows.

• isCumulative : Bool

  (c) Cumulative: multiple downsteps stack (unlimited in principle).

• uttInitialNeutral : Bool

  (d) Utterance-initially, no phonetic contrast with undownstepped.

• characteristicallyAffectsH : Bool

  (e) Characteristically affects H tones.

• functionsContrastively : Bool

  (f) Functions contrastively (phonological, syntactic, morphophonological, or lexical).

def Theories.Phonology.Autosegmental.RegisterTier.instReprDownstepProperties.repr : DownstepProperties → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instReprDownstepProperties : Repr DownstepProperties

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprDownstepProperties = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprDownstepProperties.repr }

structure Theories.Phonology.Autosegmental.RegisterTier.AnalysisInventory : Type

Inventory of primitives in a phonological analysis.

Used to compare competing analyses of the same data — the analysis with fewer primitives and processes is preferred, all else being equal (@cite{lionnet-2025} §5).

• underlyingPrimitives : Nat
• postlexicalProcesses : Nat

instance Theories.Phonology.Autosegmental.RegisterTier.instReprAnalysisInventory : Repr AnalysisInventory

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instReprAnalysisInventory = { reprPrec := Theories.Phonology.Autosegmental.RegisterTier.instReprAnalysisInventory.repr }

def Theories.Phonology.Autosegmental.RegisterTier.instReprAnalysisInventory.repr : AnalysisInventory → Nat → Std.Format

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqAnalysisInventory : DecidableEq AnalysisInventory

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqAnalysisInventory = Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqAnalysisInventory.decEq

def Theories.Phonology.Autosegmental.RegisterTier.instDecidableEqAnalysisInventory.decEq (x✝ x✝¹ : AnalysisInventory) : Decidable (x✝ = x✝¹)

Equations

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

def Theories.Phonology.Autosegmental.RegisterTier.instBEqAnalysisInventory.beq : AnalysisInventory → AnalysisInventory → Bool

Equations

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

instance Theories.Phonology.Autosegmental.RegisterTier.instBEqAnalysisInventory : BEq AnalysisInventory

Equations

• Theories.Phonology.Autosegmental.RegisterTier.instBEqAnalysisInventory = { beq := Theories.Phonology.Autosegmental.RegisterTier.instBEqAnalysisInventory.beq }

theorem Theories.Phonology.Autosegmental.RegisterTier.registerless_uniform (n : Nat) : realizePitch n [none, none, none] = [n, n, n]

Registerless sequences have uniform pitch.

theorem Theories.Phonology.Autosegmental.RegisterTier.downstep_lowers (n : Nat) : realizePitch n [none, some RegisterFeature.l] = [n, n - 1]

A single downstep lowers pitch by one step.

theorem Theories.Phonology.Autosegmental.RegisterTier.terracing (n : Nat) : realizePitch n [some RegisterFeature.l, some RegisterFeature.l, some RegisterFeature.l] = [n - 1, n - 1 - 1, n - 1 - 1 - 1]

Multiple downsteps produce cumulative terracing.

theorem Theories.Phonology.Autosegmental.RegisterTier.terracing_from_4 : realizePitch 4 [some RegisterFeature.l, some RegisterFeature.l, some RegisterFeature.l] = [3, 2, 1]

Concrete terracing from baseline 4 (mid-high on 1–5 scale).

theorem Theories.Phonology.Autosegmental.RegisterTier.h_epenthesis_before_downstep : hEpenthesis [none, some RegisterFeature.l, none] = [some RegisterFeature.h, some RegisterFeature.l, none]

h-epenthesis raises the RBU before a downstep.

theorem Theories.Phonology.Autosegmental.RegisterTier.h_epenthesis_raises_pitch : realizePitch 4 (hEpenthesis [none, some RegisterFeature.l, none]) = [5, 4, 4]

h-epenthesis + realization: the raised RBU is higher than baseline.

theorem Theories.Phonology.Autosegmental.RegisterTier.utt_initial_neutralizes : uttInitialNeutralize [some RegisterFeature.l, none, none] = [none, none, none]

Utterance-initial neutralization removes an initial downstep.

theorem Theories.Phonology.Autosegmental.RegisterTier.utt_initial_pitch : realizePitch 4 (uttInitialNeutralize [some RegisterFeature.l, none]) = [4, 4]

After neutralization, the utterance starts at baseline.

theorem Theories.Phonology.Autosegmental.RegisterTier.single_l_culminative : isCulminative [none, some RegisterFeature.l, none] = true

Culminativity: a single l is culminative.

theorem Theories.Phonology.Autosegmental.RegisterTier.double_l_not_culminative : isCulminative [some RegisterFeature.l, some RegisterFeature.l] = false

Non-culminative: two l features violate culminativity.