Tonal Root Nodes and Subtonal Features

Tone is paradigmatic. A Tonal Root Node (TRN) is a bundle of subtonal features [±upper] and [±raised] ([Yip80] [Pul86]), each of which links to a TBU (mora, syllable). This file follows [Lio22a]'s reformulation of register-tier geometry: the four tier organisation (subtonal features → TRN → TBU) is shared with [Sni99], but the features themselves are paradigmatic targets, not syntagmatic shifts.

Main definitions

• Subtonal — the two paradigmatic subtonal feature dimensions [±upper] and [±raised].
• TRN — Tonal Root Node, a bundle of Option Bool values for the two subtonal features. Linked to its Subtonal → Option Bool view by TRN.toBundle / TRN.ofBundle.
• TRN.empty, TRN.downstep, TRN.upstep — register-only TRNs for Drubea/Numèè-style systems.
• TRN.H, TRN.M, TRN.L, TRN.superHigh — the four [±u, ±r] combinations underlying the Laal-style 3-tone system.
• realizePitch, pitchDeltas, realizePitchUtterance — terracing realisation (cumulative register shifts).
• TRN.absolutePitch — paradigmatic Laal-style realisation.
• ThreeToneGap — the four typological classes of 3-tone systems.
• TBUKind, WordProsodicType, DownstepProperties, AnalysisInventory — prosodic typology primitives.
• IsCulminative — at most one [-raised] TRN per stem.
• hEpenthesis, hEpenthesisSpread — postlexical operations.
• subtonalAssimilate, mergeTRN, dockFloating — subtonal feature operations via the bundle view.

Implementation notes

Why paradigmatic, not syntagmatic

[Sni99]'s h/l features are defined both paradigmatically (specifying register half) and syntagmatically ("higher / lower than the preceding register"). [Lio22a] 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

    [±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.

Subtonal features

inductive Tone.Subtonal : Type

The two paradigmatic subtonal feature dimensions ([Lio22a] ex. 51, after [Yip80], [Pul86]).

• 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 Tone.instDecidableEqSubtonal : DecidableEq Subtonal

Equations

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

@[implicit_reducible]

instance Tone.instReprSubtonal : Repr Subtonal

Equations

• Tone.instReprSubtonal = { reprPrec := Tone.instReprSubtonal.repr }

def Tone.instReprSubtonal.repr : Subtonal → ℕ → Std.Format

Equations

• Tone.instReprSubtonal.repr Tone.Subtonal.upper prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Subtonal.upper")).group prec✝
• Tone.instReprSubtonal.repr Tone.Subtonal.raised prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.Subtonal.raised")).group prec✝

@[implicit_reducible]

instance Tone.instInhabitedSubtonal : Inhabited Subtonal

Equations

• Tone.instInhabitedSubtonal = { default := Tone.instInhabitedSubtonal.default }

Tonal root node

structure Tone.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 Subtonal → Option Bool so that DecidableEq and Repr derive automatically (and BEq follows from DecidableEq, below) 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

@[implicit_reducible]

instance Tone.instDecidableEqTRN : DecidableEq TRN

Equations

• Tone.instDecidableEqTRN = Tone.instDecidableEqTRN.decEq

def Tone.instDecidableEqTRN.decEq (x✝ x✝¹ : TRN) : Decidable (x✝ = x✝¹)

Equations

• Tone.instDecidableEqTRN.decEq { upper := a, raised := a_1 } { upper := b, raised := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Tone.instReprTRN.repr : TRN → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tone.instReprTRN : Repr TRN

Equations

• Tone.instReprTRN = { reprPrec := Tone.instReprTRN.repr }

@[implicit_reducible]

instance Tone.instInhabitedTRN : Inhabited TRN

Equations

• Tone.instInhabitedTRN = { default := Tone.instInhabitedTRN.default }

@[implicit_reducible]

instance Tone.TRN.instBEq : BEq TRN

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

Equations

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

instance Tone.TRN.instLawfulBEq : LawfulBEq TRN

@[match_pattern]

def Tone.TRN.empty : TRN

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

Equations

• Tone.TRN.empty = { upper := none, raised := none }

@[match_pattern]

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

• Tone.TRN.downstep = { upper := none, raised := some false }

@[match_pattern]

def Tone.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 ([Lio25]).

Equations

• Tone.TRN.upstep = { upper := none, raised := some true }

def Tone.TRN.H : TRN

The High tone of Laal-style 3-tone systems: [+upper, -raised] ([Lio22a] ex. 51). Highest pitch.

Equations

• Tone.TRN.H = { upper := some true, raised := some false }

def Tone.TRN.M : TRN

The Mid tone of Laal-style 3-tone systems: [-upper, +raised] ([Lio22a] ex. 51). M is one of the four [±u, ±r] combinations, derived from the binary subtonal features — not a primitive enum constructor.

Equations

• Tone.TRN.M = { upper := some false, raised := some true }

def Tone.TRN.L : TRN

The Low tone of Laal-style 3-tone systems: [-upper, -raised] ([Lio22a] ex. 51). Lowest pitch.

Equations

• Tone.TRN.L = { upper := some false, raised := some false }

def Tone.TRN.superHigh : TRN

The fourth combination [+upper, +raised] — unattested in Laal, where it is the gap of the subtonal system ([Lio22a] ex. 51: "Missing from this system is the subtonal specification [+upper, +raised]"). Provided for completeness; an attested 4-tone language or a different 3-tone gap would use this.

Equations

• Tone.TRN.superHigh = { upper := some true, raised := some true }

def Tone.TRN.toBundle (t : TRN) : Subtonal → Option Bool

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

Equations

• t.toBundle Tone.Subtonal.upper = t.upper
• t.toBundle Tone.Subtonal.raised = t.raised

def Tone.TRN.ofBundle (b : Subtonal → Option Bool) : TRN

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

Equations

• Tone.TRN.ofBundle b = { upper := b Tone.Subtonal.upper, raised := b Tone.Subtonal.raised }

@[simp]

theorem Tone.TRN.toBundle_upper (t : TRN) : t.toBundle Subtonal.upper = t.upper

@[simp]

theorem Tone.TRN.toBundle_raised (t : TRN) : t.toBundle Subtonal.raised = t.raised

@[simp]

theorem Tone.TRN.ofBundle_toBundle (t : TRN) : ofBundle t.toBundle = t

Pitch realisation

def Tone.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] ([Lio22a] §5.1). It is the realisation pattern attested in register-only systems like Drubea and Numèè ([Lio25]), 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 Tone.realizePitch : ℤ → List TRN → List ℤ

Terracing realisation: realise a TRN sequence as a sequence of pitch levels, where each [-raised] cumulatively lowers the baseline ([Sni99] [Lio25]).

Used for register-only systems (Drubea, Numèè) and for catathesis in Japanese / English intonation ([BP86]). 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

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

@[simp]

theorem Tone.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 Tone.pitchDeltas (ts : List TRN) : List ℤ

Pitch deltas — the theory-primary view ([Sni99] [Lio25]). 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

• Tone.pitchDeltas ts = Tone.realizePitch 0 ts

theorem Tone.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 Tone.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 — [Lio25] §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

• Tone.realizePitchUtterance level [] = []
• Tone.realizePitchUtterance level (t :: rest) = if t.raised = some false ∧ t.upper = none then level :: Tone.realizePitch level rest else Tone.realizePitch level (t :: rest)

def Tone.TRN.absolutePitch (t : TRN) : ℤ

Paradigmatic Laal-style pitch realisation ([Lio22a] §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

Lionnet's 3-tone typology

inductive Tone.ThreeToneGap : Type

The four classes of 3-tone system definable over the binary subtonal features [±upper]/[±raised] ([Lio22a] ex. 51): with four full specifications available, a 3-tone system realises three of them, and the unselected combination is the gap. The four-way classification by gap is a systematisation of Lionnet's binary-feature account (Laal itself has the [+upper, +raised] gap), not a typology the paper surveys.

• 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 Tone.instDecidableEqThreeToneGap : DecidableEq ThreeToneGap

Equations

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

@[implicit_reducible]

instance Tone.instReprThreeToneGap : Repr ThreeToneGap

Equations

• Tone.instReprThreeToneGap = { reprPrec := Tone.instReprThreeToneGap.repr }

def Tone.instReprThreeToneGap.repr : ThreeToneGap → ℕ → Std.Format

Equations

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

def Tone.ThreeToneGap.gap : ThreeToneGap → TRN

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

Equations

• Tone.ThreeToneGap.upperRaised.gap = Tone.TRN.superHigh
• Tone.ThreeToneGap.upperLowered.gap = Tone.TRN.H
• Tone.ThreeToneGap.lowerRaised.gap = Tone.TRN.M
• Tone.ThreeToneGap.lowerLowered.gap = Tone.TRN.L

theorem Tone.laal_gap_eq_superHigh : ThreeToneGap.upperRaised.gap = TRN.superHigh

Laal's gap is [+upper, +raised] ([Lio22a] ex. 51).

TBU and word-prosodic typology

inductive Tone.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 ([Lio25]).

• mora : TBUKind
• syllable : TBUKind

@[implicit_reducible]

instance Tone.instDecidableEqTBUKind : DecidableEq TBUKind

Equations

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

def Tone.instReprTBUKind.repr : TBUKind → ℕ → Std.Format

Equations

• Tone.instReprTBUKind.repr Tone.TBUKind.mora prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.TBUKind.mora")).group prec✝
• Tone.instReprTBUKind.repr Tone.TBUKind.syllable prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.TBUKind.syllable")).group prec✝

@[implicit_reducible]

instance Tone.instReprTBUKind : Repr TBUKind

Equations

• Tone.instReprTBUKind = { reprPrec := Tone.instReprTBUKind.repr }

inductive Tone.WordProsodicType : Type

Word-prosodic system types ([Hym06], enriched by [Lio25]).

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 Tone.instDecidableEqWordProsodicType : DecidableEq WordProsodicType

Equations

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

@[implicit_reducible]

instance Tone.instReprWordProsodicType : Repr WordProsodicType

Equations

• Tone.instReprWordProsodicType = { reprPrec := Tone.instReprWordProsodicType.repr }

def Tone.instReprWordProsodicType.repr : WordProsodicType → ℕ → Std.Format

Equations

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

structure Tone.DownstepProperties : Type

Core definitional properties of downstep, following [Leb18b] as refined by [Lio25].

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 Tone.instReprDownstepProperties.repr : DownstepProperties → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tone.instReprDownstepProperties : Repr DownstepProperties

Equations

• Tone.instReprDownstepProperties = { reprPrec := Tone.instReprDownstepProperties.repr }

structure Tone.AnalysisInventory : Type

Inventory of primitives in a phonological analysis ([Lio25]).

• underlyingPrimitives : ℕ
• postlexicalProcesses : ℕ

@[implicit_reducible]

instance Tone.instReprAnalysisInventory : Repr AnalysisInventory

Equations

• Tone.instReprAnalysisInventory = { reprPrec := Tone.instReprAnalysisInventory.repr }

def Tone.instReprAnalysisInventory.repr : AnalysisInventory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tone.instDecidableEqAnalysisInventory : DecidableEq AnalysisInventory

Equations

• Tone.instDecidableEqAnalysisInventory = Tone.instDecidableEqAnalysisInventory.decEq

def Tone.instDecidableEqAnalysisInventory.decEq (x✝ x✝¹ : AnalysisInventory) : Decidable (x✝ = x✝¹)

Equations

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

Culminativity

@[reducible, inline]

abbrev Tone.IsCulminative (ts : List TRN) : Prop

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

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

Equations

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

Postlexical operations

def Tone.hEpenthesis : List TRN → List TRN

Pre-downstep h-epenthesis ([Lio25]): 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

• Tone.hEpenthesis [] = []
• Tone.hEpenthesis [t] = [t]
• Tone.hEpenthesis ({ upper := none, raised := none } :: { upper := none, raised := some false } :: rest) = Tone.TRN.upstep :: Tone.TRN.downstep :: Tone.hEpenthesis rest
• Tone.hEpenthesis (t :: rest) = t :: Tone.hEpenthesis rest

def Tone.hEpenthesisSpread : List TRN → List TRN

Spreading h-epenthesis: raise all registerless TRNs in the sequence preceding a downstep, not just the immediately preceding one ([Lio25] §3.2). Models the abrupt-spreading variant.

Equations

• One or more equations did not get rendered due to their size.
• Tone.hEpenthesisSpread [] = []
• Tone.hEpenthesisSpread ({ upper := none, raised := some false } :: rest) = Tone.TRN.downstep :: Tone.hEpenthesisSpread rest
• Tone.hEpenthesisSpread ({ upper := none, raised := some true } :: rest) = Tone.TRN.upstep :: Tone.hEpenthesisSpread rest
• Tone.hEpenthesisSpread (t :: rest) = t :: Tone.hEpenthesisSpread rest

Subtonal feature operations

def Tone.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 ([Lio22a] §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

• Tone.subtonalAssimilate f src tgt = Tone.TRN.ofBundle (Features.Bundle.assimilate f src.toBundle tgt.toBundle)

def Tone.mergeTRN (t₁ t₂ : TRN) : TRN

Binary TRN merger ([Lio22a] ex. 53–54): merge two TRNs' subtonal features into one, taking each feature from the left TRN where it is specified and falling back to the right (Features.Bundle.merge). Models the autosegmental fusion of two associated tones ([Gol76]); the tier-level OCP merger that collapses a run of identical tones is OCP.collapse.

Equations

• Tone.mergeTRN t₁ t₂ = Tone.TRN.ofBundle (Features.Bundle.merge t₁.toBundle t₂.toBundle)

@[simp]

theorem Tone.mergeTRN_self (t : TRN) : mergeTRN t t = t

Merging a TRN with itself is the identity: mergeTRN is idempotent on equal tones.

def Tone.dockFloating (f : Subtonal) (v : Bool) (t : TRN) : TRN

Floating-feature docking ([Lio22a] §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

• Tone.dockFloating f v t = Tone.TRN.ofBundle (Features.Bundle.set f v t.toBundle)

Verification: Laal subtonal identities

theorem Tone.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 Tone.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 Tone.m_lowering_via_assimilation : subtonalAssimilate Subtonal.raised TRN.L TRN.M = TRN.L

M-lowering as [-raised] assimilation ([Lio22a] §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 Tone.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 Tone.floating_minus_raised_lowers_m : dockFloating Subtonal.raised false TRN.M = TRN.L

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

Verification: Drubea/Numèè register-only realisation

theorem Tone.registerless_uniform (n : ℤ) : realizePitch n [TRN.empty, TRN.empty, TRN.empty] = [n, n, n]

Registerless sequences have uniform pitch.

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

A single downstep lowers pitch by one step.

theorem Tone.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 Tone.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 Tone.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 Tone.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 Tone.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 Tone.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 Tone.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 Tone.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 Tone.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 Tone.single_l_culminative : IsCulminative [TRN.empty, TRN.downstep, TRN.empty]

Culminativity: a single [-raised] is culminative.

theorem Tone.double_l_not_culminative : ¬IsCulminative [TRN.downstep, TRN.downstep]

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

Monotonicity (catathesis-blocking)

@[implicit_reducible]

instance Tone.instPreorderTRN : Preorder TRN

TRN order by syntagmatic pitch effect: t₁ ≤ t₂ iff t₁ is at least as lowering as t₂. Lifted from the Int order along TRN.pitchEffect (Preorder.lift) — a Preorder, not a PartialOrder, since TRNs sharing a [raised] value share a pitch effect.

Equations

• Tone.instPreorderTRN = Preorder.lift Tone.TRN.pitchEffect

@[implicit_reducible]

instance Tone.instDecidableRelTRNLe : DecidableRel fun (x1 x2 : TRN) => x1 ≤ x2

Equations

• Tone.instDecidableRelTRNLe x✝¹ x✝ = x✝¹.pitchEffect.decLe x✝.pitchEffect

theorem Tone.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 ([BP86]): when an ip boundary resets the register, subsequent pitches are higher than if catathesis had continued from a compressed baseline.

theorem Tone.realizePitch_mono {ts₁ ts₂ : List TRN} (hts : List.Forall₂ (fun (x1 x2 : TRN) => x1 ≤ x2) 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.