Elementary ranking conditions

OT's algebraic ranking-inference layer ([Pri02]; [Rig09a]). An ERC value is a sign, so the alphabet is mathlib's SignType — W (+1, winner-preferring), L (-1, loser-preferring), e (0, neutral) — which buys ercOfProfiles as a coordinatewise SignType.sign, the antithetical ERC as pointwise negation, per-coordinate entailment as SignType's own order L ≤ e ≤ W, and the decidability instances for free.

A ranking satisfies an ERC iff its sign vector, read in the ranking's priority order, is lex-nonnegative — equivalently (ERC.satisfiedBy_iff_dominance), every L-constraint is outranked by some W-constraint ([Pri02] §0 (3)/(4)).

Main declarations

• ERCVal, ERC n — the sign alphabet and sign vectors Fin n → ERCVal.
• ERC.SatisfiedBy, ERCSet.Consistent, ERCSet.Entails — the satisfaction/consistency/entailment algebra; ERCSet.linearExtensions the satisfying rankings as a Finset.
• ercOfProfiles, tableauERC — ERCs from violation profiles and winner–loser pairs; satisfiedBy_ercOfProfiles_iff_le bridges to the Core lex order.
• simpleERC — a single-W/single-L ERC, one Hasse edge i ≫ j ([MR16]).

The three-valued alphabet ERCVal

@[reducible, inline]

abbrev OptimalityTheory.ERCVal : Type

An ERC value is a sign ([Pri02] §0): W (winner-preferring), L (loser-preferring), e (neutral). This is mathlib's SignType — see ERCVal.W, ERCVal.L, ERCVal.e.

Equations

• OptimalityTheory.ERCVal = SignType

@[reducible, match_pattern, inline]

abbrev OptimalityTheory.ERCVal.W : ERCVal

Winner-preferring value (+1).

Equations

• OptimalityTheory.ERCVal.W = SignType.pos

@[reducible, match_pattern, inline]

abbrev OptimalityTheory.ERCVal.L : ERCVal

Loser-preferring value (-1).

Equations

• OptimalityTheory.ERCVal.L = SignType.neg

@[reducible, match_pattern, inline]

abbrev OptimalityTheory.ERCVal.e : ERCVal

Neutral / indifferent value (0).

Equations

• OptimalityTheory.ERCVal.e = SignType.zero

Elementary ranking conditions

@[reducible, inline]

abbrev OptimalityTheory.ERC (n : ℕ) : Type

An elementary ranking condition over n constraints: a sign vector Fin n → ERCVal ([Pri02] §0).

Equations

• OptimalityTheory.ERC n = (Fin n → OptimalityTheory.ERCVal)

def OptimalityTheory.ERC.IsTrivial {n : ℕ} (α : ERC n) : Prop

An ERC is trivial if it has no L-constraint, so every ranking satisfies it.

Equations

• α.IsTrivial = ∀ (k : Fin n), α k ≠ OptimalityTheory.ERCVal.L

@[implicit_reducible]

instance OptimalityTheory.ERC.instDecidableIsTrivial {n : ℕ} (α : ERC n) : Decidable α.IsTrivial

Equations

• α.instDecidableIsTrivial = Fintype.decidableForallFintype

def OptimalityTheory.ERC.IsContradictory {n : ℕ} (α : ERC n) : Prop

An ERC is contradictory if it has an L-constraint but no W-constraint, so no ranking satisfies it — Prince's class 𝓛⁺.

Equations

• α.IsContradictory = ((∀ (k : Fin n), α k ≠ OptimalityTheory.ERCVal.W) ∧ ∃ (k : Fin n), α k = OptimalityTheory.ERCVal.L)

@[implicit_reducible]

instance OptimalityTheory.ERC.instDecidableIsContradictory {n : ℕ} (α : ERC n) : Decidable α.IsContradictory

Equations

• α.instDecidableIsContradictory = OptimalityTheory.ERC.instDecidableIsContradictory._aux_1 α

def OptimalityTheory.ERC.IsSimple {n : ℕ} (α : ERC n) : Prop

A simple ERC has exactly one W and one L.

Equations

• α.IsSimple = ((∃! w : Fin n, α w = OptimalityTheory.ERCVal.W) ∧ ∃! l : Fin n, α l = OptimalityTheory.ERCVal.L)

ERC satisfaction

def OptimalityTheory.ERC.SatisfiedBy {n : ℕ} (r : Ranking n) (α : ERC n) : Prop

A ranking r satisfies ERC α iff its sign vector, read in r's priority order, is lexicographically nonnegative.

Equations

• OptimalityTheory.ERC.SatisfiedBy r α = (toLex 0 ≤ r • toLex α)

theorem OptimalityTheory.ERC.lex_nonneg_iff_dominance {n : ℕ} (v : Fin n → ERCVal) : toLex 0 ≤ toLex v ↔ ∀ (p : Fin n), v p = ERCVal.L → ∃ q < p, v q = ERCVal.W

Position-space dominance, ranking-free: a sign vector is lex-nonnegative iff every L is preceded by a W.

theorem OptimalityTheory.ERC.satisfiedBy_iff_lead {n : ℕ} (r : Ranking n) (α : ERC n) : SatisfiedBy r α ↔ ∀ (he : ∃ (p : Fin n), α (r p) ≠ ERCVal.e), α (r (Fin.find (fun (k : Fin n) => α (r k) ≠ ERCVal.e) he)) = ERCVal.W

Prince's leading-entry characterization ([Pri02] §0): a ranking satisfies an ERC iff the r-earliest non-neutral constraint, when one exists, is winner-preferring.

theorem OptimalityTheory.ERC.satisfiedBy_iff_dominance {n : ℕ} (r : Ranking n) (α : ERC n) : SatisfiedBy r α ↔ ∀ (c : Fin n), α c = ERCVal.L → ∃ (w : Fin n), α w = ERCVal.W ∧ r.Dominates w c

[Pri02] §0 (3): satisfaction unfolds to the ∀∃ dominance form — every loser-preferring constraint is dominated by some winner-preferring one. Position-space dominance (lex_nonneg_iff_dominance), coordinates changed along r.

@[implicit_reducible]

instance OptimalityTheory.ERC.instDecidableSatisfiedBy {n : ℕ} (r : Ranking n) (α : ERC n) : Decidable (SatisfiedBy r α)

Equations

• OptimalityTheory.ERC.instDecidableSatisfiedBy r α = decidable_of_iff (∀ (c : Fin n), α c = OptimalityTheory.ERCVal.L → ∃ (w : Fin n), α w = OptimalityTheory.ERCVal.W ∧ r.Dominates w c) ⋯

theorem OptimalityTheory.ERC.satisfiedBy_iff_exists_dominant {n : ℕ} (r : Ranking n) (α : ERC n) [NeZero n] : SatisfiedBy r α ↔ ∃ (d : Fin n), ∀ (c : Fin n), α c = ERCVal.L → α d = ERCVal.W ∧ r.Dominates d c

[Pri02] §0 (4): the ∀∃ form is equivalent to the ∃∀ form — some W-constraint dominates every L-constraint — because the ranking is total: the leading constraint is the single witness.

theorem OptimalityTheory.ERC.trivial_satisfiedBy {n : ℕ} {α : ERC n} (htriv : α.IsTrivial) (r : Ranking n) : SatisfiedBy r α

A trivial ERC is satisfied by every ranking.

Sets of ERCs

@[reducible, inline]

abbrev OptimalityTheory.ERCSet (n : ℕ) : Type

A set of ERCs, carrying the satisfaction/consistency/entailment algebra of OT grammars. Represented as a List so that decide can search the finitely many rankings; entailment is invariant under reordering and duplication.

Equations

• OptimalityTheory.ERCSet n = List (OptimalityTheory.ERC n)

def OptimalityTheory.ERCSet.SatisfiedBy {n : ℕ} (r : Ranking n) (E : ERCSet n) : Prop

A ranking satisfies an ERC set iff it satisfies every member.

Equations

• OptimalityTheory.ERCSet.SatisfiedBy r E = ∀ α ∈ E, OptimalityTheory.ERC.SatisfiedBy r α

@[implicit_reducible]

instance OptimalityTheory.ERCSet.instDecidableSatisfiedBy {n : ℕ} (r : Ranking n) (E : ERCSet n) : Decidable (SatisfiedBy r E)

Equations

• OptimalityTheory.ERCSet.instDecidableSatisfiedBy r E = List.decidableBAll (OptimalityTheory.ERC.SatisfiedBy r) E

def OptimalityTheory.ERCSet.Consistent {n : ℕ} (E : ERCSet n) : Prop

An ERC set is consistent iff some ranking satisfies all its members.

Equations

• E.Consistent = ∃ (r : OptimalityTheory.Ranking n), OptimalityTheory.ERCSet.SatisfiedBy r E

@[implicit_reducible]

instance OptimalityTheory.ERCSet.instDecidableConsistent {n : ℕ} (E : ERCSet n) : Decidable E.Consistent

Equations

• E.instDecidableConsistent = Fintype.decidableExistsFintype

@[simp]

theorem OptimalityTheory.ERCSet.consistent_singleton {n : ℕ} {α : ERC n} : Consistent [α] ↔ ∃ (r : Ranking n), ERC.SatisfiedBy r α

A singleton is consistent iff some ranking satisfies its ERC.

def OptimalityTheory.ERCSet.linearExtensions {n : ℕ} (E : ERCSet n) : Finset (Ranking n)

The rankings consistent with an ERC set, as a Finset — its linear extensions ([MR16]).

Equations

• E.linearExtensions = {r : OptimalityTheory.Ranking n | OptimalityTheory.ERCSet.SatisfiedBy r E}

@[simp]

theorem OptimalityTheory.ERCSet.mem_linearExtensions {n : ℕ} {E : ERCSet n} {r : Ranking n} : r ∈ E.linearExtensions ↔ SatisfiedBy r E

Entailment

def OptimalityTheory.ERCSet.Entails {n : ℕ} (E E' : ERCSet n) : Prop

E entails E' iff every ranking satisfying E also satisfies E'.

Equations

• E.Entails E' = ∀ (r : OptimalityTheory.Ranking n), OptimalityTheory.ERCSet.SatisfiedBy r E → OptimalityTheory.ERCSet.SatisfiedBy r E'

theorem OptimalityTheory.ERCSet.entails_refl {n : ℕ} (E : ERCSet n) : E.Entails E

theorem OptimalityTheory.ERCSet.entails_trans {n : ℕ} {E₁ E₂ E₃ : ERCSet n} (h₁₂ : E₁.Entails E₂) (h₂₃ : E₂.Entails E₃) : E₁.Entails E₃

theorem OptimalityTheory.ERCSet.entails_of_cons {n : ℕ} (E : ERCSet n) (α : ERC n) : Entails (α :: E) E

Adding an ERC strengthens the set: α :: E entails E.

theorem OptimalityTheory.ERCSet.entails_of_forall_mem {n : ℕ} {E E' : ERCSet n} (h : ∀ α ∈ E', E.Entails [α]) : E.Entails E'

Pointwise characterization: E entails E' if it entails each member singleton.

def OptimalityTheory.ERCSet.IsSimpleSet {n : ℕ} (E : ERCSet n) : Prop

An ERC set is simple if every member is a simple ERC — a set of Hasse edges ([MR16]).

Equations

• E.IsSimpleSet = ∀ α ∈ E, α.IsSimple

Simple ERCs

def OptimalityTheory.simpleERC {n : ℕ} (i j : Fin n) : ERC n

The simple ERC asserting constraint i must dominate constraint j; all other constraints are e.

Equations

• OptimalityTheory.simpleERC i j k = if k = i then OptimalityTheory.ERCVal.W else if k = j then OptimalityTheory.ERCVal.L else OptimalityTheory.ERCVal.e

theorem OptimalityTheory.simpleERC_eq_W_iff {n : ℕ} {i j : Fin n} (k : Fin n) : simpleERC i j k = ERCVal.W ↔ k = i

The only W of simpleERC i j is at i.

theorem OptimalityTheory.simpleERC_eq_L_iff {n : ℕ} {i j : Fin n} (hij : i ≠ j) (k : Fin n) : simpleERC i j k = ERCVal.L ↔ k = j

The only L of simpleERC i j (with i ≠ j) is at j.

@[simp]

theorem OptimalityTheory.simpleERC_apply_W {n : ℕ} {i j : Fin n} : simpleERC i j i = ERCVal.W

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

theorem OptimalityTheory.simpleERC_satisfiedBy_iff {n : ℕ} {i j : Fin n} (hij : i ≠ j) (r : Ranking n) : ERC.SatisfiedBy r (simpleERC i j) ↔ r.Dominates i j

A simple ERC i ≫ j (with i ≠ j) is satisfied by r iff i dominates j under r.

theorem OptimalityTheory.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.

theorem OptimalityTheory.simpleERC_isSimple {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (simpleERC i j).IsSimple

simpleERC i j (with i ≠ j) is a simple ERC.

Bridges: profiles, tableaux, and the Core lex order

def OptimalityTheory.ercOfProfiles {n : ℕ} (winner loser : Constraints.ViolationProfile n) : ERC n

The ERC of a winner/loser violation-profile pair: the coordinatewise sign of the violation difference ([Pri02] §0; [Rig09a] Def. 3).

Equations

• OptimalityTheory.ercOfProfiles winner loser k = SignType.sign (↑(loser k) - ↑(winner k))

theorem OptimalityTheory.ercOfProfiles_eq_W_iff {n : ℕ} (w l : Constraints.ViolationProfile n) (k : Fin n) : ercOfProfiles w l k = ERCVal.W ↔ w k < l k

ercOfProfiles is W exactly where the winner has strictly fewer violations.

theorem OptimalityTheory.ercOfProfiles_eq_L_iff {n : ℕ} (w l : Constraints.ViolationProfile n) (k : Fin n) : ercOfProfiles w l k = ERCVal.L ↔ l k < w k

ercOfProfiles is L exactly where the winner has strictly more violations.

theorem OptimalityTheory.ercOfProfiles_eq_e_iff {n : ℕ} (w l : Constraints.ViolationProfile n) (k : Fin n) : ercOfProfiles w l k = ERCVal.e ↔ w k = l k

ercOfProfiles is e exactly where violations are equal.

theorem OptimalityTheory.ercOfProfiles_swap {n : ℕ} (w l : Constraints.ViolationProfile n) : ercOfProfiles l w = -ercOfProfiles w l

The antithetical ERC ([Pri02] §2): swapping winner and loser negates it.

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

Construct an ERC from a list of ERCVal, with a length proof discharged by decide for literals: def myERC : ERC 4 := ercOfList [.W, .e, .L, .e].

Equations

• OptimalityTheory.ercOfList vs h i = vs[↑i]

theorem OptimalityTheory.lex_nonneg_ercOfProfiles_iff {n : ℕ} (w l : Constraints.ViolationProfile n) : (toLex fun (x : Fin n) => 0) ≤ toLex (ercOfProfiles w l) ↔ w ≤ l

Lex-nonnegativity of the sign vector is lex-comparison of the profiles: the sign of the first difference decides both.

theorem OptimalityTheory.satisfiedBy_ercOfProfiles_iff_le {n : ℕ} (r : Ranking n) (w l : Constraints.ViolationProfile n) : ERC.SatisfiedBy r (ercOfProfiles w l) ↔ r • w ≤ r • l

ERC satisfaction is lexicographic domination: r satisfies the ERC of a winner/loser pair iff the winner's profile, read in r's priority order, is lex-≤ the loser's ([Pri02]). Precomposition with the ranking is absorbed by instantiating lex_nonneg_ercOfProfiles_iff at the ranked readings r • w, r • l.

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

The ERC of a winner-loser pair (w, l) in tableau t: the ranking requirements for w to beat l.

Equations

• OptimalityTheory.tableauERC t w l = OptimalityTheory.ercOfProfiles (t.profile w) (t.profile l)

theorem OptimalityTheory.tableauERC_satisfiedBy_iff {n : ℕ} {C : Type u_1} [DecidableEq C] (t : Tableau C n) (r : Ranking n) (w l : C) : ERC.SatisfiedBy r (tableauERC t w l) ↔ r • t.profile w ≤ r • t.profile l

Tableau form of the bridge: the winner-loser ERC is satisfied by r iff r ranks the winner at-or-above the loser under the tableau's lex evaluation.

theorem OptimalityTheory.tableauERC_satisfiedBy_id_iff {n : ℕ} {C : Type u_1} [DecidableEq C] (t : Tableau C n) (w l : C) : ERC.SatisfiedBy (Ranking.id n) (tableauERC t w l) ↔ t.profile w ≤ t.profile l

At the identity ranking, ERC satisfaction is exactly the tableau's own lex comparison — connecting ERC inference to LexMinProblem.

theorem OptimalityTheory.mem_optimal_iff_forall_satisfiedBy {n : ℕ} {C : Type u_1} [DecidableEq C] (t : Tableau C n) (w : C) : w ∈ t.optimal ↔ w ∈ t.candidates ∧ ∀ l ∈ t.candidates, ERC.SatisfiedBy (Ranking.id n) (tableauERC t w l)

A candidate is the tableau's optimum iff, under the identity ranking, its ERC against every competitor is satisfied — ERC consistency is optimality.

theorem OptimalityTheory.Tableau.ofPerm_mem_optimal_iff_satisfiedBy {C : Type u_1} [DecidableEq C] {n : ℕ} (con : Constraints.CON C n) (r : Ranking n) (candidates : List C) (h : candidates ≠ []) (w : C) : w ∈ (ofPerm con r candidates h).optimal ↔ w ∈ candidates.toFinset ∧ ∀ l ∈ candidates.toFinset, ERC.SatisfiedBy r (tableauERC (ofPerm con (Equiv.refl (Fin n)) candidates h) w l)

The Sₙ action on a fixed CON is the ERC theory: w is optimal in Tableau.ofPerm con r iff every winner–loser ERC of the identity-ranked tableau is satisfied by r — factorial typology and ERC consistency are two readouts of one symmetric-group action.