OCP-merging collapse of autosegmental representations

A merging tone realization ([Jar19]; the melody-merging naming function of [JH15], 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.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).
• realizeMerged := collapseAR ∘ 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 run-index map

def Autosegmental.runIdx {α : Type u_1} [DecidableEq α] (xs : List α) (k : ℕ) : ℕ

Run index of upper position k in xs: the index (0-based) of the OCP-run containing k, i.e. one less than the number of runs in the prefix xs[0..k]. Concretely (OCP.collapse (xs.take (k+1))).length - 1.

Equations

• Autosegmental.runIdx xs k = (OCP.collapse (List.take (k + 1) xs)).length - 1

theorem Autosegmental.runIdx_monotone {α : Type u_1} [DecidableEq α] (xs : List α) : Monotone (runIdx xs)

runIdx is monotone: later positions sit in later (or the same) runs.

theorem Autosegmental.runIdx_lt_collapse_length {α : Type u_1} [DecidableEq α] (xs : List α) {k : ℕ} (hk : k < xs.length) : runIdx xs k < (OCP.collapse xs).length

runIdx lands inside the collapsed tier: an in-bounds position maps to an in-bounds run index. The upper half of collapseAR's in-bounds proof.

@[simp]

theorem Autosegmental.runIdx_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (a : α) (k : ℕ) : runIdx (List.replicate n a) k = 0

On a constant tier every position lies in the single run: runIdx is 0.

Run-index and concatenation

The defining property of concat for the OCP quotient: runIdx commutes with the collapse-collapse seam (runIdx_append_collapse_left/right). On the A-block the prefix run-index is untouched (runIdx_append_left, plus runIdx_clean re-reading a clean tier as the identity); on the B-block the seam merges exactly when collapse xs ends in the element heading ys (runIdx_append_right, the AR shadow of List.destutter_append_length_clean).

theorem Autosegmental.runIdx_append_left {α : Type u_1} [DecidableEq α] {xs ys : List α} {k : ℕ} (h : k < xs.length) : runIdx (xs ++ ys) k = runIdx xs k

The prefix run-index is unaffected by a right append.

theorem Autosegmental.runIdx_clean {α : Type u_1} [DecidableEq α] {xs : List α} (hc : OCP.IsClean xs) {k : ℕ} (h : k < xs.length) : runIdx xs k = k

On a clean tier runIdx is the identity (no runs to merge).

theorem Autosegmental.collapse_take_succ_length {α : Type u_1} [DecidableEq α] {xs : List α} {m : ℕ} (hm : m < xs.length) : (OCP.collapse (List.take (m + 1) xs)).length = runIdx xs m + 1

The length of the collapse of a nonempty prefix is its top run-index plus one.

theorem Autosegmental.collapse_take_head? {α : Type u_1} [DecidableEq α] {xs : List α} {m : ℕ} : (OCP.collapse (List.take (m + 1) xs)).head? = xs.head?

The collapse of a prefix has the same head as the whole tier.

theorem Autosegmental.runIdx_append_right {α : Type u_1} [DecidableEq α] {xs ys : List α} {a : ℕ} (ha : a < ys.length) : runIdx (xs ++ ys) (xs.length + a) = (OCP.collapse xs).length + runIdx ys a - if (OCP.collapse xs).getLast? = ys.head? then 1 else 0

The B-part seam identity. Reading a suffix position through the collapse of an append: the run-index is the left collapse's length plus the suffix's own run-index, minus one exactly when the seam merges (List.destutter_append_length_clean).

theorem Autosegmental.runIdx_append_collapse_left {α : Type u_1} [DecidableEq α] {xs ys : List α} {k : ℕ} (h : k < xs.length) : runIdx (xs ++ ys) k = runIdx (OCP.collapse xs ++ OCP.collapse ys) (runIdx xs k)

A-block: a prefix index commutes with the collapse-collapse seam.

theorem Autosegmental.runIdx_append_collapse_right {α : Type u_1} [DecidableEq α] {xs ys : List α} {a : ℕ} (ha : a < ys.length) : runIdx (xs ++ ys) (xs.length + a) = runIdx (OCP.collapse xs ++ OCP.collapse ys) ((OCP.collapse xs).length + runIdx ys a)

B-block: a suffix index commutes with the collapse-collapse seam.

Collapse on graphs

def Autosegmental.collapseGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : Graph α β) : Graph α β

OCP-merging collapse on graphs: fuse each maximal run of identical adjacent upper labels into one node (OCP.collapse), repointing every association line (k, j) to (runIdx k, j) (the SimpleGraph.map/push idiom). The lower tier is unchanged, so a merged node inherits all the lines of its run.

Equations

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

@[simp]

theorem Autosegmental.collapseGraph_upper {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : Graph α β) : (collapseGraph A).upper = LabeledTuple.ofList (OCP.collapse A.upper.toList)

@[simp]

theorem Autosegmental.collapseGraph_lower {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : Graph α β) : (collapseGraph A).lower = A.lower

@[simp]

theorem Autosegmental.collapseGraph_links {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : Graph α β) : (collapseGraph A).links = Finset.image (Prod.map (runIdx A.upper.toList) id) A.links

theorem Autosegmental.inBounds_collapseGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] {A : Graph α β} (hA : A.InBounds) : (collapseGraph A).InBounds

collapseGraph preserves in-bounds: upper indices land in the collapsed tier (runIdx_lt_collapse_length), lower indices are unchanged.

theorem Autosegmental.isPlanar_collapseGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] {A : Graph α β} (hA : A.IsPlanar) : (collapseGraph A).IsPlanar

collapseGraph preserves planarity: the run-collapse runIdx is monotone, so pushing the links forward stays non-crossing (IsNonCrossing.image_monotone).

The collapse congruence

collapseGraph is a congruence for concat: collapsing the operands first is harmless. This is the AR-level lift of OCP.collapse_append, and the algebraic content powering the OCP quotient monoid (collapseARHom). The upper tier follows from collapse_append; the links follow because runIdx commutes with the collapse-collapse seam (runIdx_append_collapse_left/right), on link sets kept in-bounds by hypothesis.

theorem Autosegmental.collapseGraph_concat {α : Type u_1} {β : Type u_2} [DecidableEq α] {A B : Graph α β} (hA : A.InBounds) (hB : B.InBounds) : collapseGraph (A.concat B) = collapseGraph ((collapseGraph A).concat (collapseGraph B))

The collapse congruence on graphs (in-bounds operands).

Collapse on ARs

def Autosegmental.collapseAR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : AR α β

OCP-merging collapse on ARs: collapseGraph repackaged with its in-bounds proof. The AR-level lift of FreeMonoid.destutterHom — the run-collapse carrying the association lines the flat tier-string discards.

Equations

• Autosegmental.collapseAR A = { toGraph := Autosegmental.collapseGraph A.toGraph, inBounds := ⋯ }

@[simp]

theorem Autosegmental.collapseAR_toGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : (collapseAR A).toGraph = collapseGraph A.toGraph

theorem Autosegmental.collapseAR_isPlanar {α : Type u_1} {β : Type u_2} [DecidableEq α] {A : AR α β} (hA : A.IsPlanar) : (collapseAR A).IsPlanar

collapseAR preserves planarity ([Gol76]'s NCC survives OCP merging): the consumer-facing form of isPlanar_collapseGraph.

theorem Autosegmental.collapseAR_concat {α : Type u_1} {β : Type u_2} [DecidableEq α] (A B : AR α β) : collapseAR (A.concat B) = collapseAR ((collapseAR A).concat (collapseAR B))

The collapse congruence on ARs (collapseGraph_concat repackaged; inBounds is free): collapseAR descends to a homomorphism of the concat monoid.

The AR-level OCP quotient monoid

The base object AR α β carries the concatenation monoid (AR.instMonoid); collapseAR is the OCP retraction onto its OCP-clean fixed points. collapseAR_concat is the homomorphism law, so collapseAR bundles as collapseARHom : AR α β →* {A // IsCleanAR A} — the AR-level lift of FreeMonoid.destutterHom, carrying the association lines the flat tier-string discards. As a mathlib quotient, {A // IsCleanAR A} is AR α β ⧸ Con.ker collapseARHom (ocpARQuotientEquiv).

def Autosegmental.IsCleanAR {α : Type u_1} {β : Type u_2} (A : AR α β) : Prop

An AR is OCP-clean when its upper tier is (no adjacent identical autosegments).

Equations

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

@[implicit_reducible]

instance Autosegmental.decidableIsCleanAR {α : Type u_1} {β : Type u_2} [DecidableEq α] : DecidablePred IsCleanAR

Equations

• Autosegmental.decidableIsCleanAR A = Autosegmental.decidableIsCleanAR._aux_1 A

@[simp]

theorem Autosegmental.isCleanAR_collapseAR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : IsCleanAR (collapseAR A)

theorem Autosegmental.collapseAR_id_on_clean {α : Type u_1} {β : Type u_2} [DecidableEq α] {A : AR α β} (hA : IsCleanAR A) : collapseAR A = A

collapseAR fixes OCP-clean ARs: a clean upper tier is its own collapse and runIdx is then the identity, so the links are unchanged.

@[simp]

theorem Autosegmental.isCleanAR_one {α : Type u_1} {β : Type u_2} : IsCleanAR 1

@[simp]

theorem Autosegmental.collapseAR_one {α : Type u_1} {β : Type u_2} [DecidableEq α] : collapseAR 1 = 1

@[simp]

theorem Autosegmental.collapseAR_idempotent {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : collapseAR (collapseAR A) = collapseAR A

theorem Autosegmental.collapseAR_concat_left {α : Type u_1} {β : Type u_2} [DecidableEq α] (A B : AR α β) : collapseAR ((collapseAR A).concat B) = collapseAR (A.concat B)

Collapsing the left operand before concatenating is absorbed by the outer collapse.

theorem Autosegmental.collapseAR_concat_right {α : Type u_1} {β : Type u_2} [DecidableEq α] (A B : AR α β) : collapseAR (A.concat (collapseAR B)) = collapseAR (A.concat B)

Collapsing the right operand before concatenating is absorbed by the outer collapse.

The bundled AR quotient monoid

def Autosegmental.gconcatAR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A B : AR α β) : AR α β

OCP-gluing concatenation on ARs: concatenate, then merge the new boundary run. The multiplication of the AR-level OCP quotient monoid.

Equations

• Autosegmental.gconcatAR A B = Autosegmental.collapseAR (A.concat B)

@[implicit_reducible]

instance Autosegmental.instMulSubtypeARIsCleanAR {α : Type u_1} {β : Type u_2} [DecidableEq α] : Mul { A : AR α β // IsCleanAR A }

Equations

• Autosegmental.instMulSubtypeARIsCleanAR = { mul := fun (A B : { A : Autosegmental.AR α β // Autosegmental.IsCleanAR A }) => ⟨Autosegmental.gconcatAR ↑A ↑B, ⋯⟩ }

@[implicit_reducible]

instance Autosegmental.instOneSubtypeARIsCleanAR {α : Type u_1} {β : Type u_2} : One { A : AR α β // IsCleanAR A }

Equations

• Autosegmental.instOneSubtypeARIsCleanAR = { one := ⟨1, ⋯⟩ }

@[simp]

theorem Autosegmental.coe_mul_AR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A B : { A : AR α β // IsCleanAR A }) : ↑(A * B) = gconcatAR ↑A ↑B

@[simp]

theorem Autosegmental.coe_one_AR {α : Type u_1} {β : Type u_2} : ↑1 = 1

@[implicit_reducible]

instance Autosegmental.instMonoidCleanAR {α : Type u_1} {β : Type u_2} [DecidableEq α] : Monoid { A : AR α β // IsCleanAR A }

The AR-level OCP quotient monoid on the OCP-clean subtype: gconcatAR multiplication, 1 unit. Associativity is collapseAR_concat; units use collapseAR_id_on_clean.

Equations

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

def Autosegmental.collapseARHom {α : Type u_1} {β : Type u_2} [DecidableEq α] : AR α β →* { A : AR α β // IsCleanAR A }

The bundled AR-level OCP quotient map. collapseAR_concat is its map_mul; the AR-level lift of FreeMonoid.destutterHom.

Equations

• Autosegmental.collapseARHom = { toFun := fun (A : Autosegmental.AR α β) => ⟨Autosegmental.collapseAR A, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

As a mathlib quotient monoid

def Autosegmental.ocpConAR {α : Type u_1} {β : Type u_2} [DecidableEq α] : Con (AR α β)

The OCP congruence on the AR concat monoid: the kernel of collapseARHom. The AR-level OCP quotient monoid is ocpConAR.Quotient.

Equations

• Autosegmental.ocpConAR = Con.ker Autosegmental.collapseARHom

theorem Autosegmental.collapseARHom_surjective {α : Type u_1} {β : Type u_2} [DecidableEq α] : Function.Surjective ⇑collapseARHom

collapseARHom is surjective: every OCP-clean AR is its own collapse.

def Autosegmental.ocpARQuotientEquiv {α : Type u_1} {β : Type u_2} [DecidableEq α] : ocpConAR.Quotient ≃* { A : AR α β // IsCleanAR A }

First isomorphism theorem for the AR-level OCP quotient. The abstract quotient AR α β ⧸ OCP is the concrete OCP-clean model {A // IsCleanAR A} ([Jar19]'s OCP-merging realization, now carrying the association lines). Computable: an OCP-clean AR is its own collapse, the right inverse.

Equations

• Autosegmental.ocpARQuotientEquiv = Con.quotientKerEquivOfRightInverse Autosegmental.collapseARHom (fun (x : { A : Autosegmental.AR α β // Autosegmental.IsCleanAR A }) => ↑x) ⋯

The decategorification square: the OCP as a monoidal quotient

Forgetting morphisms and the lower tier, the upper-tier projection upperHom : AR α β →* FreeMonoid α (concatenation appends upper tiers) carries the AR-level OCP quotient down to the tier-level one, and the square

        (AR α β, concat)  ──collapseARHom──►  {A // IsCleanAR A}
              │                                      │
        upperHom │                                   │ upperHomClean
              ▼                                       ▼
        FreeMonoid α ──destutterHom──►  {l // IsClean l}  ≃  PresentedMonoid ⟨α | a · a = a⟩

commutes (upperHomClean_comp_collapseARHom). The bottom-right model is the monoid presented by idempotent autosegments ⟨α | a · a = a⟩ (ocpPresentation, via FreeMonoid.presentedMonoidEquiv): each autosegment is idempotent (autosegment_mul_self), which is the OCP. This is the precise sense in which the OCP is "monoidal" — a monoidal quotient, in contrast to the No-Crossing Constraint, which is a monoidal subcategory (ncc_isMonoidal); the OCP-clean objects are not closed under the monoidal product (ocp_not_isMonoidal), so no sub-object will do. The square is a MonoidHom identity in the decategorified monoid (AR α β, concat); the IsMonoidal facts live one level up, in the monoidal category (AR α β, ⊗ = coproduct).

@[simp]

theorem Autosegmental.upper_collapseAR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : (collapseAR A).upper.toList = OCP.collapse A.upper.toList

The upper tier of a collapse is the tier-level collapse of the upper tier: the engine of the decategorification square.

def Autosegmental.upperHom {α : Type u_1} {β : Type u_2} : AR α β →* FreeMonoid α

Upper-tier projection as a monoid hom AR α β →* FreeMonoid α: morpheme concatenation appends upper tiers (AR.concat_upper, LabeledTuple.toList_concat). The decategorification of an autosegmental representation to its melodic tier string.

Equations

• Autosegmental.upperHom = { toFun := fun (A : Autosegmental.AR α β) => FreeMonoid.ofList A.upper.toList, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Autosegmental.upperHom_apply {α : Type u_1} {β : Type u_2} (A : AR α β) : upperHom A = FreeMonoid.ofList A.upper.toList

def Autosegmental.upperHomClean {α : Type u_1} {β : Type u_2} [DecidableEq α] : { A : AR α β // IsCleanAR A } →* { l : List α // OCP.IsClean l }

The projection restricts to OCP-clean representations onto OCP-clean tiers: IsCleanAR is by definition cleanness of the upper tier.

Equations

• Autosegmental.upperHomClean = { toFun := fun (A : { A : Autosegmental.AR α β // Autosegmental.IsCleanAR A }) => ⟨(↑A).upper.toList, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Autosegmental.upperHomClean_comp_collapseARHom {α : Type u_1} {β : Type u_2} [DecidableEq α] : upperHomClean.comp collapseARHom = FreeMonoid.destutterHom.comp upperHom

The decategorification square commutes. Projecting to the upper tier intertwines the AR-level OCP quotient map with the tier-level one (FreeMonoid.destutterHom): collapse then project equals project then collapse.

The OCP-clean tier monoid is presented by idempotent autosegments

def Autosegmental.autosegment {α : Type u_1} (a : α) : { l : List α // OCP.IsClean l }

A single autosegment as a (trivially) OCP-clean tier.

Equations

• Autosegmental.autosegment a = ⟨[a], ⋯⟩

@[simp]

theorem Autosegmental.autosegment_mul_self {α : Type u_1} [DecidableEq α] (a : α) : autosegment a * autosegment a = autosegment a

The OCP, as a monoid equation. Fusion-gluing an autosegment to a copy of itself returns the one autosegment: each generator is idempotent, a · a = a. This is the tier-string shadow of OCP-driven fusion ([McC86]'s gemination); the multiple association it creates — one melody node linked to several timing slots — lives at the AR level (collapseARHom), which the tier-string projection discards.

def Autosegmental.ocpPresentation {α : Type u_1} [DecidableEq α] : { l : List α // OCP.IsClean l } ≃* PresentedMonoid (FreeMonoid.destutterRel α)

The OCP-clean tier monoid is the presented monoid ⟨α | a · a = a⟩ (FreeMonoid.presentedMonoidEquiv), with collapse computing its normal forms — the bottom-right corner of the decategorification square. With ocp_not_isMonoidal, this is the precise content of "the OCP is monoidal": a monoidal quotient, the counterpart to the No-Crossing Constraint's monoidal subcategory (ncc_isMonoidal).

Equations

• Autosegmental.ocpPresentation = FreeMonoid.presentedMonoidEquiv.symm

The OCP quotient does not categorify: collapse is not a reflector

collapseAR is an idempotent retraction on objects (collapseAR_idempotent, collapseAR_id_on_clean), so one might hope OCP-clean were a reflective subcategory of AR with collapseAR the reflector — the exact categorical dual of ncc_isMonoidal. It is not. An autosegmental morphism is an arbitrary label-preserving position map, so it can send a morpheme-internal geminate to two distinct like nodes of a clean target; the collapse, having already merged the geminate into one node, cannot separate them, so no universal factorization exists. The OCP quotient is therefore irreducibly decategorified: it lives on the object monoid (AR, concat), not on the category.

theorem Autosegmental.collapse_not_reflective : ∃ (A : AR Bool Unit) (B : AR Bool Unit) (g : A ⟶ B), IsCleanAR B ∧ Function.Injective g.fU.toFun ∧ (collapseAR A).upper.len < A.upper.len

collapse is not a reflector. OCP-clean is not a reflective subcategory of AR: there is a clean target B and a morphism g : A ⟶ B injective on the upper tier (it keeps a geminate apart) out of a source A whose collapse strictly merges that tier. Such a g cannot factor through the collapse — the dual of ncc_isMonoidal fails, and the OCP quotient exists only after decategorification.

J&H Theorem 5 and the tier asymmetry

[JH15] build the OCP merge into their concatenation ◦, and their Theorem 5 is that ◦ preserves the OCP. Here ◦ is gconcatAR (collapse after the bare coproduct concat), and Theorem 5 is isCleanAR_gconcatAR: OCP-clean ARs are closed under fusion-concatenation, where they are not closed under the bare coproduct (ocp_not_isMonoidal). That is the genuine sub-vs-quotient asymmetry — the NCC survives the coproduct (ncc_isMonoidal), the OCP needs the merge.

The merge acts on the upper (melody) tier only: collapseAR leaves the lower (timing) tier untouched (collapseAR_lower). So the two tier projections carry different algebra — the upper is destuttered (upper_collapseAR, the OCP quotient), the lower is free, invariant under collapse (lowerHom_collapseAR). This is [JH15]'s §7 prediction in algebraic form: the melody tier fuses, so contour tones are bounded; the timing tier does not, so spreading is unbounded.

theorem Autosegmental.isCleanAR_gconcatAR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A B : AR α β) : IsCleanAR (gconcatAR A B)

[JH15] Theorem 5. OCP-clean ARs are closed under fusion-concatenation ◦ (gconcatAR): the merge built into ◦ preserves the OCP, where the bare coproduct concat does not (ocp_not_isMonoidal). The positive half of the sub-vs-quotient dichotomy.

@[simp]

theorem Autosegmental.collapseAR_lower {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : (collapseAR A).lower = A.lower

collapseAR leaves the lower (timing) tier untouched: the merge is upper-tier only.

@[simp]

theorem Autosegmental.collapseAR_links {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : (collapseAR A).links = Finset.image (Prod.map (runIdx A.upper.toList) id) A.links

theorem Autosegmental.mem_links_collapseAR_of_upper_replicate {α : Type u_1} {β : Type u_2} [DecidableEq α] {A : AR α β} {n : ℕ} {a : α} (hA : A.upper.toList = List.replicate n a) {p : ℕ × ℕ} : p ∈ (collapseAR A).links ↔ p.1 = 0 ∧ A.IsLinkedLower p.2

OCP-merging a constant melody funnels every association line to the single surviving node: a link survives at (0, j) exactly when slot j was linked at all.

def Autosegmental.lowerHom {α : Type u_1} {β : Type u_2} : AR α β →* FreeMonoid β

Lower-tier projection as a monoid hom AR α β →* FreeMonoid β: concatenation appends lower tiers. The timing-tier decategorification, dual to upperHom.

Equations

• Autosegmental.lowerHom = { toFun := fun (A : Autosegmental.AR α β) => FreeMonoid.ofList A.lower.toList, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Autosegmental.lowerHom_apply {α : Type u_1} {β : Type u_2} (A : AR α β) : lowerHom A = FreeMonoid.ofList A.lower.toList

@[simp]

theorem Autosegmental.lowerHom_collapseAR {α : Type u_1} {β : Type u_2} [DecidableEq α] (A : AR α β) : lowerHom (collapseAR A) = lowerHom A

The timing tier is free. Unlike the melody tier — which collapse destutters (upper_collapseAR) — the lower tier is invariant under collapse: it is not quotiented. The algebraic form of the spreading/contour asymmetry ([JH15] §7).

The OCP-merging realization

def Autosegmental.realizeMerged {α : Type u_1} {β : Type u_2} [DecidableEq α] {S : Type u_3} (g₀ : S → AR α β) (w : List S) : AR α β

The OCP-merging realization ([Jar19]): realize the string via the bridge-only concat, then fuse adjacent identical upper nodes (collapseAR ∘ realize). Unlike realize, realizeMerged g₀ (Hⁿ) is a single H node multiply associated — the merge that renders unbounded tone plateauing a local AR pattern.

Equations

• Autosegmental.realizeMerged g₀ w = Autosegmental.collapseAR (Autosegmental.realize g₀ w)

@[simp]

theorem Autosegmental.realizeMerged_def {α : Type u_1} {β : Type u_2} [DecidableEq α] {S : Type u_3} (g₀ : S → AR α β) (w : List S) : realizeMerged g₀ w = collapseAR (realize g₀ w)