AGREE ↔ TSL_2 — the inequality instance (dual of OCP)

AGREE-style markedness in OT phonology is the non-identity dual of the OCP: tier-adjacent symbols must agree (be equal) rather than differ. As an instance of the generic forbidden-pair constructor mkForbidPairsOnTier (see ForbidPairs.lean), AGREE is the specialization with R := (· ≠ ·), just as the OCP is the R := (· = ·) specialization.

The duality is structural, not metaphorical: the OCP penalizes adjacent identical tier elements (the "no double" rule, forcing dissimilation); AGREE penalizes adjacent distinct tier elements (the "no different" rule, forcing assimilation/harmony). Consonant harmony, vowel harmony, and tone spreading factor through TSLGrammar.agree; dissimilation, anti-geminate, and Meeussen's rule factor through TSLGrammar.ocp. The generic TSLGrammar.ofForbiddenPairs subsumes both — and asymmetric patterns that are neither pure agreement nor pure dissimilation (directional harmony driven by morphological geometry, e.g. Kikongo nasal harmony in Studies/RoseWalker2004.lean) instantiate the generic constructor directly with their own asymmetric R.

Everything here is a one-line specialization of the generic forbidden-pair infrastructure to R := (· ≠ ·). The AGREE-specific names (agreeForbidden, AgreeCleanPair, TSLGrammar.agree, mkAgreeOnTier_zero_iff_in_agree_lang) are the canonical entry points downstream consumers reference.

Unlike the OCP, AGREE is also strictly piecewise: SPGrammar.agree and TSLGrammar.agree_lang_eq_sp show the tier projection is dispensable here, because equality is transitive.

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

Forbidden 2-factors for AGREE: pairs [some x, some y] of two distinct non-boundary symbols. The inequality-relation specialization of forbiddenPairs.

Equations

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

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

The TSL_2 grammar capturing "no two adjacent distinct symbols on the tier defined by p" — equivalently, every tier-adjacent pair agrees. The inequality-relation specialization of TSLGrammar.ofForbiddenPairs.

Equations

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

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

The AGREE relation on Option α: two augmented symbols are AGREE-clean as a pair iff they are not both some of distinct values. The inequality-relation specialization of CleanPair.

Equations

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

theorem Subregular.agreeCleanPair_some_some {α : Type} [DecidableEq α] (a b : α) : AgreeCleanPair (some a) (some b) ↔ a = b

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

The AGREE relation is boundary-vacuous (inequality-relation instance of CleanPair.isBoundaryVacuous).

theorem Subregular.mkAgreeOnTier_zero_iff_isChain {α : Type} [DecidableEq α] {C : Type} (p : α → Prop) [DecidablePred p] (extract : C → List α) (c : C) : Constraints.mkAgreeOnTier (TierProjection.byClass p) extract c = 0 ↔ List.IsChain (fun (a b : α) => ¬a ≠ b) (List.filter (fun (x : α) => decide (p x)) (extract c))

Bridge (relational form): a candidate's AGREE score is zero iff its raw string projects (under TierProjection.byClass p) to a list with no two adjacent distinct elements — i.e. all on-tier elements are equal. Inequality-relation specialization of mkForbidPairsOnTier_zero_iff_isChain.

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

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

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

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

AGREE is also strictly piecewise

Equality is transitive, so "every tier-adjacent pair agrees" and "every pair of on-tier symbols agrees, however far apart" are the same condition — and the latter reads subsequences, which are blind to the intervening material the tier projection deletes. AGREE languages are therefore SP_2 as well as TSL_2, the coincidence that lets transparent long-distance harmony be described either way ([McM16]). The OCP has no such reading: ≠ is not transitive.

def Subregular.SPGrammar.agree {α : Type u_1} (p : α → Prop) : SPGrammar α

The SP_2 grammar dual of TSLGrammar.agree p: permit every subsequence except a pair of disagreeing on-tier symbols. Shorter subsequences are permitted outright.

Equations

• Subregular.SPGrammar.agree p = {s : List α | ∀ (a b : α), s = [a, b] → p a → p b → a = b}

theorem Subregular.mem_agree_lang_iff_forall_sublist_pair {α : Type} [DecidableEq α] (p : α → Prop) [DecidablePred p] (w : List α) : w ∈ (TSLGrammar.agree p).lang ↔ ∀ (a b : α), [a, b].Sublist w → p a → p b → a = b

Membership in the AGREE language is agreement of all pairs of on-tier symbols, not just the tier-adjacent ones.

theorem Subregular.TSLGrammar.agree_lang_eq_sp {α : Type} [DecidableEq α] (p : α → Prop) [DecidablePred p] : (agree p).lang = SPGrammar.language 2 (SPGrammar.agree p)

AGREE-TSL_2 = AGREE-SP_2: the tier-based and subsequence-based descriptions of agreement generate the same language, for any tier predicate.

theorem Subregular.TSLGrammar.agree_lang_isStrictlyPiecewise {α : Type} [DecidableEq α] (p : α → Prop) [DecidablePred p] : (agree p).lang.IsStrictlyPiecewise 2

Every AGREE language is strictly 2-piecewise.