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 [Jar16a]: 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, in the strong witness form utp.requiresBothSides — perturbing either far side alone reverts the change — with the weaker utp.twoSidedUnboundedDependence as a corollary, 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 ([Jar16a]'s Ø).

• H : TBU
• O : TBU

@[instance_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✝

@[instance_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.

noncomputable def Tone.Plateauing.toRep (a : TBU) : Autosegmental.AR Sigma.fst

toAR in coordinates: the two-tier representation of one association state (melody over true, timing over false).

Equations

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

instance Tone.Plateauing.instFiniteVSigmaBoolTwoTierTRNUnitObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesToRep (a : TBU) : Finite (toRep a).obj.V

@[instance_reducible]

instance Tone.Plateauing.instDecidableEqTwoTierTRNUnitTrue : DecidableEq (Autosegmental.TwoTier TRN Unit true)

Equations

• Tone.Plateauing.instDecidableEqTwoTierTRNUnitTrue = Tone.Plateauing.instDecidableEqTwoTierTRNUnitTrue._aux_1

noncomputable def Tone.Plateauing.plateauRep (w : List TBU) : Autosegmental.AR Sigma.fst

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

Equations

• Tone.Plateauing.plateauRep w = Autosegmental.AR.hull true (Autosegmental.AR.collapse (Autosegmental.AR.realize Tone.Plateauing.toRep w) true)

instance Tone.Plateauing.instFiniteVSigmaBoolTwoTierTRNUnitObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesPlateauRep (w : List TBU) : Finite (plateauRep w).obj.V

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

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

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

The timing word of a realized string: one slot per TBU.

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

Links of 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.Plateauing.link_realizeMerged (w : List TBU) (k j : ℕ) : Autosegmental.AR.link (Autosegmental.AR.collapse (Autosegmental.AR.realize toRep w) true) true false k j ↔ k = 0 ∧ w[j]? = some TBU.H

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

theorem Tone.Plateauing.link_plateauRep (w : List TBU) (j : ℕ) : (∃ (k : ℕ), (plateauRep w).link true false k j) ↔ TBU.H ∈ List.take (j + 1) w ∧ TBU.H ∈ List.drop j w

What surfaces is the representation: slot j is H-linked in plateauRep w 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.

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.

theorem Tone.Plateauing.utp.surfaces_iff_link_plateauRep {w : List TBU} {i : ℕ} : utp.Surfaces w i ↔ ∃ (k : ℕ), (plateauRep w).link true false k i

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

@[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, definitional.

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.

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

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

theorem Tone.Plateauing.utp.twoSidedUnboundedDependence : TwoSidedUnboundedDependence utp.map

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