Unbounded tonal plateauing

Hyman and Katamba's plateauing rule for Luganda makes every tone-bearing unit between two H-toned units surface H. Over Jardine's string rendering, a word over TBU records each timing unit's association state (H associated to a H tone, O unassociated), and utp, a Tone.Surfacing process, rewrites it pointwise by its surfacing predicate, the two-sided window H ∈ w.take (i + 1) ∧ H ∈ w.drop i asking for an H at or before i and one at or after it. The map is utp.map, the surfacing set plateau.

What surfaces is the representation. The string reads back into two-tier autosegmental representations by TBU.toAR, and the output representation plateauAR w is the OCP-merged input, hull-closed — fusion then spreading. Timing slot i surfaces with H in plateauAR w exactly when utp.Surfaces w i (utp.surfaces_iff_surfacesWith_plateauAR).

The map is the flagship unbounded circumambient process: whether a position changes depends on unboundedly distant material on both sides, in the strong witness form utp.requiresBothSides — perturbing either far side alone reverts the change — with the weaker utp.twoSidedUnboundedDependence as a corollary. Studies/MeinhardtEtAl2024 excludes the map from the non-interacting bimachines, and Studies/LamontOHaraSmith2019 shows it weakly deterministic in Heinz and Lai's sense.

Main definitions

• Tone.TBU — the H/Ø string alphabet (association states; distinct from Tone.TBUKind, the phonological typology of timing units).
• Tone.TBU.toAR, Tone.plateauAR — the translation of a TBU into a one-slot representation, and the output representation (OCP-merged input, hull-closed).
• Tone.utp — plateauing as a Tone.Surfacing process; utp.map the map.
• Tone.plateau — the set of surfacing positions.

Main results

• utp.surfaces_iff_surfacesWith_plateauAR — surfacing is H-linkedness in the output representation.
• utp.map_getElem?_H_iff / utp.map_getElem?_O_iff — pointwise characterization of the map.
• utp.map_eq_plateau_indicator, plateau_eq_Icc — the output is the indicator word of an interval, from the first trigger to the last.
• utp.map_toneless, utp.map_single, utp.map_plateau — the rule schemata: toneless words and lone Hs are unchanged; everything between the outermost Hs surfaces H.
• utp.map_getElem?_H_of_getElem?_H, utp.map_mono, utp.map_map — plateauing is a closure operator in the pointwise H-order: extensive, monotone, idempotent.
• utp.mem_range_map_iff — the outputs of plateauing are the words without an H O H subsequence.
• utp.requiresBothSides — deleting either flanking H reverts the plateau target, at every distance.

References

• [HK10]
• [Jar16a]

The tone-bearing-unit alphabet

inductive Tone.TBU : Type

A tone-bearing unit's association state is H for a TBU associated to a H tone and O for an unspecified TBU (Jardine's Ø).

• H : TBU
• O : TBU

@[instance_reducible]

instance Tone.instDecidableEqTBU : DecidableEq TBU

Equations

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

@[instance_reducible]

instance Tone.instReprTBU : Repr TBU

Equations

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

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

Equations

• Tone.instReprTBU.repr Tone.TBU.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.TBU.H")).group prec✝
• Tone.instReprTBU.repr Tone.TBU.O prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tone.TBU.O")).group prec✝

The output representation

The string reads back into two-tier representations, and plateauing on representations is OCP-fusion followed by hull-closure of the association lines (Hyman and Katamba's rule as an operation on structures).

def Tone.TBU.melody : TBU → List TRN

A TBU contributes its H tone to the melody if it is H-toned, and nothing otherwise.

Equations

• Tone.TBU.H.melody = [Tone.TRN.H]
• Tone.TBU.O.melody = []

@[simp]

theorem Tone.TBU.melody_H : H.melody = [TRN.H]

@[simp]

theorem Tone.TBU.melody_O : O.melody = []

theorem Tone.TBU.length_melody (a : TBU) : a.melody.length = if a = H then 1 else 0

theorem Tone.TBU.sum_length_melody (w : List TBU) : (List.map (fun (a : TBU) => a.melody.length) w).sum = List.count H w

def Tone.TBU.toAR (a : TBU) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier TRN Unit)

A TBU translates into the primitive with one timing slot carrying the TBU's melody (Jardine's reading of the string as a representation).

Equations

• a.toAR = Autosegmental.AR.primitive a.melody ()

instance Tone.TBU.instFiniteVSigmaBoolTwoTierTRNUnitObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesToAR (a : TBU) : Finite a.toAR.obj.V

@[simp]

theorem Tone.TBU.tierWord_toAR_true (a : TBU) : Autosegmental.AR.tierWord true = a.melody

@[simp]

theorem Tone.TBU.tierWord_toAR_false (a : TBU) : Autosegmental.AR.tierWord false = [()]

@[simp]

theorem Tone.TBU.tierLength_toAR_true (a : TBU) : Autosegmental.AR.tierLength a.toAR true = a.melody.length

@[simp]

theorem Tone.TBU.tierLength_toAR_false (a : TBU) : Autosegmental.AR.tierLength a.toAR false = 1

@[simp]

theorem Tone.TBU.link_toAR (a : TBU) (p q : ℕ) : Autosegmental.AR.link a.toAR true false p q ↔ p < a.melody.length ∧ q = 0

@[simp]

theorem Tone.TBU.tierWord_realize_toAR_true (w : List TBU) : Autosegmental.AR.tierWord true = List.replicate (List.count H w) TRN.H

The melody of a realized string has one H node per H-toned TBU.

@[simp]

theorem Tone.TBU.tierWord_realize_toAR_false (w : List TBU) : Autosegmental.AR.tierWord false = List.replicate w.length ()

The timing tier of a realized string has one slot per TBU.

theorem Tone.TBU.link_realize_toAR (w : List TBU) (p j : ℕ) : Autosegmental.AR.link (Autosegmental.AR.realize toAR w) true false p j ↔ p = List.count H (List.take j w) ∧ w[j]? = some H

In a realized string, slot j links to melody node p exactly when TBU j is H-toned and p is its accumulated melody position.

theorem Tone.TBU.link_collapse_realize_toAR (w : List TBU) (k j : ℕ) : Autosegmental.AR.link (Autosegmental.AR.collapse (Autosegmental.AR.realize toAR w) true) true false k j ↔ k = 0 ∧ w[j]? = some H

In the OCP-merged realization the single fused H node (index 0) links exactly to the H-toned slots.

noncomputable def Tone.plateauAR (w : List TBU) : Autosegmental.TieredAR Bool (Autosegmental.TwoTier TRN Unit)

The output representation, in coordinates, is the OCP-merge and then the hull, both at the melody tier.

Equations

• Tone.plateauAR w = Autosegmental.AR.hull true (Autosegmental.AR.collapse (Autosegmental.AR.realize Tone.TBU.toAR w) true)

instance Tone.instFiniteVSigmaBoolTwoTierTRNUnitObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesPlateauAR (w : List TBU) : Finite (plateauAR w).obj.V

theorem Tone.link_plateauAR (w : List TBU) (k j : ℕ) : Autosegmental.AR.link (plateauAR w) true false k j ↔ k = 0 ∧ TBU.H ∈ List.take (j + 1) w ∧ TBU.H ∈ List.drop j w

In the output representation the fused H links to slot j iff some H-toned TBU lies at or before j and some at or after it, fusion then spreading read back as the string window.

theorem Tone.surfacesWith_plateauAR (w : List TBU) (j : ℕ) : Autosegmental.AR.SurfacesWith (plateauAR w) TRN.H j ↔ TBU.H ∈ List.take (j + 1) w ∧ TBU.H ∈ List.drop j w

Slot j surfaces with H in the output representation iff the string window holds.

The plateauing process

def Tone.utp : Surfacing TBU

Unbounded tonal plateauing is the surfacing process in which TBU i surfaces H iff some H-toned TBU lies at or before it and some at or after it.

Equations

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

@[simp]

theorem Tone.utp_hi : utp.hi = TBU.H

@[simp]

theorem Tone.utp_lo : utp.lo = TBU.O

theorem Tone.utp.surfaces_def {w : List TBU} {i : ℕ} : utp.Surfaces w i ↔ TBU.H ∈ List.take (i + 1) w ∧ TBU.H ∈ List.drop i w

Surfacing is, by definition, the two-sided window on the string.

theorem Tone.utp.surfaces_iff_surfacesWith_plateauAR {w : List TBU} {i : ℕ} : utp.Surfaces w i ↔ Autosegmental.AR.SurfacesWith (plateauAR w) TRN.H i

What surfaces is the representation. utp.Surfaces w i is the H-linkedness of timing slot i in the output representation plateauAR w, the OCP-merged, hull-closed realization.

theorem Tone.utp.surfaces_iff {w : List TBU} {i : ℕ} : utp.Surfaces w i ↔ (∃ j ≤ i, w[j]? = some TBU.H) ∧ ∃ j ≥ i, w[j]? = some TBU.H

Position i surfaces iff there is an H at some j ≤ i and an H at some j ≥ i.

theorem Tone.utp.surfaces_of_le_of_le {w : List TBU} {i j k : ℕ} (hi : utp.Surfaces w i) (hk : utp.Surfaces w k) (hij : i ≤ j) (hjk : j ≤ k) : utp.Surfaces w j

The surfacing set is convex, since the windows only widen.

theorem Tone.utp.H_mem_of_surfaces {w : List TBU} {i : ℕ} (h : utp.Surfaces w i) : TBU.H ∈ w

theorem Tone.utp.surfaces_reverse {w : List TBU} {i : ℕ} (hi : i < w.length) : utp.Surfaces w.reverse i ↔ utp.Surfaces w (w.length - 1 - i)

Reversal swaps the two windows.

theorem Tone.utp.surfaces_split {w : List TBU} {i : ℕ} {a : TBU} (h : w[i]? = some a) : utp.Surfaces w i ↔ a = TBU.H ∨ TBU.H ∈ List.take i w ∧ TBU.H ∈ List.drop (i + 1) w

TBU i surfaces iff it is itself a H or is strictly flanked.

theorem Tone.utp.map_getElem? {w : List TBU} {i : ℕ} : (utp.map w)[i]? = Option.map (fun (x : TBU) => if utp.Surfaces w i then TBU.H else TBU.O) w[i]?

theorem Tone.utp.map_getElem?_H_iff {w : List TBU} {j : ℕ} : (utp.map w)[j]? = some TBU.H ↔ utp.Surfaces w j

theorem Tone.utp.map_getElem?_O_iff {w : List TBU} {j : ℕ} : (utp.map w)[j]? = some TBU.O ↔ j < w.length ∧ ¬utp.Surfaces w j

theorem Tone.utp.map_reverse {w : List TBU} : utp.map w.reverse = (utp.map w).reverse

Plateauing is symmetric under string reversal.

The plateau set

def Tone.plateau (w : List TBU) : Finset ℕ

The plateau of w is the set of positions that surface H.

Equations

• Tone.plateau w = Tone.utp.support w

@[simp]

theorem Tone.mem_plateau {w : List TBU} {j : ℕ} : j ∈ plateau w ↔ utp.Surfaces w j

@[simp]

theorem Tone.plateau_nonempty {w : List TBU} : (plateau w).Nonempty ↔ TBU.H ∈ w

theorem Tone.utp.map_eq_plateau_indicator {w : List TBU} : utp.map w = List.map (fun (i : ℕ) => if i ∈ plateau w then TBU.H else TBU.O) (List.range w.length)

utp.map writes the indicator word of its plateau.

theorem Tone.plateau_eq_Icc_of {w : List TBU} {lo hi : ℕ} (hlo : w[lo]? = some TBU.H) (hhi : w[hi]? = some TBU.H) (hb : ∀ (j : ℕ), w[j]? = some TBU.H → lo ≤ j ∧ j ≤ hi) : plateau w = Finset.Icc lo hi

A word with Hs at lo and hi and none outside [lo, hi] has plateau exactly Finset.Icc lo hi.

theorem Tone.plateau_eq_Icc {w : List TBU} (hne : (plateau w).Nonempty) : plateau w = Finset.Icc ((plateau w).min' hne) ((plateau w).max' hne)

The plateau is an interval, from the first trigger to the last.

Closure laws

Plateauing is a closure operator in the pointwise H-order: extensive (utp.map_getElem?_H_of_getElem?_H), monotone (utp.map_mono), idempotent (utp.map_map). The engine is convexity: the output's Hs are the plateau, an interval, so plateauing the output surfaces nothing new (utp.surfaces_map).

theorem Tone.utp.map_getElem?_H_of_getElem?_H {w : List TBU} {i : ℕ} (h : w[i]? = some TBU.H) : (utp.map w)[i]? = some TBU.H

Every H survives plateauing.

theorem Tone.utp.surfaces_mono {w : List TBU} {i : ℕ} {w' : List TBU} (hw : ∀ (j : ℕ), w[j]? = some TBU.H → w'[j]? = some TBU.H) (h : utp.Surfaces w i) : utp.Surfaces w' i

Surfacing is monotone in the word's H-set.

theorem Tone.utp.map_mono {w w' : List TBU} (hw : ∀ (j : ℕ), w[j]? = some TBU.H → w'[j]? = some TBU.H) (j : ℕ) (h : (utp.map w)[j]? = some TBU.H) : (utp.map w')[j]? = some TBU.H

Plateauing is monotone, pointwise more Hs in giving pointwise more Hs out.

theorem Tone.utp.H_mem_map {w : List TBU} : TBU.H ∈ utp.map w ↔ TBU.H ∈ w

Plateauing preserves the presence of a trigger in both directions.

theorem Tone.utp.surfaces_map {w : List TBU} {i : ℕ} : utp.Surfaces (utp.map w) i ↔ utp.Surfaces w i

Surfacing is invariant under plateauing, since the output's Hs are the plateau, whose convexity flanks no new positions.

@[simp]

theorem Tone.plateau_map {w : List TBU} : plateau (utp.map w) = plateau w

@[simp]

theorem Tone.utp.map_map {w : List TBU} : utp.map (utp.map w) = utp.map w

Plateauing is idempotent, a plateau being already closed.

The outputs of plateauing

A word is an output of plateauing exactly when plateauing fixes it, and it is fixed exactly when no O lies between two Hs: the outputs are the words without an H O H subsequence.

theorem Tone.utp.map_eq_self_iff {w : List TBU} : utp.map w = w ↔ ∀ (i : ℕ), utp.Surfaces w i → w[i]? = some TBU.H

Plateauing fixes a word iff every surfacing position already carries H.

theorem Tone.utp.range_map : Set.range utp.map = Function.fixedPoints utp.map

Plateauing is idempotent, so its outputs are its fixed points.

theorem Tone.HOH_sublist_iff {w : List TBU} : [TBU.H, TBU.O, TBU.H].Sublist w ↔ ∃ (i : ℕ), utp.Surfaces w i ∧ w[i]? = some TBU.O

An H O H subsequence is an O at a surfacing position.

theorem Tone.utp.mem_range_map_iff {w : List TBU} : w ∈ Set.range utp.map ↔ w ∉ Language.shuffleIdeal [TBU.H, TBU.O, TBU.H]

The outputs of plateauing are the words without an H O H subsequence.

The plateauing rule

The rule schemata as theorems about utp rather than clauses of its definition.

theorem Tone.utp.map_toneless (n : ℕ) : utp.map (List.replicate n TBU.O) = List.replicate n TBU.O

A toneless word is unchanged.

theorem Tone.utp.map_single (m n : ℕ) : utp.map (List.replicate m TBU.O ++ TBU.H :: List.replicate n TBU.O) = List.replicate m TBU.O ++ TBU.H :: List.replicate n TBU.O

A word with a single H is unchanged — one H cannot trigger a plateau.

theorem Tone.utp.map_plateau (m p : ℕ) (w : List TBU) : utp.map (List.replicate m TBU.O ++ TBU.H :: (w ++ TBU.H :: List.replicate p TBU.O)) = List.replicate m TBU.O ++ (List.replicate (w.length + 2) TBU.H ++ List.replicate p TBU.O)

Everything between the outermost Hs surfaces H; the medial material w is arbitrary.

Unbounded circumambience

Whether the target surfaces is controlled by unboundedly distant flanks: instantiate the flank-witness template with 2d+2 toneless TBUs between the flanks.

theorem Tone.utp.requiresBothSides : RequiresBothSides utp.map

UTP requires both sides. Its trigger is the two-sided window conjunction, so deleting either flanking H reverts the plateau target.

theorem Tone.utp.twoSidedUnboundedDependence : TwoSidedUnboundedDependence utp.map

UTP has two-sided unbounded dependence, a corollary of its circumambience, so whether a position changes depends on unboundedly distant material on both sides.