Hausa Tone — mathlib-style

@cite{newman-2000} @cite{inkelas-1998}

Hausa is a register tone language with a two-level lexical contrast (H, L) and a derived falling contour (F = HL on a single TBU). There is no rising contour: a low followed by a high on adjacent TBUs realises as L H, never as a rising tone on one TBU (@cite{newman-2000} ch. 71).

Architectural shape

This file is the interpretation of two existing Theory interfaces in Hausa, not a parallel hierarchy:

• Phonology.Autosegmental.RegisterTier.TRN is the underlying autosegmental primitive; HausaTone is a surface inventory whose decomposition is given by toAutoseg.
• Phonology.Autosegmental.GrammaticalTone.GTSpec is the GT-trigger type. Hausa uses two of @cite{rolle-2018}'s six dominance cells — replacive-dominant and neutral. We expose smart constructors mkReplacive/mkNeutral that fix the other GTSpec fields to the Hausa defaults, register the morphemes in hausaGTs, and prove the typological signature as a universal theorem.

Per-cell facts (e.g. the plural template is dominant) appear as examples — corollaries of the smart-constructor lemmas.

inductive Fragments.Hausa.Tone.HausaTone : Type

Surface tones on a Hausa TBU (= mora). The contour F is realised only on heavy (bimoraic) syllables and decomposes as H+L on the autosegmental tier. There is no R (rising) tone: the prediction is that no Hausa surface form exhibits a single-TBU rising contour.

• H : HausaTone
• L : HausaTone
• F : HausaTone

@[implicit_reducible]

instance Fragments.Hausa.Tone.instDecidableEqHausaTone : DecidableEq HausaTone

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Tone.instReprHausaTone : Repr HausaTone

Equations

• Fragments.Hausa.Tone.instReprHausaTone = { reprPrec := Fragments.Hausa.Tone.instReprHausaTone.repr }

def Fragments.Hausa.Tone.instReprHausaTone.repr : HausaTone → ℕ → Std.Format

Equations

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

def Fragments.Hausa.Tone.instInhabitedHausaTone.default : HausaTone

Equations

• Fragments.Hausa.Tone.instInhabitedHausaTone.default = Fragments.Hausa.Tone.HausaTone.H

@[implicit_reducible]

instance Fragments.Hausa.Tone.instInhabitedHausaTone : Inhabited HausaTone

Equations

• Fragments.Hausa.Tone.instInhabitedHausaTone = { default := Fragments.Hausa.Tone.instInhabitedHausaTone.default }

def Fragments.Hausa.Tone.HausaTone.all : List HausaTone

The surface inventory in canonical order.

Equations

• Fragments.Hausa.Tone.HausaTone.all = [Fragments.Hausa.Tone.HausaTone.H, Fragments.Hausa.Tone.HausaTone.L, Fragments.Hausa.Tone.HausaTone.F]

def Fragments.Hausa.Tone.HausaTone.toAutoseg : HausaTone → List Phonology.Autosegmental.RegisterTier.TRN

Project a Hausa surface tone to its autosegmental decomposition on the underlying tone tier. The falling contour decomposes to [H, L], a level tone to a singleton.

Equations

• Fragments.Hausa.Tone.HausaTone.H.toAutoseg = [Phonology.Autosegmental.RegisterTier.TRN.H]
• Fragments.Hausa.Tone.HausaTone.L.toAutoseg = [Phonology.Autosegmental.RegisterTier.TRN.L]
• Fragments.Hausa.Tone.HausaTone.F.toAutoseg = [Phonology.Autosegmental.RegisterTier.TRN.H, Phonology.Autosegmental.RegisterTier.TRN.L]

theorem Fragments.Hausa.Tone.no_rising_contour (t : HausaTone) : t ∈ HausaTone.all → t.toAutoseg.head? = some Phonology.Autosegmental.RegisterTier.TRN.H ∨ t.toAutoseg.head? = some Phonology.Autosegmental.RegisterTier.TRN.L

No rising contour. Every surface tone in the Hausa inventory begins with H or L on the autosegmental tier. A rising tone would have to begin with L and continue to H on the same TBU; the inventory provides no such cell (@cite{newman-2000} §71.1).

def Fragments.Hausa.Tone.polarOf : Phonology.Autosegmental.RegisterTier.TRN → Phonology.Autosegmental.RegisterTier.TRN

Tonal polarity: a morpheme surfaces with the opposite tone of its host. The classic Hausa case is the linker -n of the genitive construction, which is L after a H-final host and H after a L-final host. Polarity is one of the named operations in @cite{rolle-2018} (GTOperation.polarization); we derive its behaviour structurally.

Equations

• Fragments.Hausa.Tone.polarOf { upper := some true, raised := some false } = Phonology.Autosegmental.RegisterTier.TRN.L
• Fragments.Hausa.Tone.polarOf x✝ = Phonology.Autosegmental.RegisterTier.TRN.H

theorem Fragments.Hausa.Tone.polarOf_involutive_on_HL (t : Phonology.Autosegmental.RegisterTier.TRN) : t ∈ [Phonology.Autosegmental.RegisterTier.TRN.H, Phonology.Autosegmental.RegisterTier.TRN.L] → polarOf (polarOf t) = t

Polarity is involutive on the H/L sublattice. This is what licenses polarity as a "natural" tonal operation: the linker -n swaps H and L, and applying the swap twice returns to the original.

def Fragments.Hausa.Tone.mkReplacive (name : String) (melody : Phonology.Autosegmental.GrammaticalTone.TonalMelody) : Phonology.Autosegmental.GrammaticalTone.GTSpec

Build a replacive-dominant word-level GTSpec from a name and melody. Hausa's morphological tonal templates (the plural template, the genitive linker, ...) all share these defaults: a whole valuation window, word-level GT, and auxiliary exponence (the template co-occurs with segmental material).

Equations

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

def Fragments.Hausa.Tone.mkNeutral (name : String) (melody : Phonology.Autosegmental.GrammaticalTone.TonalMelody) : Phonology.Autosegmental.GrammaticalTone.GTSpec

Build a neutral word-level GTSpec from a name and melody. Used for floating-tone clitics whose melody concatenates with the host's underlying tones rather than overwriting them.

Equations

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

def Fragments.Hausa.Tone.pluralTemplate : Phonology.Autosegmental.GrammaticalTone.GTSpec

The Hausa plural template -ōoCíi imposes an all-H melody on the base, regardless of the lexical tone of the singular (@cite{inkelas-1998}, @cite{newman-2000} §56.4). The paradigmatic case of replacive-dominant GT.

Equations

• Fragments.Hausa.Tone.pluralTemplate = Fragments.Hausa.Tone.mkReplacive "PL.-ōoCíi" [Phonology.Autosegmental.RegisterTier.TRN.H]

def Fragments.Hausa.Tone.referentialClitic : Phonology.Autosegmental.GrammaticalTone.GTSpec

The Hausa referential clitic -ⁿn attaches a floating L to the host without overwriting lexical tones (@cite{newman-2000} §31.5). The paradigmatic case of neutral GT in Hausa.

Equations

• Fragments.Hausa.Tone.referentialClitic = Fragments.Hausa.Tone.mkNeutral "REF.-ⁿn" [Phonology.Autosegmental.RegisterTier.TRN.L]

def Fragments.Hausa.Tone.hausaGTs : List Phonology.Autosegmental.GrammaticalTone.GTSpec

The morphological-tone registry: every Hausa GT trigger we formalise. Universal theorems below quantify over this list.

Equations

• Fragments.Hausa.Tone.hausaGTs = [Fragments.Hausa.Tone.pluralTemplate, Fragments.Hausa.Tone.referentialClitic]

theorem Fragments.Hausa.Tone.hausa_dominance_is_replacive_or_neutral (s : Phonology.Autosegmental.GrammaticalTone.GTSpec) : s ∈ hausaGTs → s.dominance = Phonology.Autosegmental.GrammaticalTone.GTDominance.replaciveDominant ∨ s.dominance = Phonology.Autosegmental.GrammaticalTone.GTDominance.neutral

Hausa uses only the dominant/neutral cells of the GT typology. Of @cite{rolle-2018}'s six dominance categories, Hausa morphological tone occupies exactly two: replacive-dominant (templates) and neutral (floating clitics). No subtractive, additive, melodic, or recessive GT is attested.

def Fragments.Hausa.Tone.demoStem : List (Phonology.Autosegmental.GrammaticalTone.TBU Unit)

Concrete demonstration: an all-L disyllabic stem is overwritten to H on every TBU under the plural template.

Equations

• Fragments.Hausa.Tone.demoStem = [{ seg := (), tone := Phonology.Autosegmental.RegisterTier.TRN.L }, { seg := (), tone := Phonology.Autosegmental.RegisterTier.TRN.L }]