OCP-as-Merger — the canonical normal form

@cite{goldsmith-1976} @cite{mccarthy-1981} @cite{burzio-1998} @cite{mccarthy-1995}

Two readings of the OCP coexist in the autosegmental and computational traditions:

• Prohibition (@cite{mccarthy-1986}): adjacent identical autosegments are rejected — a constraint on output well-formedness. Formalised in Linglib/Theories/Phonology/Subregular/OCP.lean as TSLGrammar.ocp p.
• Merger / repair (@cite{goldsmith-1976}, @cite{burzio-1998}'s Multiple Correspondence, @cite{mccarthy-1995}): adjacent identical autosegments are collapsed into a single multiply-linked autosegment — a transformation on representations.

This file provides the substrate operation for the merger reading at full generality — Tier.ocpCollapse over List α for any DecidableEq α — and the bridge to the prohibition reading: the canonical-form output is OCP-clean.

Why this is shared substrate

Both Phonology.Autosegmental.RegisterTier.mergeTRN (Lionnet 2022 Laal tones) and the |A|+|A| fusion of @cite{faust-lampitelli-2026} (Tigrinya/Tigre guttural synseresis) are instances of the same operation on different feature spaces. The bundle-level FeatureBundle.merge (in Featural/Bundle.lean) is an OR-of-Option building block at one level below; the OCP operation lives at the tier level and is identity-driven.

The combine argument resolves framework-specific side-information when two elements are equal under DecidableEq but carry payload (e.g. Element-Theory headedness). The default fun a _ => a is correct for strict identity (LHS preserved unchanged).

Convention: predicates as Prop

Following mathlib + the existing Phonology.Subregular.OCP style (see OCPCleanPair : Prop there), predicates in this file are Prop-valued with Decidable instances. decide recovers computability for closed instances.

The OCP-cleanness predicate is defined directly via List.Chain' (· ≠ ·) — mathlib's "no two adjacent satisfy R" predicate at R := (· ≠ ·). This pattern reuses OptimalityTheory.Correspondence's IsContiguous style (which uses List.IsChain) and slots into mathlib's chain lemmas for free.

def Phonology.Tier.ocpCollapse {α : Type u_1} [DecidableEq α] (combine : α → α → α := fun (a x : α) => a) : List α → List α

OCP-merger normal form at the tier level: collapse each maximal run of identical adjacent elements into a single element via combine. Default combine := fun a _ => a preserves the LHS, correct for strict-identity merges (Lionnet TRN OCP).

Equations

• Phonology.Tier.ocpCollapse combine [] = []
• Phonology.Tier.ocpCollapse combine (y :: rs) = Phonology.Tier.ocpCollapseAux✝ combine y rs

@[simp]

theorem Phonology.Tier.ocpCollapse_nil {α : Type u_1} [DecidableEq α] (combine : α → α → α) : ocpCollapse combine [] = []

@[simp]

theorem Phonology.Tier.ocpCollapse_singleton {α : Type u_1} [DecidableEq α] (combine : α → α → α) (x : α) : ocpCollapse combine [x] = [x]

def Phonology.Tier.IsOCPClean {α : Type u_1} [DecidableEq α] (xs : List α) : Prop

A list is OCP-clean iff no adjacent pair is identical — the universal-tier instance of the OCP. Implemented as the @cite{mccarthy-1986} prohibition condition over the entire string, via mathlib's List.IsChain predicate at R := (· ≠ ·).

Equations

• Phonology.Tier.IsOCPClean xs = List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) xs

@[implicit_reducible]

instance Phonology.Tier.instDecidableIsOCPClean {α : Type u_1} [DecidableEq α] (xs : List α) : Decidable (IsOCPClean xs)

Equations

• Phonology.Tier.instDecidableIsOCPClean xs = Phonology.Tier.instDecidableIsOCPClean._aux_1 xs

@[simp]

theorem Phonology.Tier.isOCPClean_nil {α : Type u_1} [DecidableEq α] : IsOCPClean []

@[simp]

theorem Phonology.Tier.isOCPClean_singleton {α : Type u_1} [DecidableEq α] (x : α) : IsOCPClean [x]

theorem Phonology.Tier.isOCPClean_cons_cons_iff {α : Type u_1} [DecidableEq α] (x y : α) (rs : List α) : IsOCPClean (x :: y :: rs) ↔ x ≠ y ∧ IsOCPClean (y :: rs)

theorem Phonology.Tier.ocpCollapse_head {α : Type u_1} [DecidableEq α] (combine : α → α → α) (h : ∀ (z : α), combine z z = z) (x : α) (xs : List α) : ∃ (rest : List α), ocpCollapse combine (x :: xs) = x :: rest

Under combine x x = x, ocpCollapse preserves the head.

theorem Phonology.Tier.ocpCollapse_clean {α : Type u_1} [DecidableEq α] (combine : α → α → α) (h : ∀ (z : α), combine z z = z) (xs : List α) : IsOCPClean (ocpCollapse combine xs)

OCP-cleanness of the canonical form (top-level).

theorem Phonology.Tier.ocpCollapse_idempotent_on_clean {α : Type u_1} [DecidableEq α] (combine : α → α → α) (xs : List α) (h : IsOCPClean xs) : ocpCollapse combine xs = xs

Idempotence on a clean list: ocpCollapse is the identity on OCP-clean lists.

theorem Phonology.Tier.ocpCollapse_idempotent {α : Type u_1} [DecidableEq α] (combine : α → α → α) (h : ∀ (z : α), combine z z = z) (xs : List α) : ocpCollapse combine (ocpCollapse combine xs) = ocpCollapse combine xs

Idempotence (composition form): ocpCollapse f ∘ ocpCollapse f = ocpCollapse f. Closes the OCP.lean docstring's "two readings coexist without a master bridge" gap by establishing the merger operation as a normal-form algorithm whose output is the prohibition's accepted set.