Bridge: Forbidden-Pair Markedness ↔ TSL_2

The single generic bridge connecting Optimality-theoretic forbidden-pair markedness constraints (mkForbidPairsOnTier, defined in OptimalityTheory/Constraints.lean) to tier-based strictly 2-local languages (TSLGrammar.ofForbiddenPairs, defined in Core/Computability/Subregular/ForbiddenPairs.lean).

A candidate's mkForbidPairsOnTier score is zero iff its raw string belongs to the corresponding TSL_2 language — for any choice of forbidden-pair relation R. The OCP-specific specialization (with R := (· = ·)) lives in Subregular/OCP.lean and is now a one-line corollary.

theorem Phonology.Subregular.mkForbidPairsOnTier_zero_iff_isChain {α C : Type} (name : String) (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : (Constraints.mkForbidPairsOnTier name R (Core.Tier.byClass p) extract).eval c = 0 ↔ List.IsChain (fun (a b : α) => ¬R a b) (List.filter (fun (x : α) => decide (p x)) (extract c))

Bridge (relational form): a candidate's forbidden-pair score is zero iff its raw string projects (under Tier.byClass p) to a list with no two adjacent elements related by R. The chain-side payoff of the generic forbidden-pair design.

theorem Phonology.Subregular.mkForbidPairsOnTier_zero_iff_in_lang {α C : Type} (name : String) (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : (Constraints.mkForbidPairsOnTier name R (Core.Tier.byClass p) extract).eval c = 0 ↔ extract c ∈ (Core.Computability.Subregular.TSLGrammar.ofForbiddenPairs R p).lang

Bridge (TSL_2 language form): a candidate's forbidden-pair score is zero iff its raw string is in the language of TSLGrammar.ofForbiddenPairs R p. The single generic bridge that every adjacency-based markedness constraint inherits. Composes the relational bridge mkForbidPairsOnTier_zero_iff_isChain with the carrier-level language characterization mem_ofForbiddenPairs_lang_iff_filter_isChain.