Lexicographic order on Nat-valued profiles

Lexicographic comparison on lists / functions to ℕ (LexLE): a total preorder on List Nat and a LinearOrder on the fixed-length Lex (Fin n → Nat). (The subset-inclusion order on satisfied criteria lives at Preorder.ofCriteria in Core/Order/OfCriteria.lean.)

Architecture

LexLE, LexLT are decidable Prop relations defined by structural recursion, delegating to standard combinators (And.decidable, Or.decidable). LexMinProblem C n packages a finite candidate set with a Fin n → Nat-valued score, exposing the non-empty lex-min set via Finset.exists_min_image.

Algebraic structure — ordered additive monoid

Lex (Fin n → Nat) carries:

• AddCommMonoid — componentwise addition.
• LinearOrder — the lex order.
• IsOrderedAddMonoid — additive monotonicity: adding the same vector to both sides preserves the lex order.
• IsOrderedCancelAddMonoid — strict version of the above.

Together these say: Lex (Fin n → Nat) is a standard mathlib ordered commutative monoid. Equivalently, the tropical (min-plus) semiring view via Mathlib.Algebra.Tropical.Basic.

Variable-length vs fixed-length

Variable-length (LexNatList): wraps List Nat with Preorder instances. Weakest correct structure — LexLE on variable-length lists is a preorder but not a partial order (trailing-zero ambiguity).

Fixed-length (Lex (Fin n → Nat), accessed as LexProfile Nat n): full LinearOrder (lex). Fixing the length eliminates trailing-zero ambiguity, upgrading LexLE to a linear order. LexMinProblem C n always has a non-empty lex-min set via Finset.exists_min_image.

Connection to SatisfactionOrdering

Core.Order.SatisfactionOrdering is the binary case (0/≥ 1 interpreted as "satisfied" / "not") with subset-inclusion comparison.

def Core.Optimization.Evaluation.LexLE : List ℕ → List ℕ → Prop

Lexicographic ≤ on List Nat (interpretable as cost vectors).

LexLE a b holds iff a is below b at the first position where they differ. Trailing entries are implicitly 0.

Equations

• Core.Optimization.Evaluation.LexLE [] x✝ = True
• Core.Optimization.Evaluation.LexLE (a :: as) [] = (a = 0 ∧ Core.Optimization.Evaluation.LexLE as [])
• Core.Optimization.Evaluation.LexLE (a :: as) (b :: bs) = (a < b ∨ a = b ∧ Core.Optimization.Evaluation.LexLE as bs)

def Core.Optimization.Evaluation.LexLT (a b : List ℕ) : Prop

Strict lexicographic <.

Equations

• Core.Optimization.Evaluation.LexLT a b = (Core.Optimization.Evaluation.LexLE a b ∧ ¬Core.Optimization.Evaluation.LexLE b a)

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableLexLE (a b : List ℕ) : Decidable (LexLE a b)

Equations

• Core.Optimization.Evaluation.instDecidableLexLE [] x✝ = isTrue ⋯
• Core.Optimization.Evaluation.instDecidableLexLE (a :: as) [] = Core.Optimization.Evaluation.instDecidableLexLE._aux_1 a as (Core.Optimization.Evaluation.instDecidableLexLE as [])
• Core.Optimization.Evaluation.instDecidableLexLE (a :: as) (b :: bs) = Core.Optimization.Evaluation.instDecidableLexLE._aux_3 a as b bs (Core.Optimization.Evaluation.instDecidableLexLE as bs)

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableLexLT (a b : List ℕ) : Decidable (LexLT a b)

Equations

• Core.Optimization.Evaluation.instDecidableLexLT a b = Core.Optimization.Evaluation.instDecidableLexLT._aux_1 a b

theorem Core.Optimization.Evaluation.lexLE_refl (a : List ℕ) : LexLE a a

Lexicographic ≤ is reflexive.

theorem Core.Optimization.Evaluation.lexLE_total (a b : List ℕ) (h : a.length = b.length) : LexLE a b ∨ LexLE b a

Lexicographic ≤ is total for equal-length profiles.

theorem Core.Optimization.Evaluation.lexLE_nil (b : List ℕ) : LexLE [] b

LexLE [] b holds for any b: the empty list is vacuously at-most-as-large-as any list.

theorem Core.Optimization.Evaluation.lexLE_cons_nil_iff (x : ℕ) (xs : List ℕ) : LexLE (x :: xs) [] ↔ x = 0 ∧ LexLE xs []

Characterization of LexLE (x :: xs) []: all entries must be zero.

theorem Core.Optimization.Evaluation.lexLE_cons_cons_iff (x y : ℕ) (xs ys : List ℕ) : LexLE (x :: xs) (y :: ys) ↔ x < y ∨ x = y ∧ LexLE xs ys

Characterization of LexLE (x :: xs) (y :: ys): either the head is strictly less, or the heads are equal and the tails are ≤.

theorem Core.Optimization.Evaluation.toLex_fin_le_succ {n : ℕ} (f g : Fin (n + 1) → ℕ) : toLex f ≤ toLex g ↔ f 0 < g 0 ∨ f 0 = g 0 ∧ (toLex fun (i : Fin n) => f i.succ) ≤ toLex fun (i : Fin n) => g i.succ

Pi.Lex over Fin (n+1) decomposes at index 0 (head-then-tail).

theorem Core.Optimization.Evaluation.lexLE_ofFn {n : ℕ} (f g : Fin n → ℕ) : LexLE (List.ofFn f) (List.ofFn g) ↔ toLex f ≤ toLex g

The decidable variable-length LexLE on List.ofFn agrees with the fixed-length lexicographic order toLex on Fin n → Nat (= LexProfile Nat n) — the finite-tuple analogue of mathlib's MonomialOrder.lex (we keep this bespoke computable order because mathlib's is noncomputable and Finsupp-based). This is the bridge that lets a directional constraint be spliced into a fixed-length profile as a position-block and still compare under the canonical lex EVAL ([eisner-2000]/[lamont-2022b]).

theorem Core.Optimization.Evaluation.lexLE_of_nil_right (a : List ℕ) : LexLE a [] → ∀ (c : List ℕ), LexLE a c

If LexLE a [] (all entries are zero), then LexLE a c for any c. The all-zeros profile is the minimum under LexLE.

theorem Core.Optimization.Evaluation.lexLE_trans (a b c : List ℕ) : LexLE a b → LexLE b c → LexLE a c

Lexicographic ≤ is transitive. Together with lexLE_refl and lexLE_total, this makes LexLE a total preorder on equal-length profiles — the correct algebraic structure for lex order.

theorem Core.Optimization.Evaluation.lexLT_irrefl (a : List ℕ) : ¬LexLT a a

Lexicographic < is irreflexive.

theorem Core.Optimization.Evaluation.lexLT_asymm (a b : List ℕ) (h : LexLT a b) : ¬LexLT b a

Lexicographic < is asymmetric: LexLT a b → ¬ LexLT b a.

theorem Core.Optimization.Evaluation.lexLT_trans (a b c : List ℕ) (hab : LexLT a b) (hbc : LexLT b c) : LexLT a c

Lexicographic < is transitive: LexLT a b → LexLT b c → LexLT a c.

theorem Core.Optimization.Evaluation.lexLE_antisymm (a b : List ℕ) : a.length = b.length → LexLE a b → LexLE b a → a = b

Lexicographic ≤ is antisymmetric on equal-length profiles: if two profiles of the same length are mutually ≤, they are equal.

This fails on List Nat in general (LexLE [] [0] and LexLE [0] [] both hold, but [] ≠ [0]) — the equal-length precondition eliminates the trailing-zero ambiguity that makes LexLE merely a preorder.

theorem Core.Optimization.Evaluation.exists_lexLE_minimum {α : Type u_1} (xs : List α) (hne : xs ≠ []) (f : α → List ℕ) (hlen : ∀ a ∈ xs, ∀ b ∈ xs, (f a).length = (f b).length) : ∃ x ∈ xs, ∀ y ∈ xs, LexLE (f x) (f y)

A non-empty list has a minimum element under LexLE, provided all profiles have equal length. This is the key ingredient for optimal_nonempty: the lex-min set is non-empty.

structure Core.Optimization.Evaluation.LexNatList : Type

List Nat wrapped to carry the LexLE-Preorder instance.

The bare List Nat doesn't carry a Preorder from LexLE (mathlib leaves it ambiguous); this thin wrapper provides one. Only a Preorder — not a PartialOrder — since trailing zeros are invisible (LexLE [] [0] and LexLE [0] [] both hold). For a LinearOrder, use fixed-length Lex (Fin n → Nat) (aka LexProfile Nat n).

• value : List ℕ

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableEqLexNatList : DecidableEq LexNatList

Equations

• Core.Optimization.Evaluation.instDecidableEqLexNatList = Core.Optimization.Evaluation.instDecidableEqLexNatList.decEq

def Core.Optimization.Evaluation.instDecidableEqLexNatList.decEq (x✝ x✝¹ : LexNatList) : Decidable (x✝ = x✝¹)

Equations

• Core.Optimization.Evaluation.instDecidableEqLexNatList.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Core.Optimization.Evaluation.instReprLexNatList.repr : LexNatList → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Optimization.Evaluation.instReprLexNatList : Repr LexNatList

Equations

• Core.Optimization.Evaluation.instReprLexNatList = { reprPrec := Core.Optimization.Evaluation.instReprLexNatList.repr }

@[implicit_reducible]

instance Core.Optimization.Evaluation.instLELexNatList : LE LexNatList

Equations

• Core.Optimization.Evaluation.instLELexNatList = { le := fun (a b : Core.Optimization.Evaluation.LexNatList) => Core.Optimization.Evaluation.LexLE a.value b.value }

@[implicit_reducible]

instance Core.Optimization.Evaluation.instLTLexNatList : LT LexNatList

Equations

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

@[implicit_reducible]

instance Core.Optimization.Evaluation.instPreorderLexNatList : Preorder LexNatList

Equations

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

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableLeLexNatList (a b : LexNatList) : Decidable (a ≤ b)

Equations

• Core.Optimization.Evaluation.instDecidableLeLexNatList a b = Core.Optimization.Evaluation.instDecidableLexLE a.value b.value

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableLtLexNatList (a b : LexNatList) : Decidable (a < b)

Equations

• Core.Optimization.Evaluation.instDecidableLtLexNatList a b = instDecidableAnd

theorem Core.Optimization.Evaluation.LexNatList.le_iff (a b : LexNatList) : a ≤ b ↔ LexLE a.value b.value

LexNatList.≤ is definitionally LexLE.

theorem Core.Optimization.Evaluation.LexNatList.lt_iff (a b : LexNatList) : a < b ↔ LexLT a.value b.value

LexNatList.< is definitionally LexLT.

theorem Core.Optimization.Evaluation.LexNatList.le_total (a b : LexNatList) (h : a.value.length = b.value.length) : a ≤ b ∨ b ≤ a

LexLE is total on equal-length values, expressed via LexNatList.

theorem Core.Optimization.Evaluation.lexFinNat_add_apply {n : ℕ} (a b : Lex (Fin n → ℕ)) (i : Fin n) : (a + b) i = a i + b i

Pointwise addition on Lex (Fin n → Nat) reduces componentwise.

theorem Core.Optimization.Evaluation.lexFinNat_zero_apply {n : ℕ} (i : Fin n) : 0 i = 0

The zero Lex (Fin n → Nat) is pointwise zero.

@[implicit_reducible]

instance Core.Optimization.Evaluation.instAddCommMonoidLexForallFinNat_linglib (n : ℕ) : AddCommMonoid (Lex (Fin n → ℕ))

Equations

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

instance Core.Optimization.Evaluation.instIsOrderedAddMonoidLexForallFinNat_linglib (n : ℕ) : IsOrderedAddMonoid (Lex (Fin n → ℕ))

Lex (Fin n → Nat) is an ordered additive commutative monoid: componentwise addition preserves the lexicographic ordering. The proof transfers the lex existential witness: if a < b at position i with all earlier positions equal, then a + c < b + c at the same position.

instance Core.Optimization.Evaluation.instIsOrderedCancelAddMonoidLexForallFinNat_linglib (n : ℕ) : IsOrderedCancelAddMonoid (Lex (Fin n → ℕ))

Left cancellation for lexicographic ≤.

theorem Core.Optimization.Evaluation.lexFinNatLE_iff_le {n : ℕ} (a b : Lex (Fin n → ℕ)) : Core.Optimization.Evaluation.lexFinNatLE✝ n a b ↔ a ≤ b

Bridge: lexFinNatLE agrees with ≤ on Lex (Fin n → Nat).

theorem Core.Optimization.Evaluation.lex_le_iff_forall {α : Type u_1} [LinearOrder α] {m : ℕ} (A B : Fin m → α) : toLex A ≤ toLex B ↔ ∀ (p : Fin m), B p < A p → ∃ p' < p, A p' < B p'

Lexicographic ≤ as "no uncompensated inversion": toLex A ≤ toLex B holds iff every coordinate where A strictly exceeds B is preceded (in index order) by one where A is strictly below B. Stated for any linearly-ordered codomain; used to ground OT's ERC satisfaction in the lex order.

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableLexFinNatProfileLE {n : ℕ} (a b : Lex (Fin n → ℕ)) : Decidable (a ≤ b)

Decidable ≤ on Lex (Fin n → Nat). The LinearOrder from Pi.Lex is noncomputable, but this instance provides decidable comparison via the recursive lexFinNatLE, making downstream by decide work.

Equations

• Core.Optimization.Evaluation.instDecidableLexFinNatProfileLE a b = decidable_of_iff (Core.Optimization.Evaluation.lexFinNatLE✝ n a b) ⋯

@[implicit_reducible]

instance Core.Optimization.Evaluation.instDecidableLexFinNatProfileLT {n : ℕ} (a b : Lex (Fin n → ℕ)) : Decidable (a < b)

Decidable < on Lex (Fin n → Nat).

Equations

• Core.Optimization.Evaluation.instDecidableLexFinNatProfileLT a b = decidable_of_iff (¬b ≤ a) ⋯

theorem Core.Optimization.Evaluation.lex_le_iff_lead {α : Type u_1} [LinearOrder α] {m : ℕ} (A B : Fin m → α) [DecidablePred fun (i : Fin m) => B i ≠ A i] : toLex A ≤ toLex B ↔ ∀ (he : ∃ (i : Fin m), B i ≠ A i), A (Fin.find (fun (k : Fin m) => B k ≠ A k) he) < B (Fin.find (fun (k : Fin m) => B k ≠ A k) he)

Lexicographic order is decided at the first differing coordinate: A ≤ B iff at the least index where they differ — when one exists — A is smaller. (Candidate for mathlib's Pi.Lex API.)

def Core.Optimization.Evaluation.lexFinNatOf {C : Type u_1} {n : ℕ} (atoms : Fin n → C → ℕ) (c : C) : Lex (Fin n → ℕ)

Build a Lex (Fin n → Nat) from n atom-wise evaluation functions. Given atoms as Fin n → C → Nat, produce the lex-comparable fixed-length vector for c : C.

Equations

• Core.Optimization.Evaluation.lexFinNatOf atoms c = toLex fun (i : Fin n) => atoms i c

@[simp]

theorem Core.Optimization.Evaluation.lexFinNatOf_apply {C : Type u_1} {n : ℕ} (atoms : Fin n → C → ℕ) (c : C) (i : Fin n) : lexFinNatOf atoms c i = atoms i c

@[implicit_reducible]

noncomputable instance Core.Optimization.Evaluation.instLinearOrderedAddCommMonoidWithTopWithTopLexForallFinNat_linglib (n : ℕ) : LinearOrderedAddCommMonoidWithTop (WithTop (Lex (Fin n → ℕ)))

WithTop (Lex (Fin n → Nat)) is a LinearOrderedAddCommMonoidWithTop: it extends the ordered cancel monoid with an absorbing top element. Prerequisite for the tropical semiring: mathlib's Tropical wrapper then provides CommSemiring automatically.

Equations

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

def Core.Optimization.Evaluation.argMinSet {α : Type u_1} {P : Type u_2} [DecidableEq α] (s : Finset α) (f : α → P) (r : P → P → Prop) [DecidableRel r] : Finset α

The elements of s whose image under f is r-minimal — r-below every image in s. The shared selection primitive behind LexMinProblem.lexMins (over ≤ on Lex (Fin n → Nat)) and the variable-length LexLE-minimization used by the prosodic/list-lex consumers.

Equations

• Core.Optimization.Evaluation.argMinSet s f r = {c ∈ s | ∀ d ∈ s, r (f c) (f d)}

theorem Core.Optimization.Evaluation.mem_argMinSet {α : Type u_1} {P : Type u_2} [DecidableEq α] {s : Finset α} {f : α → P} {r : P → P → Prop} [DecidableRel r] {c : α} : c ∈ argMinSet s f r ↔ c ∈ s ∧ ∀ d ∈ s, r (f c) (f d)

theorem Core.Optimization.Evaluation.argMinSet_nonempty {α : Type u_1} {P : Type u_2} [DecidableEq α] {s : Finset α} {f : α → P} {r : P → P → Prop} [DecidableRel r] (h : ∃ m ∈ s, ∀ d ∈ s, r (f m) (f d)) : (argMinSet s f r).Nonempty

theorem Core.Optimization.Evaluation.le_of_mem_argMinSet {α : Type u_1} {P : Type u_2} [DecidableEq α] [PartialOrder P] [DecidableRel fun (x1 x2 : P) => x1 ≤ x2] {s : Finset α} {f : α → P} {c d : α} (hc : c ∈ argMinSet s f fun (x1 x2 : P) => x1 ≤ x2) (hd : d ∈ s) : f c ≤ f d

A minimizer's image bounds every image in s.

theorem Core.Optimization.Evaluation.mem_argMinSet_of_eq {α : Type u_1} {P : Type u_2} [DecidableEq α] [PartialOrder P] [DecidableRel fun (x1 x2 : P) => x1 ≤ x2] {s : Finset α} {f : α → P} {c d : α} (hd : d ∈ argMinSet s f fun (x1 x2 : P) => x1 ≤ x2) (hc : c ∈ s) (he : f c = f d) : c ∈ argMinSet s f fun (x1 x2 : P) => x1 ≤ x2

Minimizer-hood factors through the image, so it transports along image equality.

theorem Core.Optimization.Evaluation.mem_argMinSet_of_eq_bot {α : Type u_1} {P : Type u_2} [DecidableEq α] [PartialOrder P] [DecidableRel fun (x1 x2 : P) => x1 ≤ x2] {s : Finset α} {f : α → P} {c : α} [OrderBot P] (hc : c ∈ s) (h0 : f c = ⊥) : c ∈ argMinSet s f fun (x1 x2 : P) => x1 ≤ x2

An element whose image is the bottom minimizes.

theorem Core.Optimization.Evaluation.argMinSet_eq_singleton_iff {α : Type u_1} {P : Type u_2} [DecidableEq α] [PartialOrder P] [DecidableRel fun (x1 x2 : P) => x1 ≤ x2] {s : Finset α} {f : α → P} {m : α} (hm : m ∈ s) : (argMinSet s f fun (x1 x2 : P) => x1 ≤ x2) = {m} ↔ ∀ c ∈ s, c ≠ m → f m < f c

The minimizer set is the singleton {m} iff m strictly minimizes.

@[simp]

theorem Core.Optimization.Evaluation.argMinSet_singleton {α : Type u_1} {P : Type u_2} [DecidableEq α] [PartialOrder P] [DecidableRel fun (x1 x2 : P) => x1 ≤ x2] (a : α) (f : α → P) : (argMinSet {a} f fun (x1 x2 : P) => x1 ≤ x2) = {a}

A singleton's sole element minimizes.

structure Core.Optimization.Evaluation.LexMinProblem (C : Type u_1) [DecidableEq C] (n : ℕ) : Type u_1

A finite candidate set C with a Fin n → Nat-valued score and a nonemptiness witness. The lex-min set is nonempty (exists_lexMin), computable (lexMins), and accessible via the IsLexMin predicate.

• candidates : Finset C
• profile : C → Lex (Fin n → ℕ)
• nonempty : self.candidates.Nonempty

def Core.Optimization.Evaluation.LexMinProblem.IsLexMin {C : Type u_1} [DecidableEq C] {n : ℕ} (t : LexMinProblem C n) (c : C) : Prop

A candidate is a lex-minimizer iff it's in the candidate set and its score is ≤ every other candidate's score.

Equations

• t.IsLexMin c = (c ∈ t.candidates ∧ ∀ c' ∈ t.candidates, t.profile c ≤ t.profile c')

theorem Core.Optimization.Evaluation.LexMinProblem.exists_lexMin {C : Type u_1} [DecidableEq C] {n : ℕ} (t : LexMinProblem C n) : ∃ (c : C), t.IsLexMin c

Every problem has a lex-minimizer. Delegates to Finset.exists_min_image — the linear-ordered image of a nonempty finset has a minimum.

def Core.Optimization.Evaluation.LexMinProblem.lexMins {C : Type u_1} [DecidableEq C] {n : ℕ} (t : LexMinProblem C n) : Finset C

The set of lex-minimizers, as an argMinSet over ≤. Computable via instDecidableLexFinNatProfileLE; consumers can use by decide to verify lex-mins on concrete problems.

Equations

• t.lexMins = Core.Optimization.Evaluation.argMinSet t.candidates t.profile fun (x1 x2 : Lex (Fin n → ℕ)) => x1 ≤ x2

theorem Core.Optimization.Evaluation.LexMinProblem.mem_lexMins_iff {C : Type u_1} [DecidableEq C] {n : ℕ} (t : LexMinProblem C n) (c : C) : c ∈ t.lexMins ↔ t.IsLexMin c

c ∈ t.lexMins iff t.IsLexMin c.

theorem Core.Optimization.Evaluation.LexMinProblem.lexMins_nonempty {C : Type u_1} [DecidableEq C] {n : ℕ} (t : LexMinProblem C n) : t.lexMins.Nonempty

The lex-min set is always nonempty.

theorem Core.Optimization.Evaluation.LexMinProblem.lexMins_subset {C : Type u_1} [DecidableEq C] {n : ℕ} (t : LexMinProblem C n) (c : C) : c ∈ t.lexMins → c ∈ t.candidates

Lex-minimizers belong to the candidate set.

def Core.Optimization.Evaluation.Finset.checkAll {α : Type} [DecidableEq α] (s : Finset α) (p : α → Bool) : Bool

Check a Bool predicate for all elements of a Finset. Computable via Finset.decidableBAll — avoids noncomputable Finset.toList.

Equations

• Core.Optimization.Evaluation.Finset.checkAll s p = decide (∀ c ∈ s, p c = true)

def Core.Optimization.Evaluation.Finset.checkAny {α : Type} [DecidableEq α] (s : Finset α) (p : α → Bool) : Bool

Check a Bool predicate for some element of a Finset.

Equations

• Core.Optimization.Evaluation.Finset.checkAny s p = decide (∃ c ∈ s, p c = true)

theorem Core.Optimization.Evaluation.lexFinNat_le_apply_zero {n : ℕ} {a b : Lex (Fin (n + 1) → ℕ)} (h : a ≤ b) : a 0 ≤ b 0

If a ≤ b lex-wise, then their first components satisfy a 0 ≤ b 0.