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))

@[instance_reducible]

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

Equations

• OCP.decidableIsClean xs = xs.instDecidableIsChainOfDecidableRel

@[instance_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.

The run-index map

def OCP.runIdx {α : Type u_3} [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

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

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

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

theorem OCP.runIdx_lt_collapse_length {α : Type u_3} [DecidableEq α] (xs : List α) {k : ℕ} (hk : k < xs.length) : runIdx xs k < (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 OCP.runIdx_replicate {α : Type u_3} [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 OCP.runIdx_append_left {α : Type u_3} [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 OCP.runIdx_clean {α : Type u_3} [DecidableEq α] {xs : List α} (hc : IsClean xs) {k : ℕ} (h : k < xs.length) : runIdx xs k = k

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

theorem OCP.collapse_take_succ_length {α : Type u_3} [DecidableEq α] {xs : List α} {m : ℕ} (hm : m < xs.length) : (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 OCP.collapse_take_head? {α : Type u_3} [DecidableEq α] {xs : List α} {m : ℕ} : (collapse (List.take (m + 1) xs)).head? = xs.head?

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

theorem OCP.runIdx_append_right {α : Type u_3} [DecidableEq α] {xs ys : List α} {a : ℕ} (ha : a < ys.length) : runIdx (xs ++ ys) (xs.length + a) = (collapse xs).length + runIdx ys a - if (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 OCP.runIdx_append_collapse_left {α : Type u_3} [DecidableEq α] {xs ys : List α} {k : ℕ} (h : k < xs.length) : runIdx (xs ++ ys) k = runIdx (collapse xs ++ collapse ys) (runIdx xs k)

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

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

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