Tonal surfacing processes

A surfacing process bundles the analysis [Jar16] gives tone-string maps: a marked tone value, and a context predicate Surfaces w i saying position i of w surfaces with it. The induced rewrite Surfacing.map writes the marked tone exactly at the surfacing positions and the default elsewhere; Surfacing.support is the surfacing set. Owning the context predicate on the process is what lets rival processes coexist: unbounded tonal plateauing (Tone.Plateauing.utp) and Copperbelt Bemba high-tone spreading (Studies/Yolyan2025) instantiate the same structure with very different predicates — plateauing's is convex and its map a closure operator, spreading's is neither — so only the genuinely shared API lives here.

The laws are the shared minimum: surfacing positions are in-domain (lt_length), the marked tone is faithful — an underlying marked tone always surfaces (surfaces_of_hi) — and the two written values are distinct (hi_ne_lo), which makes the pointwise characterizations (map_getElem?_hi_iff, map_getElem?_lo_iff) read the map exactly.

structure Tone.Surfacing (α : Type u_1) : Type u_1

A tonal surfacing process over the alphabet α: a marked tone hi, a default lo, and the context predicate saying which positions of a word surface with the mark.

• hi : α

  The marked (surfacing) tone value.

• lo : α

  The default value written at non-surfacing positions.

• Surfaces : List α → ℕ → Prop

  Position i of w surfaces with the marked tone.

• hi_ne_lo : self.hi ≠ self.lo

  The two written values are distinct.

• lt_length {w : List α} {i : ℕ} : self.Surfaces w i → i < w.length

  Surfacing positions are in-domain.

• surfaces_of_hi {w : List α} {i : ℕ} : w[i]? = some self.hi → self.Surfaces w i

  Faithfulness: an underlying marked tone surfaces.

• decSurfaces (w : List α) (i : ℕ) : Decidable (self.Surfaces w i)

  The context predicate is decidable, so the map computes.

@[implicit_reducible]

instance Tone.Surfacing.instDecidableSurfaces {α : Type u_1} (P : Surfacing α) (w : List α) (i : ℕ) : Decidable (P.Surfaces w i)

Equations

• P.instDecidableSurfaces w i = P.decSurfaces w i

def Tone.Surfacing.map {α : Type u_1} (P : Surfacing α) (w : List α) : List α

The induced rewrite: the marked tone exactly at the surfacing positions.

Equations

• P.map w = List.mapIdx (fun (i : ℕ) (x : α) => if P.Surfaces w i then P.hi else P.lo) w

@[simp]

theorem Tone.Surfacing.map_nil {α : Type u_1} (P : Surfacing α) : P.map [] = []

@[simp]

theorem Tone.Surfacing.map_length {α : Type u_1} (P : Surfacing α) {w : List α} : (P.map w).length = w.length

theorem Tone.Surfacing.map_getElem? {α : Type u_1} (P : Surfacing α) {w : List α} {i : ℕ} : (P.map w)[i]? = Option.map (fun (x : α) => if P.Surfaces w i then P.hi else P.lo) w[i]?

theorem Tone.Surfacing.map_getElem?_hi_iff {α : Type u_1} (P : Surfacing α) {w : List α} {j : ℕ} : (P.map w)[j]? = some P.hi ↔ P.Surfaces w j

theorem Tone.Surfacing.map_getElem?_lo_iff {α : Type u_1} (P : Surfacing α) {w : List α} {j : ℕ} : (P.map w)[j]? = some P.lo ↔ j < w.length ∧ ¬P.Surfaces w j

theorem Tone.Surfacing.map_getElem?_hi_of_getElem?_hi {α : Type u_1} (P : Surfacing α) {w : List α} {i : ℕ} (h : w[i]? = some P.hi) : (P.map w)[i]? = some P.hi

Faithfulness at the map level: an underlying marked tone survives.

theorem Tone.Surfacing.Surfaces.lt_length {α : Type u_1} {P : Surfacing α} {w : List α} {i : ℕ} (h : P.Surfaces w i) : i < w.length

Hypothesis-dot form of the in-domain law: h.lt_length for h : P.Surfaces w i.

theorem Tone.Surfacing.requiresBothSides_of_flanks {α : Type u_1} (P : Surfacing α) {xOn yOn xOff yOff : α} {n t : ℕ → ℕ} (hmargin : ∀ (d : ℕ), d < t d ∧ t d + d < n d + 1) (hon : ∀ (d : ℕ), P.Surfaces (Subregular.flankWord xOn P.lo yOn (n d)) (t d)) (hoffL : ∀ (d : ℕ), ¬P.Surfaces (Subregular.flankWord xOff P.lo yOn (n d)) (t d)) (hoffR : ∀ (d : ℕ), ¬P.Surfaces (Subregular.flankWord xOn P.lo yOff (n d)) (t d)) : Subregular.RequiresBothSides P.map

The flank-witness template, at the surfacing level: a process whose surfacing at a d-margined target in a flank word is switched on by the base flanks and off by either single flip requires both sides — supply only the three surfacing facts.

theorem Tone.Surfacing.requiresBothSides_of_surfaces_iff {α : Type u_1} (P : Surfacing α) (hiff : ∀ (w : List α) (i : ℕ), P.Surfaces w i ↔ (∃ j ≤ i, w[j]? = some P.hi) ∧ ∃ j ≥ i, w[j]? = some P.hi) : Subregular.RequiresBothSides P.map

Conjunctive two-sided triggers require both sides: a process that surfaces the marked tone exactly where one occurrence lies at-or-before and one at-or-after needs unboundedly distant information on both sides — the flank witness family is generic.

The surfacing set

def Tone.Surfacing.support {α : Type u_1} (P : Surfacing α) (w : List α) : Finset ℕ

The surfacing positions of w, as a finite set.

Equations

• P.support w = Finset.filter (P.Surfaces w) (Finset.range w.length)

@[simp]

theorem Tone.Surfacing.mem_support {α : Type u_1} (P : Surfacing α) {w : List α} {j : ℕ} : j ∈ P.support w ↔ P.Surfaces w j

theorem Tone.Surfacing.map_eq_indicator {α : Type u_1} (P : Surfacing α) {w : List α} : P.map w = List.map (fun (i : ℕ) => if i ∈ P.support w then P.hi else P.lo) (List.range w.length)

The map writes the indicator word of its support.