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.

def Autosegmental.Graph.hull {α : Type u_1} {β : Type u_2} (r : Graph α β) : Graph α β

Close each upper node's association set to its interval hull on the lower tier.

Equations

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

@[simp]

theorem Autosegmental.Graph.hull_upper {α : Type u_1} {β : Type u_2} (r : Graph α β) : r.hull.upper = r.upper

@[simp]

theorem Autosegmental.Graph.hull_lower {α : Type u_1} {β : Type u_2} (r : Graph α β) : r.hull.lower = r.lower

theorem Autosegmental.Graph.mem_links_hull {α : Type u_1} {β : Type u_2} {r : Graph α β} (hr : r.InBounds) {k j : ℕ} : (k, j) ∈ r.hull.links ↔ ∃ (j₁ : ℕ) (j₂ : ℕ), (k, j₁) ∈ r.links ∧ (k, j₂) ∈ r.links ∧ j₁ ≤ j ∧ j ≤ j₂

Hull membership, on an in-bounds graph: j lies between two of k's links.

theorem Autosegmental.Graph.InBounds.hull {α : Type u_1} {β : Type u_2} {r : Graph α β} (hr : r.InBounds) : r.hull.InBounds

The hull stays in bounds.

theorem Autosegmental.Graph.links_subset_hull {α : Type u_1} {β : Type u_2} {r : Graph α β} (hr : r.InBounds) : r.links ⊆ r.hull.links

Links flank themselves: the hull extends the link set.

theorem Autosegmental.Graph.hull_convex {α : Type u_1} {β : Type u_2} {r : Graph α β} (hr : r.InBounds) {k j₁ j j₂ : ℕ} (h₁ : (k, j₁) ∈ r.hull.links) (h₂ : (k, j₂) ∈ r.hull.links) (hle₁ : j₁ ≤ j) (hle₂ : j ≤ j₂) : (k, j) ∈ r.hull.links

Per-node convexity: the defining property of the hull.

def Autosegmental.AR.hull {α : Type u_1} {β : Type u_2} (A : AR α β) : AR α β

The hull on well-formed representations.

Equations

• A.hull = { toGraph := A.hull, inBounds := ⋯ }

@[simp]

theorem Autosegmental.AR.hull_upper {α : Type u_1} {β : Type u_2} (A : AR α β) : A.hull.upper = A.upper

@[simp]

theorem Autosegmental.AR.hull_lower {α : Type u_1} {β : Type u_2} (A : AR α β) : A.hull.lower = A.lower

theorem Autosegmental.AR.mem_links_hull {α : Type u_1} {β : Type u_2} {A : AR α β} {k j : ℕ} : (k, j) ∈ A.hull.links ↔ ∃ (j₁ : ℕ) (j₂ : ℕ), (k, j₁) ∈ A.links ∧ (k, j₂) ∈ A.links ∧ j₁ ≤ j ∧ j ≤ j₂

Hull membership on a well-formed representation: no side condition — the representation carries its own bounds.