Score profiles and their lexicographic order

A Profile β n is a length-n vector of β-valued evaluations (Fin n → β), and LexProfile β n is Lex (Fin n → β) carrying Pi.Lex's lexicographic order. Choices of β cover the standard numerical codomains: Nat, ℚ, ℝ, Bool.

Why a separate file?

Mathlib's Pi.Lex deliberately strips algebraic instances (assert_not_exists Monoid) — adding a Monoid to Lex would create diamonds with Pi.instMonoid. This file lifts the algebraic structure back through Lex only under the lexicographic order, where the compatibility is sound, and in maximum generality so that downstream modules can specialize to whatever value type they need.

@[reducible, inline]

abbrev Core.Optimization.Profile (β : Type u_1) (n : ℕ) : Type u_1

A length-n vector of β-valued entries. Carries no order — downstream aggregators decide.

Equations

• Core.Optimization.Profile β n = (Fin n → β)

@[reducible, inline]

abbrev Core.Optimization.LexProfile (β : Type u_1) (n : ℕ) : Type u_1

A lexicographically ordered profile: Pi.Lex of Fin n → β.

With [LinearOrder β], LexProfile β n is itself a LinearOrder (inherited from Pi.Lex). With [AddCommMonoid β] and the right monotonicity hypotheses on β, it carries IsOrderedAddMonoid and IsOrderedCancelAddMonoid (proved below).

Equations

• Core.Optimization.LexProfile β n = Lex (Fin n → β)

@[implicit_reducible]

instance Core.Optimization.LexProfile.instAddCommMonoid {β : Type u_1} {n : ℕ} [AddCommMonoid β] : AddCommMonoid (LexProfile β n)

Componentwise additive monoid structure. The axioms hold pointwise so the proofs reduce to pointwise applications of the corresponding β axioms.

Equations

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

instance Core.Optimization.LexProfile.instIsOrderedAddMonoidOfAddRightStrictMono {β : Type u_1} {n : ℕ} [AddCommMonoid β] [PartialOrder β] [AddRightStrictMono β] : IsOrderedAddMonoid (LexProfile β n)

Riggle's distributivity for general β: adding the same vector to both sides preserves lexicographic order. The witness i (first differing position) survives because right-translation by c i preserves strict inequality (AddRightStrictMono).

Note on naming: mathlib's add_lt_add_left proves a + c < b + c (the left operand changes — c is the constant added on the right) and is the additive analog of mul_lt_mul_left.

instance Core.Optimization.LexProfile.instIsOrderedCancelAddMonoidOfAddRightStrictMonoOfIsLeftCancelAddOfAddLeftReflectLT {β : Type u_1} {n : ℕ} [AddCommMonoid β] [PartialOrder β] [AddRightStrictMono β] [IsLeftCancelAdd β] [AddLeftReflectLT β] : IsOrderedCancelAddMonoid (LexProfile β n)

Left cancellation: if a + b ≤ a + c then b ≤ c. Promotes the ordered monoid to an ordered cancel monoid, which downstream is what licenses the tropical semiring derivation.