Autosegmental representations: the §4.2 axioms and their category

The well-formedness axioms of [Jar16b] §4.2, each stated on exactly the components it reads (Digraph arcs, SimpleGraph edges, a coloring c : V → ι) and read on a labeled mixed graph at the tier coloring X.tier t. AR t is the full subcategory of Graph S they carve out, monoidal under Graph.concat.

Main definitions

• IsTierOrdered, NoInternalAssoc, IsSaturated, IsPlanar, IsOCPClean: the six well-formedness axioms of [Jar16b] §4.2.
• AR t: the category of autosegmental representations — the full subcategory on Axioms 1–3, monoidal under concat.

Main results

• isTierOrdered_concat, noInternalAssoc_concat, isPlanar_concat: concatenation preserves the axioms ([JH15] Theorem 4's structural half).
• not_isTierOrdered_sum: the bridge-free coproduct leaves the axiom class; Axiom 2 forces the bridges in concat.
• AR.tierColoring: the tier map properly colors the association graph (edges_colorable).

Implementation notes

The axiom numbering follows the dissertation; [JH15] numbers the NCC and OCP as 4 and 5 and has no saturation axiom. Saturation ([Gol76]'s original well-formedness condition) is stated but never imposed. The arcs are transitively closed ([Jar19]'s reading that A represents the order), so the OCP reads adjacency as the covering relation of the arcs. Axiom 6's word-level form is AR.IsCleanAt (OCP.lean, through the hub OCP.IsClean); relating Axiom 5 to the coordinate IsNonCrossing is the TODO.

TODO

• Package AR.ofData + AR.isoOfReaderEq (NormalForm.lean) as an equivalence with the strict tuple category; reduce IsPlanar on normal forms to the per-pair IsNonCrossing of the link relation.

structure Autosegmental.IsTierOrdered {V : Type u_1} {ι : Type u_3} (A : Digraph V) (c : V → ι) extends IsStrictOrder V A.Adj : Prop

The arcs A are tier-internal and strictly totally order each fiber of c (Axioms 1–2).

• irrefl (a : V) : ¬A.Adj a a
• trans (a b c : V) : A.Adj a b → A.Adj b c → A.Adj a c
• tier_eq ⦃v w : V⦄ : A.Adj v w → c v = c w

  Arcs never leave a tier.

• total ⦃v w : V⦄ : v ≠ w → c v = c w → A.Adj v w ∨ A.Adj w v

  Distinct same-tier vertices are arc-comparable.

def Autosegmental.NoInternalAssoc {V : Type u_1} (E : SimpleGraph V) (A : Digraph V) : Prop

No association edge links arc-related vertices (Axiom 3).

Equations

• Autosegmental.NoInternalAssoc E A = ∀ ⦃v w : V⦄, E.Adj v w → ¬A.Adj v w

def Autosegmental.IsSaturated {V : Type u_1} (E : SimpleGraph V) : Prop

Every vertex meets an association edge (Axiom 4, full specification).

Equations

• Autosegmental.IsSaturated E = ∀ (v : V), ∃ (w : V), E.Adj v w

def Autosegmental.IsPlanar {V : Type u_1} (E : SimpleGraph V) (A : Digraph V) : Prop

No two association edges straddle in opposite precedence order (Axiom 5, the NCC).

Equations

• Autosegmental.IsPlanar E A = ∀ ⦃v v' w w' : V⦄, E.Adj v v' → E.Adj w w' → A.Adj v w → ¬A.Adj w' v'

def Autosegmental.IsOCPClean {V : Type u_1} {S : Type u_2} {ι : Type u_3} (A : Digraph V) (ℓ : V → S) (t : S → ι) (m : ι) : Prop

Precedence-adjacent vertices on melody tier m bear distinct labels (Axiom 6, the OCP).

Equations

• Autosegmental.IsOCPClean A ℓ t m = ∀ ⦃v w : V⦄, A.Adj v w → (∀ (u : V), ¬(A.Adj v u ∧ A.Adj u w)) → t (ℓ v) = m → ℓ v ≠ ℓ w

Axiom preservation under the graph operations

theorem Autosegmental.Graph.isTierOrdered_empty {S : Type u_2} {ι : Type u_3} (t : S → ι) : IsTierOrdered (empty S).arcs (tier t (empty S))

theorem Autosegmental.Graph.noInternalAssoc_empty {S : Type u_2} : NoInternalAssoc (empty S).edges (empty S).arcs

theorem Autosegmental.Graph.isTierOrdered_concat {S : Type u_2} {ι : Type u_3} {X : Graph S} {Y : Graph S} (t : S → ι) (h₁ : IsTierOrdered X.arcs (tier t X)) (h₂ : IsTierOrdered Y.arcs (tier t Y)) : IsTierOrdered (concat t X Y).arcs (tier t (concat t X Y))

The concatenation of tier-ordered graphs is tier-ordered.

theorem Autosegmental.Graph.noInternalAssoc_concat {S : Type u_2} {ι : Type u_3} {X : Graph S} {Y : Graph S} (t : S → ι) (h₁ : NoInternalAssoc X.edges X.arcs) (h₂ : NoInternalAssoc Y.edges Y.arcs) : NoInternalAssoc (concat t X Y).edges (concat t X Y).arcs

The concatenation of graphs with no internal association has no internal association.

theorem Autosegmental.Graph.isPlanar_concat {S : Type u_2} {ι : Type u_3} {X : Graph S} {Y : Graph S} (t : S → ι) (h₁ : IsPlanar X.edges X.arcs) (h₂ : IsPlanar Y.edges Y.arcs) : IsPlanar (concat t X Y).edges (concat t X Y).arcs

The concatenation of planar graphs is planar; this is the headline result of [Jar19].

theorem Autosegmental.Graph.not_isTierOrdered_sum {S : Type u_2} {ι : Type u_3} {X : Graph S} {Y : Graph S} (t : S → ι) (v : X.V) (w : Y.V) (htier : tier t X v = tier t Y w) : ¬IsTierOrdered (X.sum Y).arcs (tier t (X.sum Y))

The bridge-free sum of graphs sharing a tier is never tier-ordered, so Axiom 2 forces the bridges in concat.

The category of autosegmental representations

@[reducible, inline]

abbrev Autosegmental.AR {S : Type u_2} {ι : Type u_3} (t : S → ι) : Type (max u_2 (u_4 + 1))

The category of autosegmental representations over a tier assignment, given by the full subcategory on Axioms 1–3 of [Jar16b] §4.2. These are the formal literature's ARs ([Jar19], [CJ19]).

Equations

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

The monoidal structure: morpheme concatenation

def Autosegmental.AR.tierColoring {S : Type u_2} {ι : Type u_3} {t : S → ι} (X : AR t) : X.obj.edges.Coloring ι

The tier map is a proper coloring of the association graph; Goldsmith's bipartite two-tier geometry is the two-colorable case.

Equations

• X.tierColoring = SimpleGraph.Coloring.mk (Autosegmental.Graph.tier t X.obj) ⋯

theorem Autosegmental.AR.edges_colorable {S : Type u_2} {ι : Type u_3} {t : S → ι} [Fintype ι] (X : AR t) : X.obj.edges.Colorable (Fintype.card ι)

Tier arity bounds the chromatic number of the association pattern.

def Autosegmental.AR.mkIso {S : Type u_2} {ι : Type u_3} {t : S → ι} {X Y : AR t} (e : X.obj.Iso Y.obj) : X ≅ Y

A graph isomorphism as an isomorphism of representations.

Equations

• Autosegmental.AR.mkIso e = CategoryTheory.InducedCategory.isoMk { hom := e.toHom, inv := e.symm.toHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }

theorem Autosegmental.AR.hom_ext {S : Type u_2} {ι : Type u_3} {t : S → ι} {X Y : AR t} {f g : X ⟶ Y} (h : ∀ (v : X.obj.V), f.hom.toFun v = g.hom.toFun v) : f = g

Componentwise extensionality for representation morphisms.

@[instance_reducible]

instance Autosegmental.AR.instMonoidalStruct {S : Type u₁} {ι : Type u₂} {t : S → ι} : CategoryTheory.MonoidalCategoryStruct (AR t)

The monoidal structure with morpheme concatenation as tensor and the empty representation as unit. The universes are pinned because autobinding would split the instance head into a max; @[simps] feeds the tensor rewrites in NormalForm.lean.

Equations

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

@[simp]

theorem Autosegmental.AR.tensorHom_def {S : Type u₁} {ι : Type u₂} {t : S → ι} {X₁✝ Y₁✝ X₂✝ Y₂✝ : AR t} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.InducedCategory.homMk (Graph.Hom.concatMap t f.hom g.hom)

@[simp]

theorem Autosegmental.AR.leftUnitor_def {S : Type u₁} {ι : Type u₂} {t : S → ι} (X : AR t) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = mkIso (Graph.emptyConcatIso t X.obj)

@[simp]

theorem Autosegmental.AR.tensorUnit_obj {S : Type u₁} {ι : Type u₂} {t : S → ι} : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (AR t)).obj = Graph.empty S

@[simp]

theorem Autosegmental.AR.associator_def {S : Type u₁} {ι : Type u₂} {t : S → ι} (X Y Z : AR t) : CategoryTheory.MonoidalCategoryStruct.associator X Y Z = mkIso (Graph.concatAssocIso t X.obj Y.obj Z.obj)

@[simp]

theorem Autosegmental.AR.whiskerRight_def {S : Type u₁} {ι : Type u₂} {t : S → ι} {X₁✝ X₂✝ : AR t} (f : X₁✝ ⟶ X₂✝) (Y : AR t) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y = CategoryTheory.InducedCategory.homMk (Graph.Hom.concatMap t f.hom (Graph.Hom.id Y.obj))

@[simp]

theorem Autosegmental.AR.tensorObj_obj {S : Type u₁} {ι : Type u₂} {t : S → ι} (X Y : AR t) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj = Graph.concat t X.obj Y.obj

@[simp]

theorem Autosegmental.AR.whiskerLeft_def {S : Type u₁} {ι : Type u₂} {t : S → ι} (X x✝ x✝¹ : AR t) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = CategoryTheory.InducedCategory.homMk (Graph.Hom.concatMap t (Graph.Hom.id X.obj) f.hom)

@[simp]

theorem Autosegmental.AR.rightUnitor_def {S : Type u₁} {ι : Type u₂} {t : S → ι} (X : AR t) : CategoryTheory.MonoidalCategoryStruct.rightUnitor X = mkIso (Graph.concatEmptyIso t X.obj)

@[instance_reducible]

instance Autosegmental.AR.instMonoidalCategory {S : Type u_2} {ι : Type u_3} {t : S → ι} : CategoryTheory.MonoidalCategory (AR t)

The category of autosegmental representations is monoidal under concatenation; the coherence laws are [JH15] Theorems 1 and 3.

Equations

• Autosegmental.AR.instMonoidalCategory = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Autosegmental.AR.precPreserving {S : Type u_2} {ι : Type u_3} {t : S → ι} : CategoryTheory.MorphismProperty (AR t)

Precedence preservation on representations: the classical morphisms of the theory, as a monoidally-stable wide subcategory of the broad category.

Equations

• Autosegmental.AR.precPreserving f = Autosegmental.Graph.precPreserving f.hom

instance Autosegmental.AR.instIsMonoidalStablePrecPreserving {S : Type u_2} {ι : Type u_3} {t : S → ι} : precPreserving.IsMonoidalStable