The monoidal category of autosegmental representations

An autosegmental representation (APR; [Gol76]) of a word is a finite labeled bipartite graph: an upper tier of αs (the melody — tones, features), a lower tier of βs (the timing/segmental backbone), and a finite set of association lines between their positions. This file builds the object, its concatenation monoidal category, and the well-formed (planar) subcategory cut out by the No-Crossing Constraint, following [JH15].

The arc, in three layers:

• Graph α β — the bipartite object. Planarity IsPlanar is [Gol76]'s No-Crossing Constraint ([JH15] Axiom 4) — the sole structural well-formedness condition ([Pul86]); saturation (Goldsmith's original WFC) is language-particular, so floating elements are well-formed.
• AR α β — the in-bounds object (every association line falls within the tier lengths) and the base of the category; morphisms are label- and link-preserving position maps. concat is morpheme concatenation ([JH15] §5): the empty graph is the unit (Theorem 1) and concat is associative (Theorem 3). The paper calls it "a modification of [the] disjoint union"; its disjoint-union core — before the OCP-merging step, modeled separately as OCP.collapse — is the categorical coproduct (HasBinaryCoproducts), so the monoidal product is cocartesian.
• WellFormedAR α β — the full monoidal subcategory of planar ARs. The No-Crossing Constraint is morpheme-modular (ncc_isMonoidal, [JH15] Theorem 4): planarity is stable under ⊗. The OCP ([McC86]) is not (ocp_not_isMonoidal, Axiom 5) — concatenation can abut identical autosegments across a morpheme boundary — so it drives a boundary repair (OCP.collapse).

Main definitions

• Graph / AR / WellFormedAR — the three layers of the autosegmental object.
• Graph.IsPlanar — the No-Crossing Constraint, via the MonovaryOn-based NonCrossing substrate.
• AR.concat / AR.empty — concatenation and its unit; HasBinaryCoproduct exhibits concat as the categorical coproduct, empty as the initial object.
• MonoidalCategory (AR α β) / MonoidalCategory (WellFormedAR α β).

Main results

• Graph.isPlanar_concat — concatenation preserves planarity ([JH15] Theorem 4).
• ncc_isMonoidal / ocp_not_isMonoidal — the NCC is morpheme-modular, the OCP is not; ncc_modular_ocp_not is the discriminating dichotomy.
• collapse_repairs_boundary — fusion restores OCP-cleanness across a boundary.

Categorical recognition

AR α β is the Grothendieck construction ∫ F of the relation functor F : (LabeledTuple α × LabeledTuple β) ⥤ Cat sending a tier-pair (U, V) to the ⊆-poset of relations Finset (Fin U.len × Fin V.len) and a position-map pair to image-pushforward. An object is (tiers, relation); the Grothendieck fiber morphism — a ≤ in the thin poset fiber — is exactly Hom.links_preserve (image ⊆ target). So AR is the category of labeled finite bipartite graphs, and concat/empty are the coproduct/initial object it carries as such.

This is realized concretely, not via CategoryTheory.Grothendieck: the literal construction inherits only the bare Category (recorded here anyway as HasInitial and HasBinaryCoproduct), forces the Fin (m + n) length-casts that the raw-ℕ NonCrossing substrate and the omega-based consumers (Floating, LaoideKemp2026) are built to avoid, and leaves the monoidal/coproduct layer hand-built regardless — mathlib has neither a monoidal Grothendieck construction nor a cocartesian ofChosenFiniteCoproducts builder (both upstream TODOs). The choice mirrors LabeledTuple's and SimplexCategory's Fin-skeleton: state the universal properties as theorems, and keep a definitional tensorObj := concat for the decide/prop_tensor/eqToIso-coherence consumers.

Implementation notes

Tiers are LabeledTuples; links : Finset (ℕ × ℕ) keeps raw natural-number indexing — matching the MonovaryOn-based NonCrossing substrate and keeping the monoid laws free of dependent-type casts — with in-bounds a separable Prop (Graph.InBounds) rather than a structural invariant. Because the object-Monoid laws hold as strict equalities, the associator and unitors are eqToIso of mul_assoc/one_mul/mul_one, so AR is strict monoidal over its object-monoid.

The autosegmental graph (the bipartite object)

structure Autosegmental.Graph (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

A bipartite autosegmental representation: two ordered labeled tiers and a finite set of association lines (index pairs) between them.

• upper : LabeledTuple α

  The upper tier (e.g., tonal tier, melodic tier, root).

• lower : LabeledTuple β

  The lower tier (e.g., segmental backbone, skeleton, template).

• links : Finset (ℕ × ℕ)

  Association lines as a finite set of index pairs (upper-index, lower-index).

theorem Autosegmental.Graph.ext {α : Type u_1} {β : Type u_2} {x y : Graph α β} (upper : x.upper = y.upper) (lower : x.lower = y.lower) (links : x.links = y.links) : x = y

theorem Autosegmental.Graph.ext_iff {α : Type u_1} {β : Type u_2} {x y : Graph α β} : x = y ↔ x.upper = y.upper ∧ x.lower = y.lower ∧ x.links = y.links

def Autosegmental.instDecidableEqGraph.decEq {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : Graph α✝ β✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Autosegmental.instDecidableEqGraph {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] : DecidableEq (Graph α✝ β✝)

Equations

• Autosegmental.instDecidableEqGraph = Autosegmental.instDecidableEqGraph.decEq

Construction

def Autosegmental.Graph.empty {α : Type u_1} {β : Type u_2} : Graph α β

The empty bipartite representation with no tiers and no links.

Equations

• Autosegmental.Graph.empty = { upper := LabeledTuple.empty, lower := LabeledTuple.empty, links := ∅ }

Planarity (no-crossing)

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

Planar (no-crossing): the link set satisfies [Gol76]'s NCC.

Equations

• r.IsPlanar = Autosegmental.IsNonCrossing r.links

Link rewrites

def Autosegmental.Graph.link {α : Type u_1} {β : Type u_2} (r : Graph α β) (i j : ℕ) : Graph α β

Add an association line — the elementary spread step.

Equations

• r.link i j = { upper := r.upper, lower := r.lower, links := insert (i, j) r.links }

def Autosegmental.Graph.delink {α : Type u_1} {β : Type u_2} (r : Graph α β) (i j : ℕ) : Graph α β

Erase an association line — the elementary delink step.

Equations

• r.delink i j = { upper := r.upper, lower := r.lower, links := r.links.erase (i, j) }

@[simp]

theorem Autosegmental.Graph.mem_link_links {α : Type u_1} {β : Type u_2} (r : Graph α β) {i j : ℕ} {p : ℕ × ℕ} : p ∈ (r.link i j).links ↔ p = (i, j) ∨ p ∈ r.links

@[simp]

theorem Autosegmental.Graph.mem_delink_links {α : Type u_1} {β : Type u_2} (r : Graph α β) {i j : ℕ} {p : ℕ × ℕ} : p ∈ (r.delink i j).links ↔ p ≠ (i, j) ∧ p ∈ r.links

@[simp]

theorem Autosegmental.Graph.link_upper {α : Type u_1} {β : Type u_2} (r : Graph α β) (i j : ℕ) : (r.link i j).upper = r.upper

@[simp]

theorem Autosegmental.Graph.delink_upper {α : Type u_1} {β : Type u_2} (r : Graph α β) (i j : ℕ) : (r.delink i j).upper = r.upper

Index predicates

def Autosegmental.Graph.IsLinkedUpper {α : Type u_1} {β : Type u_2} (r : Graph α β) (i : ℕ) : Prop

Upper index i is linked to some lower position (no in-bounds check).

Equations

• r.IsLinkedUpper i = ∃ p ∈ r.links, p.1 = i

def Autosegmental.Graph.IsLinkedLower {α : Type u_1} {β : Type u_2} (r : Graph α β) (j : ℕ) : Prop

Lower index j is linked to some upper position (no in-bounds check).

Equations

• r.IsLinkedLower j = ∃ p ∈ r.links, p.2 = j

theorem Autosegmental.Graph.isLinkedLower_iff {α : Type u_1} {β : Type u_2} (r : Graph α β) {j : ℕ} : r.IsLinkedLower j ↔ ∃ (i : ℕ), (i, j) ∈ r.links

def Autosegmental.Graph.SurfacesWith {α : Type u_1} {β : Type u_2} (r : Graph α β) (a : α) (j : ℕ) : Prop

Lower node j surfaces with label a: some a-labeled upper node is linked to it — the labeled refinement of IsLinkedLower.

Equations

• r.SurfacesWith a j = ∃ (i : ℕ), (i, j) ∈ r.links ∧ r.upper.get? i = some a

theorem Autosegmental.Graph.SurfacesWith.isLinkedLower {α : Type u_1} {β : Type u_2} (r : Graph α β) {a : α} {j : ℕ} (h : r.SurfacesWith a j) : r.IsLinkedLower j

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableSurfacesWithOfDecidableEq {α : Type u_1} {β : Type u_2} (r : Graph α β) [DecidableEq α] (a : α) (j : ℕ) : Decidable (r.SurfacesWith a j)

Equations

• r.instDecidableSurfacesWithOfDecidableEq a j = decidable_of_iff (∃ p ∈ r.links, p.2 = j ∧ r.upper.get? p.1 = some a) ⋯

def Autosegmental.Graph.IsFloatingUpper {α : Type u_1} {β : Type u_2} (r : Graph α β) (i : ℕ) : Prop

Upper index i is floating: in-bounds but unlinked.

Equations

• r.IsFloatingUpper i = (i < r.upper.len ∧ ¬r.IsLinkedUpper i)

def Autosegmental.Graph.IsFloatingLower {α : Type u_1} {β : Type u_2} (r : Graph α β) (j : ℕ) : Prop

Lower index j is floating: in-bounds but unlinked (segmentally empty).

Equations

• r.IsFloatingLower j = (j < r.lower.len ∧ ¬r.IsLinkedLower j)

Decidability of index predicates

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableIsLinkedUpper {α : Type u_1} {β : Type u_2} (r : Graph α β) (i : ℕ) : Decidable (r.IsLinkedUpper i)

Equations

• r.instDecidableIsLinkedUpper i = Autosegmental.Graph.instDecidableIsLinkedUpper._aux_1 r i

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableIsLinkedLower {α : Type u_1} {β : Type u_2} (r : Graph α β) (j : ℕ) : Decidable (r.IsLinkedLower j)

Equations

• r.instDecidableIsLinkedLower j = Autosegmental.Graph.instDecidableIsLinkedLower._aux_1 r j

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableIsFloatingUpper {α : Type u_1} {β : Type u_2} (r : Graph α β) (i : ℕ) : Decidable (r.IsFloatingUpper i)

Equations

• r.instDecidableIsFloatingUpper i = Autosegmental.Graph.instDecidableIsFloatingUpper._aux_1 r i

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableIsFloatingLower {α : Type u_1} {β : Type u_2} (r : Graph α β) (j : ℕ) : Decidable (r.IsFloatingLower j)

Equations

• r.instDecidableIsFloatingLower j = Autosegmental.Graph.instDecidableIsFloatingLower._aux_1 r j

theorem Autosegmental.Graph.isPlanar_empty {α : Type u_1} {β : Type u_2} : empty.IsPlanar

The empty representation is planar (vacuously).

In-bounds predicate

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

Every link's indices fall within the tier lengths.

Equations

• r.InBounds = ∀ p ∈ r.links, p.1 < r.upper.len ∧ p.2 < r.lower.len

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableInBounds {α : Type u_1} {β : Type u_2} (r : Graph α β) : Decidable r.InBounds

Equations

• r.instDecidableInBounds = Autosegmental.Graph.instDecidableInBounds._aux_1 r

theorem Autosegmental.Graph.inBounds_empty {α : Type u_1} {β : Type u_2} : empty.InBounds

Concatenation ([JH15])

def Autosegmental.Graph.concat {α : Type u_1} {β : Type u_2} (A B : Graph α β) : Graph α β

[JH15] concatenation: tier-concatenation plus index-shifted link-set union.

Equations

• A.concat B = { upper := A.upper.concat B.upper, lower := A.lower.concat B.lower, links := A.links ∪ Finset.image (Autosegmental.shiftLink A.upper.len A.lower.len) B.links }

@[simp]

theorem Autosegmental.Graph.upper_concat {α : Type u_1} {β : Type u_2} (A B : Graph α β) : (A.concat B).upper = A.upper.concat B.upper

@[simp]

theorem Autosegmental.Graph.lower_concat {α : Type u_1} {β : Type u_2} (A B : Graph α β) : (A.concat B).lower = A.lower.concat B.lower

@[simp]

theorem Autosegmental.Graph.links_concat {α : Type u_1} {β : Type u_2} (A B : Graph α β) : (A.concat B).links = A.links ∪ Finset.image (shiftLink A.upper.len A.lower.len) B.links

Monoid laws ([JH15] Theorems 1, 3)

theorem Autosegmental.Graph.empty_concat {α : Type u_1} {β : Type u_2} (A : Graph α β) : empty.concat A = A

empty is a left identity for concat.

theorem Autosegmental.Graph.concat_empty {α : Type u_1} {β : Type u_2} (A : Graph α β) : A.concat empty = A

empty is a right identity for concat.

theorem Autosegmental.Graph.concat_assoc {α : Type u_1} {β : Type u_2} (A B C : Graph α β) : (A.concat B).concat C = A.concat (B.concat C)

concat is associative.

def Autosegmental.Graph.concatList {α : Type u_1} {β : Type u_2} (gs : List (Graph α β)) : Graph α β

Left-to-right concatenation of a list of graphs ([JH15] §5): tier juxtaposition with index-shifted links.

Equations

• Autosegmental.Graph.concatList gs = List.foldr Autosegmental.Graph.concat Autosegmental.Graph.empty gs

@[simp]

theorem Autosegmental.Graph.concatList_nil {α : Type u_1} {β : Type u_2} : concatList [] = empty

@[simp]

theorem Autosegmental.Graph.concatList_cons {α : Type u_1} {β : Type u_2} (g : Graph α β) (gs : List (Graph α β)) : concatList (g :: gs) = g.concat (concatList gs)

Planarity preservation ([JH15] Theorem 4)

theorem Autosegmental.Graph.isPlanar_concat {α : Type u_1} {β : Type u_2} {A B : Graph α β} (hAib : A.InBounds) (hA : A.IsPlanar) (hB : B.IsPlanar) : (A.concat B).IsPlanar

Concatenation preserves planarity, given A.InBounds: A.links and the shifted B.links are each non-crossing (monovaryOn_union + isNonCrossing_image_shiftLink), and A sits entirely before B.

theorem Autosegmental.Graph.inBounds_concat {α : Type u_1} {β : Type u_2} {A B : Graph α β} (hA : A.InBounds) (hB : B.InBounds) : (A.concat B).InBounds

Concatenation preserves in-bounds.

The in-bounds object AR and its monoidal category

structure Autosegmental.AR (α : Type u_3) (β : Type u_4) extends Autosegmental.Graph α β : Type (max u_3 u_4)

The base object of the autosegmental category: an in-bounds autosegmental graph (every association line falls within the tier lengths). Planarity is not carried here — it is the constraint defining the subcategory WellFormedAR.

• upper : LabeledTuple α
• lower : LabeledTuple β
• links : Finset (ℕ × ℕ)
• inBounds : self.InBounds

Morphisms

structure Autosegmental.AR.Hom {α : Type u_1} {β : Type u_2} (A B : AR α β) : Type

A label- and link-preserving morphism. The tier maps are LabeledTuple.Homs (each bundles a position map with its label-preservation b.label ∘ f = a.label); link preservation routes a link's (in-bounds) endpoints through those maps.

• fU : A.upper.Hom B.upper

  Vertex map on the upper tier (a label-preserving LabeledTuple morphism).

• fL : A.lower.Hom B.lower

  Vertex map on the lower tier.

• links_preserve {i j : ℕ} (hi : i < A.upper.len) (hj : j < A.lower.len) : (i, j) ∈ A.links → (↑(self.fU.toFun ⟨i, hi⟩), ↑(self.fL.toFun ⟨j, hj⟩)) ∈ B.links

  Association lines are preserved.

theorem Autosegmental.AR.Hom.ext {α : Type u_1} {β : Type u_2} {A B : AR α β} {x y : A.Hom B} (fU : x.fU = y.fU) (fL : x.fL = y.fL) : x = y

theorem Autosegmental.AR.Hom.ext_iff {α : Type u_1} {β : Type u_2} {A B : AR α β} {x y : A.Hom B} : x = y ↔ x.fU = y.fU ∧ x.fL = y.fL

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

The identity morphism.

Equations

• Autosegmental.AR.Hom.id A = { fU := LabeledTuple.Hom.id A.upper, fL := LabeledTuple.Hom.id A.lower, links_preserve := ⋯ }

def Autosegmental.AR.Hom.comp {α : Type u_1} {β : Type u_2} {A B C : AR α β} (f : A.Hom B) (g : B.Hom C) : A.Hom C

Composition of morphisms (diagrammatic: f then g).

Equations

• f.comp g = { fU := f.fU.comp g.fU, fL := f.fL.comp g.fL, links_preserve := ⋯ }

@[simp]

theorem Autosegmental.AR.Hom.id_fU {α : Type u_1} {β : Type u_2} (A : AR α β) : (id A).fU = LabeledTuple.Hom.id A.upper

@[simp]

theorem Autosegmental.AR.Hom.id_fL {α : Type u_1} {β : Type u_2} (A : AR α β) : (id A).fL = LabeledTuple.Hom.id A.lower

@[simp]

theorem Autosegmental.AR.Hom.comp_fU {α : Type u_1} {β : Type u_2} {A B C : AR α β} (f : A.Hom B) (g : B.Hom C) : (f.comp g).fU = f.fU.comp g.fU

@[simp]

theorem Autosegmental.AR.Hom.comp_fL {α : Type u_1} {β : Type u_2} {A B C : AR α β} (f : A.Hom B) (g : B.Hom C) : (f.comp g).fL = f.fL.comp g.fL

theorem Autosegmental.AR.Hom.ext_fin {α : Type u_1} {β : Type u_2} {A B : AR α β} {f g : A.Hom B} (hU : ∀ (i : Fin A.upper.len), ↑(f.fU.toFun i) = ↑(g.fU.toFun i)) (hL : ∀ (j : Fin A.lower.len), ↑(f.fL.toFun j) = ↑(g.fL.toFun j)) : f = g

Extensionality at the index level: morphisms agree if their tier maps agree on the underlying ℕ indices. Collapses the Hom.ext → LabeledTuple.Hom.ext → funext → Fin.ext ladder used throughout the category/coherence proofs.

@[implicit_reducible]

instance Autosegmental.AR.instCategoryStruct {α : Type u_1} {β : Type u_2} : CategoryTheory.CategoryStruct.{0, max u_2 u_1} (AR α β)

Equations

• Autosegmental.AR.instCategoryStruct = { Hom := Autosegmental.AR.Hom, id := Autosegmental.AR.Hom.id, comp := fun {X Y Z : Autosegmental.AR α β} (f : X.Hom Y) (g : Y.Hom Z) => f.comp g }

@[implicit_reducible]

instance Autosegmental.AR.instCategory {α : Type u_1} {β : Type u_2} : CategoryTheory.Category.{0, max u_2 u_1} (AR α β)

Equations

• Autosegmental.AR.instCategory = { toCategoryStruct := Autosegmental.AR.instCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

@[simp]

theorem Autosegmental.AR.id_fU' {α : Type u_1} {β : Type u_2} (A : AR α β) : (CategoryTheory.CategoryStruct.id A).fU = CategoryTheory.CategoryStruct.id A.upper

@[simp]

theorem Autosegmental.AR.id_fL' {α : Type u_1} {β : Type u_2} (A : AR α β) : (CategoryTheory.CategoryStruct.id A).fL = CategoryTheory.CategoryStruct.id A.lower

@[simp]

theorem Autosegmental.AR.comp_fU' {α : Type u_1} {β : Type u_2} {A B C : AR α β} (f : A ⟶ B) (g : B ⟶ C) : (CategoryTheory.CategoryStruct.comp f g).fU = f.fU.comp g.fU

@[simp]

theorem Autosegmental.AR.comp_fL' {α : Type u_1} {β : Type u_2} {A B C : AR α β} (f : A ⟶ B) (g : B ⟶ C) : (CategoryTheory.CategoryStruct.comp f g).fL = f.fL.comp g.fL

Concatenation: the tensor object

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

Morpheme concatenation ([JH15]): the tier-concatenated, index-shifted graph, in-bounds by Graph.inBounds_concat.

Equations

• A.concat B = { toGraph := A.concat B.toGraph, inBounds := ⋯ }

@[simp]

theorem Autosegmental.AR.concat_toGraph {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.concat B).toGraph = A.concat B.toGraph

@[simp]

theorem Autosegmental.AR.concat_upper {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.concat B).upper = A.upper.concat B.upper

@[simp]

theorem Autosegmental.AR.concat_lower {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.concat B).lower = A.lower.concat B.lower

theorem Autosegmental.AR.links_concat {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.concat B).links = A.links ∪ Finset.image (shiftLink A.upper.len A.lower.len) B.links

The concatenation bifunctor concatMap (the tensor on morphisms)

The tier action delegates to the keystone LabeledTuple.Hom.concatMap; only link preservation is bespoke, routing the A-block through f (unshifted) and the B-block through g (shifted past A') via Fin.appendMap_val.

def Autosegmental.AR.Hom.concatMap {α : Type u_1} {β : Type u_2} {A A' B B' : AR α β} (f : A.Hom A') (g : B.Hom B') : (A.concat B).Hom (A'.concat B')

The concatenation bifunctor on morphisms (f ⊗ g): f on the A-block, g (shifted) on the B-block. Tiers via LabeledTuple.Hom.concatMap.

Equations

• f.concatMap g = { fU := f.fU.concatMap g.fU, fL := f.fL.concatMap g.fL, links_preserve := ⋯ }

@[simp]

theorem Autosegmental.AR.Hom.concatMap_fU {α : Type u_1} {β : Type u_2} {A A' B B' : AR α β} (f : A.Hom A') (g : B.Hom B') : (f.concatMap g).fU = f.fU.concatMap g.fU

@[simp]

theorem Autosegmental.AR.Hom.concatMap_fL {α : Type u_1} {β : Type u_2} {A A' B B' : AR α β} (f : A.Hom A') (g : B.Hom B') : (f.concatMap g).fL = f.fL.concatMap g.fL

theorem Autosegmental.AR.Hom.concatMap_id {α : Type u_1} {β : Type u_2} (A B : AR α β) : (id A).concatMap (id B) = id (A.concat B)

The concat bifunctor preserves identities (tensor_id).

theorem Autosegmental.AR.Hom.concatMap_comp {α : Type u_1} {β : Type u_2} {A A' A'' B B' B'' : AR α β} (f : A.Hom A') (f' : A'.Hom A'') (g : B.Hom B') (g' : B'.Hom B'') : (f.concatMap g).comp (f'.concatMap g') = (f.comp f').concatMap (g.comp g')

The concat bifunctor preserves composition (tensor_comp).

Monoid structure on objects

def Autosegmental.AR.empty {α : Type u_1} {β : Type u_2} : AR α β

The empty (unit) object: no tiers, no links.

Equations

• Autosegmental.AR.empty = { toGraph := Autosegmental.Graph.empty, inBounds := ⋯ }

theorem Autosegmental.AR.ext_toGraph {α : Type u_1} {β : Type u_2} {A B : AR α β} (h : A.toGraph = B.toGraph) : A = B

Two ARs are equal iff their underlying graphs are (inBounds by proof irrelevance).

theorem Autosegmental.AR.ext_toGraph_iff {α : Type u_1} {β : Type u_2} {A B : AR α β} : A = B ↔ A.toGraph = B.toGraph

theorem Autosegmental.AR.toGraph_injective {α : Type u_1} {β : Type u_2} : Function.Injective toGraph

@[implicit_reducible]

instance Autosegmental.AR.instDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] : DecidableEq (AR α β)

Equations

• A.instDecidableEq B = decidable_of_iff (A.toGraph = B.toGraph) ⋯

@[implicit_reducible]

instance Autosegmental.AR.instMonoid {α : Type u_1} {β : Type u_2} : Monoid (AR α β)

Objects form a Monoid under concatenation, with empty as unit ([JH15] Theorems 1, 3): the laws lift the Graph monoid laws through ext_toGraph.

Equations

• Autosegmental.AR.instMonoid = { mul := Autosegmental.AR.concat, mul_assoc := ⋯, one := Autosegmental.AR.empty, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[simp]

theorem Autosegmental.AR.mul_eq_concat {α : Type u_1} {β : Type u_2} (A B : AR α β) : A * B = A.concat B

@[simp]

theorem Autosegmental.AR.one_eq_empty {α : Type u_1} {β : Type u_2} : 1 = empty

Concatenation is the categorical coproduct

empty is the initial object and concat the categorical coproduct — the disjoint union of the two labeled bipartite graphs, with coprojections the tier coprojections (LabeledTuple.inl/inr) carrying links forward. This is the autosegmental analogue of LabeledTuple's cocartesian structure (and of disjoint-union-of-graphs). [JH15] describes concatenation as "a modification of [the] disjoint union" (§5) with the empty graph as identity (Theorem 1); its disjoint-union core — the part before the OCP-merging modification, modeled separately as OCP.collapse — is exactly this coproduct. So the monoidal product is cocartesian.

instance Autosegmental.AR.instSubsingletonHomEmpty {α : Type u_1} {β : Type u_2} (Y : AR α β) : Subsingleton (empty ⟶ Y)

instance Autosegmental.AR.instNonemptyHomEmpty {α : Type u_1} {β : Type u_2} (Y : AR α β) : Nonempty (empty ⟶ Y)

instance Autosegmental.AR.instHasInitial {α : Type u_1} {β : Type u_2} : CategoryTheory.Limits.HasInitial (AR α β)

def Autosegmental.AR.inl {α : Type u_1} {β : Type u_2} (A B : AR α β) : A.Hom (A.concat B)

The left coprojection A ⟶ A.concat B: tier inclusions plus the identity on A's links, which sit unshifted in the first block.

Equations

• A.inl B = { fU := A.upper.inl B.upper, fL := A.lower.inl B.lower, links_preserve := ⋯ }

def Autosegmental.AR.inr {α : Type u_1} {β : Type u_2} (A B : AR α β) : B.Hom (A.concat B)

The right coprojection B ⟶ A.concat B: tier inclusions plus A's index-shift on B's links (the second block).

Equations

• A.inr B = { fU := A.upper.inr B.upper, fL := A.lower.inr B.lower, links_preserve := ⋯ }

def Autosegmental.AR.coprodDesc {α : Type u_1} {β : Type u_2} {A B T : AR α β} (f : A.Hom T) (g : B.Hom T) : (A.concat B).Hom T

The copairing of f : A ⟶ T and g : B ⟶ T: f on the first block, g on the (shifted) second block — Fin.append on tiers, case-split on links.

Equations

• Autosegmental.AR.coprodDesc f g = { fU := LabeledTuple.coprodDesc f.fU g.fU, fL := LabeledTuple.coprodDesc f.fL g.fL, links_preserve := ⋯ }

@[simp]

theorem Autosegmental.AR.inl_fU {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.inl B).fU = A.upper.inl B.upper

@[simp]

theorem Autosegmental.AR.inl_fL {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.inl B).fL = A.lower.inl B.lower

@[simp]

theorem Autosegmental.AR.inr_fU {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.inr B).fU = A.upper.inr B.upper

@[simp]

theorem Autosegmental.AR.inr_fL {α : Type u_1} {β : Type u_2} (A B : AR α β) : (A.inr B).fL = A.lower.inr B.lower

@[simp]

theorem Autosegmental.AR.coprodDesc_fU {α : Type u_1} {β : Type u_2} {A B T : AR α β} (f : A.Hom T) (g : B.Hom T) : (coprodDesc f g).fU = LabeledTuple.coprodDesc f.fU g.fU

@[simp]

theorem Autosegmental.AR.coprodDesc_fL {α : Type u_1} {β : Type u_2} {A B T : AR α β} (f : A.Hom T) (g : B.Hom T) : (coprodDesc f g).fL = LabeledTuple.coprodDesc f.fL g.fL

instance Autosegmental.AR.instHasBinaryCoproduct {α : Type u_1} {β : Type u_2} (A B : AR α β) : CategoryTheory.Limits.HasBinaryCoproduct A B

concat is the categorical coproduct: inl/inr are the coprojections and coprodDesc the copairing — the disjoint-union universal property.

instance Autosegmental.AR.instHasBinaryCoproducts {α : Type u_1} {β : Type u_2} : CategoryTheory.Limits.HasBinaryCoproducts (AR α β)

Monoidal category structure

(AR α β, concat, empty) is a monoidal category. Because the object Monoid laws hold as strict equalities, the associator and unitors are eqToIso of mul_assoc/one_mul/mul_one, so the coherence laws reduce to eqToHom algebra (pentagon, triangle) or Fin-index arithmetic (naturalities).

@[simp]

theorem Autosegmental.AR.eqToHom_fU_toFun {α : Type u_1} {β : Type u_2} {A B : AR α β} (h : A = B) : (CategoryTheory.eqToHom h).fU.toFun = Fin.cast ⋯

The upper tier map of an eqToHom, as a function: the length-cast Fin.cast (goes straight to the len level, avoiding a nested LabeledTuple eqToHom).

@[simp]

theorem Autosegmental.AR.eqToHom_fL_toFun {α : Type u_1} {β : Type u_2} {A B : AR α β} (h : A = B) : (CategoryTheory.eqToHom h).fL.toFun = Fin.cast ⋯

The lower tier map of an eqToHom, as a function.

@[simp]

theorem Autosegmental.AR.concatMap_id_eqToHom {α : Type u_1} {β : Type u_2} {W X Y : AR α β} (h : X = Y) : Hom.concatMap (CategoryTheory.CategoryStruct.id W) (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯

Tensoring an identity (left) with an eqToHom (right) is an eqToHom.

@[simp]

theorem Autosegmental.AR.concatMap_eqToHom_id {α : Type u_1} {β : Type u_2} {W X Y : AR α β} (h : X = Y) : Hom.concatMap (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.id W) = CategoryTheory.eqToHom ⋯

Tensoring an eqToHom (left) with an identity (right) is an eqToHom.

@[implicit_reducible]

instance Autosegmental.AR.instMonoidalStruct {α : Type u_1} {β : Type u_2} : CategoryTheory.MonoidalCategoryStruct (AR α β)

The tensor is concat; associator and unitors are eqToIso of the object Monoid laws (AR is strict monoidal over its object-monoid).

Equations

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

@[simp]

theorem Autosegmental.AR.whiskerRight_def {α : Type u_1} {β : Type u_2} {X₁✝ X₂✝ : AR α β} (f : X₁✝ ⟶ X₂✝) (Y : AR α β) : CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y = Hom.concatMap f (Hom.id Y)

@[simp]

theorem Autosegmental.AR.tensorObj_def {α : Type u_1} {β : Type u_2} (A B : AR α β) : CategoryTheory.MonoidalCategoryStruct.tensorObj A B = A.concat B

@[simp]

theorem Autosegmental.AR.leftUnitor_def {α : Type u_1} {β : Type u_2} (X : AR α β) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = CategoryTheory.eqToIso ⋯

@[simp]

theorem Autosegmental.AR.rightUnitor_def {α : Type u_1} {β : Type u_2} (X : AR α β) : CategoryTheory.MonoidalCategoryStruct.rightUnitor X = CategoryTheory.eqToIso ⋯

@[simp]

theorem Autosegmental.AR.tensorHom_def {α : Type u_1} {β : Type u_2} {X₁✝ Y₁✝ X₂✝ Y₂✝ : AR α β} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategoryStruct.tensorHom f g = Hom.concatMap f g

@[simp]

theorem Autosegmental.AR.tensorUnit_def {α : Type u_1} {β : Type u_2} : CategoryTheory.MonoidalCategoryStruct.tensorUnit (AR α β) = empty

@[simp]

theorem Autosegmental.AR.whiskerLeft_def {α : Type u_1} {β : Type u_2} (X x✝ x✝¹ : AR α β) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = (Hom.id X).concatMap f

@[simp]

theorem Autosegmental.AR.associator_def {α : Type u_1} {β : Type u_2} (A B C : AR α β) : CategoryTheory.MonoidalCategoryStruct.associator A B C = CategoryTheory.eqToIso ⋯

@[simp]

theorem Autosegmental.AR.tensorObj_eq_mul {α : Type u_1} {β : Type u_2} (A B : AR α β) : CategoryTheory.MonoidalCategoryStruct.tensorObj A B = A * B

The monoidal product is the object-monoid multiplication (both are concat): the explicit bridge between the categorical ⊗ and the decategorified *.

@[implicit_reducible]

instance Autosegmental.AR.instMonoidalCategory {α : Type u_1} {β : Type u_2} : CategoryTheory.MonoidalCategory (AR α β)

Equations

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

The well-formed (planar) monoidal subcategory

Planarity as a monoidal object-property

def Autosegmental.isPlanar {α : Type u_3} {β : Type u_4} : CategoryTheory.ObjectProperty (AR α β)

Planarity (Goldsmith's NCC) as a property of the base object AR.

Equations

• Autosegmental.isPlanar A = A.IsPlanar

instance Autosegmental.instIsMonoidalIsPlanar {α : Type u_3} {β : Type u_4} : isPlanar.IsMonoidal

Planarity is a monoidal property: the unit is planar and concat preserves planarity (using the left factor's in-boundedness via Graph.isPlanar_concat). This is the categorical content of [JH15]'s NCC-preservation result (their Theorem 4: every concatenation satisfies the NCC).

@[reducible, inline]

abbrev Autosegmental.WellFormedAR (α : Type u_5) (β : Type u_6) : Type (max u_5 u_6)

The well-formed autosegmental category WellFormedAR α β: the full monoidal subcategory of AR cut out by planarity. Objects are planar in-bounds graphs; the MonoidalCategory instance is inherited from AR via ObjectProperty.fullMonoidalSubcategory.

Equations

• Autosegmental.WellFormedAR α β = Autosegmental.isPlanar.FullSubcategory

@[reducible, inline]

abbrev Autosegmental.WellFormedAR.mk {α : Type u_3} {β : Type u_4} (A : AR α β) (h : A.IsPlanar) : WellFormedAR α β

Build a WellFormedAR from an in-bounds representation and a planarity proof.

Equations

• Autosegmental.WellFormedAR.mk A h = { obj := A, property := h }

The No-Crossing Constraint is morpheme-modular

theorem Autosegmental.ncc_isMonoidal {α : Type u_3} {β : Type u_4} : isPlanar.IsMonoidal

The No-Crossing Constraint ([Gol76], [Pul86]) is morpheme-modular: planarity is a monoidal property of AR, so the planar (well-formed) ARs form the monoidal subcategory WellFormedAR. This is the linguistic content witnessed by the MonoidalCategory (WellFormedAR α β) instance.

The OCP is not morpheme-modular

def Autosegmental.upperOCPClean {α : Type u_3} {β : Type u_4} : CategoryTheory.ObjectProperty (AR α β)

The OCP ([McC86]) as a property of AR: the autosegmental (upper) tier has no adjacent identical elements.

Equations

• Autosegmental.upperOCPClean A = OCP.IsClean A.upper.toList

@[implicit_reducible]

instance Autosegmental.instDecidableUpperOCPCleanOfDecidableEq {α : Type u_3} {β : Type u_4} [DecidableEq α] (A : AR α β) : Decidable (upperOCPClean A)

Equations

• Autosegmental.instDecidableUpperOCPCleanOfDecidableEq A = Autosegmental.instDecidableUpperOCPCleanOfDecidableEq._aux_1 A

theorem Autosegmental.ocp_not_isMonoidal : ¬upperOCPClean.IsMonoidal

OCP-cleanness is not closed under the bare coproduct ⊗ (concat): concatenation can abut an identical autosegment pair at the morpheme boundary — a violation present in neither factor. Witnessed by two single-autosegment reps (⟨[true], [], ∅⟩) whose concatenation has upper tier [true, true]. This is why [JH15] build the melody-tier merge into their concatenation ◦: the bare coproduct here is ◦ with the merge stripped out, and the merge restores the OCP (their Theorem 5; OCP.collapse as the repair, collapse_repairs_boundary; Collapse.isCleanAR_gconcatAR for closure under ◦). So the OCP is a monoidal quotient (closed under fusion-◦), not a monoidal sub-object (closed under the coproduct) — the dual situation to the NCC (ncc_isMonoidal).

theorem Autosegmental.ncc_modular_ocp_not : isPlanar.IsMonoidal ∧ ¬upperOCPClean.IsMonoidal

The discriminating dichotomy ([JH15] Theorems 4 vs 5): under the bare coproduct ⊗ the NCC is preserved (closed, a monoidal sub-object) but the OCP is not (boundary-spanning). The OCP is recovered only as a quotient, by the fusion merge that ◦ builds in. The two halves cannot be interchanged — that is what makes the monoidal product load-bearing rather than decorative.

Fusion as the forced boundary repair

theorem Autosegmental.collapse_repairs_boundary {α : Type u_3} {β : Type u_4} [DecidableEq α] (A B : Graph α β) : OCP.IsClean (OCP.collapse (A.concat B).upper.toList)

Because the OCP is not morpheme-modular, well-formedness must be restored at the morpheme boundary by a repair. [McC86]'s fusion (OCP.collapse) is exactly such a repair: it maps the autosegmental tier of any concatenation back into the OCP-clean set. The non-modularity of the OCP (ocp_not_isMonoidal) is what makes a repair necessary; this theorem exhibits one.