OT — Elementary Ranking Conditions (Definitions + Operations)

Pure types and operations for OT's algebraic ranking-inference layer. This module defines:

• ERCVal — the three-valued alphabet {W, L, e} for Elementary Ranking Conditions
• ERC n — an ERC over n constraints (a vector of ERCVal)
• Ranking n — a constraint ranking (a permutation of Fin n)
• ercOfProfiles — the bridge from violation profiles to ERCs
• ERC.satisfiedBy, ERCSet.consistent, ERCSet.entails — the satisfaction/consistency/entailment algebra
• tableauERC — build an ERC from a winner-loser pair in a tableau
• simpleERC — single-W/single-L ERCs corresponding to Hasse edges

These types connect the evaluation side of OT (ViolationProfile, Tableau) to the inference side (ranking requirements, consistency, typology). An ERC encodes the ranking requirements that make one candidate beat another — the intermediate level between "a specific ranking with specific evaluation functions" and "a violation profile with no connection to which constraints matter."

The ranking question

Given candidates α and β with violation profiles, the ERC [α ∼ β] answers the ranking question: exactly which rankings select α over β? A ranking satisfies [α ∼ β] iff at least one W-constraint (preferring the winner α) is ranked above all L-constraints (preferring the loser β).

References

@cite{prince-2002} — Entailed ranking arguments (original ERC formulation) @cite{merchant-riggle-2016} — OT grammars, beyond partial orders: ERC sets and antimatroids

inductive Core.Constraint.OT.ERCVal : Type

The three-valued alphabet for Elementary Ranking Conditions.

• W (winner-preferring): the constraint prefers the winner
• L (loser-preferring): the constraint prefers the loser
• e (equal): the constraint does not distinguish the candidates

• W : ERCVal
• L : ERCVal
• e : ERCVal

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableEqERCVal : DecidableEq ERCVal

Equations

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

def Core.Constraint.OT.instReprERCVal.repr : ERCVal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Constraint.OT.instReprERCVal : Repr ERCVal

Equations

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

@[implicit_reducible]

instance Core.Constraint.OT.instInhabitedERCVal : Inhabited ERCVal

Equations

• Core.Constraint.OT.instInhabitedERCVal = { default := Core.Constraint.OT.instInhabitedERCVal.default }

def Core.Constraint.OT.instInhabitedERCVal.default : ERCVal

Equations

• Core.Constraint.OT.instInhabitedERCVal.default = Core.Constraint.OT.ERCVal.W

@[implicit_reducible]

instance Core.Constraint.OT.instToStringERCVal : ToString ERCVal

Equations

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

def Core.Constraint.OT.ERC (n : ℕ) : Type

An Elementary Ranking Condition over n constraints.

An ERC is a vector Fin n → ERCVal encoding the ranking requirements for one candidate to beat another. For each constraint k:

• α k = W means constraint k prefers the winner
• α k = L means constraint k prefers the loser
• α k = e means constraint k is indifferent

A ranking satisfies the ERC iff some W-constraint is ranked above all L-constraints. See ERC.satisfiedBy below.

Equations

• Core.Constraint.OT.ERC n = (Fin n → Core.Constraint.OT.ERCVal)

@[implicit_reducible]

instance Core.Constraint.OT.instInhabitedERC {n : ℕ} : Inhabited (ERC n)

Equations

• Core.Constraint.OT.instInhabitedERC = { default := fun (x : Fin n) => Core.Constraint.OT.ERCVal.e }

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableEqERC {n : ℕ} : DecidableEq (ERC n)

Equations

• Core.Constraint.OT.instDecidableEqERC = Core.Constraint.OT.instDecidableEqERC._aux_1

def Core.Constraint.OT.ERC.wSet {n : ℕ} (α : ERC n) : Set (Fin n)

The set of W-constraints in an ERC: those preferring the winner.

Equations

• α.wSet = {k : Fin n | α k = Core.Constraint.OT.ERCVal.W}

def Core.Constraint.OT.ERC.lSet {n : ℕ} (α : ERC n) : Set (Fin n)

The set of L-constraints in an ERC: those preferring the loser.

Equations

• α.lSet = {k : Fin n | α k = Core.Constraint.OT.ERCVal.L}

def Core.Constraint.OT.ERC.eSet {n : ℕ} (α : ERC n) : Set (Fin n)

The set of e-constraints in an ERC: those indifferent between candidates.

Equations

• α.eSet = {k : Fin n | α k = Core.Constraint.OT.ERCVal.e}

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableMemFinSetWSet {n : ℕ} (α : ERC n) (k : Fin n) : Decidable (k ∈ α.wSet)

Decidable membership in W/L/e sets.

Equations

• Core.Constraint.OT.instDecidableMemFinSetWSet α k = Core.Constraint.OT.instDecidableMemFinSetWSet._aux_1 α k

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableMemFinSetLSet {n : ℕ} (α : ERC n) (k : Fin n) : Decidable (k ∈ α.lSet)

Equations

• Core.Constraint.OT.instDecidableMemFinSetLSet α k = Core.Constraint.OT.instDecidableMemFinSetLSet._aux_1 α k

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableMemFinSetESet {n : ℕ} (α : ERC n) (k : Fin n) : Decidable (k ∈ α.eSet)

Equations

• Core.Constraint.OT.instDecidableMemFinSetESet α k = Core.Constraint.OT.instDecidableMemFinSetESet._aux_1 α k

def Core.Constraint.OT.ERC.isTrivial {n : ℕ} (α : ERC n) : Prop

An ERC is trivial if it has no L-constraints — every ranking satisfies it.

Equations

• α.isTrivial = ∀ (k : Fin n), α k ≠ Core.Constraint.OT.ERCVal.L

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableIsTrivial {n : ℕ} (α : ERC n) : Decidable α.isTrivial

Equations

• Core.Constraint.OT.instDecidableIsTrivial α = Fintype.decidableForallFintype

def Core.Constraint.OT.ERC.isContradictory {n : ℕ} (α : ERC n) : Prop

An ERC is contradictory if it has no W-constraints but has at least one L-constraint — no ranking can satisfy it.

Equations

• α.isContradictory = ((∀ (k : Fin n), α k ≠ Core.Constraint.OT.ERCVal.W) ∧ ∃ (k : Fin n), α k = Core.Constraint.OT.ERCVal.L)

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableIsContradictory {n : ℕ} (α : ERC n) : Decidable α.isContradictory

Equations

• Core.Constraint.OT.instDecidableIsContradictory α = Core.Constraint.OT.instDecidableIsContradictory._aux_1 α

def Core.Constraint.OT.Ranking (n : ℕ) : Type

A ranking of n constraints, represented as a permutation of Fin n.

r i is the constraint at rank position i, where position 0 is the highest-ranked (most dominant) constraint.

Equivalently, r.symm k is the rank position of constraint k — a lower value means higher rank (more dominant).

Equations

• Core.Constraint.OT.Ranking n = Equiv.Perm (Fin n)

@[implicit_reducible]

instance Core.Constraint.OT.instInhabitedRanking {n : ℕ} : Inhabited (Ranking n)

Equations

• Core.Constraint.OT.instInhabitedRanking = { default := Equiv.refl (Fin n) }

@[implicit_reducible]

instance Core.Constraint.OT.instCoeFunRankingForallFin {n : ℕ} : CoeFun (Ranking n) fun (x : Ranking n) => Fin n → Fin n

Equations

• Core.Constraint.OT.instCoeFunRankingForallFin = { coe := Equiv.toFun }

@[simp]

theorem Core.Constraint.OT.Ranking.symm_apply_apply {n : ℕ} (r : Ranking n) (i : Fin n) : (Equiv.symm r) (r.toFun i) = i

@[simp]

theorem Core.Constraint.OT.Ranking.apply_symm_apply {n : ℕ} (r : Ranking n) (i : Fin n) : r.toFun ((Equiv.symm r) i) = i

def Core.Constraint.OT.dominates {n : ℕ} (r : Ranking n) (i j : Fin n) : Prop

Constraint i dominates constraint j under ranking r: i is ranked higher (lower position number) than j.

Equations

• Core.Constraint.OT.dominates r i j = ((Equiv.symm r) i < (Equiv.symm r) j)

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableDominates {n : ℕ} (r : Ranking n) (i j : Fin n) : Decidable (dominates r i j)

Equations

• Core.Constraint.OT.instDecidableDominates r i j = Core.Constraint.OT.instDecidableDominates._aux_1 r i j

def Core.Constraint.OT.Ranking.id (n : ℕ) : Ranking n

The identity ranking: constraint 0 is highest, n-1 is lowest. This is the "default" ranking where index order equals rank order.

Equations

• Core.Constraint.OT.Ranking.id n = Equiv.refl (Fin n)

def Core.Constraint.OT.ercOfProfiles {n : ℕ} (winner loser : Evaluation.ViolationProfile n) : ERC n

Construct an ERC from two violation profiles: the winner's and the loser's. For each constraint k:

• W if the winner has strictly fewer violations (winner-preferring)
• L if the winner has strictly more violations (loser-preferring)
• e if violations are equal (indifferent)

This is the fundamental bridge between OT's evaluation layer (ViolationProfile) and its inference layer (ERC). Every call to mkTableau that selects a winner implicitly generates ERCs for all winner-loser pairs via this function.

Equations

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

theorem Core.Constraint.OT.ercOfProfiles_w {n : ℕ} (w l : Evaluation.ViolationProfile n) (k : Fin n) : ercOfProfiles w l k = ERCVal.W ↔ w k < l k

The W-set of ercOfProfiles consists of constraints where the winner has strictly fewer violations.

theorem Core.Constraint.OT.ercOfProfiles_l {n : ℕ} (w l : Evaluation.ViolationProfile n) (k : Fin n) : ercOfProfiles w l k = ERCVal.L ↔ l k < w k

The L-set of ercOfProfiles consists of constraints where the winner has strictly more violations.

theorem Core.Constraint.OT.ercOfProfiles_e {n : ℕ} (w l : Evaluation.ViolationProfile n) (k : Fin n) : ercOfProfiles w l k = ERCVal.e ↔ w k = l k

The e-set of ercOfProfiles consists of constraints where violations are equal.

def Core.Constraint.OT.ercOfList {n : ℕ} (vs : List ERCVal) (h : vs.length = n := by decide) : ERC n

Construct an ERC from a list of ERCVal, with a proof that the list has the right length. Enables readable ERC literals in study files:

def myERC : ERC 4 := ercOfList [.W, .e, .L, .e]

Equations

• Core.Constraint.OT.ercOfList vs h i = vs.get ⟨↑i, ⋯⟩

noncomputable def Core.Constraint.OT.Ranking.ofRankFn {n : ℕ} (f : Fin n → Fin n) (hbij : Function.Bijective f) : Ranking n

Construct a Ranking n from a function assigning rank positions to constraints. f k is the rank position of constraint k (0 = highest).

Requires f to be a bijection (injective + surjective on Fin n).

Equations

• Core.Constraint.OT.Ranking.ofRankFn f hbij = (Equiv.ofBijective f hbij).symm

def Core.Constraint.OT.Ranking.swap {n : ℕ} (r : Ranking n) (i j : Fin n) : Ranking n

Swap the rank positions of two constraints.

Equations

• r.swap i j = Equiv.trans r (Equiv.swap i j)

def Core.Constraint.OT.ERC.satisfiedBy {n : ℕ} (r : Ranking n) (α : ERC n) : Prop

A ranking r satisfies ERC α iff some W-constraint is ranked above all L-constraints.

In the ranking r, position 0 is highest-ranked. r i is the constraint at position i, and r.symm k is the rank position of constraint k. So r.symm w < r.symm l means constraint w is ranked above constraint l.

This is the semantic content of an ERC: it encodes a disjunction of dominance conditions. The ERC ⟨W, e, L, e⟩ says "constraint 0 must dominate constraint 2." The ERC ⟨W, W, L, e⟩ says "constraint 0 OR constraint 1 must dominate constraint 2."

Equations

• Core.Constraint.OT.ERC.satisfiedBy r α = ∀ (l : Fin n), α l = Core.Constraint.OT.ERCVal.L → ∃ (w : Fin n), α w = Core.Constraint.OT.ERCVal.W ∧ Core.Constraint.OT.dominates r w l

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableSatisfiedBy {n : ℕ} (r : Ranking n) (α : ERC n) : Decidable (ERC.satisfiedBy r α)

Equations

• Core.Constraint.OT.instDecidableSatisfiedBy r α = Fintype.decidableForallFintype

theorem Core.Constraint.OT.ERC.trivial_satisfiedBy {n : ℕ} (α : ERC n) (htriv : α.isTrivial) (r : Ranking n) : satisfiedBy r α

A trivial ERC (no L-constraints) is satisfied by every ranking.

def Core.Constraint.OT.ERCSet.satisfiedBy {n : ℕ} (r : Ranking n) (E : List (ERC n)) : Prop

A ranking satisfies a set of ERCs iff it satisfies each one.

Equations

• Core.Constraint.OT.ERCSet.satisfiedBy r E = ∀ α ∈ E, Core.Constraint.OT.ERC.satisfiedBy r α

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableSatisfiedBy_1 {n : ℕ} (r : Ranking n) (E : List (ERC n)) : Decidable (ERCSet.satisfiedBy r E)

Equations

• Core.Constraint.OT.instDecidableSatisfiedBy_1 r E = List.decidableBAll (Core.Constraint.OT.ERC.satisfiedBy r) E

def Core.Constraint.OT.ERCSet.consistent {n : ℕ} (E : List (ERC n)) : Prop

An ERC set is consistent iff there exists at least one ranking that satisfies all ERCs in the set. An inconsistent ERC set encodes contradictory ranking requirements.

This is the decidable version — it searches over all n! rankings. For large n, use the ERC fusion algorithm instead.

Equations

• Core.Constraint.OT.ERCSet.consistent E = ∃ (r : Core.Constraint.OT.Ranking n), Core.Constraint.OT.ERCSet.satisfiedBy r E

def Core.Constraint.OT.ERCSet.linearExtensions {n : ℕ} (E : List (ERC n)) : Set (Ranking n)

The set of rankings consistent with an ERC set — its linear extensions in the terminology of @cite{merchant-riggle-2016}.

Equations

• Core.Constraint.OT.ERCSet.linearExtensions E = {r : Core.Constraint.OT.Ranking n | Core.Constraint.OT.ERCSet.satisfiedBy r E}

def Core.Constraint.OT.ERCSet.entails {n : ℕ} (E E' : List (ERC n)) : Prop

ERC set E entails ERC set E' iff every ranking satisfying E also satisfies E'. Equivalently, the linear extensions of E are a subset of the linear extensions of E'.

This is the natural preorder on ERC sets. Two ERC sets are equivalent iff they entail each other — they have the same linear extensions and describe the same OT grammar.

Equations

• Core.Constraint.OT.ERCSet.entails E E' = ∀ (r : Core.Constraint.OT.Ranking n), Core.Constraint.OT.ERCSet.satisfiedBy r E → Core.Constraint.OT.ERCSet.satisfiedBy r E'

theorem Core.Constraint.OT.ERCSet.entails_refl {n : ℕ} (E : List (ERC n)) : entails E E

Entailment is reflexive.

theorem Core.Constraint.OT.ERCSet.entails_trans {n : ℕ} (E₁ E₂ E₃ : List (ERC n)) (h₁₂ : entails E₁ E₂) (h₂₃ : entails E₂ E₃) : entails E₁ E₃

Entailment is transitive.

theorem Core.Constraint.OT.ERCSet.entails_of_cons {n : ℕ} (α : ERC n) (E : List (ERC n)) : entails (α :: E) E

Adding an ERC to a set weakens the entailment (more requirements = fewer satisfying rankings = stronger set).

theorem Core.Constraint.OT.ERCSet.entails_of_forall_mem {n : ℕ} (E E' : List (ERC n)) (h : ∀ α ∈ E', entails E [α]) : entails E E'

If every ERC in E' is already entailed by E, then E entails E'. This is the pointwise characterization.

def Core.Constraint.OT.tableauERC {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Evaluation.Tableau C n) (w l : C) : ERC n

Build an ERC from a winner-loser pair in a tableau.

Given a tableau t with candidates and violation profiles, and a designated winner w and loser l, construct the ERC that encodes the ranking requirements for w to beat l.

This is the fundamental bridge from OT evaluation to OT inference: every time a tableau selects a winner, it implicitly generates ERCs for all winner-loser pairs.

Equations

• Core.Constraint.OT.tableauERC t w l = Core.Constraint.OT.ercOfProfiles (t.profile w) (t.profile l)

def Core.Constraint.OT.ERC.isSimple {n : ℕ} (α : ERC n) : Prop

A simple ERC has exactly one W and one L — it encodes a single dominance requirement w ≫ l (constraint w must dominate constraint l).

Simple ERCs correspond to edges in the Hasse diagram of the ranking partial order. Sets of simple ERCs describe exactly the rankings representable as partial orders (@cite{merchant-riggle-2016} §1.1).

Equations

• α.isSimple = ((∃! w : Fin n, α w = Core.Constraint.OT.ERCVal.W) ∧ ∃! l : Fin n, α l = Core.Constraint.OT.ERCVal.L)

def Core.Constraint.OT.simpleERC {n : ℕ} (i j : Fin n) : ERC n

Construct a simple ERC asserting that constraint i must dominate constraint j. All other constraints are e.

Equations

• Core.Constraint.OT.simpleERC i j k = if k = i then Core.Constraint.OT.ERCVal.W else if k = j then Core.Constraint.OT.ERCVal.L else Core.Constraint.OT.ERCVal.e

@[simp]

theorem Core.Constraint.OT.simpleERC_apply_W {n : ℕ} {i j : Fin n} : simpleERC i j i = ERCVal.W

The W-position of a simple ERC.

@[simp]

theorem Core.Constraint.OT.simpleERC_apply_L {n : ℕ} {i j : Fin n} (hij : i ≠ j) : simpleERC i j j = ERCVal.L

The L-position of a simple ERC.

theorem Core.Constraint.OT.simpleERC_satisfiedBy_iff {n : ℕ} {i j : Fin n} (hij : i ≠ j) (r : Ranking n) : ERC.satisfiedBy r (simpleERC i j) ↔ dominates r i j

A simple ERC i ≫ j is satisfied by ranking r iff i dominates j under r.

theorem Core.Constraint.OT.simpleERC_consistent {n : ℕ} {i j : Fin n} (hij : i ≠ j) : ERCSet.consistent [simpleERC i j]

A simple ERC i ≫ j (with i ≠ j) is consistent: any ranking that places i strictly above j is a witness; the identity ranking works whenever the index order already has i < j, and a swap suffices otherwise. We pick a witness by transposing (i, j) if needed so that the resulting permutation puts i at a position less than j's.