OCP-merging collapse of autosegmental representations

A merging tone realization ([jardine-2019]; the melody-merging naming function of [jardine-heinz-2015], Mende example) is OCP-merging: a tonal melody Hⁿ realizes as a single H node multiply associated to the n morae, not n separate H nodes. The project's Autosegmental.AR.realize (Realization.lean) instead uses the bridge-only concat (the categorical coproduct), which keeps the n H nodes apart. This file supplies the missing merge as a post-processing retraction on the upper tier:

• collapseGraph / collapseAR — fuse each maximal run of identical adjacent upper-tier labels into one node, carrying the association lines along: a link (k, j) is repointed to (ρ k, j), where ρ (runIdx) sends an upper position to the index of its run in the collapsed tier. The lower tier is untouched, so a merged node keeps all the morae its run was associated with (multiple association).
• AR.realizeMerged := collapseAR ∘ AR.realize — the OCP-merging realization.

The upper-tier collapse is exactly OCP.collapse (= List.destutter (· ≠ ·)); the link pushforward is the SimpleGraph.map/Quiver.Push idiom (Finset.image (Prod.map ρ id)); planarity survives because ρ is monotone (IsNonCrossing.image_monotone, NonCrossing.lean).

The AR-level OCP quotient monoid

collapseAR is the AR-level lift of FreeMonoid.destutterHom: a retraction onto the OCP-clean ARs that descends to a quotient of the concat monoid AR α β. The key congruence is collapseAR_concat — the AR shadow of OCP.collapse_append, whose links half reduces to runIdx commuting with the collapse-collapse seam (runIdx_append_collapse_left/right, in turn the boundary-length lemma List.destutter_append_length_clean). It bundles as collapseARHom : AR α β →* {A // IsCleanAR A}, whose mathlib quotient (ocpARQuotientEquiv) is the concrete OCP-clean model.

Main results

• collapseGraph_concat / collapseAR_concat — the collapse congruence (in-bounds free at AR level), the AR lift of OCP.collapse_append.
• collapseAR_id_on_clean — collapseAR retracts onto its OCP-clean fixed points.
• instMonoidCleanAR / collapseARHom / ocpARQuotientEquiv — the AR-level OCP quotient monoid, its bundled hom, and the first-isomorphism equivalence.
• upperHom / upperHomClean_comp_collapseARHom — the upper-tier projection and the decategorification square: the AR-level OCP quotient maps onto the tier-level one.
• autosegment_mul_self / ocpPresentation — the tier-level OCP-clean monoid is presented by idempotent autosegments ⟨α | a · a = a⟩; the OCP is a monoidal quotient, the counterpart to the No-Crossing Constraint's monoidal subcategory (ncc_isMonoidal).
• collapse_not_reflective — that quotient does not categorify: collapse is not a reflector (a morphism can split a geminate), so the OCP quotient lives on the object monoid, not the category — the precise sense in which OCP and NCC differ.

The collapse in coordinates

The OCP merge on the graph foundation: destutter melody tier m's word and repoint its links through runIdx. Like normalize the result is a AR on a sigma-Fin carrier, but the merge is not a pullback — runIdx is monotone, not bijective — so the structural axioms are proved directly on the merged carrier.

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

Tier words after collapsing melody tier m: destuttered at m, untouched elsewhere.

Equations

• Autosegmental.AR.collapsedWord X m = Function.update (fun (i : ι) => Autosegmental.AR.tierWord i) m (OCP.collapse (Autosegmental.AR.tierWord m))

@[simp]

theorem Autosegmental.AR.collapsedWord_self {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] : collapsedWord X m m = OCP.collapse (tierWord m)

@[simp]

theorem Autosegmental.AR.collapsedWord_of_ne {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] {i : ι} (h : i ≠ m) : collapsedWord X m i = tierWord i

theorem Autosegmental.AR.collapsedWord_length_le {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (i : ι) : (collapsedWord X m i).length ≤ tierLength X i

noncomputable def Autosegmental.AR.collapseIdx {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (i : ι) (p : ℕ) : ℕ

Position repointing: runIdx on the melody tier, identity elsewhere.

Equations

• Autosegmental.AR.collapseIdx X m i p = if i = m then OCP.runIdx (Autosegmental.AR.tierWord m) p else p

@[simp]

theorem Autosegmental.AR.collapseIdx_self {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (p : ℕ) : collapseIdx X m m p = OCP.runIdx (tierWord m) p

@[simp]

theorem Autosegmental.AR.collapseIdx_of_ne {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] {i : ι} (h : i ≠ m) (p : ℕ) : collapseIdx X m i p = p

noncomputable def Autosegmental.AR.collapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] : TieredAR ι τ

The OCP-merging collapse: melody tier m destuttered, links repointed through runIdx, other tiers untouched.

Equations

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

instance Autosegmental.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesCollapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] : Finite (AR.collapse X m).obj.V

noncomputable def Autosegmental.AR.collapseFiberEnum {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (i : ι) : Fin (collapsedWord X m i).length ≃o fiber (collapse X m) i

The collapsed fiber at i is enumerated by its position range.

Equations

• Autosegmental.AR.collapseFiberEnum X m i = StrictMono.orderIsoOfSurjective (fun (p : Fin (Autosegmental.AR.collapsedWord X m i).length) => ⟨⟨i, p⟩, ⋯⟩) ⋯ ⋯

@[simp]

theorem Autosegmental.AR.tierWord_collapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (i : ι) : tierWord i = collapsedWord X m i

The collapse does what it says: its tier words are the collapsed words — destuttered at m (Function.update_self), untouched elsewhere.

theorem Autosegmental.AR.collapsedWord_tensor {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) : collapsedWord (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m i = collapsedWord (CategoryTheory.MonoidalCategoryStruct.tensorObj (collapse X m) (collapse Y m)) m i

The word half of the OCP congruence: collapsing a tensor computes the same tier words as collapsing the tensor of the collapsed factors — OCP.collapse_append lifted through the readers.

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

theorem Autosegmental.AR.vertexEquiv_collapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] {i : ι} (r : Fin (tierLength (collapse X m) i)) : vertexEquiv ⟨i, r⟩ = ⟨i, Fin.cast ⋯ r⟩

theorem Autosegmental.AR.link_collapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (i j : ι) (r s : ℕ) : link (collapse X m) i j r s ↔ ∃ (p : ℕ) (q : ℕ), link X i j p q ∧ collapseIdx X m i p = r ∧ collapseIdx X m j q = s

The collapse's links are the image of the original links under the repointing — edges_normalize's analogue for the merge.

@[simp]

theorem Autosegmental.AR.tierLength_collapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] (i : ι) : tierLength (collapse X m) i = (collapsedWord X m i).length

theorem Autosegmental.AR.collapseIdx_left {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) {p : ℕ} (hp : p < tierLength X i) : collapseIdx (CategoryTheory.MonoidalCategoryStruct.tensorObj (collapse X m) (collapse Y m)) m i (collapseIdx X m i p) = collapseIdx (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m i p

Left-block positions commute with the collapse-collapse seam.

theorem Autosegmental.AR.collapseIdx_right {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i : ι) {p : ℕ} (hp : p < tierLength Y i) : collapseIdx (CategoryTheory.MonoidalCategoryStruct.tensorObj (collapse X m) (collapse Y m)) m i (tierLength (collapse X m) i + collapseIdx Y m i p) = collapseIdx (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m i (tierLength X i + p)

Right-block positions commute with the collapse-collapse seam.

theorem Autosegmental.AR.link_collapse_tensor {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] (i j : ι) (r s : ℕ) : link (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m) i j r s ↔ link (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj (collapse X m) (collapse Y m)) m) i j r s

The link half of the OCP congruence, in ℕ coordinates.

noncomputable def Autosegmental.AR.collapseTensorFullIso {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] : (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m).obj.Iso (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj (collapse X m) (collapse Y m)) m).obj

The OCP congruence: collapsing a concatenation is isomorphic to collapsing the concatenation of the collapses — [jardine-heinz-2015]'s melody-merge law, by the classification theorem.

Equations

• Autosegmental.AR.collapseTensorFullIso X m = Autosegmental.AR.fullIsoOfReaderEq ⋯ ⋯

theorem Autosegmental.AR.cls_collapse_tensor {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] {Y : TieredAR ι τ} [Finite X.obj.V] [Finite Y.obj.V] : cls (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) m) = cls (collapse (CategoryTheory.MonoidalCategoryStruct.tensorObj (collapse X m) (collapse Y m)) m)

The OCP congruence as an equality of isomorphism classes: collapse descends to the class monoid.

def Autosegmental.AR.IsCleanAt {ι : Type u_3} {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [Finite X.obj.V] : Prop

OCP-cleanliness at melody tier m: the tier word has no adjacent repeats.

Equations

• Autosegmental.AR.IsCleanAt X m = OCP.IsClean (Autosegmental.AR.tierWord m)

theorem Autosegmental.AR.isCleanAt_collapse {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [DecidableEq (τ m)] [Finite X.obj.V] : IsCleanAt (collapse X m) m

The collapse is OCP-clean at the collapsed tier.

noncomputable def Autosegmental.realizeMerged {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (m : ι) [DecidableEq (τ m)] {S : Type u_5} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (w : List S) : TieredAR ι τ

The OCP-merging realization at melody tier m — [jardine-2019]'s merging g_T: AR.realize, then merge the melody runs.

Equations

• Autosegmental.realizeMerged m g₀ w = Autosegmental.AR.collapse (Autosegmental.AR.realize g₀ w) m

instance Autosegmental.instFiniteVSigmaObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesRealizeMerged {ι : Type u_3} [DecidableEq ι] {τ : ι → Type u_4} (m : ι) [DecidableEq (τ m)] {S : Type u_5} (g₀ : S → TieredAR ι τ) [∀ (s : S), Finite (g₀ s).obj.V] (w : List S) : Finite (realizeMerged m g₀ w).obj.V

The merged realization of word primitives

Two-tier case, melody over true: the merged realization of a string of word primitives has the readers of one representation of words — the melody destuttered, the lines repointed through the run index.

def Autosegmental.mergedLinks {α : Type u} [DecidableEq α] (melody : List α) (Lk : ℕ → ℕ → Prop) (r s : ℕ) : Prop

The lines of an OCP-merged realization: a line of the realization with its melody position repointed through the run index of the melody.

Equations

• Autosegmental.mergedLinks melody Lk r s = ∃ p < melody.length, Lk p s ∧ OCP.runIdx melody p = r

@[instance_reducible]

instance Autosegmental.instDecidableRelNatMergedLinks {α : Type u} [DecidableEq α] (melody : List α) (Lk : ℕ → ℕ → Prop) [DecidableRel Lk] : DecidableRel (mergedLinks melody Lk)

Equations

• Autosegmental.instDecidableRelNatMergedLinks melody Lk x✝¹ x✝ = id inferInstance

theorem Autosegmental.AR.link_collapse_true_false {α β : Type u} [DecidableEq α] (X : TieredAR Bool (TwoTier α β)) [Finite X.obj.V] (r s : ℕ) : link (collapse X true) true false r s ↔ ∃ p < tierLength X true, link X true false p s ∧ OCP.runIdx (tierWord true) p = r

Melody-to-timing lines of a two-tier collapse at the melody tier.

theorem Autosegmental.AR.tierWord_realizeMerged_true_of_eq_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) : tierWord true = OCP.collapse (List.map as w).flatten

theorem Autosegmental.AR.tierWord_realizeMerged_false_of_eq_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) : tierWord false = (List.map bs w).flatten

theorem Autosegmental.AR.link_realizeMerged_of_eq_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) (r s : ℕ) : link (realizeMerged true g₀ w) true false r s ↔ mergedLinks (List.map as w).flatten (blockLinks as bs L w) r s

theorem Autosegmental.AR.tierWord_realizeMerged_eq_tierWord_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) (i : Bool) : tierWord i = tierWord i

The tier words of the merged realization are those of its representation of words.

theorem Autosegmental.AR.link_realizeMerged_iff_link_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) (i j : Bool) (p q : ℕ) : link (realizeMerged true g₀ w) i j p q ↔ (ofWords (OCP.collapse (List.map as w).flatten) (List.map bs w).flatten (mergedLinks (List.map as w).flatten (blockLinks as bs L w))).link i j p q

The lines of the merged realization are those of its representation of words.

theorem Autosegmental.AR.factorEmbeds_realizeMerged_iff_of_eq_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (F : TieredAR Bool (TwoTier α β)) [Finite F.obj.V] (w : List S) : FactorEmbeds F (realizeMerged true g₀ w) ↔ FactorEmbeds F (ofWords (OCP.collapse (List.map as w).flatten) (List.map bs w).flatten (mergedLinks (List.map as w).flatten (blockLinks as bs L w)))

Embedding into the merged realization of word primitives computes on the words.

theorem Autosegmental.AR.free_realizeMerged_iff_of_eq_ofWords {α β : Type u} [DecidableEq α] {S : Type u_5} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → TieredAR Bool (TwoTier α β)) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (B : List { F : TieredAR Bool (TwoTier α β) // Finite F.obj.V }) (w : List S) : Free (realizeMerged true g₀ w) B ↔ (ofWords (OCP.collapse (List.map as w).flatten) (List.map bs w).flatten (mergedLinks (List.map as w).flatten (blockLinks as bs L w))).Free B

theorem Autosegmental.AR.covering_normalize {ι : Type u_3} {τ : ι → Type u_4} (X : TieredAR ι τ) [Finite X.obj.V] {i : ι} {p q : Fin (tierLength X i)} : ((normalize X).obj.arcs.Adj ⟨i, p⟩ ⟨i, q⟩ ∧ ∀ (u : (normalize X).obj.V), ¬((normalize X).obj.arcs.Adj ⟨i, p⟩ u ∧ (normalize X).obj.arcs.Adj u ⟨i, q⟩)) ↔ ↑q = ↑p + 1

On a normal form, one position covers another in the arc order iff it is its immediate successor.

theorem Autosegmental.AR.isCleanAt_iff_isOCPClean {ι : Type u_3} {τ : ι → Type u_4} (X : TieredAR ι τ) (m : ι) [Finite X.obj.V] : IsCleanAt X m ↔ IsOCPClean (normalize X).obj.arcs (normalize X).obj.label Sigma.fst m

The OCP bridge: tier-word cleanliness is Axiom 6 on the normal form — the coordinate OCP and [jardine-2016b]'s §4.2 axiom agree.