The Obligatory Contour Principle

The categorical, strict-identity, single-tier OCP: the ban on two identical adjacent autosegments on one tier ([Leb73], [McC86]), on a projected tier for IsCleanOn ([CJ19]). As a stringset the constraint is tier-based strictly local (TSL₂, [HRT11]), characterised in OCP. The fusion repair collapse is mathlib's List.destutter (· ≠ ·) ([Gol76], [McCP95]) — a retraction onto cleanness, input-strictly-local ([CH18]); the blocking repair block is antigemination, a guard rather than a retraction ([McC86]).

Gradient, similarity-scaled OCP ([FPB04]) is a different object and lives in the thresholded-TSL substrate, not here.

Main definitions

• OCP.IsClean / OCP.IsCleanOn — OCP-cleanness, flat and on a projected tier.
• OCP.collapse — the fusion repair (OCP-merger normal form).
• OCP.block — the blocking repair (antigemination guard).

Main results

• collapse_eq_destutter — the fusion repair is List.destutter.
• collapse_clean / collapse_eq_self_iff — collapse is the retraction onto IsClean.
• collapse_sublist — fusion never adds material.
• collapse_append — collapse is the OCP congruence: collapsing each operand before ++ is harmless, so collapse descends to the OCP quotient of (List α, ++) (the quotient monoid and its presentation ⟨α | a · a = a⟩ live on the Core.Algebra.FreeMonoid.Destutter substrate; the autosegmental reading is in Autosegmental.Collapse).
• block_eq_self — antigemination: a rule is blocked when it would violate the OCP.

The constraint

@[reducible, inline]

abbrev OCP.IsClean {α : Type u_1} (xs : List α) : Prop

A tier is OCP-clean when no adjacent pair is identical. Adjacency-only, so weaker than List.Nodup ([1, 2, 1] is clean). A reducible alias of the substrate predicate List.IsChain (· ≠ ·), so the substrate's Monoid {l // l.IsChain (· ≠ ·)} applies to OCP-clean tiers downstream.

Equations

• OCP.IsClean xs = List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) xs

@[simp]

theorem OCP.isClean_nil {α : Type u_1} : IsClean []

@[simp]

theorem OCP.isClean_singleton {α : Type u_1} (x : α) : IsClean [x]

@[simp]

theorem OCP.isClean_cons_cons_iff {α : Type u_1} (x y : α) (rs : List α) : IsClean (x :: y :: rs) ↔ x ≠ y ∧ IsClean (y :: rs)

def OCP.IsCleanOn {α : Type u_1} {β : Type u_2} (p : α → Prop) [DecidablePred p] (proj : α → β) (xs : List α) : Prop

OCP on the tier projected from xs by keeping p-elements and reading proj (tier-relativity, [CJ19]); flat IsClean is the p = ⊤, proj = id case.

Equations

• OCP.IsCleanOn p proj xs = OCP.IsClean (List.map proj (List.filter (fun (a : α) => decide (p a)) xs))

@[implicit_reducible]

instance OCP.decidableIsClean {α : Type u_1} [DecidableEq α] : DecidablePred IsClean

Equations

• OCP.decidableIsClean xs = xs.instDecidableIsChainOfDecidableRel

@[implicit_reducible]

instance OCP.decidableIsCleanOn {α : Type u_1} {β : Type u_2} [DecidableEq β] (p : α → Prop) [DecidablePred p] (proj : α → β) : DecidablePred (IsCleanOn p proj)

Equations

• OCP.decidableIsCleanOn p proj x✝ = OCP.decidableIsCleanOn._aux_1 p proj x✝

The fusion repair

def OCP.collapse {α : Type u_1} [DecidableEq α] (xs : List α) : List α

OCP-merger normal form (the fusion repair): collapse each maximal run of identical adjacent elements into one. Fusing identical autosegments returns that same autosegment, so the payload is unchanged.

Equations

• OCP.collapse xs = List.destutter (fun (x1 x2 : α) => x1 ≠ x2) xs

theorem OCP.collapse_eq_destutter {α : Type u_1} [DecidableEq α] (xs : List α) : collapse xs = List.destutter (fun (x1 x2 : α) => x1 ≠ x2) xs

@[simp]

theorem OCP.collapse_nil {α : Type u_1} [DecidableEq α] : collapse [] = []

@[simp]

theorem OCP.collapse_singleton {α : Type u_1} [DecidableEq α] (x : α) : collapse [x] = [x]

@[simp]

theorem OCP.collapse_replicate {α : Type u_1} [DecidableEq α] (n : ℕ) (a : α) : collapse (List.replicate (n + 1) a) = [a]

collapse fuses a constant run into its single autosegment.

theorem OCP.collapse_clean {α : Type u_1} [DecidableEq α] (xs : List α) : IsClean (collapse xs)

collapse lands in the OCP-clean set.

theorem OCP.collapse_idempotent_on_clean {α : Type u_1} [DecidableEq α] {xs : List α} (h : IsClean xs) : collapse xs = xs

collapse fixes OCP-clean lists.

@[simp]

theorem OCP.collapse_eq_self_iff {α : Type u_1} [DecidableEq α] (xs : List α) : collapse xs = xs ↔ IsClean xs

collapse fixes a tier iff it is OCP-clean; with collapse_clean, the retraction onto IsClean.

theorem OCP.collapse_idempotent {α : Type u_1} [DecidableEq α] (xs : List α) : collapse (collapse xs) = collapse xs

The fusion repair is a retraction onto the OCP-clean set.

Normal-form lemmas

@[simp]

theorem OCP.collapse_eq_nil {α : Type u_1} [DecidableEq α] {xs : List α} : collapse xs = [] ↔ xs = []

theorem OCP.collapse_sublist {α : Type u_1} [DecidableEq α] (xs : List α) : (collapse xs).Sublist xs

Fusion never adds material: the repair output is a sublist of the input.

theorem OCP.collapse_length_le {α : Type u_1} [DecidableEq α] (xs : List α) : (collapse xs).length ≤ xs.length

theorem OCP.mem_collapse {α : Type u_1} [DecidableEq α] {a : α} {xs : List α} (ha : a ∈ collapse xs) : a ∈ xs

The OCP congruence: collapse as a quotient homomorphism

collapse descends to a homomorphism on the OCP quotient of (List α, ++): collapsing each operand before appending is harmless. This is what makes the OCP-clean tiers under fusion-concatenation (List.destutterConcat) the quotient (List α, ++)/OCP — bundled on the Core.Algebra.FreeMonoid.Destutter substrate as FreeMonoid.destutterHom.

theorem OCP.collapse_append_left {α : Type u_1} [DecidableEq α] (x y : List α) : collapse (collapse x ++ y) = collapse (x ++ y)

Collapsing the left operand before appending does not change the result.

theorem OCP.collapse_append_right {α : Type u_1} [DecidableEq α] (x y : List α) : collapse (x ++ collapse y) = collapse (x ++ y)

Collapsing the right operand before appending does not change the result.

theorem OCP.collapse_append {α : Type u_1} [DecidableEq α] (x y : List α) : collapse (x ++ y) = collapse (collapse x ++ collapse y)

The OCP congruence. collapse is a ++→quotient homomorphism: collapsing each operand first is harmless. Thus collapse descends to the OCP quotient of (List α, ++).

The blocking repair

The substrate provides the OCP quotient monoid (OCP-clean tiers under fusion-concatenation, List.destutterConcat) and its identification with the monoid presented by idempotent autosegments ⟨α | a · a = a⟩ (Core.Algebra.FreeMonoid.Destutter). The autosegmental reading of that quotient — the decategorification square against the categorical representation, contrasting the OCP (a monoidal quotient) with the No-Crossing Constraint (a monoidal subcategory) — lives downstream in Autosegmental.Collapse, which can see both Autosegmental.ncc_isMonoidal and Autosegmental.ocp_not_isMonoidal.

def OCP.block {α : Type u_1} [DecidableEq α] (rule : List α → List α) (xs : List α) : List α

Blocking ([McC86]'s antigemination): apply rule only when it would not create an OCP violation, else leave the input untouched — a guard preventing a process, not a retraction repairing its output.

Equations

• OCP.block rule xs = if OCP.IsClean (rule xs) then rule xs else xs

theorem OCP.block_eq_rule {α : Type u_1} [DecidableEq α] (rule : List α → List α) {xs : List α} (hc : IsClean (rule xs)) : block rule xs = rule xs

theorem OCP.block_eq_self {α : Type u_1} [DecidableEq α] (rule : List α → List α) {xs : List α} (hc : ¬IsClean (rule xs)) : block rule xs = xs

Antigemination: the rule fails to apply exactly when it would create an OCP violation, leaving the input unrepaired (contrast collapse).

theorem OCP.block_isClean {α : Type u_1} [DecidableEq α] (rule : List α → List α) {xs : List α} (hx : IsClean xs) : IsClean (block rule xs)

Blocking never worsens a clean tier.