OCP (Obligatory Contour Principle) ↔ TSL_2 — the identity instance

The OCP [Gol76] [McC86] is the identity-relation instance of the generic forbidden-pair markedness constructor mkForbidPairsOnTier (see ForbidPairs.lean): the forbidden 2-factor is [some x, some x], and the corresponding TSL_2 grammar is TSLGrammar.ofForbiddenPairs (· = ·) p.

Mathematically, the unprojected (single-tier, full-alphabet) case is the linguistic instance of the classical theory of square-free words [Thu06]: a word is OCP-clean iff it contains no factor x x. Thue's construction shows infinite square-free words exist over a 3-letter alphabet, while every binary string of length ≥ 4 contains a square — i.e. binary tonal alphabets cannot satisfy a strict OCP at length, which is itself a phonological prediction.

Everything in this file is a one-line specialization of the generic forbidden-pair infrastructure to R := (· = ·). The OCP-specific names (ocpForbidden, OCPCleanPair, TSLGrammar.ocp, mkOCPOnTier_zero_iff_in_ocp_lang) are kept as the canonical entry points downstream consumers reference.

The subregular face of the OCP

This file is the subregular characterization of the OCP — one face of the unified OCP principle. It proves that the prohibition reading (a stringset rejecting adjacent identical tier-projected autosegments) is a TSL₂ language, and that its satisfaction predicate is exactly OCP.IsClean (mkOCPOnTier_zero_iff_isClean). The dual fusion repair OCP.collapse lands in the same IsClean set, and is itself a 2-Input-Strictly-Local map (collapse_isISL) — so prohibition and merger are not two coexisting formalisations but the constraint and a retraction onto it, both characterising OCP.IsClean, both subregular.

def Subregular.ocpForbidden (α : Type) [DecidableEq α] : Set (Augmented α)

Forbidden 2-factors for the OCP: pairs [some x, some x] of two identical non-boundary symbols. The identity-relation specialization of forbiddenPairs.

Equations

• Subregular.ocpForbidden α = Subregular.forbiddenPairs fun (x1 x2 : α) => x1 = x2

def Subregular.TSLGrammar.ocp {α : Type} [DecidableEq α] (p : α → Prop) [DecidablePred p] : TSLGrammar 2 α

The TSL_2 grammar capturing "no two adjacent identical symbols on the tier defined by p". The identity-relation specialization of TSLGrammar.ofForbiddenPairs.

Equations

• Subregular.TSLGrammar.ocp p = Subregular.TSLGrammar.ofForbiddenPairs (fun (x1 x2 : α) => x1 = x2) p

def Subregular.OCPCleanPair {α : Type} [DecidableEq α] : Option α → Option α → Prop

The OCP relation on Option α: two augmented symbols are OCP-clean as a pair iff they are not both some of the same value. The identity-relation specialization of CleanPair.

Equations

• Subregular.OCPCleanPair = Subregular.CleanPair fun (x1 x2 : α) => x1 = x2

theorem Subregular.ocpCleanPair_some_some {α : Type} [DecidableEq α] (a b : α) : OCPCleanPair (some a) (some b) ↔ a ≠ b

theorem Subregular.OCPCleanPair.isBoundaryVacuous {α : Type} [DecidableEq α] : IsBoundaryVacuous OCPCleanPair

The OCP relation is boundary-vacuous (identity-relation instance of CleanPair.isBoundaryVacuous).

theorem Subregular.mkOCPOnTier_zero_iff_isChain {α : Type} [DecidableEq α] {C : Type} (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : Constraints.mkOCPOnTier (TierProjection.byClass p) extract c = 0 ↔ List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) (List.filter (fun (x : α) => decide (p x)) (extract c))

Bridge (relational form): a candidate's OCP score is zero iff its raw string projects (under TierProjection.byClass p) to a list with no two adjacent identical elements. Identity-relation specialization of mkForbidPairsOnTier_zero_iff_isChain.

theorem Subregular.mkOCPOnTier_zero_iff_isClean {α : Type} [DecidableEq α] {C : Type} (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : Constraints.mkOCPOnTier (TierProjection.byClass p) extract c = 0 ↔ OCP.IsClean (List.filter (fun (x : α) => decide (p x)) (extract c))

Shared satisfaction predicate: a candidate's OCP score is zero iff its tier-projection is OCP.IsClean. This is what makes the prohibition reading (here) and the fusion repair (OCP.collapse) two faces of one principle rather than parallel formalisations — both characterise OCP.IsClean.

theorem Subregular.mkOCP_zero_iff_isClean {α C : Type} [DecidableEq α] (project : C → List α) (c : C) : Constraints.mkOCP project c = 0 ↔ OCP.IsClean (project c)

Shared satisfaction predicate (off-tier): the optimality-theoretic OCP markedness constraint mkOCP scores zero iff its projection is OCP.IsClean — routing OptimalityTheory.adjacentIdentical (the countAdjacent form behind mkOCP, consumed by Berent2026/Belth2026) through the unified predicate. The flat-string companion of mkOCPOnTier_zero_iff_isClean.

theorem Subregular.mkOCPOnTier_zero_iff_in_ocp_lang {α : Type} [DecidableEq α] {C : Type} (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : Constraints.mkOCPOnTier (TierProjection.byClass p) extract c = 0 ↔ extract c ∈ (TSLGrammar.ocp p).lang

Bridge (full TSL_2 language form): a candidate's OCP score is zero iff its raw string is in the language of the TSL_2 grammar TSLGrammar.ocp p. The two perspectives on the OCP — optimality-theoretic constraint and subregular-complexity class — are co-extensive. Identity-relation specialization of mkForbidPairsOnTier_zero_iff_in_lang.

theorem Subregular.mkOCPOnTier_zeroSet_eq {α : Type} [DecidableEq α] (p : α → Prop) [DecidablePred p] : (Constraints.mkOCPOnTier (TierProjection.byClass p) id).zeroSet = (TSLGrammar.ocp p).lang

Zero-set bridge (OCP on tier): the Language α-form restatement of mkOCPOnTier_zero_iff_in_ocp_lang (with extract := id). The OCP markedness constraint's zero-set is the corresponding OCP-TSL_2 language. Sibling of mkForbidPairsOnTier_zeroSet_eq in OTBound.lean.

The repair is subregular

theorem Subregular.collapse_isISL {α : Type} [DecidableEq α] : IsLeftInputStrictlyLocal 2 OCP.collapse

The OCP fusion repair OCP.collapse is a 2-Input-Strictly-Local string function ([CH18]): scanning left-to-right with a one-symbol window, delete a symbol iff it equals its predecessor. This completes the subregular repair face (the constraint side is the TSL₂ result above); cf. the autosegmental A-ISL classification of tonal OCP processes in [CJ19].