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 — satisfaction of one ERC; ERC.linearExtensions the rankings satisfying a Finset of them. Consistency and entailment of ERC sets are Nonempty and ⊆ of linear-extension sets — no separate algebra.
• 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

@[instance_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)

@[instance_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.

@[instance_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.

Linear extensions

Satisfaction of a Finset (ERC n) needs no vocabulary of its own: a ranking satisfies the set iff ∀ α ∈ E, α.SatisfiedBy r, the set is consistent ([Pri02]) iff (ERC.linearExtensions E).Nonempty, and E entails E' iff ERC.linearExtensions E ⊆ ERC.linearExtensions E'.

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

The rankings satisfying every member of a set of ERCs, as a Finset — its linear extensions ([MR16]).

Equations

• OptimalityTheory.ERC.linearExtensions E = {r : OptimalityTheory.Ranking n | ∀ α ∈ E, OptimalityTheory.ERC.SatisfiedBy r α}

@[simp]

theorem OptimalityTheory.ERC.mem_linearExtensions {n : ℕ} {E : Finset (ERC n)} {r : Ranking n} : r ∈ linearExtensions E ↔ ∀ α ∈ E, SatisfiedBy r α

@[simp]

theorem OptimalityTheory.ERC.linearExtensions_empty {n : ℕ} : linearExtensions ∅ = Finset.univ

The empty set constrains nothing: every ranking is a linear extension.

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_self_isTrivial {n : ℕ} (i : Fin n) : (simpleERC i i).IsTrivial

The diagonal simple ERC i ≫ i has no L, hence is trivial.

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_satisfiedBy_toRel_iff {n : ℕ} (i j : Fin n) (r : Ranking n) : ERC.SatisfiedBy r (simpleERC i j) ↔ r.toRel i j

Side-condition-free form: simpleERC i j is satisfied by r iff i is ranked at least as high as j (Ranking.toRel). On the diagonal the ERC is trivial and the relation reflexive, so no i ≠ j guard is needed.

theorem OptimalityTheory.simpleERC_consistent {n : ℕ} {i j : Fin n} (hij : i ≠ j) : (ERC.linearExtensions {simpleERC i j}).Nonempty

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.

theorem OptimalityTheory.simpleERC_isSimple_or_isTrivial {n : ℕ} (i j : Fin n) : (simpleERC i j).IsSimple ∨ (simpleERC i j).IsTrivial

Every simpleERC is simple or (on the diagonal) trivial.

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.