Hausa Tone — mathlib-style

[New00] [Ink98]

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 ([New00] ch. 71).

Architectural shape

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

• Tone.TRN is the underlying autosegmental primitive; HausaTone is a surface inventory whose decomposition is given by toAutoseg.
• Tone.GTSpec is the GT-trigger type. Hausa uses two of [Rol18]'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 Hausa.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 Hausa.instDecidableEqHausaTone : DecidableEq HausaTone

Equations

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

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

Equations

• Hausa.instReprHausaTone.repr Hausa.HausaTone.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.HausaTone.H")).group prec✝
• Hausa.instReprHausaTone.repr Hausa.HausaTone.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.HausaTone.L")).group prec✝
• Hausa.instReprHausaTone.repr Hausa.HausaTone.F prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.HausaTone.F")).group prec✝

@[implicit_reducible]

instance Hausa.instReprHausaTone : Repr HausaTone

Equations

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

@[implicit_reducible]

instance Hausa.instInhabitedHausaTone : Inhabited HausaTone

Equations

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

def Hausa.HausaTone.all : List HausaTone

The surface inventory in canonical order.

Equations

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

def Hausa.HausaTone.toAutoseg : HausaTone → List Tone.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

• Hausa.HausaTone.H.toAutoseg = [Tone.TRN.H]
• Hausa.HausaTone.L.toAutoseg = [Tone.TRN.L]
• Hausa.HausaTone.F.toAutoseg = [Tone.TRN.H, Tone.TRN.L]

theorem Hausa.no_rising_contour (t : HausaTone) : t ∈ HausaTone.all → t.toAutoseg.head? = some Tone.TRN.H ∨ t.toAutoseg.head? = some Tone.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 ([New00] §71.1).

def Hausa.polarOf : Tone.TRN → Tone.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 [Rol18] (GTOperation.polarization); we derive its behaviour structurally.

Equations

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

theorem Hausa.polarOf_involutive_on_HL (t : Tone.TRN) : t ∈ [Tone.TRN.H, Tone.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 Hausa.mkReplacive (name : String) (melody : Tone.TonalMelody) : Tone.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 Hausa.mkNeutral (name : String) (melody : Tone.TonalMelody) : Tone.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 Hausa.pluralTemplate : Tone.GTSpec

The Hausa plural template -ōoCíi imposes an all-H melody on the base, regardless of the lexical tone of the singular ([Ink98], [New00] §56.4). The paradigmatic case of replacive-dominant GT.

Equations

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

def Hausa.referentialClitic : Tone.GTSpec

The Hausa referential clitic -ⁿn attaches a floating L to the host without overwriting lexical tones ([New00] §31.5). The paradigmatic case of neutral GT in Hausa.

Equations

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

def Hausa.hausaGTs : List Tone.GTSpec

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

Equations

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

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

Hausa uses only the dominant/neutral cells of the GT typology. Of [Rol18]'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 Hausa.demoStem : List (Tone.TBU Unit)

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

Equations

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