Normal forms of autosegmental representations

Every finite representation is isomorphic to its normal form: the same representation reindexed onto the canonical vertex type (i : ι) × Fin nᵢ, each tier fiber enumerated in ascending precedence order (the fiber IsStrictTotalOrder instance → linearOrderOfSTO → monoEquivOfFin). The normal form is an AR — not a separate carrier — and normalizeIso is definitional: normalize pulls the graph back along the enumeration equivalence.

Main definitions

• AR.fiber, AR.fiberEnum, AR.vertexEquiv: the tier fibers of a finite representation and their canonical enumerations.
• AR.tierLength, AR.tierWord, AR.linkRel, AR.link: the tuple reading — per-tier sizes, label words, and position-coordinate links.
• AR.normalize: the normal form; AR.ofData: representations from tuple data.

Main results

• AR.normalizeIso: X.normalize ≅ X.
• AR.arcs_normalize, AR.edges_normalize: on normal forms the arcs are the ascending position order and the edges are linkRel — [JH15]'s tiered presentation recovered as a theorem.
• AR.tierWord_tensor, AR.link_tensor: concatenation appends tier words and shifts links blockwise.
• AR.isoOfReaderEq: (tierWord, link) is a complete isomorphism invariant.

@[reducible, inline]

abbrev Autosegmental.TieredAR (ι : Type u_3) (τ : ι → Type u_4) : Type (max (max u_3 u_4) (u_5 + 1))

Representations over the sigma alphabet (i : ι) × τ i with its native tier projection Sigma.fst — the coordinate carrier of the normal-form theory.

Equations

• Autosegmental.TieredAR ι τ = Autosegmental.AR Sigma.fst

def Autosegmental.AR.fiber {ι : Type u_1} {τ : ι → Type u_2} (X : TieredAR ι τ) (i : ι) : Type u_3

The vertices of X.obj labelled to tier i.

Equations

• Autosegmental.AR.fiber X i = { v : X.obj.V // (X.obj.label v).fst = i }

def Autosegmental.AR.fiberLabel {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} {i : ι} (v : fiber X i) : τ i

The τ i component of a fiber element, extracted from the labeling by transporting along the fiber's tier-membership witness.

Equations

• Autosegmental.AR.fiberLabel v = ⋯ ▸ (X.obj.label ↑v).snd

theorem Autosegmental.AR.label_fiber {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} {i : ι} (v : fiber X i) : X.obj.label ↑v = ⟨i, fiberLabel v⟩

The label of a fiber element decomposes as tier plus fiberLabel.

instance Autosegmental.AR.fiber.instFinite {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) : Finite (fiber X i)

instance Autosegmental.AR.fiber.instIsStrictTotalOrder {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} (i : ι) : IsStrictTotalOrder (fiber X i) fun (a b : fiber X i) => X.obj.arcs.Adj ↑a ↑b

The arcs restricted to a tier fiber form a strict total order.

@[implicit_reducible]

noncomputable instance Autosegmental.AR.fiber.instLinearOrder {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} (i : ι) : LinearOrder (fiber X i)

Classical linear order on the fiber, from IsStrictTotalOrder via linearOrderOfSTO.

Equations

• Autosegmental.AR.fiber.instLinearOrder i = linearOrderOfSTO fun (a b : Autosegmental.AR.fiber X i) => X.obj.arcs.Adj ↑a ↑b

noncomputable def Autosegmental.AR.tierLength {ι : Type u_1} {τ : ι → Type u_2} (X : TieredAR ι τ) [Finite X.obj.V] (i : ι) : ℕ

The number of tier-i vertices.

Equations

• Autosegmental.AR.tierLength X i = Fintype.card (Autosegmental.AR.fiber X i)

noncomputable def Autosegmental.AR.fiberEnum {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) : Fin (tierLength X i) ≃o fiber X i

The canonical ascending enumeration of a tier fiber.

Equations

• Autosegmental.AR.fiberEnum i = monoEquivOfFin (Autosegmental.AR.fiber X i) ⋯

noncomputable def Autosegmental.AR.vertexEquiv {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] : (i : ι) × Fin (tierLength X i) ≃ X.obj.V

The canonical enumeration of a finite representation's vertex type: tier fibers in ascending precedence order, assembled over the tier index.

Equations

• Autosegmental.AR.vertexEquiv = (Equiv.sigmaCongrRight fun (i : ι) => (Autosegmental.AR.fiberEnum i).toEquiv).trans (Equiv.sigmaFiberEquiv fun (v : X.obj.V) => (X.obj.label v).fst)

noncomputable def Autosegmental.AR.tierWord {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) : List (τ i)

The tier-i label word: the fiber's labels read off in ascending precedence order — the tier content the normal form canonicalizes.

Equations

• Autosegmental.AR.tierWord i = List.ofFn fun (p : Fin (Autosegmental.AR.tierLength X i)) => Autosegmental.AR.fiberLabel ((Autosegmental.AR.fiberEnum i) p)

@[simp]

theorem Autosegmental.AR.length_tierWord {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) : (tierWord i).length = tierLength X i

noncomputable def Autosegmental.AR.linkRel {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i j : ι) (p : Fin (tierLength X i)) (q : Fin (tierLength X j)) : Prop

The link relation in position coordinates: tier-i position p associates to tier-j position q. With tierWord, the complete tuple reading of a finite representation.

Equations

• Autosegmental.AR.linkRel i j p q = X.obj.edges.Adj (Autosegmental.AR.vertexEquiv ⟨i, p⟩) (Autosegmental.AR.vertexEquiv ⟨j, q⟩)

theorem Autosegmental.AR.linkRel_def {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] {i j : ι} {p : Fin (tierLength X i)} {q : Fin (tierLength X j)} : linkRel i j p q ↔ X.obj.edges.Adj (vertexEquiv ⟨i, p⟩) (vertexEquiv ⟨j, q⟩)

noncomputable def Autosegmental.AR.normalize {ι : Type u_1} {τ : ι → Type u_2} (X : TieredAR ι τ) [Finite X.obj.V] : TieredAR ι τ

The normal form: X reindexed onto the canonical vertex type by pulling edges, arcs, and labels back along vertexEquiv. A AR — the normal form is not a separate kind of object.

Equations

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

noncomputable def Autosegmental.AR.normalizeFullIso {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] : (normalize X).obj.Iso X.obj

The normal form is fully isomorphic to the original.

Equations

• Autosegmental.AR.normalizeFullIso = { toEquiv := Autosegmental.AR.vertexEquiv, edges_iff := ⋯, arcs_iff := ⋯, label_comp := ⋯ }

noncomputable def Autosegmental.AR.normalizeIso {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] : normalize X ≅ X

The normal form is isomorphic to the original.

Equations

• Autosegmental.AR.normalizeIso = Autosegmental.AR.mkIso Autosegmental.AR.normalizeFullIso

theorem Autosegmental.AR.edges_normalize {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i j : ι) (p : Fin (tierLength X i)) (q : Fin (tierLength X j)) : (normalize X).obj.edges.Adj ⟨i, p⟩ ⟨j, q⟩ ↔ linkRel i j p q

On normal forms the edges are exactly linkRel.

theorem Autosegmental.AR.arcs_normalize {ι : Type u_1} {τ : ι → Type u_2} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) (p q : Fin (tierLength X i)) : (normalize X).obj.arcs.Adj ⟨i, p⟩ ⟨i, q⟩ ↔ p < q

On normal forms the arcs are the ascending position order.

Tier words of tensors

Concatenation appends tier content: within a tier, the bridge arc puts every left-factor vertex before every right-factor vertex, so the tensor's fiber is the lexicographic sum of the factors' fibers and its ascending enumeration is the two enumerations in sequence (Subsingleton (Fin n ≃o ·) — monotone enumerations are unique).

instance Autosegmental.AR.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesTensorObjTieredAR {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] : Finite (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj.V

def Autosegmental.AR.fiberTensorEquiv {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} (i : ι) : fiber (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i ≃ fiber X i ⊕ fiber Y i

A tensor's tier fiber splits as the sum of the factors' fibers.

Equations

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

@[simp]

theorem Autosegmental.AR.tierLength_tensor {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) : tierLength (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i = tierLength X i + tierLength Y i

noncomputable def Autosegmental.AR.tensorEnum {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) : Fin (tierLength X i + tierLength Y i) ≃o fiber (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i

The blockwise enumeration of a tensor's fiber: left factor first, then right — monotone because the bridge arc orders the blocks.

Equations

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

theorem Autosegmental.AR.tensorEnum_apply_castAdd {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) (p : Fin (tierLength X i)) : (tensorEnum i) (Fin.castAdd (tierLength Y i) p) = (fiberTensorEquiv i).symm (Sum.inl ((fiberEnum i) p))

theorem Autosegmental.AR.tensorEnum_apply_natAdd {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) (p : Fin (tierLength Y i)) : (tensorEnum i) (Fin.natAdd (tierLength X i) p) = (fiberTensorEquiv i).symm (Sum.inr ((fiberEnum i) p))

theorem Autosegmental.AR.fiberLabel_symm_inl {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} {i : ι} (w : fiber X i) : fiberLabel ((fiberTensorEquiv i).symm (Sum.inl w)) = fiberLabel w

theorem Autosegmental.AR.fiberLabel_symm_inr {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} {i : ι} (w : fiber Y i) : fiberLabel ((fiberTensorEquiv i).symm (Sum.inr w)) = fiberLabel w

theorem Autosegmental.AR.tierWord_eq_ofFn {ι : Type u_3} {τ : ι → Type u_4} {Z : TieredAR ι τ} [Finite Z.obj.V] {i : ι} {n : ℕ} (e : Fin n ≃o fiber Z i) : tierWord i = List.ofFn fun (p : Fin n) => fiberLabel (e p)

Any monotone enumeration computes the tier word.

@[simp]

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

The tier word of a tensor is the concatenation of the factors' tier words.

theorem Autosegmental.AR.fiberEnum_tensor {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) : fiberEnum i = (Fin.castOrderIso ⋯).trans (tensorEnum i)

theorem Autosegmental.AR.vertexEquiv_tensor_of_lt {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] {i : ι} {r : Fin (tierLength (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i)} (h : ↑r < tierLength X i) : vertexEquiv ⟨i, r⟩ = Sum.inl (vertexEquiv ⟨i, ⟨↑r, h⟩⟩)

theorem Autosegmental.AR.vertexEquiv_tensor_of_ge {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] {i : ι} {r : Fin (tierLength (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i)} (h : tierLength X i ≤ ↑r) : vertexEquiv ⟨i, r⟩ = Sum.inr (vertexEquiv ⟨i, ⟨↑r - tierLength X i, ⋯⟩⟩)

instance Autosegmental.AR.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesTensorUnitTieredAR {ι : Type u_3} {τ : ι → Type u_4} : Finite (CategoryTheory.MonoidalCategoryStruct.tensorUnit (TieredAR ι τ)).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_unit {ι : Type u_3} {τ : ι → Type u_4} (i : ι) : tierWord i = []

Readers in ℕ coordinates

link reads the link relation at plain ℕ positions (out-of-bounds positions link to nothing); linearize is the two-tier phonetic reading. link_tensor is the blockwise companion of tierWord_tensor.

def Autosegmental.AR.link {ι : Type u_3} {τ : ι → Type u_4} (X : TieredAR ι τ) [Finite X.obj.V] (i j : ι) (p q : ℕ) : Prop

Tier-i position p links to tier-j position q, in ℕ coordinates (out-of-bounds positions link to nothing).

Equations

• Autosegmental.AR.link X i j p q = ∃ (hp : p < Autosegmental.AR.tierLength X i) (hq : q < Autosegmental.AR.tierLength X j), Autosegmental.AR.linkRel i j ⟨p, hp⟩ ⟨q, hq⟩

noncomputable def Autosegmental.AR.linearize {ι : Type u_3} {τ : ι → Type u_4} (X : TieredAR ι τ) [Finite X.obj.V] (i j : ι) : List (τ j × List (τ i))

The two-tier reading of tiers i over j: each tier-j position's label paired with its linked tier-i labels in ascending order.

Equations

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

theorem Autosegmental.AR.forall_link_iff_bounded {ι : Type u_3} {τ : ι → Type u_4} {F : TieredAR ι τ} [Finite F.obj.V] {C : ι → ι → ℕ → ℕ → Prop} : (∀ (i j : ι) (p q : ℕ), link F i j p q → C i j p q) ↔ ∀ (i j : ι), ∀ p < tierLength F i, ∀ q < tierLength F j, link F i j p q → C i j p q

Link conditions are supported on the factor's tier ranges.

theorem Autosegmental.AR.link_tensor {ι : Type u_3} {τ : ι → Type u_4} {X Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i j : ι) (p q : ℕ) : link (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) i j p q ↔ link X i j p q ∨ tierLength X i ≤ p ∧ tierLength X j ≤ q ∧ link Y i j (p - tierLength X i) (q - tierLength X j)

Tensor links are blockwise: within the left factor, or within the right factor shifted by the left factor's tier lengths — no cross-factor links.

Classification: the readers determine the representation

Two finite representations with the same tier words and the same links are isomorphic — (tierWord, link) is a complete invariant, [JH15]'s tiered tuples as the classification of finite representations.

theorem Autosegmental.AR.label_vertexEquiv {ι : Type u_3} {τ : ι → Type u_4} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) (p : Fin (tierLength X i)) : (X.obj.label (vertexEquiv ⟨i, p⟩)).fst = i

The label of a canonical vertex sits on its own tier.

theorem Autosegmental.AR.linkRel_iff_link {ι : Type u_3} {τ : ι → Type u_4} {X : TieredAR ι τ} [Finite X.obj.V] {i j : ι} {p : Fin (tierLength X i)} {q : Fin (tierLength X j)} : linkRel i j p q ↔ link X i j ↑p ↑q

theorem Autosegmental.AR.tierWord_getElem {ι : Type u_3} {τ : ι → Type u_4} {X : TieredAR ι τ} [Finite X.obj.V] {i : ι} (p : Fin (tierLength X i)) : (tierWord i)[↑p] = fiberLabel ((fiberEnum i) p)

theorem Autosegmental.AR.label_normalize {ι : Type u_3} {τ : ι → Type u_4} {X : TieredAR ι τ} [Finite X.obj.V] {i : ι} (p : Fin (tierLength X i)) : (normalize X).obj.label ⟨i, p⟩ = ⟨i, fiberLabel ((fiberEnum i) p)⟩

theorem Autosegmental.AR.arcs_normalize_ne {ι : Type u_3} {τ : ι → Type u_4} {X : TieredAR ι τ} [Finite X.obj.V] {i j : ι} (h : i ≠ j) (p : Fin (tierLength X i)) (q : Fin (tierLength X j)) : ¬(normalize X).obj.arcs.Adj ⟨i, p⟩ ⟨j, q⟩

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

Links are symmetric in coordinates.

theorem Autosegmental.AR.not_link_self_tier {ι : Type u_3} {τ : ι → Type u_4} {X : TieredAR ι τ} [Finite X.obj.V] (i : ι) (p q : ℕ) : ¬link X i i p q

Same-tier vertices are never linked.

noncomputable def Autosegmental.AR.fullIsoOfReaderEq {ι : Type u_3} {τ : ι → Type u_4} {A : TieredAR ι τ} {B : TieredAR ι τ} [Finite A.obj.V] [Finite B.obj.V] (hw : ∀ (i : ι), tierWord i = tierWord i) (hl : ∀ (i j : ι) (p q : ℕ), link A i j p q ↔ link B i j p q) : A.obj.Iso B.obj

The classification isomorphism as a full-structure Graph.Iso.

Equations

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

noncomputable def Autosegmental.AR.isoOfReaderEq {ι : Type u_3} {τ : ι → Type u_4} {A B : TieredAR ι τ} [Finite A.obj.V] [Finite B.obj.V] (hw : ∀ (i : ι), tierWord i = tierWord i) (hl : ∀ (i j : ι) (p q : ℕ), link A i j p q ↔ link B i j p q) : A ≅ B

Finite representations with equal tier words and equal links are isomorphic; the tuple reading is a complete invariant.

Equations

• Autosegmental.AR.isoOfReaderEq hw hl = Autosegmental.AR.mkIso (Autosegmental.AR.fullIsoOfReaderEq hw hl)

Building representations from tuple data

The constructor inverse to the readers: tier words plus a position-coordinate link relation determine a representation on the canonical carrier. This is the tiered presentation as a function — the essential-surjectivity direction of the classification.

def Autosegmental.AR.ofData {ι : Type u_3} {τ : ι → Type u_4} (ws : (i : ι) → List (τ i)) (L : ι → ι → ℕ → ℕ → Prop) : TieredAR ι τ

The representation presented by tier words ws and cross-tier links L (positions in ℕ coordinates; same-tier and out-of-bounds pairs are ignored, and same-tier links are excluded by construction). Arcs are the ascending position order on each tier.

Equations

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

instance Autosegmental.AR.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesOfData {ι : Type u_3} {τ : ι → Type u_4} [Finite ι] {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} : Finite (ofData ws L).obj.V

noncomputable def Autosegmental.AR.ofDataFiberEnum {ι : Type u_3} {τ : ι → Type u_4} {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} (i : ι) : Fin (ws i).length ≃o fiber (ofData ws L) i

The canonical carrier's fiber at i is its position range.

Equations

• Autosegmental.AR.ofDataFiberEnum i = StrictMono.orderIsoOfSurjective (fun (p : Fin (ws i).length) => ⟨⟨i, p⟩, ⋯⟩) ⋯ ⋯

theorem Autosegmental.AR.tierLength_ofData {ι : Type u_3} {τ : ι → Type u_4} [Finite ι] {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} (i : ι) : tierLength (ofData ws L) i = (ws i).length

theorem Autosegmental.AR.fiberEnum_ofData {ι : Type u_3} {τ : ι → Type u_4} [Finite ι] {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} (i : ι) : fiberEnum i = (Fin.castOrderIso ⋯).trans (ofDataFiberEnum i)

theorem Autosegmental.AR.vertexEquiv_ofData {ι : Type u_3} {τ : ι → Type u_4} [Finite ι] {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} {i : ι} (r : Fin (tierLength (ofData ws L) i)) : vertexEquiv ⟨i, r⟩ = ⟨i, Fin.cast ⋯ r⟩

@[simp]

theorem Autosegmental.AR.tierWord_ofData {ι : Type u_3} {τ : ι → Type u_4} [Finite ι] {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} (i : ι) : tierWord i = ws i

ofData reads back its words.

theorem Autosegmental.AR.link_ofData {ι : Type u_3} {τ : ι → Type u_4} [Finite ι] {ws : (i : ι) → List (τ i)} {L : ι → ι → ℕ → ℕ → Prop} (i j : ι) (p q : ℕ) : link (ofData ws L) i j p q ↔ i ≠ j ∧ p < (ws i).length ∧ q < (ws j).length ∧ (L i j p q ∨ L j i q p)

ofData reads back its links, symmetrized, on in-bounds cross-tier pairs.