Constraint Profiles — General Codomain

A Profile β n is a vector of n β-valued evaluations: the result of applying n constraints to one candidate. The codomain β is left generic so that the same algebraic apparatus serves several constraint frameworks:

• β = Nat — standard OT violation counts
• β = ℚ or ℝ — weighted Harmonic Grammar / MaxEnt scores
• β = Bool — Stochastic OT satisfaction patterns

LexProfile β n wraps Fin n → β in Lex so that Pi.Lex's lexicographic order kicks in. The familiar OT type ViolationProfile n from Core.Constraint.Evaluation is exactly LexProfile Nat n.

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.

The same proofs as Core.Constraint.Evaluation (for Nat), but generalized — add_lt_add_left, add_left_cancel, lt_of_add_lt_add_left in place of their Nat.* specializations.

@[reducible, inline]

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

A pure constraint profile: n evaluations, each yielding a value in β. Carries no order — aggregators (lex, weighted-sum, ...) decide how to combine.

Equations

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

@[reducible, inline]

abbrev Core.Constraint.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).

ViolationProfile n from Core.Constraint.Evaluation is the β = Nat specialization.

Equations

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

@[implicit_reducible]

instance Core.Constraint.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.Constraint.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.Constraint.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.