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/Language/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.

Main definitions

• Constraints.Constraint.zeroSet — the zero-violation language of a constraint, the Constraint → Language primitive these bridges characterize. It lives here, not in Constraints/Defs.lean, so the framework-neutral constraint vocabulary stays free of Computability.

def Constraints.Constraint.zeroSet {α : Type u_1} (c : Constraint (List α)) : Language α

The language of list candidates that satisfy c (zero violations), as a Language α. Lets the eval = 0 predicate compose with Language.IsRegular and the project's subregular classifiers (IsTierStrictlyLocal, IsBTC).

Equations

• c.zeroSet = {w : List α | c w = 0}

theorem Constraints.Constraint.mem_zeroSet {α : Type u_1} (c : Constraint (List α)) (w : List α) : w ∈ c.zeroSet ↔ c w = 0

theorem Subregular.mkForbidPairsOnTier_zero_iff_isChain {α C : Type} (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : Constraints.mkForbidPairsOnTier R (TierProjection.byClass p) extract 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 TierProjection.byClass p) to a list with no two adjacent elements related by R. The chain-side payoff of the generic forbidden-pair design.

theorem Subregular.mkForbidPairsOnTier_zero_iff_in_lang {α C : Type} (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : Constraints.mkForbidPairsOnTier R (TierProjection.byClass p) extract c = 0 ↔ extract c ∈ (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.