Optimality Theory — Core Vocabulary

OT-specific vocabulary layered on Core.Constraint.Evaluation. Provides named constraints with a faithfulness/markedness distinction, convenience constructors for building tableaux from ranked constraint lists, and factorial typology computation.

Connection to Evaluation

Core.Constraint.Evaluation provides the generic engine (LexLE, Tableau, Tableau.optimal). This module adds OT-specific structure: constraint families, named constraints, mkTableau for building tableaux from ranked constraint lists, and factorial typology computation.

inductive Core.Constraint.OT.ConstraintFamily : Type

Constraint families in OT.

• faithfulness : ConstraintFamily

  Faithfulness: penalizes deviation from the input.

• markedness : ConstraintFamily

  Markedness: penalizes marked structures in the output.

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableEqConstraintFamily : DecidableEq ConstraintFamily

Equations

• Core.Constraint.OT.instDecidableEqConstraintFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Constraint.OT.instReprConstraintFamily : Repr ConstraintFamily

Equations

• Core.Constraint.OT.instReprConstraintFamily = { reprPrec := Core.Constraint.OT.instReprConstraintFamily.repr }

def Core.Constraint.OT.instReprConstraintFamily.repr : ConstraintFamily → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Core.Constraint.OT.NamedConstraint (C : Type u_1) : Type u_1

A named OT constraint with family classification. eval c returns the number of violations candidate c incurs.

The name field is purely documentary — no evaluation function reads it. It defaults to "" so constraints can be defined without a name when the string label adds no information.

• name : String
• family : ConstraintFamily
• eval : C → ℕ

def Core.Constraint.OT.mkMark {C : Type u_1} (name : String) (P : C → Prop) [DecidablePred P] : NamedConstraint C

Build a binary markedness constraint (violated → 1, otherwise 0).

Takes a Prop-valued predicate with [DecidablePred] so that callers can use propositional equality (=) and other Prop predicates rather than Bool-valued operators (==). Decidability is required to evaluate the constraint on a candidate.

Equations

• Core.Constraint.OT.mkMark name P = { name := name, family := Core.Constraint.OT.ConstraintFamily.markedness, eval := fun (c : C) => if P c then 1 else 0 }

def Core.Constraint.OT.mkFaith {C : Type u_1} (name : String) (P : C → Prop) [DecidablePred P] : NamedConstraint C

Build a binary faithfulness constraint (violated → 1, otherwise 0).

Takes a Prop-valued predicate with [DecidablePred] so that callers can use propositional equality (=) and other Prop predicates rather than Bool-valued operators (==).

Equations

• Core.Constraint.OT.mkFaith name P = { name := name, family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := fun (c : C) => if P c then 1 else 0 }

def Core.Constraint.OT.mkMarkGrad {C : Type u_1} (name : String) (violations : C → ℕ) : NamedConstraint C

Build a gradient markedness constraint with a Nat-valued violation count.

Equations

• Core.Constraint.OT.mkMarkGrad name violations = { name := name, family := Core.Constraint.OT.ConstraintFamily.markedness, eval := violations }

def Core.Constraint.OT.mkFaithGrad {C : Type u_1} (name : String) (violations : C → ℕ) : NamedConstraint C

Build a gradient faithfulness constraint with a Nat-valued violation count.

Equations

• Core.Constraint.OT.mkFaithGrad name violations = { name := name, family := Core.Constraint.OT.ConstraintFamily.faithfulness, eval := violations }

def Core.Constraint.OT.NamedConstraint.comap {C : Type u_1} {D : Type u_2} (f : C → D) (c : NamedConstraint D) : NamedConstraint C

Pull a NamedConstraint D back along a candidate map f : C → D. The name and family are inherited; the new eval composes the original with the projection. Lets paper-specific carrier types reuse a constraint defined on a more general carrier.

Equations

• Core.Constraint.OT.NamedConstraint.comap f c = { name := c.name, family := c.family, eval := c.eval ∘ f }

@[simp]

theorem Core.Constraint.OT.NamedConstraint.comap_eval {C : Type u_1} {D : Type u_2} (f : C → D) (c : NamedConstraint D) (x : C) : (comap f c).eval x = c.eval (f x)

@[simp]

theorem Core.Constraint.OT.NamedConstraint.comap_name {C : Type u_1} {D : Type u_2} (f : C → D) (c : NamedConstraint D) : (comap f c).name = c.name

@[simp]

theorem Core.Constraint.OT.NamedConstraint.comap_family {C : Type u_1} {D : Type u_2} (f : C → D) (c : NamedConstraint D) : (comap f c).family = c.family

def Core.Constraint.OT.NamedConstraint.zeroSet {α : Type u_1} (c : NamedConstraint (List α)) : Language α

The zero-violation set of a NamedConstraint over list candidates, viewed as a Language α. Lets the OT-side eval = 0 predicate compose with mathlib's Language.IsRegular and the project's IsTierStrictlyLocal/IsBTC classifiers. The dot-notation form c.zeroSet is the canonical access pattern.

Equations

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

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

def Core.Constraint.OT.mkProfile {C : Type u_1} (ranking : List (NamedConstraint C)) (c : C) : Evaluation.ViolationProfile ranking.length

Build a ViolationProfile ranking.length from a ranked list of named constraints. This is the fixed-length analog of the profile computation inside mkTableau — use it to inspect or compare violation counts outside a tableau context.

Equations

• Core.Constraint.OT.mkProfile ranking c = Core.Constraint.Evaluation.buildViolationProfile (fun (i : Fin ranking.length) (c : C) => (ranking.get i).eval c) c

def Core.Constraint.OT.vpOfList {n : ℕ} (vs : List ℕ) (h : vs.length = n := by decide) : Evaluation.ViolationProfile n

Create a ViolationProfile n from a List Nat literal.

The length proof defaults to by decide, so study files can write readable profile comparisons without an explicit proof:

theorem t24a_profile : mkProfile ranking c = vpOfList [2, 2, 0] := by native_decide

Equations

• Core.Constraint.OT.vpOfList vs h = toLex fun (i : Fin n) => vs.get ⟨↑i, ⋯⟩

def Core.Constraint.OT.permutations {α : Type u_1} : List α → List (List α)

All permutations of a list.

Equations

• Core.Constraint.OT.permutations [] = [[]]
• Core.Constraint.OT.permutations (x_1 :: xs) = List.flatMap (Core.Constraint.OT.insertEverywhere✝ x_1) (Core.Constraint.OT.permutations xs)

theorem Core.Constraint.OT.mem_of_mem_permutations {α : Type u_1} {x : α} {l l' : List α} : l' ∈ permutations l → x ∈ l' → x ∈ l

Elements of any permutation of l are elements of l.

theorem Core.Constraint.OT.permutations_subset {α : Type u_1} {l l' : List α} (hp : l' ∈ permutations l) (x : α) : x ∈ l' → x ∈ l

A permutation of constraints has the same elements, so any con ∈ ranking for ranking ∈ permutations constraints satisfies con ∈ constraints.

def Core.Constraint.OT.mkTableau {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (NamedConstraint C)) (h : candidates ≠ [] := by decide) : Evaluation.Tableau C ranking.length

Build a Tableau C ranking.length from a candidate list and ranking.

Candidates are deduplicated via List.toFinset; profiles are fixed-length ViolationProfile n built via buildViolationProfile.

Study files use this as:

(mkTableau candidates ranking h).optimal = {.winner}

where {.winner} is a Finset literal.

Equations

• One or more equations did not get rendered due to their size.

theorem Core.Constraint.OT.mkTableau_optimal_mem {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (NamedConstraint C)) (h : candidates ≠ []) (c : C) : c ∈ (mkTableau candidates ranking h).optimal → c ∈ candidates

Candidates in mkTableau ... .optimal belong to the original list.

theorem Core.Constraint.OT.mkTableau_isOptimal_zero_first {C : Type u_1} [DecidableEq C] (candidates : List C) (con : NamedConstraint C) (rest : List (NamedConstraint C)) (h : candidates ≠ []) (hExists : ∃ c₀ ∈ candidates, con.eval c₀ = 0) (c : C) : (mkTableau candidates (con :: rest) h).IsOptimal c → con.eval c = 0

If any candidate has 0 violations on the top-ranked constraint, then every optimal candidate has 0 violations on it.

This is the structural backbone of constraint dominance: once a faithfulness constraint (like MxBM-C) is promoted to the top of the ranking, it forces all winners to satisfy it perfectly. Uses ViolationProfile.le_apply_zero to extract the first component of the lexicographic comparison.

theorem Core.Constraint.OT.mkTableau_optimal_zero_first {C : Type u_1} [DecidableEq C] (candidates : List C) (con : NamedConstraint C) (rest : List (NamedConstraint C)) (h : candidates ≠ []) (hExists : ∃ c₀ ∈ candidates, con.eval c₀ = 0) (c : C) : c ∈ (mkTableau candidates (con :: rest) h).optimal → con.eval c = 0

∈ .optimal version of mkTableau_isOptimal_zero_first.

theorem Core.Constraint.OT.ViolationProfile.zero_le {n : ℕ} (p : Evaluation.ViolationProfile n) : 0 ≤ p

The zero ViolationProfile n is the minimum: 0 ≤ p for all p. This is the structural reason that a candidate with zero violations on every constraint wins under any ranking.

Proof: 0 ≤ p iff ¬(p < 0). Under Pi.Lex, p < 0 requires ∃ i, p i < 0 i, but 0 i = 0 and Nat has no negative values.

theorem Core.Constraint.OT.mkTableau_zero_isOptimal {C : Type u_1} [DecidableEq C] (candidates : List C) (ranking : List (NamedConstraint C)) (h : candidates ≠ []) (c : C) (hc : c ∈ candidates) (hzero : ∀ con ∈ ranking, con.eval c = 0) : c ∈ (mkTableau candidates ranking h).optimal

If a candidate in mkTableau has 0 violations on every constraint, it is optimal.

theorem Core.Constraint.OT.mkTableau_zero_optimal_allRankings {C : Type u_1} [DecidableEq C] (candidates : List C) (constraints : List (NamedConstraint C)) (h : candidates ≠ []) (c : C) (hc : c ∈ candidates) (hzero : ∀ con ∈ constraints, con.eval c = 0) (ranking : List (NamedConstraint C)) : ranking ∈ permutations constraints → c ∈ (mkTableau candidates ranking h).optimal

If a candidate has 0 violations on every constraint in a set, it is optimal under every permutation of those constraints.

This is the structural backbone of adj_always_initial in Marco & Rasin (2026): the uniform-initial adjective paradigm has [0,0,0,0] on all four OP constraints, so it wins regardless of ranking. The proof reduces to mkTableau_zero_isOptimal after using permutations_subset to show that elements of a permutation are elements of the original list.

def Core.Constraint.OT.mkFactorialOptima {C : Type u_1} [DecidableEq C] (candidates : List C) (constraints : List (NamedConstraint C)) (h : candidates ≠ [] := by decide) : List (Finset C)

For each permutation of constraints, compute the set of optimal candidates as a Finset. Return the list of distinct optimal sets.

This is the core of OT factorial typology: the number of distinct optimal sets equals the number of language types predicted by the constraint set.

Equations

• One or more equations did not get rendered due to their size.

def Core.Constraint.OT.mkFactorialTypologySize {C : Type u_1} [DecidableEq C] (candidates : List C) (constraints : List (NamedConstraint C)) (h : candidates ≠ [] := by decide) : ℕ

Number of distinct language types predicted by the factorial typology. Equals |mkFactorialOptima|.

Equations

• Core.Constraint.OT.mkFactorialTypologySize candidates constraints h = (Core.Constraint.OT.mkFactorialOptima candidates constraints h).length