The association hull

Graph.hull closes each upper node's association set to its interval hull on the lower tier: (k, j) is a hull link iff j lies between two of k's links. This is the representational content of tonal spreading-to-a-span: [HK10]'s plateauing rule, applied after OCP-fusion, is exactly the hull of the fused H's associations (Phonology/Tone/Plateauing).

Hull-closure of a multi-node melody can violate the no-crossing constraint (two interleaved hulls cross); the phonological operation applies to the fused representation, where the melody is a single node and the hull is planar.

Main results

• mem_links_hull — hull membership as flanking (Graph form with explicit bounds; side-condition-free AR.mem_links_hull for well-formed representations).
• links_subset_hull — the hull extends the link set.
• hull_convex — per-node convexity: the defining property of the hull.
• AR.hull — the operation on well-formed representations.

noncomputable def Autosegmental.AR.hull {ι : Type u_3} {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] : TieredAR ι τ

Close each tier-m node's association set to its interval hull on each other tier.

Equations

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

instance Autosegmental.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesHull {ι : Type u_3} [Finite ι] {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] : Finite (AR.hull m X).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_hull {ι : Type u_3} [Finite ι] {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] (i : ι) : tierWord i = tierWord i

theorem Autosegmental.AR.link_hull_left {ι : Type u_3} [Finite ι] {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {j : ι} (hj : m ≠ j) {p q : ℕ} (hq : q < tierLength X j) : link (hull m X) m j p q ↔ ∃ (q₁ : ℕ) (q₂ : ℕ), link X m j p q₁ ∧ link X m j p q₂ ∧ q₁ ≤ q ∧ q ≤ q₂

Hull membership at the melody tier: q lies between two of p's links.

theorem Autosegmental.AR.link_hull_of_ne {ι : Type u_3} [Finite ι] {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {i j : ι} (hi : i ≠ m) (hj : j ≠ m) (p q : ℕ) : link (hull m X) i j p q ↔ link X i j p q

Links not involving the melody tier pass through the hull unchanged.

theorem Autosegmental.AR.link_subset_hull {ι : Type u_3} [Finite ι] {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {i j : ι} {p q : ℕ} (h : link X i j p q) : link (hull m X) i j p q

Melody links flank themselves: the hull extends the link relation.

theorem Autosegmental.AR.link_hull_convex {ι : Type u_3} [Finite ι] {τ : ι → Type u_4} (m : ι) (X : TieredAR ι τ) [Finite X.obj.V] {j : ι} (hj : m ≠ j) {p q₁ q q₂ : ℕ} (hq : q < tierLength X j) (h₁ : link (hull m X) m j p q₁) (h₂ : link (hull m X) m j p q₂) (hle₁ : q₁ ≤ q) (hle₂ : q ≤ q₂) : link (hull m X) m j p q

Per-node convexity at the melody tier: the defining property of the hull.