Lionnet (2022): The features and geometry of tone in Laal

[Lio22b]

Laal (isolate, southern Chad) has three contrastive tone heights H/M/L. Lionnet argues for a subtonal analysis à la [Yip80]/[Pul86] (two register features [±upper], [±raised]) linked to a Tonal Root Node ([Sni20]): H = [+upper, −raised], M = [−upper, +raised], L = [−upper, −raised], with the fourth combination [+upper, +raised] the systematic gap. This featural specification gives a unified account of the otherwise-puzzling Mid tone — its exclusivity (*MX/XM) and its instability (M-lowering).

What this formalizes

• §5.1 the featural analysis — the substrate TRN.H/M/L encode Lionnet's (51).
• §3 M-exclusivity (*MX/XM) over the attested stem melodies.
• §5.2 M-lowering as [−raised] assimilation (subtonalAssimilate): a [−raised] trigger (H or L) turns the only [+raised] tone, M, into L.
• §5.5 the ventive suffix as a floating [−raised] with [upper] from the root (dockFloating).
• §5.6 the [+upper, +raised] gap (Table-4 type-A system).
• §5.2 (ex. 53–55, 58) the optional OCP-[raised] merger — consuming the OCP fusion repair.

What this does NOT formalize

• §6.1–6.3 base-pattern reduction, replacive full-tone spread, and high-tone spread (the full-TRN spreading/deletion processes), and the vowel-harmony patterns of §2 — these need the broader autosegmental spreading machinery.
• §7 the alternatives (tone-as-unit, M-as-zero).

Honest scope notes

M-lowering proper is [−raised] assimilation, not OCP-merger; and *MX/XM is an agreement constraint (*[α raised][β raised]), the opposite of the identity-OCP. The OCP API is consumed only for the merger of (53–55)/(58), which Lionnet presents explicitly as optional ("not necessary in the present analysis" / "or fusion"). It is included because it is the merger face of the same OCP principle whose prohibition face lives in OCP.

The subtonal featural analysis (§5.1)

def Lionnet2022Laal.toneToTRN : Laal.Prosody.Tone → Tone.TRN

Lionnet's featural analysis (ex. 51) as a map into the register-tier TRN encoding: H = [+upper, −raised], M = [−upper, +raised], L = [−upper, −raised].

Equations

• Lionnet2022Laal.toneToTRN Laal.Prosody.Tone.H = Tone.TRN.H
• Lionnet2022Laal.toneToTRN Laal.Prosody.Tone.M = Tone.TRN.M
• Lionnet2022Laal.toneToTRN Laal.Prosody.Tone.L = Tone.TRN.L

theorem Lionnet2022Laal.featural_analysis : Tone.TRN.H = { upper := some true, raised := some false } ∧ Tone.TRN.M = { upper := some false, raised := some true } ∧ Tone.TRN.L = { upper := some false, raised := some false }

The substrate TRN.H/M/L encode exactly Lionnet's (51) feature matrix.

theorem Lionnet2022Laal.tones_distinct_as_TRN : (List.map toneToTRN [Laal.Prosody.Tone.H, Laal.Prosody.Tone.M, Laal.Prosody.Tone.L]).Nodup

The three tones are featurally distinct — the analysis distinguishes them.

theorem Lionnet2022Laal.minimalTriplet_distinct_tones : (List.map (fun (x : Laal.Prosody.StemEntry) => x.melody) Laal.Prosody.minimalTriplet).Nodup

The minimal triplet (ex. 8) contrasts in tone alone: pairwise-distinct melodies on one segmental frame.

M-exclusivity: *MX/XM (§3)

theorem Lionnet2022Laal.M_exclusive (m : List Laal.Prosody.Tone) : m ∈ Laal.Prosody.attestedMelodies → Laal.Prosody.Tone.M ∈ m → ∀ t ∈ m, t = Laal.Prosody.Tone.M

M-exclusivity (*MX/XM): in every attested stem melody, if M occurs then the melody is all M — M never co-occurs with a different tone at stem level.

M-lowering as [−raised] assimilation (§5.2)

theorem Lionnet2022Laal.mLowering_from_L : Tone.subtonalAssimilate Tone.Subtonal.raised Tone.TRN.L Tone.TRN.M = Tone.TRN.L

M-lowering is [−raised] assimilation: an L trigger ([−raised]) spreads its [raised] value onto M (the only [+raised] tone), turning it into L.

theorem Lionnet2022Laal.mLowering_from_H : Tone.subtonalAssimilate Tone.Subtonal.raised Tone.TRN.H Tone.TRN.M = Tone.TRN.L

M-lowering from a [−raised] H trigger likewise turns M into L.

theorem Lionnet2022Laal.H_stable : Tone.subtonalAssimilate Tone.Subtonal.raised Tone.TRN.L Tone.TRN.H = Tone.TRN.H

Only M is targeted: H is inert under [−raised] assimilation (already [−raised]), explaining why H- and L-toned roots never lower.

theorem Lionnet2022Laal.L_stable : Tone.subtonalAssimilate Tone.Subtonal.raised Tone.TRN.H Tone.TRN.L = Tone.TRN.L

L is likewise inert under [−raised] assimilation.

The ventive suffix (§5.5)

theorem Lionnet2022Laal.ventive_after_H : Tone.dockFloating Tone.Subtonal.raised false Tone.TRN.H = Tone.TRN.H

The ventive suffix (ex. 60) is a floating [−raised] feature with [upper] inherited from the root: dockFloating .raised false. It surfaces as H after a [+upper] (H) root and as L after [−upper] (M or L) roots — the M-lowering realisation kárá/dàgà/jàrà.

theorem Lionnet2022Laal.ventive_after_M : Tone.dockFloating Tone.Subtonal.raised false Tone.TRN.M = Tone.TRN.L

theorem Lionnet2022Laal.ventive_after_L : Tone.dockFloating Tone.Subtonal.raised false Tone.TRN.L = Tone.TRN.L

The [+upper, +raised] gap (§5.6)

def Lionnet2022Laal.laalToneInventory : List Tone.TRN

The Laal tone inventory, as TRNs.

Equations

• Lionnet2022Laal.laalToneInventory = List.map Lionnet2022Laal.toneToTRN [Laal.Prosody.Tone.H, Laal.Prosody.Tone.M, Laal.Prosody.Tone.L]

theorem Lionnet2022Laal.superHigh_is_the_gap : Tone.TRN.superHigh ∉ laalToneInventory

The fourth feature combination [+upper, +raised] (TRN.superHigh) is absent: it is the systematic gap that makes Laal a Table-4 type-A system (§5.6).

The optional OCP-[raised] merger (§5.2, ex. 53–55, 58)

theorem Lionnet2022Laal.ocp_raised_merge_LL : OCP.collapse [Tone.TRN.L, Tone.TRN.L] = [Tone.TRN.L]

Lionnet (ex. 54–55, 58) notes — but explicitly does not adopt — an optional OCP-[raised] economy under which two adjacent identical [−raised] autosegments fuse into one multiply-linked autosegment. When two adjacent tones are fully identical, that fusion is OCP.collapse: two adjacent L tones collapse to one.

theorem Lionnet2022Laal.ocp_raised_is_tier_relative : ¬OCP.IsCleanOn (fun (x : Tone.TRN) => True) (fun (x : Tone.TRN) => x.raised) [Tone.TRN.H, Tone.TRN.L] ∧ OCP.IsClean [Tone.TRN.H, Tone.TRN.L]

OCP-[raised] is tier-relative ([CJ19]): it constrains the [raised]-projected tier (IsCleanOn reading .raised), not whole TRNs. H and L are distinct tones but both [−raised], so adjacent they violate OCP-[raised] even though [TRN.H, TRN.L] is clean as a whole-TRN tier.

theorem Lionnet2022Laal.ocp_raised_merge_clean (tier : List Tone.TRN) : OCP.IsClean (OCP.collapse (List.map (fun (x : Tone.TRN) => x.raised) tier))

Under the optional economy, fusing adjacent identical [raised] autosegments leaves the [raised]-projected tier OCP-clean — the faithful tier-relative reading of Lionnet (ex. 54–55, 58), via the substrate retraction collapse_clean. The merger face of the same OCP principle whose prohibition (TSL₂) face lives in OCP.

The register-tier geometry on the multi-tier substrate (§5–§6)

[Lio22a]'s geometry (ex. 52) is a hub-and-spoke around the Tonal Root Node: the [±upper] register tier, the [±raised] tier, and the mora (TBU) tier each associate to the TRN. On the general substrate Autosegmental.MultiAR this is a four-tier graph. Its point over the TRN bundle used above: each subtonal feature is a tier of its own, so it can be manipulated independently of the whole TRN — [Lio22a]'s partial activity (§5, e.g. [−raised] assimilation) — which a bundled TRN record cannot structurally express. Whole-TRN operations (§6) act on the TRN↔mora layer; both live on one object.

@[reducible, inline]

abbrev Lionnet2022Laal.laalTier : Fin 4 → Type

The four Laal tone tiers: [±upper] register, [±raised], the TRN, the mora.

Equations

• Lionnet2022Laal.laalTier = ![Option Bool, Option Bool, Unit, Unit]

def Lionnet2022Laal.mForm : Autosegmental.MultiAR laalTier

A one-TRN M-toned form (M = [−upper, +raised], [Lio22a] ex. 51): the register [−upper] and [+raised] features and the single mora each associate to the one TRN.

Equations

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

theorem Lionnet2022Laal.mForm_planar : mForm.IsPlanar

The form is planar — each spoke's single association is non-crossing (per-pair NCC).

def Lionnet2022Laal.delinkRaised (G : Autosegmental.MultiAR laalTier) : Autosegmental.MultiAR laalTier

Partial activity (§5): delinking the [−raised] feature acts on the [raised]↔TRN layer (tier-pair (1,2)) alone.

Equations

• Lionnet2022Laal.delinkRaised G = { toMultiGraph := have __src := G.toMultiGraph; { tiers := __src.tiers, links := Lionnet2022Laal.delinkedLinks✝ G }, inBounds := ⋯ }

theorem Lionnet2022Laal.partial_indep_of_full (G : Autosegmental.MultiAR laalTier) : (delinkRaised G).links 2 3 = G.links 2 3

Delinking the subtonal [−raised] feature leaves the whole-TRN layer (TRN↔mora, tier-pair (2,3)) untouched: partial activity is independent of full activity — the structural content of [Lio22a]'s subtonal-feature autonomy, impossible to state on a bundled TRN.

theorem Lionnet2022Laal.delinkRaised_erases (G : Autosegmental.MultiAR laalTier) : (delinkRaised G).links 1 2 = ∅

And it does remove the [raised]↔TRN association.