diff --git a/Linglib.lean b/Linglib.lean
index d526c1c63..b135e236c 100644
--- a/Linglib.lean
+++ b/Linglib.lean
@@ -309,6 +309,8 @@ import Linglib.Syntax.Binding.SpecificityCondition
 import Linglib.Features.Prominence
 import Linglib.Features.OntologicalCategory
 import Linglib.Features.Genericity
+import Linglib.Core.CategoryTheory.Monoidal.LabeledTuple
+import Linglib.Core.Data.Fin.Tuple.Basic
 import Linglib.Core.Data.List.Bookend
 import Linglib.Core.Data.List.Chain
 import Linglib.Core.Data.List.DropRight
diff --git a/Linglib/Core/CategoryTheory/Monoidal/LabeledTuple.lean b/Linglib/Core/CategoryTheory/Monoidal/LabeledTuple.lean
new file mode 100644
index 000000000..7bd7dd370
--- /dev/null
+++ b/Linglib/Core/CategoryTheory/Monoidal/LabeledTuple.lean
@@ -0,0 +1,288 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+import Mathlib.Algebra.Group.Defs
+import Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
+import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Linglib.Core.Data.Fin.Tuple.Basic
+
+/-!
+# The monoidal category of labeled finite tuples
+
+`[UPSTREAM]` candidate for `Mathlib/CategoryTheory/Monoidal/`. A `LabeledTuple α`
+is a finite tuple of `α`s: a length `n` and a labeling `Fin n → α`. Morphisms are
+**label-preserving position maps** (`f : Fin a.len → Fin b.len` with
+`b.label ∘ f = a.label`); this is a skeleton of `Over α` (finite `α`-labeled
+sets) on `Fin`-objects.
+
+Concatenation (`Fin.append` on labels, `+` on lengths) is the **categorical
+coproduct** and `empty` the **initial object**, so the category is *cocartesian*:
+its `MonoidalCategory` and `SymmetricCategory` are obtained for free from
+`monoidalOfHasFiniteCoproducts`/`symmetricOfHasFiniteCoproducts` (unlike
+`AugmentedSimplexCategory`, whose monotone maps make its ordinal sum *not* a
+coproduct, forcing a bespoke monoidal structure). The tensor is `concat` up to
+the chosen-coproduct isomorphism.
+
+The concrete `Fin`-skeletal `concat`/`Hom.concatMap` defs (with their
+`Fin.appendMap` action) are kept alongside: downstream clients that need the
+literal `Fin (a.len + b.len)` carrier — e.g. autosegmental tiers with typed
+links — consume those directly rather than the opaque coproduct tensor.
+
+## Main definitions
+
+* `LabeledTuple α` — a length-indexed labeled tuple; the object.
+* `LabeledTuple.Hom a b` — a label-preserving position map.
+* `LabeledTuple.concat` — concatenation; `LabeledTuple.empty` the unit.
+* `LabeledTuple.Hom.concatMap` — the concatenation bifunctor on morphisms.
+* `MonoidalCategory`/`SymmetricCategory (LabeledTuple α)` — the cocartesian
+  structure: `concat` as `⊗` (up to coproduct iso), `empty` as `𝟙_`.
+-/
+
+universe u
+
+open CategoryTheory MonoidalCategory
+
+/-- A finite tuple of `α`s: a length and a labeling. -/
+structure LabeledTuple (α : Type u) where
+  /-- The length of the tuple. -/
+  len : ℕ
+  /-- The labeling of the positions. -/
+  label : Fin len → α
+
+namespace LabeledTuple
+
+variable {α : Type u}
+
+/-- Tuples are comparable when labels are: compare lengths, then the labelings
+    (decidable as `Fin len` is a `Fintype`). Reduces under `decide`. -/
+instance [DecidableEq α] : DecidableEq (LabeledTuple α)
+  | ⟨la, fa⟩, ⟨lb, fb⟩ =>
+    if h : la = lb then by subst h; exact decidable_of_iff (fa = fb) (by simp)
+    else isFalse fun he => h (congrArg len he)
+
+/-- A label-preserving position map. -/
+@[ext]
+structure Hom (a b : LabeledTuple α) where
+  /-- The underlying position map. -/
+  toFun : Fin a.len → Fin b.len
+  /-- The map preserves labels. -/
+  label_comp : b.label ∘ toFun = a.label
+
+namespace Hom
+variable {a b c : LabeledTuple α}
+
+/-- The identity morphism. -/
+def id (a : LabeledTuple α) : Hom a a := ⟨_root_.id, Function.comp_id a.label⟩
+
+/-- Composition of morphisms (diagrammatic: `f` then `g`). -/
+def comp (f : Hom a b) (g : Hom b c) : Hom a c :=
+  ⟨g.toFun ∘ f.toFun, by rw [← Function.comp_assoc, g.label_comp, f.label_comp]⟩
+
+@[simp] theorem id_toFun (a : LabeledTuple α) : (Hom.id a).toFun = _root_.id := rfl
+@[simp] theorem comp_toFun (f : Hom a b) (g : Hom b c) :
+    (f.comp g).toFun = g.toFun ∘ f.toFun := rfl
+
+end Hom
+
+instance : Category (LabeledTuple α) where
+  Hom := Hom
+  id := Hom.id
+  comp f g := f.comp g
+  id_comp _ := by apply Hom.ext; rfl
+  comp_id _ := by apply Hom.ext; rfl
+  assoc _ _ _ := by apply Hom.ext; rfl
+
+@[simp] theorem id_toFun' (a : LabeledTuple α) : (𝟙 a : Hom a a).toFun = _root_.id := rfl
+@[simp] theorem comp_toFun' {a b c : LabeledTuple α} (f : a ⟶ b) (g : b ⟶ c) :
+    (f ≫ g).toFun = g.toFun ∘ f.toFun := rfl
+
+/-- The index map of an `eqToHom` is the length-cast `finCongr`. -/
+@[simp] theorem eqToHom_toFun {a b : LabeledTuple α} (h : a = b) :
+    (eqToHom h).toFun = finCongr (congrArg len h) := by cases h; rfl
+
+/-! ### Concatenation -/
+
+/-- Concatenation of labeled tuples: lengths add, labels `Fin.append`. -/
+def concat (a b : LabeledTuple α) : LabeledTuple α where
+  len := a.len + b.len
+  label := Fin.append a.label b.label
+
+/-- The empty tuple — the monoidal unit. -/
+def empty : LabeledTuple α where
+  len := 0
+  label := Fin.elim0
+
+@[simp] theorem empty_len : (empty : LabeledTuple α).len = 0 := rfl
+
+/-- The labeled tuple of a list: its length, positionally labeled. The ergonomic
+    bridge for clients that build tiers from `List` literals. -/
+def ofList (l : List α) : LabeledTuple α := ⟨l.length, l.get⟩
+
+@[simp] theorem ofList_len (l : List α) : (ofList l).len = l.length := rfl
+@[simp] theorem ofList_label (l : List α) : (ofList l).label = l.get := rfl
+
+/-- The underlying list of labels, in position order. -/
+def toList (a : LabeledTuple α) : List α := List.ofFn a.label
+
+@[simp] theorem toList_length (a : LabeledTuple α) : a.toList.length = a.len := by
+  simp [toList]
+
+@[simp] theorem toList_ofList (l : List α) : (ofList l).toList = l := by
+  simp [toList, ofList]
+
+/-- Raw `ℕ`-indexed access, out-of-range to `none`: the positional view for
+    clients that index tiers by `ℕ` (subgraph embedding, surface bookkeeping). -/
+def get? (a : LabeledTuple α) (i : ℕ) : Option α :=
+  if h : i < a.len then some (a.label ⟨i, h⟩) else none
+
+@[simp] theorem ofList_get? (l : List α) (i : ℕ) : (ofList l).get? i = l[i]? := by
+  simp only [get?, ofList_len, ofList_label]
+  split <;> rename_i h
+  · rw [List.getElem?_eq_getElem h, List.get_eq_getElem]
+  · rw [List.getElem?_eq_none (by omega)]
+
+theorem get?_eq_getElem? (a : LabeledTuple α) (i : ℕ) : a.get? i = a.toList[i]? := by
+  unfold get?
+  split <;> rename_i h
+  · rw [List.getElem?_eq_getElem (by simpa using h)]; simp [toList, List.getElem_ofFn]
+  · rw [List.getElem?_eq_none (by simpa using h)]
+
+@[simp] theorem concat_len (a b : LabeledTuple α) : (a.concat b).len = a.len + b.len := rfl
+@[simp] theorem concat_label (a b : LabeledTuple α) :
+    (a.concat b).label = Fin.append a.label b.label := rfl
+
+@[simp] theorem toList_concat (a b : LabeledTuple α) :
+    (a.concat b).toList = a.toList ++ b.toList := by
+  unfold toList
+  rw [concat_label]
+  exact List.ofFn_fin_append a.label b.label
+
+/-- Raw access into a concatenation: left block through `a`, right through `b`. -/
+theorem get?_concat_left {a b : LabeledTuple α} {i : ℕ} (h : i < a.len) :
+    (a.concat b).get? i = a.get? i := by
+  rw [get?_eq_getElem?, toList_concat, get?_eq_getElem?,
+    List.getElem?_append_left (by simpa using h)]
+
+theorem get?_concat_right (a b : LabeledTuple α) (j : ℕ) :
+    (a.concat b).get? (a.len + j) = b.get? j := by
+  rw [get?_eq_getElem?, toList_concat, get?_eq_getElem?,
+    List.getElem?_append_right (by simp)]
+  simp [toList_length]
+
+/-- The concatenation bifunctor on morphisms: `Fin.appendMap` of the position
+    maps. Label preservation is exactly `Fin`-append naturality. -/
+def Hom.concatMap {a a' b b' : LabeledTuple α} (f : Hom a a') (g : Hom b b') :
+    Hom (a.concat b) (a'.concat b') :=
+  ⟨Fin.appendMap f.toFun g.toFun, Fin.append_comp_appendMap f.label_comp g.label_comp⟩
+
+@[simp] theorem Hom.concatMap_toFun {a a' b b' : LabeledTuple α} (f : Hom a a') (g : Hom b b') :
+    (f.concatMap g).toFun = Fin.appendMap f.toFun g.toFun := rfl
+
+theorem Hom.concatMap_id (a b : LabeledTuple α) :
+    (Hom.id a).concatMap (Hom.id b) = Hom.id (a.concat b) := by
+  apply Hom.ext; simp [concatMap, Hom.id]
+
+theorem Hom.concatMap_comp {a a' a'' b b' b'' : LabeledTuple α}
+    (f : Hom a a') (f' : Hom a' a'') (g : Hom b b') (g' : Hom b' b'') :
+    (f.comp f').concatMap (g.comp g') = (f.concatMap g).comp (f'.concatMap g') := by
+  apply Hom.ext; simp [concatMap, Hom.comp, Fin.appendMap_comp]
+
+/-! ### Monoid structure on objects -/
+
+/-- Extensionality via a length equality and a cast-compatible labeling. The
+    auto-generated structure `ext` would demand an unusable `HEq` on `label`
+    (which depends on `len`), and the cast dependency here defeats the `@[ext]`
+    generator, so this is a plain extensionality lemma. -/
+theorem ext {a b : LabeledTuple α} (hlen : a.len = b.len)
+    (hlabel : a.label = b.label ∘ Fin.cast hlen) : a = b := by
+  obtain ⟨la, fa⟩ := a; obtain ⟨lb, fb⟩ := b
+  cases hlen
+  simp only [Fin.cast_refl, Function.comp_id] at hlabel
+  subst hlabel; rfl
+
+theorem concat_assoc (a b c : LabeledTuple α) :
+    (a.concat b).concat c = a.concat (b.concat c) :=
+  ext (Nat.add_assoc ..) (by simp only [concat_label]; exact Fin.append_assoc ..)
+
+theorem empty_concat (a : LabeledTuple α) : empty.concat a = a :=
+  ext (Nat.zero_add _) (by simp only [concat_label]; exact Fin.elim0_append _)
+
+theorem concat_empty (a : LabeledTuple α) : a.concat empty = a :=
+  ext (Nat.add_zero _) (by simp only [concat_label]; exact Fin.append_elim0 _)
+
+/-- Objects form a `Monoid` under concatenation, with `empty` as unit. -/
+instance instMonoid : Monoid (LabeledTuple α) where
+  mul := concat
+  one := empty
+  mul_assoc := concat_assoc
+  one_mul := empty_concat
+  mul_one := concat_empty
+
+@[simp] theorem mul_eq_concat (a b : LabeledTuple α) : a * b = a.concat b := rfl
+@[simp] theorem one_eq_empty : (1 : LabeledTuple α) = empty := rfl
+
+/-! ### Cocartesian monoidal structure
+
+`empty` is the initial object and `concat` the categorical coproduct (with
+coprojections `Fin.castAdd`/`Fin.natAdd`), so the category is cocartesian and its
+`MonoidalCategory`/`SymmetricCategory` come for free. -/
+
+open Limits
+
+instance (Y : LabeledTuple α) : Subsingleton (empty ⟶ Y) :=
+  ⟨fun _ _ => by apply Hom.ext; funext i; exact i.elim0⟩
+
+instance (Y : LabeledTuple α) : Nonempty (empty ⟶ Y) :=
+  ⟨⟨Fin.elim0, by funext i; exact i.elim0⟩⟩
+
+instance : HasInitial (LabeledTuple α) :=
+  hasInitial_of_unique empty
+
+/-- The left coprojection `a ⟶ a.concat b`. -/
+def inl (a b : LabeledTuple α) : Hom a (a.concat b) :=
+  ⟨Fin.castAdd b.len, by funext i; exact Fin.append_left a.label b.label i⟩
+
+/-- The right coprojection `b ⟶ a.concat b`. -/
+def inr (a b : LabeledTuple α) : Hom b (a.concat b) :=
+  ⟨Fin.natAdd a.len, by funext i; exact Fin.append_right a.label b.label i⟩
+
+@[simp] theorem inl_toFun (a b : LabeledTuple α) : (inl a b).toFun = Fin.castAdd b.len := rfl
+@[simp] theorem inr_toFun (a b : LabeledTuple α) : (inr a b).toFun = Fin.natAdd a.len := rfl
+
+/-- The copairing of `f : a ⟶ T` and `g : b ⟶ T`, glued by `Fin.append`. -/
+def coprodDesc {a b T : LabeledTuple α} (f : Hom a T) (g : Hom b T) : Hom (a.concat b) T where
+  toFun := Fin.append f.toFun g.toFun
+  label_comp := by
+    funext i
+    refine Fin.addCases (fun j => ?_) (fun j => ?_) i
+    · simpa using congrFun f.label_comp j
+    · simpa using congrFun g.label_comp j
+
+@[simp] theorem coprodDesc_toFun {a b T : LabeledTuple α} (f : Hom a T) (g : Hom b T) :
+    (coprodDesc f g).toFun = Fin.append f.toFun g.toFun := rfl
+
+/-- `concat` is the categorical coproduct, with `inl`/`inr` the coprojections. -/
+instance (a b : LabeledTuple α) : HasBinaryCoproduct a b :=
+  HasColimit.mk
+    { cocone := BinaryCofan.mk (inl a b) (inr a b)
+      isColimit := BinaryCofan.IsColimit.mk _ (fun f g => coprodDesc f g)
+        (fun f g => by apply Hom.ext; funext i; simp)
+        (fun f g => by apply Hom.ext; funext i; simp)
+        (fun f g m h₁ h₂ => by
+          apply Hom.ext; funext i
+          refine Fin.addCases (fun j => ?_) (fun j => ?_) i
+          · simpa using congrFun (congrArg Hom.toFun h₁) j
+          · simpa using congrFun (congrArg Hom.toFun h₂) j) }
+
+instance : HasBinaryCoproducts (LabeledTuple α) := hasBinaryCoproducts_of_hasColimit_pair _
+
+noncomputable instance : MonoidalCategory (LabeledTuple α) :=
+  monoidalOfHasFiniteCoproducts _
+
+noncomputable instance : SymmetricCategory (LabeledTuple α) :=
+  symmetricOfHasFiniteCoproducts _
+
+end LabeledTuple
diff --git a/Linglib/Core/Data/Fin/Tuple/Basic.lean b/Linglib/Core/Data/Fin/Tuple/Basic.lean
new file mode 100644
index 000000000..a9f9a9a6c
--- /dev/null
+++ b/Linglib/Core/Data/Fin/Tuple/Basic.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Robert Hawkins. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Hawkins
+-/
+import Mathlib.Logic.Equiv.Fin.Basic
+import Mathlib.Data.Fin.Tuple.Basic
+
+/-!
+# `Fin.appendMap`: `Fin.append` as a bifunctor on index maps
+
+`[UPSTREAM]` candidate for `Mathlib/Data/Fin/Tuple/Basic.lean`. Mathlib has
+`Fin.append` (the action of `+` on *tuples*) and its naturality only for `Fin.cast`
+maps; it lacks the action of `+` on arbitrary index *maps*. `Fin.appendMap f g`
+routes a `Fin (m + n)` index through `f` on the left block and `g` on the right,
+and is functorial (`appendMap_id`/`appendMap_comp`) with `Fin.append` natural in it
+(`append_comp_appendMap`).
+-/
+
+namespace Fin
+
+variable {m m' m'' n n' n'' : ℕ}
+
+/-- The action of `+` on index maps: `f` on the left block, `g` on the right. -/
+def appendMap (f : Fin m → Fin m') (g : Fin n → Fin n') : Fin (m + n) → Fin (m' + n') :=
+  finSumFinEquiv ∘ Sum.map f g ∘ finSumFinEquiv.symm
+
+@[simp] theorem appendMap_castAdd (f : Fin m → Fin m') (g : Fin n → Fin n') (i : Fin m) :
+    appendMap f g (Fin.castAdd n i) = Fin.castAdd n' (f i) := by
+  simp [appendMap]
+
+@[simp] theorem appendMap_natAdd (f : Fin m → Fin m') (g : Fin n → Fin n') (j : Fin n) :
+    appendMap f g (Fin.natAdd m j) = Fin.natAdd m' (g j) := by
+  simp [appendMap]
+
+/-- Value characterisation: left-block indices route through `f`, right-block
+    (shifted) through `g`. -/
+theorem appendMap_val (f : Fin m → Fin m') (g : Fin n → Fin n') (k : Fin (m + n)) :
+    (appendMap f g k : ℕ) =
+      if h : (k : ℕ) < m then (f ⟨k, h⟩ : ℕ)
+      else (g ⟨(k : ℕ) - m, by have := k.2; omega⟩ : ℕ) + m' := by
+  refine Fin.addCases (fun a => ?_) (fun b => ?_) k
+  · rw [dif_pos (by simp)]; simp
+  · rw [dif_neg (by simp)]; simp; omega
+
+@[simp] theorem appendMap_id : appendMap (id : Fin m → _) (id : Fin n → _) = id := by
+  simp [appendMap]
+
+theorem appendMap_comp (f : Fin m → Fin m') (f' : Fin m' → Fin m'')
+    (g : Fin n → Fin n') (g' : Fin n' → Fin n'') :
+    appendMap (f' ∘ f) (g' ∘ g) = appendMap f' g' ∘ appendMap f g := by
+  funext k; simp [appendMap, Equiv.symm_apply_apply, Sum.map_map]
+
+/-- **`Fin.append` is natural in its index maps**: a block-routing map intertwines
+    the two appended tuples. The label-preservation core for concatenation. -/
+theorem append_comp_appendMap {α : Type*} {a : Fin m → α} {a' : Fin m' → α}
+    {b : Fin n → α} {b' : Fin n' → α} {f : Fin m → Fin m'} {g : Fin n → Fin n'}
+    (hf : a' ∘ f = a) (hg : b' ∘ g = b) :
+    Fin.append a' b' ∘ appendMap f g = Fin.append a b := by
+  subst hf hg
+  funext k
+  simp only [Function.comp_apply]
+  refine Fin.addCases (fun i => ?_) (fun j => ?_) k <;> simp
+
+end Fin
diff --git a/Linglib/Phonology/Autosegmental/AR.lean b/Linglib/Phonology/Autosegmental/AR.lean
index 2f62ae7e4..b45746b8a 100644
--- a/Linglib/Phonology/Autosegmental/AR.lean
+++ b/Linglib/Phonology/Autosegmental/AR.lean
@@ -3,49 +3,31 @@ Copyright (c) 2026 Robert Hawkins. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Hawkins
 -/
-import Mathlib.Logic.Equiv.Fin.Basic
 import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Monoidal.Category
+import Linglib.Core.Data.Fin.Tuple.Basic
 import Linglib.Phonology.Autosegmental.Graph
 
 /-!
 # The monoidal category of autosegmental representations
 
 `Autosegmental.AR α β` is the base object of the autosegmental category: an
-in-bounds `Graph α β` (an `upper` tier of `α`s, a `lower` tier of `β`s, and a
-finite set of association lines, with every line falling within the tier
-lengths). In-boundedness is *constitutive* — a graph with an out-of-range link
-is junk, not an object — whereas planarity ([goldsmith-1976]'s No-Crossing
-Constraint) is a *constraint* that carves out a full monoidal subcategory
-(`WellFormedAR`, in `WellFormed.lean`).
-
-Morphisms are `Fin`-indexed, label- and link-preserving vertex maps
-(`AR.Hom`). The monoidal product is morpheme concatenation
-([jardine-heinz-2015]), with the empty representation as unit; the associator
-and unitors are `eqToIso` of the underlying object `Monoid` laws, so `AR` is
-strict monoidal over its object-monoid.
+in-bounds `Graph α β`. In-boundedness is constitutive; planarity
+([goldsmith-1976]'s No-Crossing Constraint) is the *constraint* carving out the
+full monoidal subcategory `WellFormedAR` (`WellFormedAR.lean`). The monoidal
+product is morpheme concatenation ([jardine-heinz-2015]) with the empty
+representation as unit; associator and unitors are `eqToIso` of the object
+`Monoid` laws, so `AR` is strict monoidal over its object-monoid.
 
 ## Main definitions
 
 * `AR α β` — the in-bounds autosegmental graph; the base object.
-* `AR.Hom A B` — a `Fin`-indexed label- and link-preserving morphism;
-  `Hom.id`/`Hom.comp` make `AR α β` a `Category`.
-* `AR.concat` — morpheme concatenation; `AR.empty` the unit
-  (`Monoid (AR α β)`).
-* `AR.Hom.concatMap` — the concatenation bifunctor on morphisms (`tensorHom`).
+* `AR.Hom A B` — a label/link-preserving morphism whose tier maps are
+  `LabeledTuple.Hom`s; `Category (AR α β)` via `id`/`comp`.
+* `AR.concat` — morpheme concatenation; `AR.empty` the unit (`Monoid (AR α β)`).
+* `AR.Hom.concatMap` — the concatenation bifunctor on morphisms (`tensorHom`);
+  its tier action delegates to `LabeledTuple.Hom.concatMap`.
 * `MonoidalCategory (AR α β)` — `concat` as `⊗`, `empty` as `𝟙_`.
-
-## Implementation notes
-
-Tiers are `Fin`-indexed in the *morphisms* (`fUpper : Fin A.upper.length →
-Fin B.upper.length`), giving extensionality for free, while the *object*'s
-`links : Finset (ℕ × ℕ)` stays raw-`ℕ`-indexed (matching the `MonovaryOn`-based
-planarity substrate). The bridge between the two is `AR.upperIdx`/`lowerIdx`,
-which read a link's in-bounds endpoints as `Fin` indices via the `inBounds`
-field. `concatMap`'s index maps are assembled from `finSumFinEquiv` and
-`finCongr` (the non-definitional `(A.concat B).length = A.length + B.length`);
-their behaviour is pinned by the value-characterisation lemmas
-`concatUpper_val`/`concatLower_val`.
 -/
 
 namespace Autosegmental
@@ -63,50 +45,56 @@ structure AR (α β : Type*) extends Graph α β where
 namespace AR
 
 /-- `Fin` index of a link's upper endpoint (in bounds by `A.inBounds`). -/
-def upperIdx (A : AR α β) {p : ℕ × ℕ} (hp : p ∈ A.links) : Fin A.upper.length :=
+def upperIdx (A : AR α β) {p : ℕ × ℕ} (hp : p ∈ A.links) : Fin A.upper.len :=
   ⟨p.1, (A.inBounds p hp).1⟩
 
 /-- `Fin` index of a link's lower endpoint. -/
-def lowerIdx (A : AR α β) {p : ℕ × ℕ} (hp : p ∈ A.links) : Fin A.lower.length :=
+def lowerIdx (A : AR α β) {p : ℕ × ℕ} (hp : p ∈ A.links) : Fin A.lower.len :=
   ⟨p.2, (A.inBounds p hp).2⟩
 
+@[simp] theorem upperIdx_val (A : AR α β) {p : ℕ × ℕ} (hp : p ∈ A.links) :
+    (A.upperIdx hp : ℕ) = p.1 := rfl
+
+@[simp] theorem lowerIdx_val (A : AR α β) {p : ℕ × ℕ} (hp : p ∈ A.links) :
+    (A.lowerIdx hp : ℕ) = p.2 := rfl
+
 /-! ### Morphisms -/
 
-/-- A label- and link-preserving morphism, `Fin`-indexed on the tiers. The
-    label conditions use total `getElem` (no `Option`); link preservation reads
-    the endpoints as `Fin` indices via `upperIdx`/`lowerIdx`. -/
+/-- A label- and link-preserving morphism. The tier maps are `LabeledTuple.Hom`s
+    (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. -/
 @[ext]
 structure Hom (A B : AR α β) where
-  /-- Vertex map on the upper tier. -/
-  fUpper : Fin A.upper.length → Fin B.upper.length
+  /-- Vertex map on the upper tier (a label-preserving `LabeledTuple` morphism). -/
+  fU : LabeledTuple.Hom A.upper B.upper
   /-- Vertex map on the lower tier. -/
-  fLower : Fin A.lower.length → Fin B.lower.length
-  /-- The upper map preserves labels. -/
-  upper_label : ∀ i, B.upper[fUpper i] = A.upper[i]
-  /-- The lower map preserves labels. -/
-  lower_label : ∀ j, B.lower[fLower j] = A.lower[j]
+  fL : LabeledTuple.Hom A.lower B.lower
   /-- Association lines are preserved. -/
-  links_preserve : ∀ {p : ℕ × ℕ} (hp : p ∈ A.links),
-    ((fUpper (A.upperIdx hp) : ℕ), (fLower (A.lowerIdx hp) : ℕ)) ∈ B.links
+  links_preserve : ∀ {i j : ℕ} (hi : i < A.upper.len) (hj : j < A.lower.len),
+    (i, j) ∈ A.links → ((fU.toFun ⟨i, hi⟩ : ℕ), (fL.toFun ⟨j, hj⟩ : ℕ)) ∈ B.links
 
 namespace Hom
 variable {A B C : AR α β}
 
 /-- The identity morphism. -/
 def id (A : AR α β) : Hom A A where
-  fUpper := _root_.id
-  fLower := _root_.id
-  upper_label _ := rfl
-  lower_label _ := rfl
-  links_preserve hp := hp
+  fU := LabeledTuple.Hom.id A.upper
+  fL := LabeledTuple.Hom.id A.lower
+  links_preserve _ _ h := h
 
-/-- Composition of morphisms (diagrammatic order: `f.comp g` is `f` then `g`). -/
+/-- Composition of morphisms (diagrammatic: `f` then `g`). -/
 def comp (f : Hom A B) (g : Hom B C) : Hom A C where
-  fUpper := g.fUpper ∘ f.fUpper
-  fLower := g.fLower ∘ f.fLower
-  upper_label i := by simp only [Function.comp_apply, g.upper_label, f.upper_label]
-  lower_label j := by simp only [Function.comp_apply, g.lower_label, f.lower_label]
-  links_preserve hp := g.links_preserve (f.links_preserve hp)
+  fU := f.fU.comp g.fU
+  fL := f.fL.comp g.fL
+  links_preserve hi hj h := by
+    have key := g.links_preserve (f.fU.toFun ⟨_, hi⟩).isLt (f.fL.toFun ⟨_, hj⟩).isLt
+      (f.links_preserve hi hj h)
+    simpa [LabeledTuple.Hom.comp] using key
+
+@[simp] theorem id_fU (A : AR α β) : (Hom.id A).fU = LabeledTuple.Hom.id A.upper := rfl
+@[simp] theorem id_fL (A : AR α β) : (Hom.id A).fL = LabeledTuple.Hom.id A.lower := rfl
+@[simp] theorem comp_fU (f : Hom A B) (g : Hom B C) : (f.comp g).fU = f.fU.comp g.fU := rfl
+@[simp] theorem comp_fL (f : Hom A B) (g : Hom B C) : (f.comp g).fL = f.fL.comp g.fL := rfl
 
 end Hom
 
@@ -120,6 +108,13 @@ instance : Category (AR α β) where
   comp_id _ := by apply Hom.ext <;> rfl
   assoc _ _ _ := by apply Hom.ext <;> rfl
 
+@[simp] theorem id_fU' (A : AR α β) : (𝟙 A : Hom A A).fU = 𝟙 A.upper := rfl
+@[simp] theorem id_fL' (A : AR α β) : (𝟙 A : Hom A A).fL = 𝟙 A.lower := rfl
+@[simp] theorem comp_fU' {A B C : AR α β} (f : A ⟶ B) (g : B ⟶ C) :
+    (f ≫ g).fU = f.fU.comp g.fU := rfl
+@[simp] theorem comp_fL' {A B C : AR α β} (f : A ⟶ B) (g : B ⟶ C) :
+    (f ≫ g).fL = f.fL.comp g.fL := rfl
+
 /-! ### Concatenation: the tensor object -/
 
 /-- Morpheme concatenation ([jardine-heinz-2015]): the tier-concatenated,
@@ -128,176 +123,73 @@ def concat (A B : AR α β) : AR α β where
   toGraph := A.toGraph.concat B.toGraph
   inBounds := Graph.inBounds_concat A.inBounds B.inBounds
 
-theorem concat_upper_len (A B : AR α β) :
-    (A.concat B).upper.length = A.upper.length + B.upper.length := by
-  show (A.toGraph.concat B.toGraph).upper.length = _
-  simp [Graph.upper_concat]
+@[simp] theorem concat_toGraph (A B : AR α β) :
+    (A.concat B).toGraph = A.toGraph.concat B.toGraph := rfl
 
-theorem concat_lower_len (A B : AR α β) :
-    (A.concat B).lower.length = A.lower.length + B.lower.length := by
-  show (A.toGraph.concat B.toGraph).lower.length = _
-  simp [Graph.lower_concat]
+@[simp] theorem concat_upper (A B : AR α β) :
+    (A.concat B).upper = A.upper.concat B.upper := rfl
 
-theorem upper_concat (A B : AR α β) : (A.concat B).upper = A.upper ++ B.upper := rfl
-
-theorem lower_concat (A B : AR α β) : (A.concat B).lower = A.lower ++ B.lower := rfl
+@[simp] theorem concat_lower (A B : AR α β) :
+    (A.concat B).lower = A.lower.concat B.lower := rfl
 
 theorem links_concat (A B : AR α β) :
     (A.concat B).links =
-      A.links ∪ B.links.image (shiftLink A.upper.length A.lower.length) := rfl
+      A.links ∪ B.links.image (shiftLink A.upper.len A.lower.len) := rfl
+
+/-! ### The concatenation bifunctor `concatMap` (the tensor on morphisms)
 
-/-! ### 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`. -/
 
 namespace Hom
 variable {A A' B B' : AR α β}
 
-/-- Underlying upper index map of the concat bifunctor: `f` on the A-block,
-    `g` (shifted) on the B-block, via `finSumFinEquiv`. -/
-def concatUpper (f : Hom A A') (g : Hom B B') :
-    Fin (A.concat B).upper.length → Fin (A'.concat B').upper.length :=
-  finCongr (concat_upper_len A' B').symm ∘ finSumFinEquiv ∘
-    Sum.map f.fUpper g.fUpper ∘ finSumFinEquiv.symm ∘ finCongr (concat_upper_len A B)
-
-/-- Underlying lower index map of the concat bifunctor. -/
-def concatLower (f : Hom A A') (g : Hom B B') :
-    Fin (A.concat B).lower.length → Fin (A'.concat B').lower.length :=
-  finCongr (concat_lower_len A' B').symm ∘ finSumFinEquiv ∘
-    Sum.map f.fLower g.fLower ∘ finSumFinEquiv.symm ∘ finCongr (concat_lower_len A B)
-
-/-- Value characterisation of `concatUpper`: A-indices route through `f`,
-    B-indices (shifted) through `g`. -/
-theorem concatUpper_val (f : Hom A A') (g : Hom B B')
-    (i : Fin (A.concat B).upper.length) :
-    (concatUpper f g i : ℕ) =
-      if h : (i : ℕ) < A.upper.length then (f.fUpper ⟨i, h⟩ : ℕ)
-      else (g.fUpper ⟨(i : ℕ) - A.upper.length,
-        by have e := concat_upper_len A B; have := i.2; omega⟩ : ℕ) + A'.upper.length := by
-  obtain ⟨i', rfl⟩ : ∃ i', i = (finCongr (concat_upper_len A B)).symm i' :=
-    ⟨finCongr (concat_upper_len A B) i, by simp⟩
-  refine Fin.addCases (fun a => ?_) (fun b => ?_) i'
-  · rw [dif_pos (by simp)]; simp [concatUpper]
-  · rw [dif_neg (by simp)]; simp [concatUpper]; omega
-
-theorem concatLower_val (f : Hom A A') (g : Hom B B')
-    (j : Fin (A.concat B).lower.length) :
-    (concatLower f g j : ℕ) =
-      if h : (j : ℕ) < A.lower.length then (f.fLower ⟨j, h⟩ : ℕ)
-      else (g.fLower ⟨(j : ℕ) - A.lower.length,
-        by have e := concat_lower_len A B; have := j.2; omega⟩ : ℕ) + A'.lower.length := by
-  obtain ⟨j', rfl⟩ : ∃ j', j = (finCongr (concat_lower_len A B)).symm j' :=
-    ⟨finCongr (concat_lower_len A B) j, by simp⟩
-  refine Fin.addCases (fun a => ?_) (fun b => ?_) j'
-  · rw [dif_pos (by simp)]; simp [concatLower]
-  · rw [dif_neg (by simp)]; simp [concatLower]; omega
-
-/-- `concatUpper` routes an A-tier index through `f`. -/
-theorem concatUpper_lt (f : Hom A A') (g : Hom B B')
-    (i : Fin (A.concat B).upper.length) (h : (i : ℕ) < A.upper.length) :
-    (concatUpper f g i : ℕ) = (f.fUpper ⟨i, h⟩ : ℕ) := by
-  rw [concatUpper_val, dif_pos h]
-
-/-- `concatUpper` routes a B-tier index through `g`, shifted past `A'`. -/
-theorem concatUpper_ge (f : Hom A A') (g : Hom B B')
-    (i : Fin (A.concat B).upper.length) (h : ¬ (i : ℕ) < A.upper.length) :
-    (concatUpper f g i : ℕ) =
-      (g.fUpper ⟨(i : ℕ) - A.upper.length,
-        by have e := concat_upper_len A B; have := i.2; omega⟩ : ℕ) + A'.upper.length := by
-  rw [concatUpper_val, dif_neg h]
-
-theorem concatLower_lt (f : Hom A A') (g : Hom B B')
-    (j : Fin (A.concat B).lower.length) (h : (j : ℕ) < A.lower.length) :
-    (concatLower f g j : ℕ) = (f.fLower ⟨j, h⟩ : ℕ) := by
-  rw [concatLower_val, dif_pos h]
-
-theorem concatLower_ge (f : Hom A A') (g : Hom B B')
-    (j : Fin (A.concat B).lower.length) (h : ¬ (j : ℕ) < A.lower.length) :
-    (concatLower f g j : ℕ) =
-      (g.fLower ⟨(j : ℕ) - A.lower.length,
-        by have e := concat_lower_len A B; have := j.2; omega⟩ : ℕ) + A'.lower.length := by
-  rw [concatLower_val, dif_neg h]
-
 /-- The concatenation bifunctor on morphisms (`f ⊗ g`): `f` on the A-block,
-    `g` (shifted) on the B-block. -/
+    `g` (shifted) on the B-block. Tiers via `LabeledTuple.Hom.concatMap`. -/
 def concatMap (f : Hom A A') (g : Hom B B') : Hom (A.concat B) (A'.concat B') where
-  fUpper := concatUpper f g
-  fLower := concatLower f g
-  upper_label i := by
-    show (A'.upper ++ B'.upper)[concatUpper f g i] = (A.upper ++ B.upper)[i]
-    rw [Fin.getElem_fin, Fin.getElem_fin]
-    rcases lt_or_ge (i : ℕ) A.upper.length with h | h
-    · have hb : (concatUpper f g i : ℕ) < A'.upper.length := by
-        rw [concatUpper_lt f g i h]; exact (f.fUpper ⟨i, h⟩).isLt
-      rw [List.getElem_append_left hb, List.getElem_append_left h]
-      have hl := f.upper_label ⟨i, h⟩
-      rw [Fin.getElem_fin, Fin.getElem_fin] at hl
-      rw [← hl]; congr 1; exact concatUpper_lt f g i h
-    · have hb : A'.upper.length ≤ (concatUpper f g i : ℕ) := by
-        rw [concatUpper_ge f g i (by omega)]; omega
-      rw [List.getElem_append_right hb, List.getElem_append_right h]
-      have hl := g.upper_label ⟨(i : ℕ) - A.upper.length, by
-        have e := concat_upper_len A B; have := i.2; omega⟩
-      rw [Fin.getElem_fin, Fin.getElem_fin] at hl
-      rw [← hl]; congr 1; rw [concatUpper_ge f g i (by omega)]; omega
-  lower_label j := by
-    show (A'.lower ++ B'.lower)[concatLower f g j] = (A.lower ++ B.lower)[j]
-    rw [Fin.getElem_fin, Fin.getElem_fin]
-    rcases lt_or_ge (j : ℕ) A.lower.length with h | h
-    · have hb : (concatLower f g j : ℕ) < A'.lower.length := by
-        rw [concatLower_lt f g j h]; exact (f.fLower ⟨j, h⟩).isLt
-      rw [List.getElem_append_left hb, List.getElem_append_left h]
-      have hl := f.lower_label ⟨j, h⟩
-      rw [Fin.getElem_fin, Fin.getElem_fin] at hl
-      rw [← hl]; congr 1; exact concatLower_lt f g j h
-    · have hb : A'.lower.length ≤ (concatLower f g j : ℕ) := by
-        rw [concatLower_ge f g j (by omega)]; omega
-      rw [List.getElem_append_right hb, List.getElem_append_right h]
-      have hl := g.lower_label ⟨(j : ℕ) - A.lower.length, by
-        have e := concat_lower_len A B; have := j.2; omega⟩
-      rw [Fin.getElem_fin, Fin.getElem_fin] at hl
-      rw [← hl]; congr 1; rw [concatLower_ge f g j (by omega)]; omega
-  links_preserve {p} hp := by
-    show ((concatUpper f g ((A.concat B).upperIdx hp) : ℕ),
-          (concatLower f g ((A.concat B).lowerIdx hp) : ℕ)) ∈ (A'.concat B').links
-    have hmem : p ∈ A.links ∪ B.links.image (shiftLink A.upper.length A.lower.length) := hp
-    rw [Finset.mem_union] at hmem
-    rw [links_concat, Finset.mem_union]
-    rcases hmem with hA | hB
-    · left
-      obtain ⟨hAu, hAl⟩ := A.inBounds p hA
-      rw [concatUpper_lt f g _ hAu, concatLower_lt f g _ hAl]
-      exact f.links_preserve hA
-    · right
-      rw [Finset.mem_image] at hB ⊢
-      obtain ⟨q, hq, rfl⟩ := hB
-      refine ⟨(↑(g.fUpper (B.upperIdx hq)), ↑(g.fLower (B.lowerIdx hq))),
-        g.links_preserve hq, ?_⟩
-      rw [concatUpper_ge f g _ (by simp [AR.upperIdx, shiftLink]),
-        concatLower_ge f g _ (by simp [AR.lowerIdx, shiftLink])]
-      simp only [shiftLink, Prod.mk.injEq]
-      refine ⟨?_, ?_⟩ <;>
-        · congr 2
-          apply Fin.ext
-          simp [AR.upperIdx, AR.lowerIdx]
-
-@[simp] theorem concatMap_fUpper (f : Hom A A') (g : Hom B B') :
-    (concatMap f g).fUpper = concatUpper f g := rfl
-
-@[simp] theorem concatMap_fLower (f : Hom A A') (g : Hom B B') :
-    (concatMap f g).fLower = concatLower f g := rfl
+  fU := LabeledTuple.Hom.concatMap f.fU g.fU
+  fL := LabeledTuple.Hom.concatMap f.fL g.fL
+  links_preserve {i j} hi hj h := by
+    simp only [links_concat, Finset.mem_union, Finset.mem_image, shiftLink,
+      Prod.exists, Prod.mk.injEq, LabeledTuple.Hom.concatMap_toFun] at h ⊢
+    rcases h with hA | ⟨a, b, hab, hai, hbj⟩
+    · obtain ⟨hiu, hjl⟩ := A.inBounds (i, j) hA
+      left
+      rw [Fin.appendMap_val, dif_pos hiu, Fin.appendMap_val, dif_pos hjl]
+      exact f.links_preserve hiu hjl hA
+    · obtain ⟨hau, hbl⟩ := B.inBounds (a, b) hab
+      subst hai hbj
+      right
+      refine ⟨(g.fU.toFun ⟨a, hau⟩ : ℕ), (g.fL.toFun ⟨b, hbl⟩ : ℕ),
+        g.links_preserve hau hbl hab, ?_, ?_⟩
+      · rw [Fin.appendMap_val, dif_neg (show ¬ (a + A.upper.len) < A.upper.len by omega)]
+        congr 2; apply Fin.ext; simp
+      · rw [Fin.appendMap_val, dif_neg (show ¬ (b + A.lower.len) < A.lower.len by omega)]
+        congr 2; apply Fin.ext; simp
+
+@[simp] theorem concatMap_fU (f : Hom A A') (g : Hom B B') :
+    (concatMap f g).fU = LabeledTuple.Hom.concatMap f.fU g.fU := rfl
+
+@[simp] theorem concatMap_fL (f : Hom A A') (g : Hom B B') :
+    (concatMap f g).fL = LabeledTuple.Hom.concatMap f.fL g.fL := rfl
 
 /-- The concat bifunctor preserves identities (`tensor_id`). -/
 theorem concatMap_id (A B : AR α β) :
     concatMap (Hom.id A) (Hom.id B) = Hom.id (A.concat B) := by
   apply Hom.ext <;>
-    · funext x; apply Fin.ext; simp [concatMap, concatUpper, concatLower, Hom.id]
+    simp only [concatMap_fU, concatMap_fL, id_fU, id_fL, LabeledTuple.Hom.concatMap_id,
+      concat_upper, concat_lower]
 
 /-- The concat bifunctor preserves composition (`tensor_comp`). -/
 theorem concatMap_comp {A A' A'' B B' B'' : AR α β}
     (f : Hom A A') (f' : Hom A' A'') (g : Hom B B') (g' : Hom B' B'') :
     (concatMap f g).comp (concatMap f' g') = concatMap (f.comp f') (g.comp g') := by
-  apply Hom.ext <;>
-    · funext x; apply Fin.ext
-      simp [concatMap, concatUpper, concatLower, comp, Function.comp_def, Sum.map_map]
+  apply Hom.ext
+  · simp only [comp_fU, concatMap_fU]
+    exact (LabeledTuple.Hom.concatMap_comp f.fU f'.fU g.fU g'.fU).symm
+  · simp only [comp_fL, concatMap_fL]
+    exact (LabeledTuple.Hom.concatMap_comp f.fL f'.fL g.fL g'.fL).symm
 
 end Hom
 
@@ -337,22 +229,15 @@ algebra (pentagon, triangle) or `Fin`-index arithmetic (naturalities).
 
 open CategoryTheory MonoidalCategory
 
-@[simp] theorem id_fUpper (A : AR α β) : (𝟙 A : Hom A A).fUpper = _root_.id := rfl
-@[simp] theorem id_fLower (A : AR α β) : (𝟙 A : Hom A A).fLower = _root_.id := rfl
-
-@[simp] theorem comp_fUpper {A B C : AR α β} (f : A ⟶ B) (g : B ⟶ C) :
-    (f ≫ g).fUpper = g.fUpper ∘ f.fUpper := rfl
-@[simp] theorem comp_fLower {A B C : AR α β} (f : A ⟶ B) (g : B ⟶ C) :
-    (f ≫ g).fLower = g.fLower ∘ f.fLower := rfl
-
-/-- The upper index map of an `eqToHom` is the length-cast `finCongr`. -/
-@[simp] theorem eqToHom_fUpper {A B : AR α β} (h : A = B) :
-    (eqToHom h).fUpper = finCongr (congrArg (fun X => X.upper.length) h) := by
+/-- 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 eqToHom_fU_toFun {A B : AR α β} (h : A = B) :
+    (eqToHom h).fU.toFun = Fin.cast (congrArg (fun X => X.upper.len) h) := by
   cases h; rfl
 
-/-- The lower index map of an `eqToHom` is the length-cast `finCongr`. -/
-@[simp] theorem eqToHom_fLower {A B : AR α β} (h : A = B) :
-    (eqToHom h).fLower = finCongr (congrArg (fun X => X.lower.length) h) := by
+/-- The lower tier map of an `eqToHom`, as a function. -/
+@[simp] theorem eqToHom_fL_toFun {A B : AR α β} (h : A = B) :
+    (eqToHom h).fL.toFun = Fin.cast (congrArg (fun X => X.lower.len) h) := by
   cases h; rfl
 
 /-- Tensoring an identity (left) with an `eqToHom` (right) is an `eqToHom`. -/
@@ -386,31 +271,26 @@ instance : MonoidalCategory (AR α β) :=
     (associator_naturality := by
       intro X₁ X₂ X₃ Y₁ Y₂ Y₃ f₁ f₂ f₃
       apply Hom.ext <;>
-        · funext x
+        · apply LabeledTuple.Hom.ext
+          funext x
           apply Fin.ext
-          simp [Hom.concatUpper_val, Hom.concatLower_val, concat_upper_len,
-            concat_lower_len, Nat.sub_sub]
+          simp [Fin.appendMap_val, Nat.sub_sub]
           split_ifs <;> omega)
     (leftUnitor_naturality := by
       intro X Y f
       apply Hom.ext <;>
-        · funext x
+        · apply LabeledTuple.Hom.ext
+          funext x
           apply Fin.ext
-          simp [Hom.concatUpper_val, Hom.concatLower_val, empty, Graph.empty]
+          simp [Fin.appendMap_val, empty, Graph.empty]
           rfl)
     (rightUnitor_naturality := by
       intro X Y f
-      apply Hom.ext
-      · funext x
-        apply Fin.ext
-        simp [Hom.concatUpper_val, empty, Graph.empty]
-        rw [dif_pos (lt_of_lt_of_eq x.isLt (by simp [upper_concat, empty, Graph.empty]))]
-        rfl
-      · funext x
-        apply Fin.ext
-        simp [Hom.concatLower_val, empty, Graph.empty]
-        rw [dif_pos (lt_of_lt_of_eq x.isLt (by simp [lower_concat, empty, Graph.empty]))]
-        rfl)
+      apply Hom.ext <;>
+        · apply LabeledTuple.Hom.ext
+          funext x
+          apply Fin.ext
+          simp [Fin.appendMap_val, empty, Graph.empty])
     (pentagon := by intros; simp [eqToHom_trans])
     (triangle := by intros; simp [eqToHom_trans])
 
diff --git a/Linglib/Phonology/Autosegmental/Floating.lean b/Linglib/Phonology/Autosegmental/Floating.lean
index 555aef1ae..307523286 100644
--- a/Linglib/Phonology/Autosegmental/Floating.lean
+++ b/Linglib/Phonology/Autosegmental/Floating.lean
@@ -117,7 +117,7 @@ structure FloatingForm (S T : Type*)
     prints only segments and underlying tier elements; debug-only. -/
 instance {S T : Type*} [Repr S] [Repr T] : Repr (FloatingForm S T) where
   reprPrec f _ :=
-    f!"⟨lower={repr (f.lower.map SegSpec.seg)}, upper={repr f.upper}⟩"
+    f!"⟨lower={repr (f.lower.toList.map SegSpec.seg)}, upper={repr f.upper.toList}⟩"
 
 namespace FloatingForm
 
@@ -137,8 +137,8 @@ variable {S T : Type*} [DecidableEq S] [DecidableEq T] (f : FloatingForm S T)
     nothing deleted, all underlying links intact. -/
 def mkInput (lower : List (SegSpec S)) (upper : List (TierSpec T))
     (links : Finset Link) : FloatingForm S T :=
-  { lower := lower
-    upper := upper
+  { lower := .ofList lower
+    upper := .ofList upper
     links := links
     deletedTier := ∅
     surfaceLinks := links }
@@ -146,14 +146,14 @@ def mkInput (lower : List (SegSpec S)) (upper : List (TierSpec T))
 /-! ### Morphemic structure -/
 
 /-- The morpheme of the `k`-th upper-tier element, or `none` if out of range. -/
-def upperMorpheme? (k : TierIdx) : Option Morpheme := (f.upper[k]?).map TierSpec.morpheme
+def upperMorpheme? (k : TierIdx) : Option Morpheme := (f.upper.get? (k)).map TierSpec.morpheme
 
 /-- The morpheme of the `i`-th lower-tier element, or `none` if out of range. -/
-def lowerMorpheme? (i : SegIdx) : Option Morpheme := (f.lower[i]?).map SegSpec.morpheme
+def lowerMorpheme? (i : SegIdx) : Option Morpheme := (f.lower.get? (i)).map SegSpec.morpheme
 
 /-- Every morpheme occurring on either tier. -/
 def morphemes : Finset Morpheme :=
-  (f.lower.map SegSpec.morpheme).toFinset ∪ (f.upper.map TierSpec.morpheme).toFinset
+  (f.lower.toList.map SegSpec.morpheme).toFinset ∪ (f.upper.toList.map TierSpec.morpheme).toFinset
 
 /-! ### Predicates on tier elements and links -/
 
@@ -175,7 +175,7 @@ abbrev IsFloating (k : TierIdx) : Prop := f.IsAlive k ∧ ¬ f.IsLinked k
     endpoints share a morpheme. Out-of-range indices on either side make this
     false. -/
 abbrev IsTautomorphic (l : Link) : Prop :=
-  f.upperMorpheme? l.fst = f.lowerMorpheme? l.snd ∧ (f.upper[l.fst]?).isSome
+  f.upperMorpheme? l.fst = f.lowerMorpheme? l.snd ∧ (f.upper.get? (l.fst)).isSome
 
 /-! ### Faithfulness: surface vs underlying -/
 
@@ -220,9 +220,9 @@ abbrev Crosses (k : TierIdx) (i : SegIdx) : Prop :=
     enforces well-formedness: without it a floating tone could dock across an
     intervening linked tone. -/
 def gen : Finset (FloatingForm S T) :=
-  let aliveIdxs := (Finset.range f.upper.length).filter (λ k => f.IsAlive k)
+  let aliveIdxs := (Finset.range f.upper.len).filter (λ k => f.IsAlive k)
   let floatIdxs := aliveIdxs.filter (λ k => ¬ f.IsLinked k)
-  let segIdxs := Finset.range f.lower.length
+  let segIdxs := Finset.range f.lower.len
   let deleteOps := aliveIdxs.image (λ k => f.deleteTierElem k)
   let insertOps := ((floatIdxs ×ˢ segIdxs).filter
     (λ ⟨k, i⟩ => ¬ f.Crosses k i)).image (λ ⟨k, i⟩ => f.insertLink k i)
@@ -234,42 +234,42 @@ def gen : Finset (FloatingForm S T) :=
     is `1` iff `upper[k]` is currently floating, else `0`. Drives directional
     floating constraints (e.g. `*FLOAT`). -/
 def floatIndicator : List ℕ :=
-  (List.range f.upper.length).map λ k => if f.IsFloating k then 1 else 0
+  (List.range f.upper.len).map λ k => if f.IsFloating k then 1 else 0
 
 /-- Upper-tier elements surface-linked to backbone position `i`, in tier order
     (smallest index first). `List.range`-based so the result is naturally sorted
     and reduces under kernel `decide` (avoiding `Finset.sort`, which doesn't
     unfold structurally). -/
 def linksTo (i : SegIdx) : List TierIdx :=
-  (List.range f.upper.length).filter λ k => (k, i) ∈ f.surfaceLinks
+  (List.range f.upper.len).filter λ k => (k, i) ∈ f.surfaceLinks
 
 /-- Sequence of tier values linked to backbone position `i`, in tier
     order. -/
 def tierValues (i : SegIdx) : List T :=
-  (f.linksTo i).filterMap λ k => f.upper[k]?.map TierSpec.value
+  (f.linksTo i).filterMap λ k => (f.upper.get? k).map TierSpec.value
 
 /-! ### Tier and morpheme subsequences -/
 
 /-- Indices of alive (non-deleted) underlying upper-tier elements, in tier
     order; `List.range`-based so it reduces under kernel `decide`. -/
 def aliveTierIdxs : List TierIdx :=
-  (List.range f.upper.length).filter (λ k => f.IsAlive k)
+  (List.range f.upper.len).filter (λ k => f.IsAlive k)
 
 /-- Lower-tier (backbone) indices belonging to morpheme `m`, in order.
     Out-of-range indices are excluded by construction. -/
 def segsOfMorpheme (m : Morpheme) : List SegIdx :=
-  (List.range f.lower.length).filter (λ i => f.lowerMorpheme? i = some m)
+  (List.range f.lower.len).filter (λ i => f.lowerMorpheme? i = some m)
 
 /-! ### Position counts -/
 
 /-- Count upper-tier positions satisfying decidable `p`. `List.range`-based so it
     reduces under kernel `decide` (avoiding `Finset` pipelines). -/
 def countUpper (p : TierIdx → Prop) [DecidablePred p] : ℕ :=
-  (List.range f.upper.length).countP (λ k => decide (p k))
+  (List.range f.upper.len).countP (λ k => decide (p k))
 
 /-- Count lower-tier (backbone) positions satisfying decidable `p`. -/
 def countLower (p : SegIdx → Prop) [DecidablePred p] : ℕ :=
-  (List.range f.lower.length).countP (λ i => decide (p i))
+  (List.range f.lower.len).countP (λ i => decide (p i))
 
 end FloatingForm
 
diff --git a/Linglib/Phonology/Autosegmental/Graph.lean b/Linglib/Phonology/Autosegmental/Graph.lean
index 97b541f64..512a97431 100644
--- a/Linglib/Phonology/Autosegmental/Graph.lean
+++ b/Linglib/Phonology/Autosegmental/Graph.lean
@@ -5,14 +5,16 @@ Authors: Robert Hawkins
 -/
 import Mathlib.Data.Finset.Image
 import Mathlib.Algebra.Group.Defs
+import Linglib.Core.CategoryTheory.Monoidal.LabeledTuple
 import Linglib.Phonology.Autosegmental.NonCrossing
 
 /-!
 # Autosegmental graph (the AR object)
 
 A `Autosegmental.Graph α β` is a finite ordered bipartite labeled relation
-between two tiers: an `upper` list of `α`s, a `lower` list of `β`s, and a
-`Finset` of association lines (index pairs). It is the standard *autosegmental
+between two tiers: an `upper` tier of `α`s, a `lower` tier of `β`s (each a
+`LabeledTuple` — a length plus a positional labeling), and a `Finset` of
+association lines (index pairs). It is the standard *autosegmental
 representation* (AR) of [goldsmith-1976] and the computational-phonology
 tradition ([jardine-2017], [chandlee-jardine-2019], [burness-mcmullin-2020]).
 
@@ -45,25 +47,30 @@ through a shared tier is not (it breaks planarity).
 
 ## Implementation notes
 
-`links : Finset (ℕ × ℕ)` uses raw natural-number indexing (matching the
-`MonovaryOn`-based `NonCrossing` substrate); in-bounds is a `Prop` (`InBounds`),
-not a structural invariant, and well-formedness conditions are separate `Prop`s
-rather than bundled invariants. A `Finset` permits multi-edges natively
-(spreading, geminates, contour tones). The label-merging variant of `concat`
-(unbounded spreading), multi-tier feature geometry, and the OT
+Tiers are `LabeledTuple`s (a length plus a labeling `Fin len → ·`), so the tier
+algebra — concatenation, the `Fin`-indexed morphism maps in `AR.lean` — delegates
+to the `LabeledTuple` keystone. `links : Finset (ℕ × ℕ)` keeps raw
+natural-number indexing (matching the `MonovaryOn`-based `NonCrossing` substrate,
+and keeping the monoid laws free of dependent-type casts); in-bounds is a `Prop`
+(`InBounds`), not a structural invariant, and well-formedness conditions are
+separate `Prop`s rather than bundled invariants. A `Finset` permits multi-edges
+natively (spreading, geminates, contour tones). The label-merging variant of
+`concat` (unbounded spreading), multi-tier feature geometry, and the OT
 underlying/surface split are paper-specific and live in consumers, not here.
 -/
 
 namespace Autosegmental
 
-/-- A bipartite autosegmental representation: two ordered tiers and a finite
-    set of association lines (index pairs) between them. -/
+open scoped CategoryTheory
+
+/-- A bipartite autosegmental representation: two ordered labeled tiers and a
+    finite set of association lines (index pairs) between them. -/
 @[ext]
 structure Graph (α β : Type*) where
   /-- The upper tier (e.g., tonal tier, melodic tier, root). -/
-  upper : List α
+  upper : LabeledTuple α
   /-- The lower tier (e.g., segmental backbone, skeleton, template). -/
-  lower : List β
+  lower : LabeledTuple β
   /-- Association lines as a finite set of index pairs
       `(upper-index, lower-index)`. -/
   links : Finset (ℕ × ℕ)
@@ -76,10 +83,10 @@ variable {α β : Type*} (r : Graph α β)
 /-! ### Construction -/
 
 /-- The empty bipartite representation with no tiers and no links. -/
-def empty : Graph α β := ⟨[], [], ∅⟩
+def empty : Graph α β := ⟨LabeledTuple.empty, LabeledTuple.empty, ∅⟩
 
 /-- Tiers with no links — the underlying form before any docking. -/
-def ofTiers (upper : List α) (lower : List β) : Graph α β :=
+def ofTiers (upper : LabeledTuple α) (lower : LabeledTuple β) : Graph α β :=
   ⟨upper, lower, ∅⟩
 
 /-! ### Planarity (no-crossing) -/
@@ -99,11 +106,11 @@ def IsLinkedLower (j : ℕ) : Prop :=
 
 /-- Upper index `i` is **floating**: in-bounds but unlinked. -/
 def IsFloatingUpper (i : ℕ) : Prop :=
-  i < r.upper.length ∧ ¬ r.IsLinkedUpper i
+  i < r.upper.len ∧ ¬ r.IsLinkedUpper i
 
 /-- Lower index `j` is **floating**: in-bounds but unlinked (*segmentally empty*). -/
 def IsFloatingLower (j : ℕ) : Prop :=
-  j < r.lower.length ∧ ¬ r.IsLinkedLower j
+  j < r.lower.len ∧ ¬ r.IsLinkedLower j
 
 /-! ### Decidability of index predicates -/
 
@@ -114,20 +121,20 @@ instance (j : ℕ) : Decidable (r.IsLinkedLower j) :=
   inferInstanceAs (Decidable (∃ p ∈ r.links, p.snd = j))
 
 instance (i : ℕ) : Decidable (r.IsFloatingUpper i) :=
-  inferInstanceAs (Decidable (i < r.upper.length ∧ ¬ r.IsLinkedUpper i))
+  inferInstanceAs (Decidable (i < r.upper.len ∧ ¬ r.IsLinkedUpper i))
 
 instance (j : ℕ) : Decidable (r.IsFloatingLower j) :=
-  inferInstanceAs (Decidable (j < r.lower.length ∧ ¬ r.IsLinkedLower j))
+  inferInstanceAs (Decidable (j < r.lower.len ∧ ¬ r.IsLinkedLower j))
 
 /-! ### Saturation and Goldsmith's WFC -/
 
 /-- **Saturated**: every in-bounds upper index is linked. -/
 def IsSaturatedUpper : Prop :=
-  ∀ i, i < r.upper.length → r.IsLinkedUpper i
+  ∀ i, i < r.upper.len → r.IsLinkedUpper i
 
 /-- **Saturated**: every in-bounds lower index is linked. -/
 def IsSaturatedLower : Prop :=
-  ∀ j, j < r.lower.length → r.IsLinkedLower j
+  ∀ j, j < r.lower.len → r.IsLinkedLower j
 
 /-- [goldsmith-1979]'s original WFC: planar *and* both tiers saturated.
     Post-[pulleyblank-1986], only `IsPlanar` is structural. -/
@@ -186,7 +193,7 @@ theorem isPlanar_empty : (empty : Graph α β).IsPlanar := by
   simp [IsPlanar, empty]
 
 /-- `ofTiers` produces a planar representation (no links to cross). -/
-theorem isPlanar_ofTiers (upper : List α) (lower : List β) :
+theorem isPlanar_ofTiers (upper : LabeledTuple α) (lower : LabeledTuple β) :
     (ofTiers upper lower).IsPlanar := by
   simp [IsPlanar, ofTiers]
 
@@ -194,7 +201,7 @@ theorem isPlanar_ofTiers (upper : List α) (lower : List β) :
 
 /-- Every link's indices fall within the tier lengths. -/
 def InBounds : Prop :=
-  ∀ p ∈ r.links, p.fst < r.upper.length ∧ p.snd < r.lower.length
+  ∀ p ∈ r.links, p.fst < r.upper.len ∧ p.snd < r.lower.len
 
 instance : Decidable r.InBounds := by
   unfold InBounds; infer_instance
@@ -202,7 +209,7 @@ instance : Decidable r.InBounds := by
 theorem inBounds_empty : (empty : Graph α β).InBounds := by
   simp [InBounds, empty]
 
-theorem inBounds_ofTiers (upper : List α) (lower : List β) :
+theorem inBounds_ofTiers (upper : LabeledTuple α) (lower : LabeledTuple β) :
     (ofTiers upper lower).InBounds := by
   simp [InBounds, ofTiers]
 
@@ -231,39 +238,39 @@ theorem shiftLink_comp (a₁ a₂ b₁ b₂ : ℕ) :
 /-- [jardine-heinz-2015] concatenation: tier-concatenation plus
     index-shifted link-set union. -/
 def concat (A B : Graph α β) : Graph α β where
-  upper := A.upper ++ B.upper
-  lower := A.lower ++ B.lower
-  links := A.links ∪ B.links.image (shiftLink A.upper.length A.lower.length)
+  upper := A.upper.concat B.upper
+  lower := A.lower.concat B.lower
+  links := A.links ∪ B.links.image (shiftLink A.upper.len A.lower.len)
 
 @[simp] theorem upper_concat (A B : Graph α β) :
-    (A.concat B).upper = A.upper ++ B.upper := rfl
+    (A.concat B).upper = A.upper.concat B.upper := rfl
 
 @[simp] theorem lower_concat (A B : Graph α β) :
-    (A.concat B).lower = A.lower ++ B.lower := rfl
+    (A.concat B).lower = A.lower.concat B.lower := rfl
 
 @[simp] theorem links_concat (A B : Graph α β) :
     (A.concat B).links =
-      A.links ∪ B.links.image (shiftLink A.upper.length A.lower.length) := rfl
+      A.links ∪ B.links.image (shiftLink A.upper.len A.lower.len) := rfl
 
 /-! #### Monoid laws ([jardine-heinz-2015] Theorems 1, 3) -/
 
 /-- `empty` is a left identity for `concat`. -/
-theorem empty_concat (A : Graph α β) : empty.concat A = A := by
-  ext <;> simp [empty, shiftLink_zero]
+theorem empty_concat (A : Graph α β) : empty.concat A = A :=
+  Graph.ext (LabeledTuple.empty_concat A.upper) (LabeledTuple.empty_concat A.lower)
+    (by simp [empty, shiftLink_zero])
 
 /-- `empty` is a right identity for `concat`. -/
-theorem concat_empty (A : Graph α β) : A.concat empty = A := by
-  ext <;> simp [empty]
+theorem concat_empty (A : Graph α β) : A.concat empty = A :=
+  Graph.ext (LabeledTuple.concat_empty A.upper) (LabeledTuple.concat_empty A.lower)
+    (by simp [empty])
 
 /-- `concat` is associative. -/
 theorem concat_assoc (A B C : Graph α β) :
-    (A.concat B).concat C = A.concat (B.concat C) := by
-  ext
-  · simp [List.append_assoc]
-  · simp [List.append_assoc]
-  · simp only [links_concat, upper_concat, lower_concat, List.length_append,
-               Finset.image_union, Finset.image_image, shiftLink_comp]
-    rw [Finset.union_assoc]
+    (A.concat B).concat C = A.concat (B.concat C) :=
+  Graph.ext (LabeledTuple.concat_assoc A.upper B.upper C.upper)
+    (LabeledTuple.concat_assoc A.lower B.lower C.lower)
+    (by simp only [links_concat, upper_concat, lower_concat, LabeledTuple.concat_len,
+          Finset.image_union, Finset.image_image, shiftLink_comp]; rw [Finset.union_assoc])
 
 /-! #### Planarity preservation ([jardine-heinz-2015] Theorem 4) -/
 
@@ -286,7 +293,7 @@ theorem inBounds_concat {A B : Graph α β}
     (hA : A.InBounds) (hB : B.InBounds) : (A.concat B).InBounds := by
   rintro p hp
   simp only [links_concat, Finset.mem_union, Finset.mem_image, upper_concat, lower_concat,
-    List.length_append] at hp ⊢
+    LabeledTuple.concat_len] at hp ⊢
   obtain hp | ⟨q, hq, rfl⟩ := hp
   · have := hA p hp; omega
   · have := hB q hq; simp only [shiftLink]; omega
diff --git a/Linglib/Phonology/Autosegmental/Subgraph.lean b/Linglib/Phonology/Autosegmental/Subgraph.lean
index 7b9697af2..81fd7f7b4 100644
--- a/Linglib/Phonology/Autosegmental/Subgraph.lean
+++ b/Linglib/Phonology/Autosegmental/Subgraph.lean
@@ -44,8 +44,8 @@ variable {α β : Type*}
     offset `δₗ` in G's lower tier, and all of F's association lines are present
     in G shifted by `(δᵤ, δₗ)`. -/
 def IsSubgraphAt (F G : Graph α β) (δᵤ δₗ : Nat) : Prop :=
-  (∀ i, i < F.upper.length → G.upper[i + δᵤ]? = F.upper[i]?) ∧
-  (∀ j, j < F.lower.length → G.lower[j + δₗ]? = F.lower[j]?) ∧
+  (∀ i, i < F.upper.len → G.upper.get? (i + δᵤ) = F.upper.get? i) ∧
+  (∀ j, j < F.lower.len → G.lower.get? (j + δₗ) = F.lower.get? j) ∧
   (∀ p ∈ F.links, (p.fst + δᵤ, p.snd + δₗ) ∈ G.links)
 
 instance [DecidableEq α] [DecidableEq β] (F G : Graph α β) (δᵤ δₗ : Nat) :
@@ -55,8 +55,8 @@ instance [DecidableEq α] [DecidableEq β] (F G : Graph α β) (δᵤ δₗ : Na
 /-- `F` **subgraph-embeds** into `G` iff some offset `(δᵤ, δₗ)` places F as a
     contiguous block inside G — [jardine-2017]'s connected-subgraph embedding. -/
 def SubgraphEmbeds (F G : Graph α β) : Prop :=
-  ∃ δᵤ ∈ Finset.range (G.upper.length + 1),
-  ∃ δₗ ∈ Finset.range (G.lower.length + 1),
+  ∃ δᵤ ∈ Finset.range (G.upper.len + 1),
+  ∃ δₗ ∈ Finset.range (G.lower.len + 1),
     IsSubgraphAt F G δᵤ δₗ
 
 instance [DecidableEq α] [DecidableEq β] (F G : Graph α β) :
diff --git a/Linglib/Phonology/Autosegmental/WellFormedAR.lean b/Linglib/Phonology/Autosegmental/WellFormedAR.lean
index 6ba802646..bdb137605 100644
--- a/Linglib/Phonology/Autosegmental/WellFormedAR.lean
+++ b/Linglib/Phonology/Autosegmental/WellFormedAR.lean
@@ -97,15 +97,15 @@ theorem ncc_isMonoidal : (isPlanar (α := α) (β := β)).IsMonoidal := inferIns
 
 /-- The OCP ([mccarthy-1986]) as a property of `AR`: the autosegmental (upper)
     tier has no adjacent identical elements. -/
-def upperOCPClean : ObjectProperty (AR α β) := fun A => OCP.IsClean A.upper
+def upperOCPClean : ObjectProperty (AR α β) := fun A => OCP.IsClean A.upper.toList
 
 instance [DecidableEq α] (A : AR α β) : Decidable (upperOCPClean A) :=
-  inferInstanceAs (Decidable (OCP.IsClean A.upper))
+  inferInstanceAs (Decidable (OCP.IsClean A.upper.toList))
 
 /-- A single-autosegment representation `⟨[true], [], ∅⟩`; concatenating it with
     itself produces the OCP-violating tier `[true, true]`. `Bool`/`Unit` is the
     smallest label/backbone pair admitting two equal upper elements. -/
-private def ocpWitness : AR Bool Unit := ⟨⟨[true], [], ∅⟩, by decide⟩
+private def ocpWitness : AR Bool Unit := ⟨⟨.ofList [true], .empty, ∅⟩, by decide⟩
 
 /-- The OCP is **not** morpheme-modular: concatenation can create an adjacent
     identical autosegment pair at the morpheme boundary — a violation present in
@@ -140,7 +140,7 @@ theorem ncc_modular_ocp_not :
     (`ocp_not_isMonoidal`) is what makes a repair *necessary*; this theorem
     exhibits one. -/
 theorem collapse_repairs_boundary [DecidableEq α] (A B : Graph α β) :
-    OCP.IsClean (OCP.collapse (A.concat B).upper) :=
+    OCP.IsClean (OCP.collapse (A.concat B).upper.toList) :=
   OCP.collapse_clean _
 
 end Autosegmental
diff --git a/Linglib/Phonology/Tone/Constraints.lean b/Linglib/Phonology/Tone/Constraints.lean
index fad6e75a3..c8d2fec32 100644
--- a/Linglib/Phonology/Tone/Constraints.lean
+++ b/Linglib/Phonology/Tone/Constraints.lean
@@ -60,7 +60,7 @@ on `FloatingForm`; only the `TRN`-reading predicate is here. -/
 
 /-- The tone at index `k` has value `t`. -/
 abbrev ToneHasValue (k : TierIdx) (t : TRN) : Prop :=
-  (f.upper[k]?).map TierSpec.value = some t
+  (f.upper.get? k).map TierSpec.value = some t
 
 /-! ### *FLOAT (Directional) -/
 
@@ -91,7 +91,7 @@ def starTautDock : DirectionalConstraint (FloatingForm S TRN) :=
 /-- The tone indices counting toward morpheme `m`'s tonal mass: surviving
     underlying tones of `m`, plus tones surface-linked to TBUs of `m`. -/
 def tonesForMorpheme (m : Morpheme) : Finset TierIdx :=
-  let ownAlive := (Finset.range f.upper.length).filter fun k =>
+  let ownAlive := (Finset.range f.upper.len).filter fun k =>
     f.IsAlive k ∧ f.upperMorpheme? k = some m
   let docked := (f.surfaceLinks.filter fun l => f.lowerMorpheme? l.snd = some m).image Prod.fst
   ownAlive ∪ docked
@@ -137,7 +137,7 @@ def starFall : DirectionalConstraint (FloatingForm S TRN) :=
 def starMlessL : DirectionalConstraint (FloatingForm S TRN) :=
   .ofCount "*M<L" .markedness (fun f =>
     let aliveValues : List TRN :=
-      f.aliveTierIdxs.filterMap (f.upper[·]?.map TierSpec.value)
+      f.aliveTierIdxs.filterMap (fun k => (f.upper.get? k).map TierSpec.value)
     (aliveValues.zip aliveValues.tail).countP (fun p => decide (p = (TRN.M, TRN.L))))
 
 /-! ### HAVETONE -/
diff --git a/Linglib/Studies/AkinboFwangwar2026.lean b/Linglib/Studies/AkinboFwangwar2026.lean
index 839b25112..96e86ab33 100644
--- a/Linglib/Studies/AkinboFwangwar2026.lean
+++ b/Linglib/Studies/AkinboFwangwar2026.lean
@@ -141,21 +141,21 @@ section SingleRoot
 /-- Does TBU `i` bear a tone of value `t` from morpheme `m`? -/
 def isGramTbu (t : TRN) (m : Morpheme) (f : MwaghavulForm) (i : SegIdx) : Bool :=
   (f.linksTo i).any fun k =>
-    (f.upper[k]?).any fun ts => decide (ts.value = t ∧ ts.morpheme = m)
+    (f.upper.get? k).any fun ts => decide (ts.value = t ∧ ts.morpheme = m)
 
 /-- L-ANCHOR-`t`-from-`m`: number of TBUs (in tier order) before the
     leftmost gram-`t`-from-`m` TBU. If no such TBU exists, every TBU
     counts (full TBU count). -/
 def lAnchTone (t : TRN) (m : Morpheme) (f : MwaghavulForm) : Nat :=
-  match (List.range f.lower.length).findIdx? (isGramTbu t m f) with
+  match (List.range f.lower.len).findIdx? (isGramTbu t m f) with
   | some i => i
-  | none   => f.lower.length
+  | none   => f.lower.len
 
 /-- R-ANCHOR-`t`-from-`m`: counted from the right edge. -/
 def rAnchTone (t : TRN) (m : Morpheme) (f : MwaghavulForm) : Nat :=
-  match (List.range f.lower.length).reverse.findIdx? (isGramTbu t m f) with
+  match (List.range f.lower.len).reverse.findIdx? (isGramTbu t m f) with
   | some i => i
-  | none   => f.lower.length
+  | none   => f.lower.len
 
 /-- MAX-Tone (per autosegment): count of deleted ulTier entries.
     Matches paper p. 26 per-autosegment counting. -/
@@ -293,7 +293,7 @@ def candE : MwaghavulForm :=
     INTEGRITY-Mᵥ fatally penalises this copying. -/
 def candF : MwaghavulForm :=
   { input with
-    upper := [rootL, vbzM, vbzM]
+    upper := .ofList [rootL, vbzM, vbzM]
     deletedTier := {0}
     surfaceLinks := {(1, 0), (2, 1)} }
 
diff --git a/Linglib/Studies/Jardine2017.lean b/Linglib/Studies/Jardine2017.lean
index 82ee04733..ecb8fb816 100644
--- a/Linglib/Studies/Jardine2017.lean
+++ b/Linglib/Studies/Jardine2017.lean
@@ -118,22 +118,22 @@ namespace Mende
 /-- `mbû` 'owl' (1σ, HL contour). Both H and L associate to the
     single syllable. Contour at the right edge — the only edge. -/
 def mbû : AR where
-  upper := [.H, .L]
-  lower := [.σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ]
   links := {(0, 0), (1, 0)}
 
 /-- `ngìlà` 'dog' (2σ, HL melody, one tone per syllable). -/
 def ngìlà : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ]
   links := {(0, 0), (1, 1)}
 
 /-- `félàmà` 'junction' (3σ, HL melody with L-spread to right two
     syllables: HLL surface). The diagnostic case for Mende: L
     spreads at the *right* edge. -/
 def félàmà : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ, .σ]
   links := {(0, 0), (1, 1), (1, 2)}
 
 /-! ### §2.1 Forbidden subgraphs ([jardine-2017] eq. 21)
@@ -148,23 +148,23 @@ appear in any well-formed Mende AR.
     tier. The L's presence is what makes the H "non-final" — there's
     another tone to its right. -/
 def forbidden_nonfinal_H : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ]
   links := {(0, 0), (0, 1)}
 
 /-- **(21b) non-final L spreading**: `¬ L→H : σ σ`. An L tone linked
     to two consecutive σs, with an H tone following. -/
 def forbidden_nonfinal_L : AR where
-  upper := [.L, .H]
-  lower := [.σ, .σ]
+  upper := .ofList [.L, .H]
+  lower := .ofList [.σ, .σ]
   links := {(0, 0), (0, 1)}
 
 /-- **(21c) non-final contour**: `¬ H L : σ→σ`. A contour (H and L
     both linked to one σ), with another σ following on the TBU tier.
     The trailing σ makes the contour-bearing σ "non-final". -/
 def forbidden_nonfinal_contour : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ]
   links := {(0, 0), (1, 0)}
 
 /-- The Mende grammar's forbidden block patterns ([jardine-2017] (21a–c)): a
@@ -219,15 +219,15 @@ namespace Hausa
 
 /-- `fáadi` 'fall' (2σ, HL melody one-to-one). -/
 def fáadi : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ]
   links := {(0, 0), (1, 1)}
 
 /-- `háantúnàa` 'noses' (3σ, HHL — H spreads at the *left* edge to
     the first two syllables). The Hausa diagnostic. -/
 def háantúnàa : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ, .σ]
   links := {(0, 0), (0, 1), (1, 2)}
 
 /-! ### §3.1 Forbidden subgraphs ([jardine-2017] eq. 22)
@@ -242,21 +242,21 @@ mirror; the third forbids a non-initial contour.
     tonal tier followed by an H linked to two σs — the H is
     non-initial (preceded by L). -/
 def forbidden_noninitial_H : AR where
-  upper := [.L, .H]
-  lower := [.σ, .σ]
+  upper := .ofList [.L, .H]
+  lower := .ofList [.σ, .σ]
   links := {(1, 0), (1, 1)}
 
 /-- **(22b) non-initial L spreading** (mirror). -/
 def forbidden_noninitial_L : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ]
   links := {(1, 0), (1, 1)}
 
 /-- **(22c) non-initial contour**: a σ preceded by another σ on
     the TBU tier, with a contour H L linked to the second σ. -/
 def forbidden_noninitial_contour : AR where
-  upper := [.H, .L]
-  lower := [.σ, .σ]
+  upper := .ofList [.H, .L]
+  lower := .ofList [.σ, .σ]
   links := {(0, 1), (1, 1)}
 
 /-! ### §3.2 Attested Hausa forms satisfy the Hausa grammar -/
diff --git a/Linglib/Studies/LaoideKemp2026.lean b/Linglib/Studies/LaoideKemp2026.lean
index 8ac3715d1..6c71f5622 100644
--- a/Linglib/Studies/LaoideKemp2026.lean
+++ b/Linglib/Studies/LaoideKemp2026.lean
@@ -242,23 +242,47 @@ association lines by the prefix's tier lengths.
 /-- The historic-tense exponent: a floating `(d)` melodic segment,
     no skeleton, no associations ([laoide-kemp-2026] Fig. 1). -/
 def historicExponent : Graph (TierSpec Segment) (SegSpec CVKind) where
-  upper := [mel .dPrime mHist]
-  lower := []
+  upper := .ofList [mel .dPrime mHist]
+  lower := .empty
   links := ∅
 
 /-- The past-tense impersonal exponent: an empty CV unit (`[C, V]`
     skeleton), no melody, no associations ([laoide-kemp-2026] §6.2,
     Fig. 5). -/
 def impersonalExponent : Graph (TierSpec Segment) (SegSpec CVKind) where
-  upper := []
-  lower := [slot .C mImpers, slot .V mImpers]
+  upper := .empty
+  lower := .ofList [slot .C mImpers, slot .V mImpers]
   links := ∅
 
 /-- Wrap a bare association graph as an input `FloatingForm` (surface
     state = underlying state). -/
 private def ofGraph (g : Graph (TierSpec Segment) (SegSpec CVKind)) :
     FloatingForm CVKind Segment :=
-  FloatingForm.mkInput g.lower g.upper g.links
+  FloatingForm.mkInput g.lower.toList g.upper.toList g.links
+
+/-- Rebuilding a `LabeledTuple` from its underlying list is the identity (up to
+    the length-cast packaged in `LabeledTuple.ext`). The round-trip
+    `mkInput` performs on the tiers is therefore inert. -/
+private theorem ofList_toList {γ : Type*} (a : LabeledTuple γ) :
+    LabeledTuple.ofList a.toList = a := by
+  refine LabeledTuple.ext (by simp) ?_
+  funext i
+  simp only [LabeledTuple.ofList_label, LabeledTuple.toList, List.get_eq_getElem,
+    Function.comp_apply, List.getElem_ofFn]
+  congr 1
+
+/-- `ofGraph` preserves the underlying graph: the `.toList`/`.ofList` round-trip
+    on the tiers cancels (`ofList_toList`) and the links pass through unchanged. -/
+@[simp] private theorem ofGraph_toGraph (g : Graph (TierSpec Segment) (SegSpec CVKind)) :
+    (ofGraph g).toGraph = g := by
+  unfold ofGraph FloatingForm.mkInput
+  cases g with
+  | mk upper lower links =>
+    simp only [Graph.mk.injEq]
+    exact ⟨ofList_toList upper, ofList_toList lower, trivial⟩
+
+@[simp] private theorem ofGraph_surfaceLinks (g : Graph (TierSpec Segment) (SegSpec CVKind)) :
+    (ofGraph g).surfaceLinks = g.links := rfl
 
 /-- Prefix the historic-tense exponent onto a stem (Fig. 1): floating
     `(d)` becomes melody index 0; the stem's melody shifts right by one. -/
@@ -293,7 +317,7 @@ so `{L}` cannot reach it and the *f* stays unmutated.
 /-- The melody index of the consonant linked to the leftmost skeletal
     slot (skeleton position 0), if any — the target of `{L}`. -/
 def initialConsonantIdx (f : FloatingForm CVKind Segment) : Option Nat :=
-  (List.range f.upper.length).find? (fun k => (k, 0) ∈ f.surfaceLinks)
+  (List.range f.upper.len).find? (fun k => (k, 0) ∈ f.surfaceLinks)
 
 /-- Apply lenition: if the consonant on the leftmost skeletal slot is
     `f`, delete its melodic content on the surface (leaving the slot
@@ -301,7 +325,7 @@ def initialConsonantIdx (f : FloatingForm CVKind Segment) : Option Nat :=
     are out of scope for the *d'* distribution question. -/
 def lenite (f : FloatingForm CVKind Segment) : FloatingForm CVKind Segment :=
   match initialConsonantIdx f with
-  | some k => if f.upper[k]?.map TierSpec.value = some .f then f.deleteTierElem k else f
+  | some k => if (f.upper.get? k).map TierSpec.value = some .f then f.deleteTierElem k else f
   | none   => f
 
 /-! ## §6 The docking predicate
@@ -316,14 +340,14 @@ linking convention.
 
 /-- Skeleton position `j` is a C-slot. -/
 def isCSlot (f : FloatingForm CVKind Segment) (j : Nat) : Prop :=
-  (f.lower[j]?).map SegSpec.seg = some .C
+  (f.lower.get? j).map SegSpec.seg = some .C
 
 instance (f : FloatingForm CVKind Segment) (j : Nat) : Decidable (isCSlot f j) :=
   inferInstanceAs (Decidable (_ = _))
 
 /-- Skeleton position `j` is a V-slot. -/
 def isVSlot (f : FloatingForm CVKind Segment) (j : Nat) : Prop :=
-  (f.lower[j]?).map SegSpec.seg = some .V
+  (f.lower.get? j).map SegSpec.seg = some .V
 
 instance (f : FloatingForm CVKind Segment) (j : Nat) : Decidable (isVSlot f j) :=
   inferInstanceAs (Decidable (_ = _))
@@ -440,7 +464,8 @@ dissolved). -/
     ([bermudez-otero-2012]'s strict modularity) — not a non-local
     insertion rule. -/
 theorem withHist_eq_concat (stem : FloatingForm CVKind Segment) :
-    (withHist stem).toGraph = historicExponent.concat stem.toGraph := rfl
+    (withHist stem).toGraph = historicExponent.concat stem.toGraph := by
+  rw [withHist, ofGraph_toGraph]
 
 /-- `historicExponent` is in-bounds: it has no links, so the condition
     is vacuous. -/
@@ -482,7 +507,7 @@ theorem dPrime_right_invariant :
 *every* suffix. The floating `(d)` shifts melody indices only, so
 surface-linkedness of a skeletal slot reduces to the stem's underlying
 links; and suffix material concatenated on the right lands at skeletal
-positions `≥ stem.lower.length`, never touching slots `0`/`1`. The
+positions `≥ stem.lower.len`, never touching slots `0`/`1`. The
 docking configuration is therefore determined by the stem's left edge
 alone — the formal content of strict modularity (no look-ahead). -/
 
@@ -495,7 +520,7 @@ private theorem isLinkedLower_withHist (X : FloatingForm CVKind Segment) (j : Na
       X.toGraph.links.image (Graph.shiftLink 1 0) := by
     show (historicExponent.concat X.toGraph).links = _
     rw [Graph.links_concat]
-    simp [historicExponent, Graph.empty]
+    simp [historicExponent]
   constructor
   · rintro ⟨p, hp, hpj⟩
     rw [hlinks, Finset.mem_image] at hp
@@ -512,11 +537,11 @@ private theorem isLinkedLower_withHist (X : FloatingForm CVKind Segment) (j : Na
     rw [hlinks, Finset.mem_image]
     exact ⟨(a, j), ha, by simp [Graph.shiftLink]⟩
 
-/-- A link to a low skeletal slot (`j < stem.lower.length`) is unaffected
+/-- A link to a low skeletal slot (`j < stem.lower.len`) is unaffected
     by appending a suffix: the suffix's links are shifted to slots
-    `≥ stem.lower.length`, never reaching `j`. -/
+    `≥ stem.lower.len`, never reaching `j`. -/
 private theorem linked_concat_low (stem suffix : FloatingForm CVKind Segment) {j : Nat}
-    (hj : j < stem.lower.length) :
+    (hj : j < stem.lower.len) :
     (∃ a, (a, j) ∈ (stem.toGraph.concat suffix.toGraph).links) ↔
       ∃ a, (a, j) ∈ stem.toGraph.links := by
   rw [Graph.links_concat]
@@ -538,8 +563,16 @@ private theorem linked_concat_low (stem suffix : FloatingForm CVKind Segment) {j
     floating `(d)` contributes no skeletal slot. -/
 private theorem withHist_lower (Y : FloatingForm CVKind Segment) :
     (withHist Y).lower = Y.toGraph.lower := by
-  show (historicExponent.concat Y.toGraph).lower = Y.toGraph.lower
-  rw [Graph.lower_concat]; simp [historicExponent]
+  rw [show (withHist Y).lower = (withHist Y).toGraph.lower from rfl, withHist_eq_concat,
+    Graph.lower_concat]
+  simp [historicExponent, LabeledTuple.empty_concat]
+
+/-- The melodic (upper) tier of a historic form is `(d)` concatenated with the
+    stem's — used to compute upper-tier lengths in the locality proofs. -/
+private theorem withHist_upper (Y : FloatingForm CVKind Segment) :
+    (withHist Y).upper = historicExponent.upper.concat Y.toGraph.upper := by
+  rw [show (withHist Y).upper = (withHist Y).toGraph.upper from rfl, withHist_eq_concat,
+    Graph.upper_concat]
 
 /-- **The general no-look-ahead theorem.** For *any* suffix, the
     `(d)`-docking configuration of the historic-tense form is determined
@@ -551,17 +584,16 @@ private theorem withHist_lower (Y : FloatingForm CVKind Segment) :
     which holds for in-bounds stems; this is the configuration-level
     statement, on which it rests.) -/
 theorem dDockable_withHist_concat_right (stem suffix : FloatingForm CVKind Segment)
-    (h2 : 2 ≤ stem.lower.length) :
+    (h2 : 2 ≤ stem.lower.len) :
     dDockable (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))) ↔
       dDockable (withHist stem) := by
-  have hlow : ∀ j, j < stem.lower.length →
-      (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).lower[j]? =
-        (withHist stem).lower[j]? := by
+  have hlow : ∀ j, j < stem.lower.len →
+      (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).lower.get? j =
+        (withHist stem).lower.get? j := by
     intro j hj
-    rw [withHist_lower, withHist_lower]
-    show (stem.toGraph.concat suffix.toGraph).lower[j]? = stem.toGraph.lower[j]?
-    rw [Graph.lower_concat, List.getElem?_append_left hj]
-  have hlink : ∀ j, j < stem.lower.length →
+    rw [withHist_lower, withHist_lower, ofGraph_toGraph,
+      Graph.lower_concat, LabeledTuple.get?_concat_left hj]
+  have hlink : ∀ j, j < stem.lower.len →
       ((withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).surfaceGraph.IsLinkedLower j ↔
         (withHist stem).surfaceGraph.IsLinkedLower j) := by
     intro j hj
@@ -582,12 +614,12 @@ link with an out-of-range melody index would sit outside `withHist
 stem`'s `initialConsonantIdx` search range but inside the longer suffixed
 range, and `lenite` could target different indices. -/
 
-/-- A surface link to a low skeletal slot (`j < stem.lower.length`) is
+/-- A surface link to a low skeletal slot (`j < stem.lower.len`) is
     present in the suffixed form iff present in the stem's — the
     pointwise (per `(k, j)`) version of `linked_concat_low`, used both
     for `initialConsonantIdx` and after `deleteTierElem`. -/
 private theorem mem_surfaceLinks_concat (stem suffix : FloatingForm CVKind Segment)
-    {k j : Nat} (hj : j < stem.lower.length) :
+    {k j : Nat} (hj : j < stem.lower.len) :
     (k, j) ∈ (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).surfaceLinks ↔
       (k, j) ∈ (withHist stem).surfaceLinks := by
   have hsB : (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).surfaceLinks =
@@ -600,7 +632,7 @@ private theorem mem_surfaceLinks_concat (stem suffix : FloatingForm CVKind Segme
     rw [Graph.links_concat]; simp [historicExponent]
   rw [hsB, hsA, Graph.links_concat, Finset.image_union, Finset.mem_union]
   have hfalse : (k, j) ∉ (suffix.toGraph.links.image
-      (Graph.shiftLink stem.upper.length stem.lower.length)).image (Graph.shiftLink 1 0) := by
+      (Graph.shiftLink stem.upper.len stem.lower.len)).image (Graph.shiftLink 1 0) := by
     rw [Finset.image_image, Finset.mem_image]
     rintro ⟨⟨a, b⟩, _, he⟩
     have hsnd := congrArg Prod.snd he
@@ -632,25 +664,24 @@ private theorem find?_range_stable {p : Nat → Bool} {m n : Nat} (hmn : m ≤ n
     by `InBounds`, the stem's slot-0 links sit inside its own melody
     range, so the longer suffixed search finds no extra match. -/
 private theorem initialConsonantIdx_concat (stem suffix : FloatingForm CVKind Segment)
-    (h2 : 2 ≤ stem.lower.length) (hib : stem.toGraph.InBounds) :
+    (h2 : 2 ≤ stem.lower.len) (hib : stem.toGraph.InBounds) :
     initialConsonantIdx (withHist (ofGraph (stem.toGraph.concat suffix.toGraph)))
       = initialConsonantIdx (withHist stem) := by
   have hpt : (fun k => decide ((k, 0) ∈
         (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).surfaceLinks)) =
       (fun k => decide ((k, 0) ∈ (withHist stem).surfaceLinks)) :=
     funext fun k => decide_eq_decide.mpr (mem_surfaceLinks_concat stem suffix (by omega))
-  have eA : (withHist stem).upper.length = stem.toGraph.upper.length + 1 := by
-    show (historicExponent.concat stem.toGraph).upper.length = _
-    simp [Graph.upper_concat, historicExponent]
+  have eA : (withHist stem).upper.len = stem.toGraph.upper.len + 1 := by
+    rw [withHist_upper]; simp [historicExponent, Nat.add_comm]
   unfold initialConsonantIdx
   rw [hpt]
   apply find?_range_stable
-  · show (withHist stem).upper.length ≤
-      (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper.length
-    have eB : (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper.length =
-        stem.toGraph.upper.length + suffix.toGraph.upper.length + 1 := by
-      show (historicExponent.concat (stem.toGraph.concat suffix.toGraph)).upper.length = _
-      simp [Graph.upper_concat, historicExponent]
+  · show (withHist stem).upper.len ≤
+      (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper.len
+    have eB : (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper.len =
+        stem.toGraph.upper.len + suffix.toGraph.upper.len + 1 := by
+      rw [withHist_upper, ofGraph_toGraph, Graph.upper_concat]
+      simp [historicExponent, LabeledTuple.concat_len]; omega
     omega
   · intro i hi
     simp only [decide_eq_false_iff_not]
@@ -669,19 +700,18 @@ private theorem initialConsonantIdx_concat (stem suffix : FloatingForm CVKind Se
     melody index `k`: `deleteTierElem k` only filters `surfaceLinks` and
     leaves the lower tier, so the slot-0/1 agreement survives. -/
 private theorem dDockable_deleteTierElem_concat (stem suffix : FloatingForm CVKind Segment)
-    (h2 : 2 ≤ stem.lower.length) (k : Nat) :
+    (h2 : 2 ≤ stem.lower.len) (k : Nat) :
     dDockable ((withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).deleteTierElem k) ↔
       dDockable ((withHist stem).deleteTierElem k) := by
-  have hlow : ∀ j, j < stem.lower.length →
-      ((withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).deleteTierElem k).lower[j]? =
-        ((withHist stem).deleteTierElem k).lower[j]? := by
+  have hlow : ∀ j, j < stem.lower.len →
+      ((withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).deleteTierElem k).lower.get? j =
+        ((withHist stem).deleteTierElem k).lower.get? j := by
     intro j hj
-    show (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).lower[j]? =
-      (withHist stem).lower[j]?
-    rw [withHist_lower, withHist_lower]
-    show (stem.toGraph.concat suffix.toGraph).lower[j]? = stem.toGraph.lower[j]?
-    rw [Graph.lower_concat, List.getElem?_append_left hj]
-  have hlink : ∀ j, j < stem.lower.length →
+    show (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).lower.get? j =
+      (withHist stem).lower.get? j
+    rw [withHist_lower, withHist_lower, ofGraph_toGraph,
+      Graph.lower_concat, LabeledTuple.get?_concat_left hj]
+  have hlink : ∀ j, j < stem.lower.len →
       (((withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).deleteTierElem k).surfaceGraph.IsLinkedLower j ↔
         ((withHist stem).deleteTierElem k).surfaceGraph.IsLinkedLower j) := by
     intro j hj
@@ -710,24 +740,20 @@ private theorem dDockable_deleteTierElem_concat (stem suffix : FloatingForm CVKi
     the paper's central claim, in full: preverbal *d'* never looks
     rightward past the word it attaches to. -/
 theorem dPrimeSurfaces_withHist_concat_right (stem suffix : FloatingForm CVKind Segment)
-    (h2 : 2 ≤ stem.lower.length) (hib : stem.toGraph.InBounds) :
+    (h2 : 2 ≤ stem.lower.len) (hib : stem.toGraph.InBounds) :
     dPrimeSurfaces (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))) ↔
       dPrimeSurfaces (withHist stem) := by
   have hk : ∀ k, initialConsonantIdx (withHist stem) = some k →
-      (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper[k]? =
-        (withHist stem).upper[k]? := by
+      (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper.get? k =
+        (withHist stem).upper.get? k := by
     intro k hoi
-    have hk_lt : k < (withHist stem).upper.length :=
+    have hk_lt : k < (withHist stem).upper.len :=
       List.mem_range.mp (List.mem_of_find?_eq_some hoi)
     have hsplit : (withHist (ofGraph (stem.toGraph.concat suffix.toGraph))).upper =
-        (withHist stem).upper ++ suffix.toGraph.upper := by
-      show (historicExponent.concat (stem.toGraph.concat suffix.toGraph)).upper = _
-      show historicExponent.upper ++ (stem.toGraph.concat suffix.toGraph).upper = _
-      rw [Graph.upper_concat]
-      show historicExponent.upper ++ (stem.toGraph.upper ++ suffix.toGraph.upper) = _
-      rw [← List.append_assoc]
-      rfl
-    rw [hsplit, List.getElem?_append_left hk_lt]
+        (withHist stem).upper.concat suffix.toGraph.upper := by
+      rw [withHist_upper, ofGraph_toGraph, Graph.upper_concat, withHist_upper,
+        LabeledTuple.concat_assoc]
+    rw [hsplit, LabeledTuple.get?_concat_left hk_lt]
   unfold dPrimeSurfaces lenite
   rw [initialConsonantIdx_concat stem suffix h2 hib]
   cases hoi : initialConsonantIdx (withHist stem) with
@@ -813,7 +839,7 @@ the full category `AR α β`: a label-preserving reindexing
 (`AR.Hom`) can move a non-initial element into initial position, after
 which there is *no* morphism between the delinked images at all
 (`delinkInitial_not_functorial`). But over the morphisms that **preserve
-which element is initial** — `fLower j = 0 → j = 0`, satisfied by every
+which element is initial** — `fL j = 0 → j = 0`, satisfied by every
 precedence-preserving `SubgraphEmbeds` translation — it lifts to a genuine
 functor (`delinkInitial_map`, with `delinkInitial_map_id` /
 `delinkInitial_map_comp`). This is the categorical content of the
@@ -840,16 +866,14 @@ def delinkInitial (A : AR α β) : AR α β where
     the hypothesis: a translation sends slot `j` to `j + δ`, which is `0`
     only when `j = 0`. -/
 def delinkInitial_map {A B : AR α β} (f : AR.Hom A B)
-    (hf : ∀ j, (f.fLower j : ℕ) = 0 → (j : ℕ) = 0) :
+    (hf : ∀ (j : Fin A.lower.len), (f.fL.toFun j : ℕ) = 0 → (j : ℕ) = 0) :
     AR.Hom (delinkInitial A) (delinkInitial B) where
-  fUpper := f.fUpper
-  fLower := f.fLower
-  upper_label := f.upper_label
-  lower_label := f.lower_label
-  links_preserve {p} hp := by
-    have hpA : p ∈ A.links := Finset.mem_of_mem_filter p hp
-    refine Finset.mem_filter.mpr ⟨f.links_preserve hpA, fun h0 => ?_⟩
-    exact (Finset.mem_filter.mp hp).2 (hf ((delinkInitial A).lowerIdx hp) h0)
+  fU := f.fU
+  fL := f.fL
+  links_preserve {i j} hi hj h := by
+    rw [delinkInitial_links, Finset.mem_filter] at h ⊢
+    obtain ⟨hmem, hne⟩ := h
+    exact ⟨f.links_preserve hi hj hmem, fun h0 => hne (hf ⟨j, hj⟩ h0)⟩
 
 /-- Functor law: `delinkInitial_map` preserves identities. -/
 theorem delinkInitial_map_id (A : AR α β) :
@@ -858,9 +882,9 @@ theorem delinkInitial_map_id (A : AR α β) :
 
 /-- Functor law: `delinkInitial_map` preserves composition. -/
 theorem delinkInitial_map_comp {A B C : AR α β} (f : AR.Hom A B) (g : AR.Hom B C)
-    (hf : ∀ j, (f.fLower j : ℕ) = 0 → (j : ℕ) = 0)
-    (hg : ∀ j, (g.fLower j : ℕ) = 0 → (j : ℕ) = 0)
-    (hfg : ∀ j, ((f.comp g).fLower j : ℕ) = 0 → (j : ℕ) = 0) :
+    (hf : ∀ (j : Fin A.lower.len), (f.fL.toFun j : ℕ) = 0 → (j : ℕ) = 0)
+    (hg : ∀ (j : Fin B.lower.len), (g.fL.toFun j : ℕ) = 0 → (j : ℕ) = 0)
+    (hfg : ∀ (j : Fin A.lower.len), ((f.comp g).fL.toFun j : ℕ) = 0 → (j : ℕ) = 0) :
     delinkInitial_map (f.comp g) hfg =
       (delinkInitial_map f hf).comp (delinkInitial_map g hg) := by
   apply AR.Hom.ext <;> rfl
@@ -869,19 +893,24 @@ end Frontier
 
 /-! ### The negative counterexample -/
 
-private def negA : AR ℕ ℕ := ⟨⟨[0], [0, 1], {(0, 1)}⟩, by decide⟩
-private def negB : AR ℕ ℕ := ⟨⟨[0], [1, 0], {(0, 0)}⟩, by decide⟩
+private def negA : AR ℕ ℕ := ⟨⟨.ofList [0], .ofList [0, 1], {(0, 1)}⟩, by decide⟩
+private def negB : AR ℕ ℕ := ⟨⟨.ofList [0], .ofList [1, 0], {(0, 0)}⟩, by decide⟩
 
 /-- A label-preserving reindexing that **swaps** the two skeletal slots,
     moving the slot-1 element into initial position. A valid `AR.Hom`
-    that does *not* reflect slot 0 (`fLower 1 = 0`). The `Fin`-indexed maps
+    that does *not* reflect slot 0 (`fL 1 = 0`). The `Fin`-indexed maps
     need no canonical-shift bookkeeping. -/
 private def negSwap : AR.Hom negA negB where
-  fUpper := _root_.id
-  fLower := fun j => if (j : ℕ) = 0 then ⟨1, by decide⟩ else ⟨0, by decide⟩
-  upper_label := by decide
-  lower_label := by decide
-  links_preserve := by decide
+  fU := ⟨_root_.id, by decide⟩
+  fL := ⟨fun j => if (j : ℕ) = 0 then ⟨1, by decide⟩ else ⟨0, by decide⟩, by decide⟩
+  links_preserve := by
+    intro i j hi hj h
+    have hij : (i, j) = (0, 1) := by
+      have : (i, j) ∈ ({(0, 1)} : Finset (ℕ × ℕ)) := h
+      simpa using this
+    obtain ⟨rfl, rfl⟩ := Prod.mk.injEq .. ▸ hij
+    show ((0 : ℕ), (0 : ℕ)) ∈ negB.links
+    decide
 
 /-- **`delinkInitial` is not a functor on the full category.** `negSwap`
     is a morphism `negA → negB`, yet after delinking there is *no* morphism
@@ -896,7 +925,9 @@ theorem delinkInitial_not_functorial :
       IsEmpty (AR.Hom (delinkInitial A) (delinkInitial B)) :=
   ⟨negA, negB, negSwap, ⟨fun g => by
     have hp : ((0, 1) : ℕ × ℕ) ∈ (delinkInitial negA).links := by decide
-    have h := g.links_preserve hp
+    have hi : (0 : ℕ) < (delinkInitial negA).upper.len := by decide
+    have hj : (1 : ℕ) < (delinkInitial negA).lower.len := by decide
+    have h := g.links_preserve hi hj hp
     have hempty : (delinkInitial negB).links = ∅ := by decide
     rw [hempty] at h
     simp at h⟩⟩
diff --git a/Linglib/Studies/McPhersonLamont2026.lean b/Linglib/Studies/McPhersonLamont2026.lean
index b980ce5a0..97a92da79 100644
--- a/Linglib/Studies/McPhersonLamont2026.lean
+++ b/Linglib/Studies/McPhersonLamont2026.lean
@@ -1007,8 +1007,8 @@ open Tone (TRN)
     `(i, i)` connects them. All resulting links are tautomorphic. -/
 def FloatingForm.ofTBUList {S : Type*} (host : List (TBU S)) (m : Morpheme) :
     FloatingForm S TRN where
-  lower := host.map (fun tbu => { seg := tbu.seg, morpheme := m })
-  upper := host.map (fun tbu => { value := tbu.tone, morpheme := m })
+  lower := .ofList (host.map (fun tbu => { seg := tbu.seg, morpheme := m }))
+  upper := .ofList (host.map (fun tbu => { value := tbu.tone, morpheme := m }))
   links := ((List.range host.length).map (fun i => (i, i))).toFinset
   deletedTier := ∅
   surfaceLinks := ((List.range host.length).map (fun i => (i, i))).toFinset
@@ -1051,9 +1051,9 @@ theorem FloatingForm.exists_multi_tone_TBU :
     ∃ f : FloatingForm Unit TRN, ∃ i : SegIdx, 2 ≤ (f.linksTo i).length := by
   refine ⟨?_, 0, ?_⟩
   · exact
-    { lower := [{ seg := (), morpheme := { form := "m" } }]
+    { lower := .ofList [{ seg := (), morpheme := { form := "m" } }]
       upper :=
-        [{ value := TRN.H, morpheme := { form := "m" } },
+        .ofList [{ value := TRN.H, morpheme := { form := "m" } },
          { value := TRN.L, morpheme := { form := "m" } }]
       links := ∅
       deletedTier := ∅