Unbounded tonal plateauing

[HK10]'s plateauing rule for Luganda: every tone-bearing unit between two H-toned units surfaces H. Formalized over the string rendering of [Jar16]: 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. What surfaces is the representation: utp.Surfaces w i is by definition H-linkedness of timing node i in the output representation plateauAR w (the OCP-merged input, hull-closed — fusion then spreading); the string reading is the derived utp.surfaces_def. The map is utp.map, the surfacing set plateau.

The map is the flagship unbounded circumambient process: whether a position changes depends on unboundedly distant material on both sides (utp.isUnboundedCircumambient), and in the strong witness form utp.requiresBothSides — perturbing either far side alone reverts the change — which feeds the weak-determinism exclusion theorems of Studies/Jardine2016Tone (bimachine rendering) and Studies/Yolyan2025 (BMRS rendering).

Main definitions

• Tone.Plateauing.TBU — the H/Ø string alphabet (association states; distinct from Tone.TBUKind, the phonological typology of timing units).
• Tone.Plateauing.plateauAR — the output representation (OCP-merged input, hull-closed); utp.Surfaces is H-linkedness in it, via Graph.SurfacesWith and Graph.hull (Phonology/Autosegmental/Hull.lean).
• Tone.Plateauing.utp — plateauing as a Tone.Surfacing process; utp.map the map.
• Tone.Plateauing.plateau — the set of surfacing positions.

Main results

• utp.map_getElem?_H_iff / utp.map_getElem?_O_iff — pointwise characterization of the map.
• utp_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.requiresBothSides — deleting either flanking H reverts the plateau target, at every distance.
• realizeMerged_toAR_map — the commuting square: the merged representation of the output string is the output representation plateauAR.

The tone-bearing-unit alphabet

inductive Tone.Plateauing.TBU : Type

A tone-bearing unit's association state: H is a TBU associated to a H tone, O an unspecified TBU ([Jar16]'s Ø).

• H : TBU
• O : TBU

@[implicit_reducible]

instance Tone.Plateauing.instDecidableEqTBU : DecidableEq TBU

Equations

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

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

Equations

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

@[implicit_reducible]

instance Tone.Plateauing.instReprTBU : Repr TBU

Equations

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

The output representation

The string rendering embeds into autosegmental representations, and plateauing on representations is OCP-fusion followed by hull-closure of the association lines ([HK10]'s rule as an operation on structures). What surfaces is the representation: utp.Surfaces is by definition H-linkedness in the output representation plateauAR w; the string-level take/drop reading is the derived characterization utp.surfaces_def.

def Tone.Plateauing.toAR : TBU → Autosegmental.AR TRN Unit

A H-toned TBU is one H melody node linked to its timing unit; a toneless TBU a bare timing unit.

Equations

• Tone.Plateauing.toAR Tone.Plateauing.TBU.H = Autosegmental.AR.single Tone.TRN.H ()
• Tone.Plateauing.toAR Tone.Plateauing.TBU.O = Autosegmental.AR.bare ()

theorem Tone.Plateauing.linearize_realize_toAR (w : List TBU) : (Autosegmental.realize toAR w).linearize = List.map (fun (a : TBU) => ((), if a = TBU.H then [TRN.H] else [])) w

theorem Tone.Plateauing.upper_realize_toAR (v : List TBU) : (Autosegmental.realize toAR v).upper.toList = List.replicate (List.count TBU.H v) TRN.H

theorem Tone.Plateauing.lower_realize_toAR (v : List TBU) : (Autosegmental.realize toAR v).lower.toList = List.replicate v.length ()

The lower tier of the realization is the bare timing tier.

theorem Tone.Plateauing.isLinkedLower_realize_toAR {w : List TBU} {j : ℕ} : (Autosegmental.realize toAR w).IsLinkedLower j ↔ w[j]? = some TBU.H

A timing node of the input representation is linked iff its TBU is H-toned.

theorem Tone.Plateauing.mem_links_realizeMerged_toAR {w : List TBU} {p : ℕ × ℕ} : p ∈ (Autosegmental.realizeMerged toAR w).links ↔ p.1 = 0 ∧ w[p.2]? = some TBU.H

The merged input representation: one fused H, linked to exactly the H-positions.

theorem Tone.Plateauing.upper_realizeMerged_toAR (v : List TBU) : (Autosegmental.realizeMerged toAR v).upper.toList = if TBU.H ∈ v then [TRN.H] else []

The melodic tier of the merged representation: one fused H if any, else empty.

theorem Tone.Plateauing.lower_realizeMerged_toAR (v : List TBU) : (Autosegmental.realizeMerged toAR v).lower.toList = List.replicate v.length ()

The timing tier survives merging: the bare tier of the input's length.

theorem Tone.Plateauing.upper_get?_realizeMerged_toAR {w : List TBU} (hw : TBU.H ∈ w) : (Autosegmental.realizeMerged toAR w).upper.get? 0 = some TRN.H

With any H present, the fused melody node is the H at index 0.

def Tone.Plateauing.plateauAR (w : List TBU) : Autosegmental.AR TRN Unit

The output representation: fuse, then spread — the merged input, hull-closed.

Equations

• Tone.Plateauing.plateauAR w = (Autosegmental.realizeMerged Tone.Plateauing.toAR w).hull

@[simp]

theorem Tone.Plateauing.plateauAR_upper {w : List TBU} : (plateauAR w).upper = (Autosegmental.realizeMerged toAR w).upper

@[simp]

theorem Tone.Plateauing.plateauAR_lower {w : List TBU} : (plateauAR w).lower = (Autosegmental.realizeMerged toAR w).lower

theorem Tone.Plateauing.mem_links_plateauAR {w : List TBU} {k j : ℕ} : (k, j) ∈ (plateauAR w).links ↔ k = 0 ∧ (∃ i ≤ j, w[i]? = some TBU.H) ∧ ∃ i ≥ j, w[i]? = some TBU.H

A link of the output representation: the fused node, over a flanked position.

theorem Tone.Plateauing.surfacesWith_plateauAR {w : List TBU} {i : ℕ} : (plateauAR w).SurfacesWith TRN.H i ↔ TBU.H ∈ List.take (i + 1) w ∧ TBU.H ∈ List.drop i w

What surfaces is the representation: i is H-linked in plateauAR w iff some H-toned TBU lies at or before i and some at or after it — the string-level reading.

The plateauing process

def Tone.Plateauing.utp : Surfacing TBU

Unbounded tonal plateauing as a surfacing process: a TBU surfaces the marked tone H iff its timing node is H-linked in the output representation.

Equations

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

@[simp]

theorem Tone.Plateauing.utp.hi_def : utp.hi = TBU.H

@[simp]

theorem Tone.Plateauing.utp.lo_def : utp.lo = TBU.O

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

The string-level reading of surfacing: the windowed form, now derived.

theorem Tone.Plateauing.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

Positionwise reading of surfacing: a H at some j ≤ i and a H at some j ≥ i.

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

The surfacing set is convex: the windows only widen.

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

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

Reversal symmetry: under reverse the two windows swap.

theorem Tone.Plateauing.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.Plateauing.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.Plateauing.utp.map_getElem?_H_iff {w : List TBU} {j : ℕ} : (utp.map w)[j]? = some TBU.H ↔ utp.Surfaces w j

theorem Tone.Plateauing.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.Plateauing.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.Plateauing.plateau (w : List TBU) : Finset ℕ

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

Equations

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

@[simp]

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

@[simp]

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

theorem Tone.Plateauing.utp_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.Plateauing.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

Sandwich characterization: a word with Hs at lo and hi and none outside [lo, hi] has plateau exactly Finset.Icc lo hi.

theorem Tone.Plateauing.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.Plateauing.utp.map_getElem?_H_of_getElem?_H {w : List TBU} {i : ℕ} (h : w[i]? = some TBU.H) : (utp.map w)[i]? = some TBU.H

Extensivity: every H survives plateauing.

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

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

theorem Tone.Plateauing.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

Monotonicity: pointwise more Hs in, pointwise more Hs out.

theorem Tone.Plateauing.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.Plateauing.utp.surfaces_map {w : List TBU} {i : ℕ} : utp.Surfaces (utp.map w) i ↔ utp.Surfaces w i

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

@[simp]

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

@[simp]

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

Idempotence: a plateau is already closed.

The plateauing rule

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

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

A toneless word is unchanged.

theorem Tone.Plateauing.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.Plateauing.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.

The commuting square

The string map linearizes the representational operation: realizing the output string gives back exactly the output representation. utp.Surfaces reads plateauAR by definition; the square closes the loop at the level of whole representations.

theorem Tone.Plateauing.realizeMerged_toAR_map (w : List TBU) : Autosegmental.realizeMerged toAR (utp.map w) = plateauAR w

The commuting square: the merged representation of the output string is the output representation — fusion-plus-spreading followed by linearization equals utp.map followed by realization.

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.Plateauing.utp.requiresBothSides : Subregular.RequiresBothSides utp.map

UTP requires both sides ([HL13]): its trigger is the two-sided window conjunction, so deleting either flanking H reverts the plateau target.

theorem Tone.Plateauing.utp.isUnboundedCircumambient : Subregular.IsUnboundedCircumambient utp.map

UTP is an unbounded circumambient process: whether a position changes depends on unboundedly distant material on both sides.