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 strict dominance relation between constraints and Ranking.toRel its reflexive closure — the ranking as a total order, from which the ranking is recoverable (toRel_le_toRel_iff). 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)

theorem OptimalityTheory.total_eq_of_le {α : Type u_1} {r s : α → α → Prop} [ht : Std.Total r] [ha : Std.Antisymm s] (h : r ≤ s) : r = s

A total relation is maximal among antisymmetric relations: anything above it in the pointwise lattice collapses back onto it.

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)

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

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

The ranking as a total order

def OptimalityTheory.Ranking.toRel {n : ℕ} (r : Ranking n) : Fin n → Fin n → Prop

The ranking as its dominance-or-equal relation: r.toRel i j iff i is ranked at least as high as j — the reflexive closure of Dominates (toRel_iff), and a total order on constraints.

Equations

• r.toRel i j = ((Equiv.symm r) i ≤ (Equiv.symm r) j)

@[instance_reducible]

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

Equations

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

instance OptimalityTheory.Ranking.instIsPartialOrderFinToRel {n : ℕ} (r : Ranking n) : IsPartialOrder (Fin n) r.toRel

instance OptimalityTheory.Ranking.instTotalFinToRel {n : ℕ} (r : Ranking n) : Std.Total r.toRel

theorem OptimalityTheory.Ranking.toRel_iff {n : ℕ} (r : Ranking n) {i j : Fin n} : r.toRel i j ↔ i = j ∨ r.Dominates i j

toRel is the reflexive closure of Dominates.

theorem OptimalityTheory.Ranking.toRel_iff_dominates {n : ℕ} (r : Ranking n) {i j : Fin n} (hij : i ≠ j) : r.toRel i j ↔ r.Dominates i j

On distinct constraints, toRel is Dominates.

@[simp]

theorem OptimalityTheory.Ranking.toRel_mul {n : ℕ} (g σ : Ranking n) (i j : Fin n) : (g * σ).toRel i j ↔ σ.toRel (g⁻¹ i) (g⁻¹ j)

Relabeling constraints by g pulls the induced order back along g⁻¹.

theorem OptimalityTheory.Ranking.toRel_injective {n : ℕ} : Function.Injective toRel

A ranking is recoverable from its induced total order.

theorem OptimalityTheory.Ranking.toRel_le_toRel_iff {n : ℕ} {σ τ : Ranking n} : σ.toRel ≤ τ.toRel ↔ σ = τ

Total orders comparable in the relation lattice coincide, so toRel is rigid: nothing sits strictly between two ranking-induced orders.

theorem OptimalityTheory.Ranking.exists_toRel_eq {n : ℕ} (s : Fin n → Fin n → Prop) [IsLinearOrder (Fin n) s] : ∃ (σ : Ranking n), σ.toRel = s

Every linear order on Fin n is the induced order of a ranking — the surjectivity companion to toRel_injective: enumerate the constraints in s-order (Finset.sort) and read off the ranking.