Tonal Root Nodes and Subtonal Features

@cite{lionnet-2022} @cite{pulleyblank-1986} @cite{yip-1980} @cite{snider-1990} @cite{snider-1999} @cite{snider-2020} @cite{lionnet-2025}

Tone is paradigmatic. A Tonal Root Node (TRN) is a bundle of subtonal features [±upper] and [±raised] (@cite{yip-1980} @cite{pulleyblank-1986}), each of which links to a TBU (mora, syllable). This file follows @cite{lionnet-2022}'s reformulation of register-tier geometry: the four tier organisation (subtonal features → TRN → TBU) is shared with @cite{snider-1999}, but the features themselves are paradigmatic targets, not syntagmatic shifts.

Why paradigmatic, not syntagmatic

@cite{snider-1999}'s h/l features are defined both paradigmatically (specifying register half) and syntagmatically ("higher / lower than the preceding register"). @cite{lionnet-2022} (§3) argues this dual definition is overloaded: the same feature does double duty as a representational primitive and as a phonological process trigger. Switching to purely paradigmatic [±upper]/[±raised] separates the two roles — the features are the representation, the operations (spreading, OCP merger, deletion) are the processes.

Geometry (@cite{lionnet-2022} ex. 52)

    [±upper]    Register-half subtonal feature tier
    [±raised]   Within-register subtonal feature tier
       ○        Tonal Root Node (TRN) — bundles both features
       |
      TBU       Tone-bearing unit (mora / syllable)

A TRN is the structural node that gathers a [±upper] value and a [±raised] value and links them to a TBU. Either or both features may be underspecified (none), with surface values filled in by default.

Three-level systems and the Lionnet typology

With binary [±upper] and [±raised], four full specifications are possible. @cite{lionnet-2022} (§4) observes that three-level tone systems pick three of these four, and the choice of which combination is the gap defines four typological classes:

• Laal: gap is [+u, +r]; H = [+u, -r], M = [-u, +r], L = [-u, -r]
• (other three systems are predicted but rarer)

This file provides the named TRNs for the Laal pattern (H, M, L), the register-only TRNs (empty, downstep, upstep) used by Drubea and Numèè (@cite{lionnet-2025}), and the typology of all four 3-tone systems.

Two realisation modes

A TRN sequence can be realised as pitch in two ways:

1. Paradigmatic (Laal-style, @cite{lionnet-2022}): each TRN's pitch is 2·[upper] + [raised], computed independently. No terracing. See TRN.absolutePitch.

2. Terracing (Drubea/Numèè register-only systems, @cite{lionnet-2025}): each [-raised] shifts the running register baseline downward; [+raised] upward. Cumulative. See realizePitch.

The choice is a property of the language, not the representation. Drubea/Numèè are register-only systems where the only feature that ever varies is [raised] — Lionnet 2022's framework subsumes them as a degenerate case.

inductive Phonology.Autosegmental.RegisterTier.Subtonal : Type

The two paradigmatic subtonal feature dimensions (@cite{lionnet-2022} ex. 52, after @cite{yip-1980}, @cite{pulleyblank-1986}).

• upper: which register half (upper / lower)
• raised: which target within the register (higher / lower)

Each takes a value in Bool: true ≡ +, false ≡ -. A subtonal feature is none (underspecified), some true (+), or some false (-).

• upper : Subtonal
• raised : Subtonal

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableEqSubtonal : DecidableEq Subtonal

Equations

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

def Phonology.Autosegmental.RegisterTier.instReprSubtonal.repr : Subtonal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprSubtonal : Repr Subtonal

Equations

• Phonology.Autosegmental.RegisterTier.instReprSubtonal = { reprPrec := Phonology.Autosegmental.RegisterTier.instReprSubtonal.repr }

def Phonology.Autosegmental.RegisterTier.instInhabitedSubtonal.default : Subtonal

Equations

• Phonology.Autosegmental.RegisterTier.instInhabitedSubtonal.default = Phonology.Autosegmental.RegisterTier.Subtonal.upper

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instInhabitedSubtonal : Inhabited Subtonal

Equations

• Phonology.Autosegmental.RegisterTier.instInhabitedSubtonal = { default := Phonology.Autosegmental.RegisterTier.instInhabitedSubtonal.default }

structure Phonology.Autosegmental.RegisterTier.TRN : Type

A Tonal Root Node: a structural node that bundles a [±upper] and a [±raised] subtonal-feature value and links them to a TBU.

Either or both fields may be none (underspecified). For the register-only Drubea/Numèè system the upper field is uniformly none; for full 3-tone Laal both fields are usually specified.

Implemented as a structure rather than FeatureBundle Subtonal Bool so that DecidableEq, BEq, and Repr derive automatically and so that decide-based proofs over concrete TRN literals reduce cleanly. The bundle view is recovered by TRN.toBundle.

• upper : Option Bool
• raised : Option Bool

def Phonology.Autosegmental.RegisterTier.instDecidableEqTRN.decEq (x✝ x✝¹ : TRN) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableEqTRN : DecidableEq TRN

Equations

• Phonology.Autosegmental.RegisterTier.instDecidableEqTRN = Phonology.Autosegmental.RegisterTier.instDecidableEqTRN.decEq

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprTRN : Repr TRN

Equations

• Phonology.Autosegmental.RegisterTier.instReprTRN = { reprPrec := Phonology.Autosegmental.RegisterTier.instReprTRN.repr }

def Phonology.Autosegmental.RegisterTier.instReprTRN.repr : TRN → ℕ → Std.Format

Equations

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

def Phonology.Autosegmental.RegisterTier.instInhabitedTRN.default : TRN

Equations

• Phonology.Autosegmental.RegisterTier.instInhabitedTRN.default = { upper := default, raised := default }

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instInhabitedTRN : Inhabited TRN

Equations

• Phonology.Autosegmental.RegisterTier.instInhabitedTRN = { default := Phonology.Autosegmental.RegisterTier.instInhabitedTRN.default }

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.TRN.instBEq : BEq TRN

Boolean equality on TRN as decidable equality, so that LawfulBEq holds. Required for simp-based reasoning over (t == t).

Equations

• Phonology.Autosegmental.RegisterTier.TRN.instBEq = { beq := fun (a b : Phonology.Autosegmental.RegisterTier.TRN) => decide (a = b) }

instance Phonology.Autosegmental.RegisterTier.TRN.instLawfulBEq : LawfulBEq TRN

@[match_pattern]

def Phonology.Autosegmental.RegisterTier.TRN.empty : TRN

The empty / fully underspecified TRN. In the Drubea/Numèè register- only system, this is the registerless mora.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.empty = { upper := none, raised := none }

@[match_pattern]

def Phonology.Autosegmental.RegisterTier.TRN.downstep : TRN

A floating [-raised] subtonal feature, no [upper] value. In the register-only system this is the downstep TRN: it lowers the running register baseline.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.downstep = { upper := none, raised := some false }

@[match_pattern]

def Phonology.Autosegmental.RegisterTier.TRN.upstep : TRN

A floating [+raised] subtonal feature, no [upper] value. In the register-only system this is the upstep TRN — used by pre-downstep h-epenthesis (@cite{lionnet-2025}).

Equations

• Phonology.Autosegmental.RegisterTier.TRN.upstep = { upper := none, raised := some true }

def Phonology.Autosegmental.RegisterTier.TRN.H : TRN

The High tone of Laal-style 3-tone systems: [+upper, -raised] (@cite{lionnet-2022} §4). Highest pitch.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.H = { upper := some true, raised := some false }

def Phonology.Autosegmental.RegisterTier.TRN.M : TRN

The Mid tone of Laal-style 3-tone systems: [-upper, +raised] (@cite{lionnet-2022} §4). M is not primitive — it is one of the four [±u, ±r] combinations, derived from the binary subtonal features. The Lionnet move: there is no TRN.M enum constructor; M is just a name for a particular bundle.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.M = { upper := some false, raised := some true }

def Phonology.Autosegmental.RegisterTier.TRN.L : TRN

The Low tone of Laal-style 3-tone systems: [-upper, -raised] (@cite{lionnet-2022} §4). Lowest pitch.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.L = { upper := some false, raised := some false }

def Phonology.Autosegmental.RegisterTier.TRN.superHigh : TRN

The fourth combination [+upper, +raised] — unattested in Laal, where it is the gap of the 3-tone system (@cite{lionnet-2022} §4). Provided for typological completeness; an attested 4-tone language or a different 3-tone gap would use this.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.superHigh = { upper := some true, raised := some true }

def Phonology.Autosegmental.RegisterTier.TRN.toBundle (t : TRN) : Featural.FeatureBundle Subtonal Bool

View a TRN as a FeatureBundle Subtonal Bool (the parametric foundation in Phonology.Featural.Bundle). The bundle algebra (merge, assimilate, delete, set, refines) is then directly available via this view.

Equations

• t.toBundle Phonology.Autosegmental.RegisterTier.Subtonal.upper = t.upper
• t.toBundle Phonology.Autosegmental.RegisterTier.Subtonal.raised = t.raised

def Phonology.Autosegmental.RegisterTier.TRN.ofBundle (b : Featural.FeatureBundle Subtonal Bool) : TRN

Recover a TRN from a generic subtonal-feature bundle. Inverse of toBundle.

Equations

• Phonology.Autosegmental.RegisterTier.TRN.ofBundle b = { upper := b Phonology.Autosegmental.RegisterTier.Subtonal.upper, raised := b Phonology.Autosegmental.RegisterTier.Subtonal.raised }

@[simp]

theorem Phonology.Autosegmental.RegisterTier.TRN.toBundle_upper (t : TRN) : t.toBundle Subtonal.upper = t.upper

@[simp]

theorem Phonology.Autosegmental.RegisterTier.TRN.toBundle_raised (t : TRN) : t.toBundle Subtonal.raised = t.raised

@[simp]

theorem Phonology.Autosegmental.RegisterTier.TRN.ofBundle_toBundle (t : TRN) : ofBundle t.toBundle = t

def Phonology.Autosegmental.RegisterTier.TRN.pitchEffect (t : TRN) : ℤ

Syntagmatic register shift contributed by a TRN, used by the terracing realisation realizePitch. Reads only the [raised] subtonal feature: [-raised] lowers, [+raised] raises, underspecified is inert.

This is not the paradigmatic interpretation of [raised] (@cite{lionnet-2022} §3). It is the realisation pattern attested in register-only systems like Drubea and Numèè (@cite{lionnet-2025}), where each [-raised] triggers a downstep operation that resets the register baseline.

Equations

• t.pitchEffect = match t.raised with | none => 0 | some false => -1 | some true => 1

def Phonology.Autosegmental.RegisterTier.realizePitch : ℤ → List TRN → List ℤ

Terracing realisation: realise a TRN sequence as a sequence of pitch levels, where each [-raised] cumulatively lowers the baseline (@cite{snider-1999} @cite{lionnet-2025}).

Used for register-only systems (Drubea, Numèè) and for catathesis in Japanese / English intonation (@cite{beckman-pierrehumbert-1986}). For the paradigmatic Laal-style realisation see TRN.absolutePitch.

Defined by direct case-split on the [raised] value so that realizePitch n [TRN.empty, …] reduces to n :: … definitionally (the alternative level + t.pitchEffect form does not reduce for opaque n : Int, since n + 0 = n is not definitional).

Equations

• Phonology.Autosegmental.RegisterTier.realizePitch x✝ [] = []
• Phonology.Autosegmental.RegisterTier.realizePitch x✝ ({ upper := upper, raised := none } :: rest) = x✝ :: Phonology.Autosegmental.RegisterTier.realizePitch x✝ rest
• Phonology.Autosegmental.RegisterTier.realizePitch x✝ ({ upper := upper, raised := some false } :: rest) = (x✝ - 1) :: Phonology.Autosegmental.RegisterTier.realizePitch (x✝ - 1) rest
• Phonology.Autosegmental.RegisterTier.realizePitch x✝ ({ upper := upper, raised := some true } :: rest) = (x✝ + 1) :: Phonology.Autosegmental.RegisterTier.realizePitch (x✝ + 1) rest

@[simp]

theorem Phonology.Autosegmental.RegisterTier.realizePitch_cons (level : ℤ) (t : TRN) (rest : List TRN) : realizePitch level (t :: rest) = (level + t.pitchEffect) :: realizePitch (level + t.pitchEffect) rest

A uniform cons rewrite for realizePitch in terms of pitchEffect.

def Phonology.Autosegmental.RegisterTier.pitchDeltas (ts : List TRN) : List ℤ

Pitch deltas — the theory-primary view (@cite{snider-1999} @cite{lionnet-2025}). Cumulative register shifts produced by a TRN sequence, expressed as integer offsets from the start. There is no privileged "zero" pitch; only the differences are meaningful.

Equations

• Phonology.Autosegmental.RegisterTier.pitchDeltas ts = Phonology.Autosegmental.RegisterTier.realizePitch 0 ts

theorem Phonology.Autosegmental.RegisterTier.realizePitch_eq_pitchDeltas_shift (n : ℤ) (ts : List TRN) : realizePitch n ts = List.map (fun (x : ℤ) => x + n) (pitchDeltas ts)

realizePitch n ts is pitchDeltas ts shifted by the offset n.

def Phonology.Autosegmental.RegisterTier.realizePitchUtterance (level : ℤ) : List TRN → List ℤ

Utterance-initial phonetic neutralisation: an utterance-initial [-raised] TRN is realised at the starting pitch (no preceding register to contrast with — @cite{lionnet-2025} §3.5, §4.5). The feature is not removed from the underlying form: it remains phonologically active for blocking pre-downstep h-epenthesis on itself and for feeding raising on a following registerless TRN.

Equations

• One or more equations did not get rendered due to their size.
• Phonology.Autosegmental.RegisterTier.realizePitchUtterance level [] = []

def Phonology.Autosegmental.RegisterTier.TRN.absolutePitch (t : TRN) : ℤ

Paradigmatic Laal-style pitch realisation (@cite{lionnet-2022} §4). Pitch is computed from [upper] (×2) plus [raised] (×1), independently per TRN — no terracing, no register-baseline state.

Unspecified features contribute 0. The four combinations give: H = 2, M = 1, L = 0, superHigh = 3 (Laal's gap).

Equations

• t.absolutePitch = (if t.upper = some true then 2 else 0) + if t.raised = some true then 1 else 0

inductive Phonology.Autosegmental.RegisterTier.ThreeToneGap : Type

The four typological classes of 3-tone systems (@cite{lionnet-2022} §4). Each class picks three of the four [±upper, ±raised] combinations; the unselected combination is the gap.

• upperRaised : ThreeToneGap

  Gap = [+upper, +raised] (Laal pattern).

• upperLowered : ThreeToneGap

  Gap = [+upper, -raised].

• lowerRaised : ThreeToneGap

  Gap = [-upper, +raised].

• lowerLowered : ThreeToneGap

  Gap = [-upper, -raised].

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableEqThreeToneGap : DecidableEq ThreeToneGap

Equations

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

def Phonology.Autosegmental.RegisterTier.instReprThreeToneGap.repr : ThreeToneGap → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprThreeToneGap : Repr ThreeToneGap

Equations

• Phonology.Autosegmental.RegisterTier.instReprThreeToneGap = { reprPrec := Phonology.Autosegmental.RegisterTier.instReprThreeToneGap.repr }

def Phonology.Autosegmental.RegisterTier.ThreeToneGap.gap : ThreeToneGap → TRN

Which TRN combination is the gap for a given 3-tone language type.

Equations

• Phonology.Autosegmental.RegisterTier.ThreeToneGap.upperRaised.gap = Phonology.Autosegmental.RegisterTier.TRN.superHigh
• Phonology.Autosegmental.RegisterTier.ThreeToneGap.upperLowered.gap = Phonology.Autosegmental.RegisterTier.TRN.H
• Phonology.Autosegmental.RegisterTier.ThreeToneGap.lowerRaised.gap = Phonology.Autosegmental.RegisterTier.TRN.M
• Phonology.Autosegmental.RegisterTier.ThreeToneGap.lowerLowered.gap = Phonology.Autosegmental.RegisterTier.TRN.L

theorem Phonology.Autosegmental.RegisterTier.laalGap : ThreeToneGap.upperRaised.gap = TRN.superHigh

The Laal-style 3-tone system gap is [+upper, +raised] (@cite{lionnet-2022} §4).

inductive Phonology.Autosegmental.RegisterTier.TBUKind : Type

The prosodic domain that carries TRN specifications. In most tone languages this is the syllable; in Drubea and Numèè it is the mora (@cite{lionnet-2025}).

• mora : TBUKind
• syllable : TBUKind

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableEqTBUKind : DecidableEq TBUKind

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprTBUKind : Repr TBUKind

Equations

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

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

Equations

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

inductive Phonology.Autosegmental.RegisterTier.WordProsodicType : Type

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

Tone systems split into tone-based (paradigmatic — full TRN contrasts) and register-based (only [raised] varies, with cumulative terracing realisation).

• toneBased : WordProsodicType

  Paradigmatic H/L contrast (e.g., Yoruba, Mandarin).

• registerBased : WordProsodicType

  Syntagmatic downstep contrast (e.g., Drubea, Numèè).

• stressAccent : WordProsodicType

  Prominence-based (e.g., English, Russian).

• mixed : WordProsodicType

  Both tone and register (e.g., Paicî, Baga Pukur).

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableEqWordProsodicType : DecidableEq WordProsodicType

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprWordProsodicType : Repr WordProsodicType

Equations

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

structure Phonology.Autosegmental.RegisterTier.DownstepProperties : Type

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

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprDownstepProperties : Repr DownstepProperties

Equations

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

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

Equations

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

structure Phonology.Autosegmental.RegisterTier.AnalysisInventory : Type

Inventory of primitives in a phonological analysis (@cite{lionnet-2025}).

• underlyingPrimitives : ℕ
• postlexicalProcesses : ℕ

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

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instReprAnalysisInventory : Repr AnalysisInventory

Equations

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

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableEqAnalysisInventory : DecidableEq AnalysisInventory

Equations

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

def 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 Phonology.Autosegmental.RegisterTier.IsCulminative (ts : List TRN) : Prop

Register culminativity: at most one [-raised] TRN per stem.

Holds for all native Drubea and Numèè stems (@cite{lionnet-2025} §3.10). The Lionnet 2022 framing: a stem contains at most one bundle whose [raised] value is some false.

Equations

• Phonology.Autosegmental.RegisterTier.IsCulminative ts = (List.countP (fun (t : Phonology.Autosegmental.RegisterTier.TRN) => t.raised == some false) ts ≤ 1)

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidablePredListTRNIsCulminative : DecidablePred IsCulminative

Equations

• Phonology.Autosegmental.RegisterTier.instDecidablePredListTRNIsCulminative x✝ = (List.countP (fun (t : Phonology.Autosegmental.RegisterTier.TRN) => t.raised == some false) x✝).decLe 1

def Phonology.Autosegmental.RegisterTier.hEpenthesis : List TRN → List TRN

Pre-downstep h-epenthesis (@cite{lionnet-2025}): insert an upstep TRN immediately before a downstep, on a registerless host.

The rule fires when an empty (⟨none, none⟩) TRN is immediately followed by a downstep TRN (⟨none, some false⟩); the empty TRN is replaced by an upstep (⟨none, some true⟩). An underlying downstep blocks the rule on itself — that is the diagnostic that survives utterance-initial phonetic neutralisation.

Equations

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

def Phonology.Autosegmental.RegisterTier.hEpenthesisSpread : List TRN → List TRN

Spreading h-epenthesis: raise all registerless TRNs in the sequence preceding a downstep, not just the immediately preceding one (@cite{lionnet-2025} §3.2). Models the abrupt-spreading variant.

Equations

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

def Phonology.Autosegmental.RegisterTier.subtonalAssimilate (f : Subtonal) (src tgt : TRN) : TRN

Subtonal assimilation at feature f: the target TRN takes its value at f from the source TRN, leaving its other feature untouched. The Laal M-lowering rule (@cite{lionnet-2022} §5.2) is subtonalAssimilate Subtonal.raised src tgt: a [-raised] value spreads from src to tgt, so a target M (⟨-u, +r⟩) becomes L (⟨-u, -r⟩) without altering its [upper] value.

Equations

• Phonology.Autosegmental.RegisterTier.subtonalAssimilate f src tgt = Phonology.Autosegmental.RegisterTier.TRN.ofBundle (Phonology.Featural.FeatureBundle.assimilate f src.toBundle tgt.toBundle)

def Phonology.Autosegmental.RegisterTier.mergeTRN (t₁ t₂ : TRN) : TRN

OCP merger: collapse a sequence of TRNs with identical subtonal feature values into a single multiply-linked TRN (@cite{lionnet-2022} ex. 53–54). The Bundle-level merger (FeatureBundle.merge) takes the value from the left TRN where it is specified, falling back to the right.

Two readings of the OCP — note on theoretical heterogeneity. The autosegmental tradition (@cite{goldsmith-1976}) treats the OCP as a transformation — adjacent identical autosegments at the melodic level are merged into a single multiply-linked autosegment. That is the reading mergeTRN implements: a repair operation. The subregular tradition (@cite{mccarthy-1986}) treats the OCP as a prohibition — a constraint on output well-formedness that rejects strings containing adjacent identical autosegments. The prohibition reading is formalized by Phonology.Subregular.OCP's TSLGrammar.ocp (Core/Computability/Subregular/ForbiddenPairs.lean plus Theories/Phonology/Subregular/OCP.lean) and the OT-side mkOCPOnTier constraint. The two readings are operationally distinct (transformation vs. language-membership predicate) and coexist in linglib without a master bridge — the autosegmental formalization fixes a representation, the subregular formalization classifies a stringset.

Equations

• Phonology.Autosegmental.RegisterTier.mergeTRN t₁ t₂ = Phonology.Autosegmental.RegisterTier.TRN.ofBundle (t₁.toBundle.merge t₂.toBundle)

def Phonology.Autosegmental.RegisterTier.deleteSubtonal (f : Subtonal) (t : TRN) : TRN

TRN-level deletion (@cite{lionnet-2022} §6.2): delete a TRN's contribution at one subtonal feature, returning to underspecified. Used in replaceness operations where a TRN is partially erased before a floating feature docks.

Equations

• Phonology.Autosegmental.RegisterTier.deleteSubtonal f t = Phonology.Autosegmental.RegisterTier.TRN.ofBundle (Phonology.Featural.FeatureBundle.delete f t.toBundle)

def Phonology.Autosegmental.RegisterTier.dockFloating (f : Subtonal) (v : Bool) (t : TRN) : TRN

Floating-feature docking (@cite{lionnet-2022} §5.3): a free [±f] subtonal feature docks onto a target TRN, overwriting whatever value it had at f. Used for the morphosyntactic [-raised] suffix in Laal that triggers M-lowering.

Equations

• Phonology.Autosegmental.RegisterTier.dockFloating f v t = Phonology.Autosegmental.RegisterTier.TRN.ofBundle (Phonology.Featural.FeatureBundle.set f v t.toBundle)

theorem Phonology.Autosegmental.RegisterTier.laal_three_tones : TRN.H ≠ TRN.M ∧ TRN.M ≠ TRN.L ∧ TRN.H ≠ TRN.L ∧ TRN.H ≠ TRN.superHigh ∧ TRN.M ≠ TRN.superHigh ∧ TRN.L ≠ TRN.superHigh

The Laal H/M/L tones are exactly three of the four binary [±u, ±r] combinations — the gap is superHigh.

theorem Phonology.Autosegmental.RegisterTier.laal_paradigmatic_pitch : TRN.L.absolutePitch = 0 ∧ TRN.M.absolutePitch = 1 ∧ TRN.H.absolutePitch = 2 ∧ TRN.superHigh.absolutePitch = 3

Paradigmatic pitch ordering: L < M < H < superHigh.

theorem Phonology.Autosegmental.RegisterTier.m_lowering_via_assimilation : subtonalAssimilate Subtonal.raised TRN.L TRN.M = TRN.L

M-lowering as [-raised] assimilation (@cite{lionnet-2022} §5.2). When a [-raised] source assimilates onto an M target, the result is L: M's [+raised] is overwritten to [-raised], and its [-upper] is preserved.

Critically, the [upper] feature is not changed — this is what makes the operation subtonal-level rather than full-tone replacement.

theorem Phonology.Autosegmental.RegisterTier.m_lowering_vacuous_on_m : subtonalAssimilate Subtonal.raised TRN.M TRN.M = TRN.M

The same operation has no effect when the source itself is M: assimilating [+raised] onto M leaves M unchanged.

theorem Phonology.Autosegmental.RegisterTier.floating_minus_raised_lowers_m : dockFloating Subtonal.raised false TRN.M = TRN.L

Floating [-raised] docking onto M produces L (@cite{lionnet-2022} §5.3): the morphosyntactic suffix is a free floating feature that overwrites the target's [raised] value.

theorem Phonology.Autosegmental.RegisterTier.registerless_uniform (n : ℤ) : realizePitch n [TRN.empty, TRN.empty, TRN.empty] = [n, n, n]

Registerless sequences have uniform pitch.

theorem Phonology.Autosegmental.RegisterTier.downstep_lowers (n : ℤ) : realizePitch n [TRN.empty, TRN.downstep] = [n, n - 1]

A single downstep lowers pitch by one step.

theorem Phonology.Autosegmental.RegisterTier.terracing (n : ℤ) : realizePitch n [TRN.downstep, TRN.downstep, TRN.downstep] = [n - 1, n - 1 - 1, n - 1 - 1 - 1]

Multiple downsteps produce cumulative terracing.

theorem Phonology.Autosegmental.RegisterTier.terracing_deltas : pitchDeltas [TRN.downstep, TRN.downstep, TRN.downstep] = [-1, -2, -3]

Deltas-only view of three downsteps: pitch falls by 1, 2, 3 register steps from the start. No anchor required.

theorem Phonology.Autosegmental.RegisterTier.terracing_from_4 : realizePitch 4 [TRN.downstep, TRN.downstep, TRN.downstep] = [3, 2, 1]

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

theorem Phonology.Autosegmental.RegisterTier.h_epenthesis_before_downstep : hEpenthesis [TRN.empty, TRN.downstep, TRN.empty] = [TRN.upstep, TRN.downstep, TRN.empty]

h-epenthesis raises the registerless TRN before a downstep.

theorem Phonology.Autosegmental.RegisterTier.h_epenthesis_raises_pitch : realizePitch 4 (hEpenthesis [TRN.empty, TRN.downstep, TRN.empty]) = [5, 4, 4]

h-epenthesis + realisation: the raised TRN is higher than baseline.

theorem Phonology.Autosegmental.RegisterTier.l_blocks_own_h_epenthesis : hEpenthesis [TRN.downstep, TRN.downstep] = [TRN.downstep, TRN.downstep]

An underlying downstep blocks h-epenthesis on itself: the rule only targets registerless TRNs immediately preceding a downstep. This is what the underlying initial downstep (preserved by realizePitchUtterance) buys us — the contrast /X ⁺Y/ (raises X) vs /⁺X ⁺Y/ (no raising on ⁺X) survives even when the initial X is utterance-initial and phonetically flat.

theorem Phonology.Autosegmental.RegisterTier.utt_initial_phonetic_suppression : realizePitchUtterance 4 [TRN.downstep, TRN.empty, TRN.empty] = [4, 4, 4]

Phonetic suppression of an utterance-initial downstep: the realized pitch sequence starts flat, indistinguishable from a registerless initial.

theorem Phonology.Autosegmental.RegisterTier.utt_initial_only_first : realizePitchUtterance 4 [TRN.downstep, TRN.downstep, TRN.empty] = [4, 3, 3]

The phonetic neutralisation is only utterance-initial: a non-initial downstep still drops pitch, even after the suppression rule fires.

theorem Phonology.Autosegmental.RegisterTier.utt_initial_l_underlyingly_present : IsCulminative [TRN.downstep, TRN.empty] ∧ realizePitchUtterance 4 [TRN.downstep, TRN.empty] = realizePitch 4 [TRN.empty, TRN.empty]

Underlying culminativity is preserved under utterance-initial suppression: an initial downstep still counts toward the stem-level [-raised] budget. The phonetic interface does not delete it.

theorem Phonology.Autosegmental.RegisterTier.single_l_culminative : IsCulminative [TRN.empty, TRN.downstep, TRN.empty]

Culminativity: a single [-raised] is culminative.

theorem Phonology.Autosegmental.RegisterTier.double_l_not_culminative : ¬IsCulminative [TRN.downstep, TRN.downstep]

Non-culminativity: two [-raised] TRNs violate culminativity.

def Phonology.Autosegmental.RegisterTier.TRN.le (t₁ t₂ : TRN) : Prop

TRN-level pitch-effect ordering: t₁ ≤ t₂ iff t₁ has a smaller syntagmatic pitch effect than t₂. Equivalent to "t₁ is at least as lowering as t₂".

Equations

• t₁.le t₂ = (t₁.pitchEffect ≤ t₂.pitchEffect)

@[implicit_reducible]

instance Phonology.Autosegmental.RegisterTier.instDecidableRelTRNLe : DecidableRel TRN.le

Equations

• Phonology.Autosegmental.RegisterTier.instDecidableRelTRNLe x✝¹ x✝ = x✝¹.pitchEffect.decLe x✝.pitchEffect

theorem Phonology.Autosegmental.RegisterTier.realizePitch_baseline_mono (ts : List TRN) {n m : ℤ} (h : n ≤ m) : List.Forall₂ (fun (x1 x2 : ℤ) => x1 ≤ x2) (realizePitch n ts) (realizePitch m ts)

Monotonicity of realizePitch in the baseline: a higher starting pitch produces pointwise higher output for any fixed TRN sequence.

Structural basis for catathesis blocking (@cite{beckman-pierrehumbert-1986}): when an ip boundary resets the register, subsequent pitches are higher than if catathesis had continued from a compressed baseline.

theorem Phonology.Autosegmental.RegisterTier.realizePitch_mono {ts₁ ts₂ : List TRN} (hts : List.Forall₂ TRN.le ts₁ ts₂) {n m : ℤ} (hnm : n ≤ m) : List.Forall₂ (fun (x1 x2 : ℤ) => x1 ≤ x2) (realizePitch n ts₁) (realizePitch m ts₂)

Full monotonicity of realizePitch: pointwise lowering features plus a lower baseline give pointwise lower output. Subsumes realizePitch_baseline_mono.