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 ι — the sign alphabet and sign vectors ι → ERCVal over the constraints ι.
• ERC.SatisfiedBy — satisfaction of one ERC by a ranking Ranking ι n; ERC.linearExtensions the permutations of Fin n 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 vectors and winner–loser pairs; satisfiedBy_ercOfProfiles_iff_le bridges to the Core lex order, and Tableau.ofPerm_mem_optimal_iff_satisfiedBy identifies optimality with ERC satisfaction.
• simpleERC — a single-W/single-L ERC, one Hasse edge i ≫ j ([MR16b]).

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 (ι : Type u_2) : Type u_2

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

Equations

• OptimalityTheory.ERC ι = (ι → OptimalityTheory.ERCVal)

def OptimalityTheory.ERC.IsTrivial {ι : Type u_1} (α : ERC ι) : Prop

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

Equations

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

@[instance_reducible]

instance OptimalityTheory.ERC.instDecidableIsTrivialOfFintype {ι : Type u_1} (α : ERC ι) [Fintype ι] : Decidable α.IsTrivial

Equations

• α.instDecidableIsTrivialOfFintype = Fintype.decidableForallFintype

def OptimalityTheory.ERC.IsContradictory {ι : Type u_1} (α : ERC ι) : 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 : ι), α k ≠ OptimalityTheory.ERCVal.W) ∧ ∃ (k : ι), α k = OptimalityTheory.ERCVal.L)

@[instance_reducible]

instance OptimalityTheory.ERC.instDecidableIsContradictoryOfFintype {ι : Type u_1} (α : ERC ι) [Fintype ι] : Decidable α.IsContradictory

Equations

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

def OptimalityTheory.ERC.IsSimple {ι : Type u_1} (α : ERC ι) : Prop

A simple ERC has exactly one W and one L.

Equations

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

ERC satisfaction

def OptimalityTheory.ERC.SatisfiedBy {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (α : ERC ι) : 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 ≤ toLex (α ∘ ⇑r))

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 {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (α : ERC ι) : 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 {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (α : ERC ι) : SatisfiedBy r α ↔ ∀ (c : ι), α c = ERCVal.L → ∃ (w : ι), α 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 {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (α : ERC ι) : Decidable (SatisfiedBy r α)

Equations

• OptimalityTheory.ERC.instDecidableSatisfiedBy r α = { decide := decide ¬toLex (α ∘ ⇑r) < toLex 0, reflects_decide := ⋯ }

theorem OptimalityTheory.ERC.satisfiedBy_iff_exists_dominant {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (α : ERC ι) [NeZero n] : SatisfiedBy r α ↔ ∃ (d : ι), ∀ (c : ι), α 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 {ι : Type u_1} {n : ℕ} {α : ERC ι} (htriv : α.IsTrivial) (r : Ranking ι n) : SatisfiedBy r α

A trivial ERC is satisfied by every ranking.

Linear extensions

Satisfaction of a Finset (ERC (Fin 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 (Fin n))) : Finset (Ranking (Fin n) n)

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

Equations

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

@[simp]

theorem OptimalityTheory.ERC.mem_linearExtensions {n : ℕ} {E : Finset (ERC (Fin n))} {r : Ranking (Fin n) 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 {ι : Type u_1} [DecidableEq ι] (i j : ι) : ERC ι

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 {ι : Type u_1} [DecidableEq ι] {i j : ι} (k : ι) : simpleERC i j k = ERCVal.W ↔ k = i

The only W of simpleERC i j is at i.

theorem OptimalityTheory.simpleERC_eq_L_iff {ι : Type u_1} [DecidableEq ι] {i j : ι} (hij : i ≠ j) (k : ι) : 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 {ι : Type u_1} [DecidableEq ι] {i j : ι} : simpleERC i j i = ERCVal.W

theorem OptimalityTheory.simpleERC_apply_L {ι : Type u_1} [DecidableEq ι] {i j : ι} (hij : i ≠ j) : simpleERC i j j = ERCVal.L

theorem OptimalityTheory.simpleERC_self_isTrivial {ι : Type u_1} [DecidableEq ι] (i : ι) : (simpleERC i i).IsTrivial

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

theorem OptimalityTheory.simpleERC_satisfiedBy_iff {ι : Type u_1} {n : ℕ} [DecidableEq ι] {i j : ι} (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 {ι : Type u_1} {n : ℕ} [DecidableEq ι] (i j : ι) (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 {ι : Type u_1} [DecidableEq ι] {i j : ι} (hij : i ≠ j) : (simpleERC i j).IsSimple

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

theorem OptimalityTheory.simpleERC_isSimple_or_isTrivial {ι : Type u_1} [DecidableEq ι] (i j : ι) : (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 {ι : Type u_1} (winner loser : ι → ℕ) : ERC ι

The ERC of a winner/loser pair of violation vectors: 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 {ι : Type u_1} (w l : ι → ℕ) (k : ι) : 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 {ι : Type u_1} (w l : ι → ℕ) (k : ι) : 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 {ι : Type u_1} (w l : ι → ℕ) (k : ι) : ercOfProfiles w l k = ERCVal.e ↔ w k = l k

ercOfProfiles is e exactly where violations are equal.

theorem OptimalityTheory.ercOfProfiles_swap {ι : Type u_1} (w l : ι → ℕ) : 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 (Fin n)

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

Equations

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

theorem OptimalityTheory.lex_nonneg_ercOfProfiles_iff {n : ℕ} (w l : ViolationProfile n) : (toLex fun (x : Fin n) => 0) ≤ toLex (ercOfProfiles (ofLex w) (ofLex 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 {ι : Type u_1} {n : ℕ} (r : Ranking ι n) (w l : ι → ℕ) : ERC.SatisfiedBy r (ercOfProfiles w l) ↔ toLex (w ∘ ⇑r) ≤ toLex (l ∘ ⇑r)

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

def OptimalityTheory.tableauERC {n : ℕ} {C : Type u_2} [DecidableEq C] (t : Tableau C n) (w l : C) : ERC (Fin 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 (ofLex (t.profile w)) (ofLex (t.profile l))

theorem OptimalityTheory.tableauERC_satisfiedBy_iff {n : ℕ} {C : Type u_2} [DecidableEq C] (t : Tableau C n) (r : Ranking (Fin n) 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_2} [DecidableEq C] (t : Tableau C n) (w l : C) : ERC.SatisfiedBy 1 (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 the tableau's winner set.

theorem OptimalityTheory.mem_optimal_iff_forall_satisfiedBy {n : ℕ} {C : Type u_2} [DecidableEq C] (t : Tableau C n) (w : C) : w ∈ t.optimal ↔ w ∈ t.candidates ∧ ∀ l ∈ t.candidates, ERC.SatisfiedBy 1 (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 {ι : Type u_1} {n : ℕ} {C : Type u_2} [DecidableEq C] (con : ConstraintSet C ι) (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 (ercOfProfiles (fun (x : ι) => con x w) fun (x : ι) => con x l)

Optimality under a ranking is ERC satisfaction: w is optimal in Tableau.ofPerm con r iff r satisfies the winner–loser ERC of w against every competitor, so factorial typology and ERC consistency are two readouts of one constraint set.