OT–Subregular Bridge: Bound and Counterexample

A NamedConstraint's zero-set — { w | c.eval w = 0 } — sometimes lands in a subregular class (TSL_2, SP_2, …) and sometimes does not. This file makes the bound visible:

1. Existing bridges, in zero-set form: every mkForbidPairsOnTier constraint has a TSL_2 zero-set (mkForbidPairsOnTier_zeroSet_eq). Restatement of mkForbidPairsOnTier_zero_iff_in_lang in Language α form so it composes with mathlib's Language.IsRegular.

2. Supraregular counterexample: there is a NamedConstraint (List AB) whose zero-set is the classical non-regular language { aⁿ bⁿ | n ≥ 0 } (exists_namedConstraint_zeroSet_not_isRegular). Shows the bridge cannot be stated as "every NamedConstraint has a subregular zero-set" — only constraints in specific schema classes (forbidden-pair on tier, OCP on tier, agree on tier, …) inherit the bridge.

The argument for non-regularity uses mathlib's Language.IsRegular.finite_range_leftQuotient: distinct prefixes aⁿ give distinct left quotients of { aⁿ bⁿ }, so the range of leftQuotient is infinite, contradicting regularity. This is the classical Myhill–Nerode argument @cite{nerode-1958} @cite{myhill-1957}.

Phonologically the takeaway is negative: NamedConstraints are too expressive to be classified by subregular complexity alone. Phonologists who want a subregular guarantee on their constraint set must restrict to one of the schema-specific constructors with a known bridge — mkForbidPairsOnTier, mkOCPOnTier, mkAgreeOnTier, mkForbidSingletonOnTier. The mkMarkGrad escape hatch (arbitrary violation count) admits supraregular constraints.

This file is the OT-side dual of the existing class-specific bridges in Phonology/Subregular/ForbidPairs.lean, OCP.lean, Agree.lean. The positive bridges show which constraint constructors land inside TSL_2; this file shows that the OT vocabulary is broader than the subregular hierarchy.

theorem Phonology.Subregular.OTBound.mkForbidPairsOnTier_zeroSet_eq {α : Type} (name : String) (R : α → α → Prop) [DecidableRel R] (p : α → Prop) [DecidablePred p] : (Constraints.mkForbidPairsOnTier name R (Core.Tier.byClass p) id).zeroSet = (Core.Computability.Subregular.TSLGrammar.ofForbiddenPairs R p).lang

Zero-set bridge (forbidden-pair on tier): the zero-set of a forbidden-pair markedness constraint is the language of the corresponding TSL_2 grammar. Restatement of mkForbidPairsOnTier_zero_iff_in_lang (with extract := id) in Language α form so downstream regularity arguments can use the zero-set side directly.

def Phonology.Subregular.OTBound.supraregularConstraint : Core.Constraint.OT.NamedConstraint (List AB)

The supraregular NamedConstraint: violates iff the candidate is not balanced. Built via mkMarkGrad (the escape-hatch constructor that admits arbitrary Nat-valued violation counts) — not via any of the schema constructors with a TSL_k/SP_k/BTC bridge.

Equations

• Phonology.Subregular.OTBound.supraregularConstraint = Core.Constraint.OT.mkMarkGrad "BAL" fun (w : List AB) => if IsBalanced w then 0 else 1

@[simp]

theorem Phonology.Subregular.OTBound.supraregularConstraint_eval (w : List AB) : supraregularConstraint.eval w = if IsBalanced w then 0 else 1

theorem Phonology.Subregular.OTBound.supraregularConstraint_zeroSet : supraregularConstraint.zeroSet = balancedAB

The zero-set of supraregularConstraint is exactly balancedAB — the classical non-regular { aⁿ bⁿ }.

theorem Phonology.Subregular.OTBound.exists_namedConstraint_zeroSet_not_isRegular : ∃ (c : Core.Constraint.OT.NamedConstraint (List AB)), ¬c.zeroSet.IsRegular

Headline: there exists a NamedConstraint whose zero-set is not regular. The OT→subregular bridge cannot be stated as "every NamedConstraint has a subregular zero-set" — class-specific schema restrictions are necessary. The witness is built via the mkMarkGrad escape hatch with a { aⁿ bⁿ }-membership predicate as the violation count.