Constraint rankings

A constraint ranking is a permutation of Fin n ([Pri02]'s total domination order ≫): r i is the constraint at rank position i, position 0 most dominant. Ranking.Dominates is the induced dominance relation between constraints; the Tableau machinery evaluates under a ranking, and the elementary-ranking-condition layer (ElementaryRankingCondition.lean) infers rankings from winner–loser pairs.

@[reducible, inline]

abbrev OptimalityTheory.Ranking (n : ℕ) : Type

A constraint ranking: a permutation of Fin n ([Pri02]'s total domination order ≫). r i is the constraint at rank position i (position 0 is most dominant); r.symm k is the rank position of k.

Equations

• OptimalityTheory.Ranking n = Equiv.Perm (Fin n)

def OptimalityTheory.Ranking.Dominates {n : ℕ} (r : Ranking n) (i j : Fin n) : Prop

Constraint i dominates constraint j under r: it sits at a lower (more dominant) rank position.

Equations

• r.Dominates i j = ((Equiv.symm r) i < (Equiv.symm r) j)

@[implicit_reducible]

instance OptimalityTheory.Ranking.instDecidableDominates {n : ℕ} (r : Ranking n) (i j : Fin n) : Decidable (r.Dominates i j)

Equations

• r.instDecidableDominates i j = OptimalityTheory.Ranking.instDecidableDominates._aux_1 r i j

@[simp]

theorem OptimalityTheory.Ranking.dominates_apply_iff {n : ℕ} (r : Ranking n) {p q : Fin n} : r.Dominates (r p) (r q) ↔ p < q

Dominance between ranked positions is position order.

def OptimalityTheory.Ranking.id (n : ℕ) : Ranking n

The identity ranking: rank position equals constraint index.

Equations

• OptimalityTheory.Ranking.id n = Equiv.refl (Fin n)

@[simp]

theorem OptimalityTheory.Ranking.id_dominates_iff {n : ℕ} {i j : Fin n} : (id n).Dominates i j ↔ i < j

Under the identity ranking, dominance is index order.

@[implicit_reducible]

instance OptimalityTheory.Ranking.instSMulLexForallFin {n : ℕ} {α : Type u_1} : SMul (Ranking n) (Lex (Fin n → α))

The ranking's reading of a lex-ordered vector: coordinate p of r • v is the value of v at the constraint ranked p-th. Reordering is the one operation that breaks and reconstitutes the lex order — the Sₙ action whose orbit structure is constraint ranking. (With this convention the action is a right action: (r * s) • v = s • r • v.)

Equations

• OptimalityTheory.Ranking.instSMulLexForallFin = { smul := fun (r : OptimalityTheory.Ranking n) (v : Lex (Fin n → α)) => toLex fun (p : Fin n) => ofLex v (r p) }

@[simp]

theorem OptimalityTheory.Ranking.smul_apply {n : ℕ} {α : Type u_1} (r : Ranking n) (v : Lex (Fin n → α)) (p : Fin n) : ofLex (r • v) p = ofLex v (r p)

@[simp]

theorem OptimalityTheory.Ranking.id_smul {n : ℕ} {α : Type u_1} (v : Lex (Fin n → α)) : id n • v = v

theorem OptimalityTheory.Ranking.exists_dominates {n : ℕ} {i j : Fin n} (hij : i ≠ j) : ∃ (r : Ranking n), r.Dominates i j

Any two distinct constraints can be ranked either way: some ranking makes i dominate j.