Constraint Evaluation

@cite{erlewine-2016} @cite{kratzer-1991}

Unified framework for constraint-based candidate evaluation, supporting two comparison modes:

1. Lexicographic (Optimality Theory): constraints are strictly ranked; the first constraint where candidates differ determines the winner. Used in phonology (@cite{prince-smolensky-1993}/2004) and syntactic competition.

2. Subset inclusion (Satisfaction ordering): a candidate is at least as good as another iff it satisfies every criterion the other satisfies. Used in @cite{kratzer-1991}'s modal semantics (see SatisfactionOrdering.lean).

Both select optimal candidates from a set. They differ in comparison: LexLE yields a total preorder (OT always picks a winner); SatLE yields a preorder (incomparable candidates possible, as in Kratzer's semantics).

Architecture

Each comparison is a decidable Prop relation (LexLE, SatLE, LexLT). Decidable instances are defined by structural recursion, delegating to standard combinators (And.decidable, Or.decidable). Tableau C n provides the Finset-based OT tableau with ViolationProfile n profiles; study files use mkTableau (in Core.Constraint.OT) for concrete evaluation.

Algebraic Structure — Violation Semiring

Following @cite{riggle-2009}, violation profiles form a commutative semiring (the "violation semiring") with two operations:

• ⊎ (merge): componentwise addition of violation counts — combining violations from multiple constraints. This is the AddCommMonoid.
• ⊗ (choose winner): min under harmonic inequality — selecting the more harmonic candidate. This is min from the LinearOrder.

The compatibility axiom (add_le_add_left) is Riggle's distributivity: adding violations to both candidates preserves which one wins. This is the structural property that makes OT optimization decomposable — every subpath of an optimal path is itself optimal (Dijkstra's principle).

ViolationProfile n carries a LinearOrder (the ⊗ operation), an AddCommMonoid (the ⊎ operation), and IsOrderedAddMonoid (the compatibility axiom). Together, these encode Riggle's violation semiring as a standard mathlib ordered monoid.

Different OT variants correspond to different ordered monoids on the same carrier: classical OT uses lexicographic order; Harmonic Grammar uses weighted-sum order (the standard tropical semiring).

Order Instances

Variable-length (LexProfile, SatProfile): wrap List Nat with Preorder instances. These are the weakest correct structures — LexLE on variable-length lists is a preorder but not a partial order (trailing-zero ambiguity).

Fixed-length (ViolationProfile n, SatViolationProfile n): wrap Fin n → Nat with full LinearOrder (lexicographic) or Preorder (satisfaction). Fixing the length eliminates the trailing-zero ambiguity, upgrading LexLE to a linear order: reflexive, transitive, antisymmetric, and total.

Tableau C n is a Finset-based OT tableau with ViolationProfile n profiles. Optimality always exists via Finset.exists_min_image.

Connection to SatisfactionOrdering

Core.SatisfactionOrdering.SatisfactionOrdering is the special case where violations are binary (0 = satisfied, ≥1 = violated) and comparison uses subset inclusion (SatLE). A SatisfactionOrdering with criteria [c₁,..., cₙ] induces the profile fun a => [if satisfies a c₁ then 0 else 1,..., if satisfies a cₙ then 0 else 1], and atLeastAsGood coincides with SatLE on this profile.

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

Lexicographic ≤ on violation profiles.

LexLE a b holds iff a is at least as harmonic as b — at the first position where profiles differ, a has fewer violations. Missing entries are implicitly 0.

Equations

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

def Core.Constraint.Evaluation.SatLE : List ℕ → List ℕ → Prop

Subset-inclusion ≤ on violation profiles.

SatLE a b holds iff every constraint that b satisfies (has 0 violations), a also satisfies. This is a preorder (reflexive, transitive) but not a partial order on List Nat — non-zero values are interchangeable (e.g., SatLE [1] [2] and SatLE [2] [1] both hold). On binary {0,1} profiles it becomes a partial order.

Unlike LexLE, SatLE is not total — incomparable candidates are possible. This is @cite{kratzer-1991}'s ordering on worlds relative to a premise set.

Equations

• Core.Constraint.Evaluation.SatLE [] x✝ = True
• Core.Constraint.Evaluation.SatLE (a :: as) [] = (a = 0 ∧ Core.Constraint.Evaluation.SatLE as [])
• Core.Constraint.Evaluation.SatLE (a :: as) (b :: bs) = ((b ≠ 0 ∨ a = 0) ∧ Core.Constraint.Evaluation.SatLE as bs)

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

Strict lexicographic <.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableSatLE (a b : List ℕ) : Decidable (SatLE a b)

Equations

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

@[implicit_reducible]

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

Equations

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

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

Lexicographic ≤ is reflexive.

theorem Core.Constraint.Evaluation.satLE_refl (a : List ℕ) : SatLE a a

Satisfaction ≤ is reflexive.

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

Lexicographic ≤ is total for equal-length profiles: OT always determines a winner (modulo ties). Key difference from SatLE.

theorem Core.Constraint.Evaluation.satLE_not_total : ¬∀ (a b : List ℕ), SatLE a b ∨ SatLE b a

SatLE is NOT total: candidates can be incomparable when each satisfies a constraint the other violates.

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

LexLE [] b holds for any b: the empty profile is vacuously at least as harmonic as any profile.

theorem Core.Constraint.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.Constraint.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.Constraint.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.Constraint.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 OT harmony ordering.

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

Lexicographic < is irreflexive.

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

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

theorem Core.Constraint.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.Constraint.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.Constraint.Evaluation.exists_lexLE_minimum {α : Type} (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: OT always picks at least one winner.

theorem Core.Constraint.Evaluation.satLE_nil (b : List ℕ) : SatLE [] b

SatLE [] b holds for any b: the empty profile vacuously satisfies the inclusion condition.

theorem Core.Constraint.Evaluation.satLE_cons_nil_iff (x : ℕ) (xs : List ℕ) : SatLE (x :: xs) [] ↔ x = 0 ∧ SatLE xs []

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

theorem Core.Constraint.Evaluation.satLE_cons_cons_iff (x y : ℕ) (xs ys : List ℕ) : SatLE (x :: xs) (y :: ys) ↔ (y ≠ 0 ∨ x = 0) ∧ SatLE xs ys

Characterization of SatLE (x :: xs) (y :: ys): if y is satisfied (zero) then x must also be satisfied, and the tails must be ordered.

theorem Core.Constraint.Evaluation.satLE_of_nil_right (a : List ℕ) : SatLE a [] → ∀ (c : List ℕ), SatLE a c

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

theorem Core.Constraint.Evaluation.satLE_trans (a b c : List ℕ) : SatLE a b → SatLE b c → SatLE a c

Satisfaction ≤ is transitive. Together with satLE_refl, this makes SatLE a preorder on violation profiles. Unlike LexLE, SatLE is NOT antisymmetric on List Nat (see satLE_not_antisymm) — it IS antisymmetric on binary {0,1} profiles, where it becomes a partial order.

theorem Core.Constraint.Evaluation.satLE_not_antisymm : ¬∀ (a b : List ℕ), SatLE a b → SatLE b a → a = b

SatLE is not antisymmetric on List Nat: non-zero values are interchangeable since SatLE only distinguishes 0 from ≥1.

@cite{blutner-2000}'s blocking relation lives at maximum generality in Core/Constraint/Superoptimal.lean as the Set-valued Blocks profile S p (Prop, decidable on Finset witnesses via Blocks.decidableOnFinset). The legacy List-based IsBlocked/blocked pair was retired at 0.230.570 in favour of the Set/Finset substrate + superoptimalSet/superoptimal API.

@cite{blutner-2000}'s superoptimality (weak BiOT, eq. 14) lives at Core/Constraint/Superoptimal.lean as the dual API:

- **`superoptimalSet pairs profile`** — Set-valued, anchored in mathlib's
  `OrderHom.gfp` over the `Set α` complete lattice. The abstract canonical
  form for structural arguments (uniqueness, ranking-invariance across
  BiOT variants, strong⊂weak meta-theorem).
- **`superoptimal pairs profile`** — Finset-native computable form,
  consumer-facing for per-paper `decide` proofs. Bridge to the abstract
  gfp via `superoptimal_coe_eq_set`.

Strong BiOT (eq. 9) is in the same file as `IsStrongOptimal` (Set-valued
Prop) + `strongOptimal` (Finset-native), with the structural
`isStrongOptimal_imp_mem_superoptimalSet` meta-theorem (Blutner p. 12)
proved coinductively against `OrderHom.gfp` — no algorithmic detour
through iterated removal.

Iterative removal (the algorithm equivalent to strong BiOT for typical
cases) is no longer formalized: `strongOptimal` IS the strong-BiOT
Finset, and `superoptimal` IS the weak-BiOT Finset. The illustrative
"iterative ≠ weak" point is captured directly by the existence of the
re-admission step in `superoptimalLoop`. 

structure Core.Constraint.Evaluation.LexProfile : Type

Violation profile ordered by lexicographic ≤ (OT harmony ordering).

Wraps List Nat so that ≤ means LexLE — the standard OT comparison where the first differing constraint determines the winner. This is a Preorder (reflexive, transitive) but not a PartialOrder on List Nat: trailing zeros are invisible (LexLE [] [0] and LexLE [0] [] both hold). For a LinearOrder on fixed-length profiles, use ViolationProfile n.

• profile : List ℕ

def Core.Constraint.Evaluation.instDecidableEqLexProfile.decEq (x✝ x✝¹ : LexProfile) : Decidable (x✝ = x✝¹)

Equations

• Core.Constraint.Evaluation.instDecidableEqLexProfile.decEq { profile := a } { profile := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableEqLexProfile : DecidableEq LexProfile

Equations

• Core.Constraint.Evaluation.instDecidableEqLexProfile = Core.Constraint.Evaluation.instDecidableEqLexProfile.decEq

def Core.Constraint.Evaluation.instReprLexProfile.repr : LexProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instReprLexProfile : Repr LexProfile

Equations

• Core.Constraint.Evaluation.instReprLexProfile = { reprPrec := Core.Constraint.Evaluation.instReprLexProfile.repr }

@[implicit_reducible]

instance Core.Constraint.Evaluation.instLELexProfile : LE LexProfile

Equations

• Core.Constraint.Evaluation.instLELexProfile = { le := fun (a b : Core.Constraint.Evaluation.LexProfile) => Core.Constraint.Evaluation.LexLE a.profile b.profile }

@[implicit_reducible]

instance Core.Constraint.Evaluation.instLTLexProfile : LT LexProfile

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instPreorderLexProfile : Preorder LexProfile

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableLeLexProfile (a b : LexProfile) : Decidable (a ≤ b)

Equations

• Core.Constraint.Evaluation.instDecidableLeLexProfile a b = Core.Constraint.Evaluation.instDecidableLexLE a.profile b.profile

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableLtLexProfile (a b : LexProfile) : Decidable (a < b)

Equations

• Core.Constraint.Evaluation.instDecidableLtLexProfile a b = instDecidableAnd

theorem Core.Constraint.Evaluation.LexProfile.le_iff (a b : LexProfile) : a ≤ b ↔ LexLE a.profile b.profile

LexProfile.≤ is definitionally LexLE.

theorem Core.Constraint.Evaluation.LexProfile.lt_iff (a b : LexProfile) : a < b ↔ LexLT a.profile b.profile

LexProfile.< is definitionally LexLT.

theorem Core.Constraint.Evaluation.LexProfile.le_total (a b : LexProfile) (h : a.profile.length = b.profile.length) : a ≤ b ∨ b ≤ a

LexLE is total on equal-length profiles, expressed via LexProfile.

structure Core.Constraint.Evaluation.SatProfile : Type

Violation profile ordered by satisfaction ≤ (Kratzer ordering).

Wraps List Nat so that ≤ means SatLE — a candidate is at least as good as another iff it satisfies every constraint the other satisfies. This is a Preorder (reflexive, transitive) but neither antisymmetric (non-zero values are interchangeable) nor total (incomparable candidates are possible).

• profile : List ℕ

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableEqSatProfile : DecidableEq SatProfile

Equations

• Core.Constraint.Evaluation.instDecidableEqSatProfile = Core.Constraint.Evaluation.instDecidableEqSatProfile.decEq

def Core.Constraint.Evaluation.instDecidableEqSatProfile.decEq (x✝ x✝¹ : SatProfile) : Decidable (x✝ = x✝¹)

Equations

• Core.Constraint.Evaluation.instDecidableEqSatProfile.decEq { profile := a } { profile := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Constraint.Evaluation.instReprSatProfile : Repr SatProfile

Equations

• Core.Constraint.Evaluation.instReprSatProfile = { reprPrec := Core.Constraint.Evaluation.instReprSatProfile.repr }

def Core.Constraint.Evaluation.instReprSatProfile.repr : SatProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instLESatProfile : LE SatProfile

Equations

• Core.Constraint.Evaluation.instLESatProfile = { le := fun (a b : Core.Constraint.Evaluation.SatProfile) => Core.Constraint.Evaluation.SatLE a.profile b.profile }

@[implicit_reducible]

instance Core.Constraint.Evaluation.instLTSatProfile : LT SatProfile

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instPreorderSatProfile : Preorder SatProfile

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableLeSatProfile (a b : SatProfile) : Decidable (a ≤ b)

Equations

• Core.Constraint.Evaluation.instDecidableLeSatProfile a b = Core.Constraint.Evaluation.instDecidableSatLE a.profile b.profile

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableLtSatProfile (a b : SatProfile) : Decidable (a < b)

Equations

• Core.Constraint.Evaluation.instDecidableLtSatProfile a b = instDecidableAnd

theorem Core.Constraint.Evaluation.SatProfile.le_iff (a b : SatProfile) : a ≤ b ↔ SatLE a.profile b.profile

SatProfile.≤ is definitionally SatLE.

theorem Core.Constraint.Evaluation.SatProfile.not_le_total : ¬∀ (a b : SatProfile), a ≤ b ∨ b ≤ a

SatLE is NOT total: incomparable candidates are possible.

@[reducible, inline]

abbrev Core.Constraint.Evaluation.ViolationProfile (n : ℕ) : Type

Fixed-length violation profile: n constraints, each recording a natural number of violations.

Defined as Lex (Fin n → Nat) — mathlib's type synonym that equips Pi-types with lexicographic ordering. The three layers of structure are:

• LinearOrder: from Pi.Lex — lexicographic comparison (min = Riggle's ⊗, choose winner)
• AddCommMonoid: componentwise addition of violation counts (Riggle's ⊎, merge violations)
• IsOrderedCancelAddMonoid: compatibility — adding violations preserves the harmony ordering (Riggle's distributivity, Dijkstra's principle)

Unlike LexProfile (which wraps List Nat and is only a Preorder), ViolationProfile n is a full LinearOrder: reflexive, transitive, antisymmetric, and total. The linear order guarantees that every non-empty candidate set has a unique minimum (= the OT winner).

Equations

• Core.Constraint.Evaluation.ViolationProfile n = Lex (Fin n → ℕ)

theorem Core.Constraint.Evaluation.ViolationProfile.add_apply {n : ℕ} (a b : ViolationProfile n) (i : Fin n) : (a + b) i = a i + b i

Pointwise addition on ViolationProfile n reduces componentwise.

theorem Core.Constraint.Evaluation.ViolationProfile.zero_apply {n : ℕ} (i : Fin n) : 0 i = 0

The zero ViolationProfile n is pointwise zero.

@[implicit_reducible]

instance Core.Constraint.Evaluation.instAddCommMonoidViolationProfile (n : ℕ) : AddCommMonoid (ViolationProfile n)

Equations

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

instance Core.Constraint.Evaluation.instIsOrderedAddMonoidViolationProfile (n : ℕ) : IsOrderedAddMonoid (ViolationProfile n)

ViolationProfile n is an ordered additive commutative monoid: componentwise addition of violations preserves the lexicographic ordering. This is @cite{riggle-2009}'s violation semiring — the AddCommMonoid is the ⊎ (merge) operation, and min from the LinearOrder is the ⊗ (choose winner) operation. Distributivity of ⊗ over ⊎ is exactly add_le_add_left.

The proof works by transferring the lex existential witness: if a < b at position i with all earlier positions equal, then a + c < b + c at the same position i (Nat addition preserves strict inequality).

instance Core.Constraint.Evaluation.instIsOrderedCancelAddMonoidViolationProfile (n : ℕ) : IsOrderedCancelAddMonoid (ViolationProfile n)

Left cancellation for lexicographic ≤: if a + b ≤ a + c then b ≤ c. This strengthens the ordered monoid to an ordered cancel monoid, which is needed for the tropical semiring derivation.

def Core.Constraint.Evaluation.vpLE (n : ℕ) : (Fin n → ℕ) → (Fin n → ℕ) → Prop

Lexicographic ≤ on Fin n → Nat, defined by recursion on n. This computable relation is the decision procedure for ≤ on ViolationProfile n (see vpLE_iff_le).

Equations

• Core.Constraint.Evaluation.vpLE 0 x_3 x_4 = True
• Core.Constraint.Evaluation.vpLE n.succ a b = (a 0 < b 0 ∨ a 0 = b 0 ∧ Core.Constraint.Evaluation.vpLE n (a ∘ Fin.succ) (b ∘ Fin.succ))

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableVpLE (n : ℕ) (a b : Fin n → ℕ) : Decidable (vpLE n a b)

Equations

• One or more equations did not get rendered due to their size.
• Core.Constraint.Evaluation.instDecidableVpLE 0 x_3 x_4 = isTrue trivial

theorem Core.Constraint.Evaluation.vpLE_iff_le {n : ℕ} (a b : ViolationProfile n) : vpLE n a b ↔ a ≤ b

Bridge theorem: vpLE is equivalent to ≤ on ViolationProfile n.

This connects the computable recursive comparison (vpLE, defined by structural recursion on n) to the algebraic LinearOrder on ViolationProfile n (derived from Pi.Lex). The bridge enables decidable ≤ on ViolationProfile n (see instDecidableVpProfileLE), which in turn makes Tableau.optimal computable.

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableVpProfileLE {n : ℕ} (a b : ViolationProfile n) : Decidable (a ≤ b)

Decidable ≤ on ViolationProfile n, via vpLE.

This makes ViolationProfile n computationally comparable despite the LinearOrder being noncomputable (from Pi.Lex). With this instance, Tableau.optimal becomes computable: study files can use by decide to verify OT winners on Tableau C n.

Equations

• Core.Constraint.Evaluation.instDecidableVpProfileLE a b = decidable_of_iff (Core.Constraint.Evaluation.vpLE n a b) ⋯

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableVpProfileLT {n : ℕ} (a b : ViolationProfile n) : Decidable (a < b)

Decidable < on ViolationProfile n, from decidable ≤.

Equations

• Core.Constraint.Evaluation.instDecidableVpProfileLT a b = decidable_of_iff (¬b ≤ a) ⋯

def Core.Constraint.Evaluation.buildViolationProfile {C : Type u_1} {n : ℕ} (constraints : Fin n → C → ℕ) (c : C) : ViolationProfile n

Build a ViolationProfile n from n constraint evaluation functions.

Given constraints as Fin n → C → Nat (constraint i evaluated on candidate c yields violation count constraints i c), produce the fixed-length violation profile for candidate c.

This is the bridge between the study-file workflow (define individual constraint functions) and the algebraic Tableau C n infrastructure.

Equations

• Core.Constraint.Evaluation.buildViolationProfile constraints c = toLex fun (i : Fin n) => constraints i c

@[implicit_reducible]

noncomputable instance Core.Constraint.Evaluation.instLinearOrderedAddCommMonoidWithTopWithTopViolationProfile (n : ℕ) : LinearOrderedAddCommMonoidWithTop (WithTop (ViolationProfile n))

WithTop (ViolationProfile n) is a LinearOrderedAddCommMonoidWithTop: it extends the ordered cancel monoid with a top element (V^∞ in Riggle's notation) that absorbs addition. This is the final prerequisite for the tropical semiring — mathlib's Tropical wrapper then gives us CommSemiring (Tropical (WithTop (ViolationProfile n))) for free.

Equations

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

def Core.Constraint.Evaluation.svpLE {n : ℕ} (a b : Fin n → ℕ) : Prop

Pointwise satisfaction ≤ on Fin n → Nat: a ≤ b iff every constraint that b satisfies (has 0 violations), a also satisfies.

This is a Preorder but not a PartialOrder: non-zero values are interchangeable (e.g., [1] ≤ [2] and [2] ≤ [1] both hold).

Equations

• Core.Constraint.Evaluation.svpLE a b = ∀ (i : Fin n), b i = 0 → a i = 0

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableSvpLE {n : ℕ} (a b : Fin n → ℕ) : Decidable (svpLE a b)

Equations

• Core.Constraint.Evaluation.instDecidableSvpLE a b = Fintype.decidableForallFintype

structure Core.Constraint.Evaluation.SatViolationProfile (n : ℕ) : Type

Fixed-length violation profile ordered by satisfaction ≤ (Kratzer ordering). a ≤ b iff a satisfies every constraint that b satisfies.

• val : Fin n → ℕ

theorem Core.Constraint.Evaluation.SatViolationProfile.ext_iff {n : ℕ} {x y : SatViolationProfile n} : x = y ↔ x.val = y.val

theorem Core.Constraint.Evaluation.SatViolationProfile.ext {n : ℕ} {x y : SatViolationProfile n} (val : x.val = y.val) : x = y

def Core.Constraint.Evaluation.instDecidableEqSatViolationProfile.decEq {n✝ : ℕ} (x✝ x✝¹ : SatViolationProfile n✝) : Decidable (x✝ = x✝¹)

Equations

• Core.Constraint.Evaluation.instDecidableEqSatViolationProfile.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableEqSatViolationProfile {n✝ : ℕ} : DecidableEq (SatViolationProfile n✝)

Equations

• Core.Constraint.Evaluation.instDecidableEqSatViolationProfile = Core.Constraint.Evaluation.instDecidableEqSatViolationProfile.decEq

@[implicit_reducible]

instance Core.Constraint.Evaluation.instLESatViolationProfile (n : ℕ) : LE (SatViolationProfile n)

Equations

• Core.Constraint.Evaluation.instLESatViolationProfile n = { le := fun (a b : Core.Constraint.Evaluation.SatViolationProfile n) => Core.Constraint.Evaluation.svpLE a.val b.val }

@[implicit_reducible]

instance Core.Constraint.Evaluation.instLTSatViolationProfile (n : ℕ) : LT (SatViolationProfile n)

Equations

• Core.Constraint.Evaluation.instLTSatViolationProfile n = { lt := fun (a b : Core.Constraint.Evaluation.SatViolationProfile n) => a ≤ b ∧ ¬b ≤ a }

@[implicit_reducible]

instance Core.Constraint.Evaluation.instPreorderSatViolationProfile (n : ℕ) : Preorder (SatViolationProfile n)

Equations

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

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableLeSatViolationProfile {n : ℕ} (a b : SatViolationProfile n) : Decidable (a ≤ b)

Equations

• Core.Constraint.Evaluation.instDecidableLeSatViolationProfile a b = Core.Constraint.Evaluation.instDecidableSvpLE a.val b.val

@[implicit_reducible]

instance Core.Constraint.Evaluation.instDecidableLtSatViolationProfile {n : ℕ} (a b : SatViolationProfile n) : Decidable (a < b)

Equations

• Core.Constraint.Evaluation.instDecidableLtSatViolationProfile a b = instDecidableAnd

structure Core.Constraint.Evaluation.Tableau (C : Type u_1) [DecidableEq C] (n : ℕ) : Type u_1

An OT tableau with n ranked constraints and candidate type C.

Uses Finset C for the candidate set (guaranteeing finiteness and deduplication) and ViolationProfile n for fixed-length profiles with decidable LinearOrder.

• candidates : Finset C
• profile : C → ViolationProfile n
• nonempty : self.candidates.Nonempty

def Core.Constraint.Evaluation.Tableau.IsOptimal {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (c : C) : Prop

A candidate is optimal iff it belongs to the candidate set and its profile is ≤ every other candidate's profile.

Equations

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

theorem Core.Constraint.Evaluation.Tableau.exists_optimal {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) : ∃ (c : C), t.IsOptimal c

Every tableau has an optimal candidate. This is the structural guarantee of OT: the LinearOrder on ViolationProfile n ensures a minimum always exists in any non-empty finite set.

Proof delegates to Finset.exists_min_image — the general fact that a linear-ordered image of a non-empty finset has a minimum.

def Core.Constraint.Evaluation.Tableau.optimal {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) : Finset C

Set of optimal candidates. Computable via instDecidableVpProfileLE: the Finset.filter tests ∀ c' ∈ candidates, profile c ≤ profile c' using the decidable ≤ on ViolationProfile n. Study files can verify OT winners with by decide on concrete tableaux.

Equations

• t.optimal = {c ∈ t.candidates | ∀ c' ∈ t.candidates, t.profile c ≤ t.profile c'}

theorem Core.Constraint.Evaluation.Tableau.mem_optimal_iff {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (c : C) : c ∈ t.optimal ↔ t.IsOptimal c

c ∈ t.optimal iff t.IsOptimal c.

theorem Core.Constraint.Evaluation.Tableau.optimal_nonempty {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) : t.optimal.Nonempty

The optimal set is always non-empty: OT always picks a winner.

theorem Core.Constraint.Evaluation.Tableau.optimal_subset {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (c : C) : c ∈ t.optimal → c ∈ t.candidates

Optimal candidates belong to the candidate set.

def Core.Constraint.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. Use this to verify properties of optimal candidates in native_decide proofs.

Equations

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

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

Check a Bool predicate for some element of a Finset.

Computable via Finset.decidableBEx — avoids noncomputable Finset.toList.

Equations

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

theorem Core.Constraint.Evaluation.ViolationProfile.le_apply_zero {n : ℕ} {a b : ViolationProfile (n + 1)} (h : a ≤ b) : a 0 ≤ b 0

If a ≤ b lexicographically, then the first component satisfies a 0 ≤ b 0. Extracting the first component is the algebraic backbone of isOptimal_zero_first: if the first constraint has 0 violations for any candidate, all optimal candidates must also have 0 violations on it.