Jardine (2017): tone-association patterns as forbidden subgraphs

[Jar17b]

[Jar17b] argues that tone-association patterns over autosegmental representations are computationally local in a well-defined sense: each pattern's well-formedness can be specified by a finite set of forbidden connected subgraphs. An AR is well-formed under a grammar {¬ F₁, ..., ¬ Fₙ} iff none of the Fᵢ embeds into it.

This gives a restrictive theory of tonal well-formedness that:

• makes clear typological predictions (the paper covers Mende, Hausa, Northern Karanga Shona, Kukuya, Hirosaki Japanese);
• contrasts with derivational/global accounts (*VαCVβ constraints, directionality parameters) which can overgenerate;
• admits a learning algorithm based on "scanning window" inspection.

Coverage

This file formalises §3.1 + §5.1 of [Jar17b]: the Mende right-edge multiple-association pattern and the contrasting Hausa left-edge pattern. Hirosaki Japanese (§5.3), Northern Karanga Shona (§5.1's second half), and Kukuya (§5.2) are sketched in the docstring as future extensions — each follows the same Graph- based forbidden-subgraph schema.

Second consumer of Autosegmental.Graph after Studies/LaoideKemp2026.lean. Exercises the SubgraphEmbeds predicate (precedence-preserving translation embedding), which Laoide-Kemp doesn't touch.

Main definitions

• Tone, TBU — label types for the tonal and timing tiers.
• AR — Graph Tone TBU, an autosegmental representation in Jardine's sense.
• Mende.attested — three worked Mende ARs from [Jar17b] eq. (5): mbû ('owl', HL contour on 1σ), ngìlà ('dog', H L on 2σ), félàmà ('junction', HLL with L-spread on 3σ).
• Mende.forbidden_* — three forbidden subgraphs from eq. (21): non-final H spreading, non-final L spreading, non-final contour.
• Hausa.attested — Hausa ARs with left-edge multiple association (eq. 7).
• Hausa.forbidden_* — non-initial spreading + non-initial contour (eq. 22).
• Per-attested-form theorems: each attested AR does NOT contain any forbidden subgraph.

Convention

Jardine 2017 draws forbidden subgraphs with explicit H→L precedence arrows on the tone tier and σ→σ arrows on the TBU tier. In Graph Tone TBU, precedence is implicit in list order: the upper tier is List Tone, the lower is List TBU. The SubgraphEmbeds predicate captures the paper's connected-subgraph embedding by requiring a translation mapping (consecutive positions in F map to consecutive positions in G).

§1 Label types

Jardine 2017 uses H and L for tones and σ (syllable) or μ (mora) for tone-bearing units, plus # for tier boundaries. Boundaries (#) appear in some grammars (e.g., Northern Karanga Shona eq. (24)) but not in the Mende/Hausa grammars formalised here; we include the constructor for future extensions.

inductive Jardine2017.Tone : Type

Tonal-tier label.

• H : Tone
• L : Tone
• bdry : Tone

  Word/tier boundary marker (#). Used by some grammars (e.g., Northern Karanga Shona in [Jar17b] eq. 24); not used in the Mende/Hausa formalisations below.

@[instance_reducible]

instance Jardine2017.instDecidableEqTone : DecidableEq Tone

Equations

• Jardine2017.instDecidableEqTone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Jardine2017.instReprTone : Repr Tone

Equations

• Jardine2017.instReprTone = { reprPrec := Jardine2017.instReprTone.repr }

def Jardine2017.instReprTone.repr : Tone → ℕ → Std.Format

Equations

• Jardine2017.instReprTone.repr Jardine2017.Tone.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2017.Tone.H")).group prec✝
• Jardine2017.instReprTone.repr Jardine2017.Tone.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2017.Tone.L")).group prec✝
• Jardine2017.instReprTone.repr Jardine2017.Tone.bdry prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2017.Tone.bdry")).group prec✝

inductive Jardine2017.TBU : Type

Tone-bearing unit label. Most patterns in [Jar17b] use the syllable σ; Hirosaki Japanese (§5.3) uses the mora μ.

• σ : TBU
• μ : TBU
• bdry : TBU

  TBU-tier boundary marker.

@[instance_reducible]

instance Jardine2017.instDecidableEqTBU : DecidableEq TBU

Equations

• Jardine2017.instDecidableEqTBU x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Jardine2017.instReprTBU.repr : TBU → ℕ → Std.Format

Equations

• Jardine2017.instReprTBU.repr Jardine2017.TBU.σ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2017.TBU.σ")).group prec✝
• Jardine2017.instReprTBU.repr Jardine2017.TBU.μ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2017.TBU.μ")).group prec✝
• Jardine2017.instReprTBU.repr Jardine2017.TBU.bdry prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Jardine2017.TBU.bdry")).group prec✝

@[instance_reducible]

instance Jardine2017.instReprTBU : Repr TBU

Equations

• Jardine2017.instReprTBU = { reprPrec := Jardine2017.instReprTBU.repr }

@[reducible, inline]

abbrev Jardine2017.ARep : Type (u_1 + 1)

An autosegmental representation in Jardine 2017's sense, on the graph foundation: tones over TBUs (with implicit precedence by position), links as association lines.

Equations

• Jardine2017.ARep = Autosegmental.AR Sigma.fst

def Jardine2017.mkL (links : List (ℕ × ℕ)) (i j : Bool) (p q : ℕ) : Prop

Link presentations from finite pair lists (melody position, TBU position).

Equations

• Jardine2017.mkL links i j p q = (i = true ∧ j = false ∧ (p, q) ∈ links)

@[instance_reducible]

instance Jardine2017.instDecidableMkL (links : List (ℕ × ℕ)) (i j : Bool) (p q : ℕ) : Decidable (mkL links i j p q)

Equations

• Jardine2017.instDecidableMkL links i j p q = Jardine2017.instDecidableMkL._aux_1 links i j p q

@[reducible, inline]

abbrev Jardine2017.mk (tones : List Tone) (tbus : List TBU) (links : List (ℕ × ℕ)) : ARep

Build a representation from a tone melody, a TBU string, and links.

Equations

• Jardine2017.mk tones tbus links = Autosegmental.AR.ofData (fun (b : Bool) => match b with | true => tones | false => tbus) (Jardine2017.mkL links)

theorem Jardine2017.mk_embeds_iff {tF tX : List Tone} {bF bX : List TBU} {lF lX : List (ℕ × ℕ)} : Autosegmental.AR.FactorEmbeds (mk tF bF lF) (mk tX bX lX) ↔ Autosegmental.dataEmbeds (fun (b : Bool) => match b with | true => tF | false => bF) (fun (b : Bool) => match b with | true => tX | false => bX) (mkL lF) (mkL lX)

Non-embedding verdicts compute: the spec plus kernel evaluation.

§2 Mende: right-edge multiple association

[Jar17b] §3.1, eq. (5)

In Mende, tonal plateaus (a single tone associated to multiple syllables) and contour tones (multiple tones on one syllable) are restricted to the right word edge.

@[reducible, inline]

abbrev Jardine2017.Mende.mbû : ARep

mbû 'owl' (1σ, HL contour).

Equations

• Jardine2017.Mende.mbû = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ] [(0, 0), (1, 0)]

@[reducible, inline]

abbrev Jardine2017.Mende.ngìlà : ARep

ngìlà 'dog' (2σ, HL melody, one tone per syllable).

Equations

• Jardine2017.Mende.ngìlà = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Mende.félàmà : ARep

félàmà 'junction' (3σ, HL melody with L-spread to the right two syllables: HLL surface). The diagnostic case for Mende.

Equations

• Jardine2017.Mende.félàmà = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (1, 1), (1, 2)]

@[reducible, inline]

abbrev Jardine2017.Mende.forbidden_nonfinal_H : ARep

(21a) non-final H spreading: an H linked to two consecutive σs with an L following on the tonal tier.

Equations

• Jardine2017.Mende.forbidden_nonfinal_H = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (0, 1)]

@[reducible, inline]

abbrev Jardine2017.Mende.forbidden_nonfinal_L : ARep

(21b) non-final L spreading (mirror).

Equations

• Jardine2017.Mende.forbidden_nonfinal_L = Jardine2017.mk [Jardine2017.Tone.L, Jardine2017.Tone.H] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (0, 1)]

@[reducible, inline]

abbrev Jardine2017.Mende.forbidden_nonfinal_contour : ARep

(21c) non-final contour: an HL contour on a σ with another σ following.

Equations

• Jardine2017.Mende.forbidden_nonfinal_contour = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (1, 0)]

§2.2 Attested forms satisfy the Mende grammar ([Jar17b] §5.1)

theorem Jardine2017.Mende.mbû_no_nonfinal_H : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_H mbû

theorem Jardine2017.Mende.mbû_no_nonfinal_L : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_L mbû

theorem Jardine2017.Mende.mbû_no_nonfinal_contour : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_contour mbû

theorem Jardine2017.Mende.ngìlà_no_nonfinal_H : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_H ngìlà

theorem Jardine2017.Mende.ngìlà_no_nonfinal_L : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_L ngìlà

theorem Jardine2017.Mende.ngìlà_no_nonfinal_contour : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_contour ngìlà

theorem Jardine2017.Mende.félàmà_no_nonfinal_H : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_H félàmà

theorem Jardine2017.Mende.félàmà_no_nonfinal_L : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_L félàmà

theorem Jardine2017.Mende.félàmà_no_nonfinal_contour : ¬Autosegmental.AR.FactorEmbeds forbidden_nonfinal_contour félàmà

§3 Hausa: left-edge multiple association ([Jar17b] eq. (7), (22))

@[reducible, inline]

abbrev Jardine2017.Hausa.fáadi : ARep

fáadi 'fall' (2σ, HL melody one-to-one).

Equations

• Jardine2017.Hausa.fáadi = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Hausa.háantúnàa : ARep

háantúnàa 'noses' (3σ, HHL — H spreads at the left edge).

Equations

• Jardine2017.Hausa.háantúnàa = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 0), (0, 1), (1, 2)]

@[reducible, inline]

abbrev Jardine2017.Hausa.forbidden_noninitial_H : ARep

(22a) non-initial H spreading: an L preceding an H linked to two σs.

Equations

• Jardine2017.Hausa.forbidden_noninitial_H = Jardine2017.mk [Jardine2017.Tone.L, Jardine2017.Tone.H] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(1, 0), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Hausa.forbidden_noninitial_L : ARep

(22b) non-initial L spreading (mirror).

Equations

• Jardine2017.Hausa.forbidden_noninitial_L = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(1, 0), (1, 1)]

@[reducible, inline]

abbrev Jardine2017.Hausa.forbidden_noninitial_contour : ARep

(22c) non-initial contour: a σ preceded by another σ, bearing an HL contour.

Equations

• Jardine2017.Hausa.forbidden_noninitial_contour = Jardine2017.mk [Jardine2017.Tone.H, Jardine2017.Tone.L] [Jardine2017.TBU.σ, Jardine2017.TBU.σ] [(0, 1), (1, 1)]

§3.2 Attested Hausa forms satisfy the Hausa grammar

theorem Jardine2017.Hausa.fáadi_no_noninitial_H : ¬Autosegmental.AR.FactorEmbeds forbidden_noninitial_H fáadi

theorem Jardine2017.Hausa.fáadi_no_noninitial_L : ¬Autosegmental.AR.FactorEmbeds forbidden_noninitial_L fáadi

theorem Jardine2017.Hausa.fáadi_no_noninitial_contour : ¬Autosegmental.AR.FactorEmbeds forbidden_noninitial_contour fáadi

theorem Jardine2017.Hausa.háantúnàa_no_noninitial_H : ¬Autosegmental.AR.FactorEmbeds forbidden_noninitial_H háantúnàa

theorem Jardine2017.Hausa.háantúnàa_no_noninitial_L : ¬Autosegmental.AR.FactorEmbeds forbidden_noninitial_L háantúnàa

theorem Jardine2017.Hausa.háantúnàa_no_noninitial_contour : ¬Autosegmental.AR.FactorEmbeds forbidden_noninitial_contour háantúnàa

§4 The Mende/Hausa contrast: same shape, opposite edges

[Jar17b] §3.1 and §5.1

Mende's félàmà (HLL on 3σ, L-spread at right edge) is exactly the kind of pattern Hausa's grammar would forbid (its mirror is a non-initial L spread). Conversely, Hausa's háantúnàa (HHL on 3σ, H-spread at left edge) is exactly what Mende's grammar forbids.

This pair makes Jardine's locality thesis concrete: each language's grammar is a finite set of forbidden subgraphs, and the difference between Mende and Hausa is the side of the word edge to which the prohibition applies.

theorem Jardine2017.hausa_haantunaa_violates_mende : Autosegmental.AR.FactorEmbeds Mende.forbidden_nonfinal_H Hausa.háantúnàa

The Hausa attested form háantúnàa (HHL = H-spread to first 2σ) contains exactly the structural pattern that Mende's grammar forbids: non-final H spreading. This makes Mende and Hausa mutually exclusive on their diagnostic forms.

theorem Jardine2017.mende_felama_violates_hausa : Autosegmental.AR.FactorEmbeds Hausa.forbidden_noninitial_L Mende.félàmà

Symmetrically, Mende's félàmà (HLL = L-spread to last 2σ) contains Hausa's forbidden non-initial-L pattern.

§5 Future extensions

The paper covers three further patterns not formalised here. Each extends the same Graph-based forbidden-subgraph schema and would be a natural addition to this file.

• Northern Karanga Shona (§5.1 second half, eq. 23-28): a positional pattern where the leftmost H of a verb stem spreads maximally as far as the third syllable; medial L blocks multiple-H association. Grammar (24) uses boundary symbols (#) on both tiers; the Tone.bdry and TBU.bdry constructors are in place for this extension.

• Kukuya (§5.2, eq. 30-33): a quality-sensitive pattern where H tones cannot multiply associate in the presence of L, while L can spread freely. Encoded as the conjunction of Mende-grammar forbidden subgraphs (for non-final H association) and Hausa-grammar forbidden subgraphs (for non-initial H association), plus a non-final-contour ban.

• Hirosaki Japanese (§5.3, eq. 35-38): a culminativity constraint: at most one H per word, F (falling) only word-finally, H never spreads to multiple TBUs (here moras μ, not syllables). Demonstrates that the Graph substrate handles arbitrary TBU types (the TBU.μ constructor is already in place).

The deferred items are all ≤ 100 LOC each in the same shape as the Mende/Hausa above: enumerate attested forms, enumerate forbidden subgraphs, prove non-embedding by decide. They can be added incrementally as needed.