Multi-tier autosegmental graphs

MultiGraph τ is the autosegmental representation at general tier arity: n heterogeneously-typed ordered tiers (tiers i : LabeledTuple (τ i), with τ : Fin n → Type u) plus, for every ordered tier-pair (i, j), a Finset (ℕ × ℕ) of association links (links i j; empty ⇒ the pair does not associate). This is [Jar17]'s autosegmental phonological graph at arbitrary arity, and the home of [Lio22a]'s register-tier tone geometry (subtonal-feature tiers + a mora tier around a Tonal Root Node hub).

The classical bipartite Graph α β (Graph.lean) is the n = 2 case. It is a separate first-class structure (so it keeps extends/.toGraph/anonymous- constructor ergonomics and independent universes); the two are related by the monoidal inclusion functor rather than a defeq view — see Inclusion.lean.

Design (three-reviewer mathlib panel, 2026-06-24)

• Heterogeneous tiers τ : Fin n → Type u — per-tier static typing, fiberwise.
• Links per ordered tier-pair (i j) → Finset (ℕ × ℕ) — keeps concat's shift fiberwise; the associating topology is {(i,j) | links i j ≠ ∅}.
• Planarity stays binary, per pair (IsPlanar := ∀ i j, IsNonCrossing (links i j)): the existing MonovaryOn-based NCC reused pointwise — no N-ary planarity theory.

structure Autosegmental.MultiGraph {n : ℕ} (τ : Fin n → Type u) : Type u

A multi-tier autosegmental graph: n heterogeneously-typed ordered tiers plus a Finset (ℕ × ℕ) of association links on each ordered tier-pair.

• tiers (i : Fin n) : LabeledTuple (τ i)

  The n heterogeneously-typed ordered tiers.

• links (i j : Fin n) : Finset (ℕ × ℕ)

  Association links per ordered tier-pair; empty ⇒ the pair does not associate.

theorem Autosegmental.MultiGraph.ext {n : ℕ} {τ : Fin n → Type u} {x y : MultiGraph τ} (tiers : x.tiers = y.tiers) (links : x.links = y.links) : x = y

theorem Autosegmental.MultiGraph.ext_iff {n : ℕ} {τ : Fin n → Type u} {x y : MultiGraph τ} : x = y ↔ x.tiers = y.tiers ∧ x.links = y.links

@[implicit_reducible]

instance Autosegmental.MultiGraph.instDecidableEq {n : ℕ} {τ : Fin n → Type u} [(i : Fin n) → DecidableEq (τ i)] : DecidableEq (MultiGraph τ)

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_iff (x✝¹.tiers = x✝.tiers ∧ x✝¹.links = x✝.links) ⋯

Well-formedness predicates

def Autosegmental.MultiGraph.IsPlanar {n : ℕ} {τ : Fin n → Type u} (G : MultiGraph τ) : Prop

Planarity: every tier-pair's link set is non-crossing — the binary MonovaryOn NCC applied pointwise per pair (no N-ary generalization).

Equations

• G.IsPlanar = ∀ (i j : Fin n), Autosegmental.IsNonCrossing (G.links i j)

@[implicit_reducible]

instance Autosegmental.MultiGraph.instDecidableIsPlanar {n : ℕ} {τ : Fin n → Type u} (G : MultiGraph τ) : Decidable G.IsPlanar

Equations

• G.instDecidableIsPlanar = Autosegmental.MultiGraph.instDecidableIsPlanar._aux_1 G

def Autosegmental.MultiGraph.InBounds {n : ℕ} {τ : Fin n → Type u} (G : MultiGraph τ) : Prop

In-bounds: every link's endpoints fall within the respective tier lengths.

Equations

• G.InBounds = ∀ (i j : Fin n), ∀ p ∈ G.links i j, p.1 < (G.tiers i).len ∧ p.2 < (G.tiers j).len

@[implicit_reducible]

instance Autosegmental.MultiGraph.instDecidableInBounds {n : ℕ} {τ : Fin n → Type u} (G : MultiGraph τ) : Decidable G.InBounds

Equations

• G.instDecidableInBounds = Autosegmental.MultiGraph.instDecidableInBounds._aux_1 G

The empty graph

def Autosegmental.MultiGraph.empty {n : ℕ} {τ : Fin n → Type u} : MultiGraph τ

The empty multigraph: every tier empty, no links.

Equations

• Autosegmental.MultiGraph.empty = { tiers := fun (x : Fin n) => LabeledTuple.empty, links := fun (x x_1 : Fin n) => ∅ }

@[simp]

theorem Autosegmental.MultiGraph.empty_tiers {n : ℕ} {τ : Fin n → Type u} (i : Fin n) : empty.tiers i = LabeledTuple.empty

@[simp]

theorem Autosegmental.MultiGraph.empty_links {n : ℕ} {τ : Fin n → Type u} (i j : Fin n) : empty.links i j = ∅

theorem Autosegmental.MultiGraph.isPlanar_empty {n : ℕ} {τ : Fin n → Type u} : empty.IsPlanar

theorem Autosegmental.MultiGraph.inBounds_empty {n : ℕ} {τ : Fin n → Type u} : empty.InBounds

Concatenation ([JH15], fiberwise coproduct)

def Autosegmental.MultiGraph.concat {n : ℕ} {τ : Fin n → Type u} (A B : MultiGraph τ) : MultiGraph τ

Concatenation: tier-wise LabeledTuple.concat, and per-pair link union with B's links shifted past A's tier lengths on each coordinate.

Equations

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

@[simp]

theorem Autosegmental.MultiGraph.concat_tiers {n : ℕ} {τ : Fin n → Type u} (A B : MultiGraph τ) (i : Fin n) : (A.concat B).tiers i = (A.tiers i).concat (B.tiers i)

@[simp]

theorem Autosegmental.MultiGraph.concat_links {n : ℕ} {τ : Fin n → Type u} (A B : MultiGraph τ) (i j : Fin n) : (A.concat B).links i j = A.links i j ∪ Finset.image (shiftLink (A.tiers i).len (A.tiers j).len) (B.links i j)

Monoid laws

theorem Autosegmental.MultiGraph.empty_concat {n : ℕ} {τ : Fin n → Type u} (A : MultiGraph τ) : empty.concat A = A

theorem Autosegmental.MultiGraph.concat_empty {n : ℕ} {τ : Fin n → Type u} (A : MultiGraph τ) : A.concat empty = A

theorem Autosegmental.MultiGraph.concat_assoc {n : ℕ} {τ : Fin n → Type u} (A B C : MultiGraph τ) : (A.concat B).concat C = A.concat (B.concat C)

@[implicit_reducible]

instance Autosegmental.MultiGraph.instMonoid {n : ℕ} {τ : Fin n → Type u} : Monoid (MultiGraph τ)

Equations

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

Predicate preservation

theorem Autosegmental.MultiGraph.isPlanar_concat {n : ℕ} {τ : Fin n → Type u} {A B : MultiGraph τ} (hAib : A.InBounds) (hA : A.IsPlanar) (hB : B.IsPlanar) : (A.concat B).IsPlanar

Concatenation preserves planarity, given A.InBounds.

theorem Autosegmental.MultiGraph.inBounds_concat {n : ℕ} {τ : Fin n → Type u} {A B : MultiGraph τ} (hA : A.InBounds) (hB : B.InBounds) : (A.concat B).InBounds

Concatenation preserves in-bounds.