Violation Semiring — OT/HG Unification

@cite{riggle-2009}

OT and HG are instances of a single algebraic framework: evaluation over a commutative semiring. Violation profiles form a commutative semiring V (the violation semiring); real-valued costs form the standard tropical semiring T. HG weights define a structure-preserving map from V to T.

The two semirings (Example 2 of @cite{riggle-2009})

V = Tropical (WithTop (ViolationProfile n)) — the violation semiring:

• ⊕ (tropical addition) = min under harmonic inequality (choose winner)
• ⊗ (tropical multiplication) = componentwise + (merge violations)
• 0̃ = ⊤ (V^∞ — the infinitely bad candidate, additive identity for min)
• 1̃ = zero profile (∅ — the perfect candidate, multiplicative identity)

T = Tropical (WithTop ℚ≥0) — the tropical semiring:

• ⊕ = min of costs (choose winner)
• ⊗ = + of costs (merge costs)
• 0̃ = ∞ (infinitely bad, identity for min)
• 1̃ = 0 (no cost, identity for +)

OT evaluates in V; HG evaluates in T. The weight assignment w : Fin n → ℚ induces a map V → T via the weighted sum v ↦ Σ wᵢ · vᵢ. This map always preserves ⊗ (merge/tropical multiplication — linearity of the dot product). It preserves ⊕ (min/tropical addition) when weights are exponentially separated — which is exactly the content of the HG–OT agreement theorem (@cite{smolensky-legendre-2006}, formalized in Core.Constraint.OTLimit).

Monotonicity (Dijkstra's Principle)

In both V and T, merging violations can only make things worse: ∀ a b, a ≤ a ⊎ b. This is the property that makes shortest-path algorithms applicable to OT optimization. Riggle: "every subpath of an optimal input–output mapping is itself an optimal mapping."

@[reducible, inline]

abbrev Core.Constraint.ViolationSemiring.VS (n : ℕ) : Type

The violation semiring (@cite{riggle-2009} Definition 2, Example 2): Tropical (WithTop (ViolationProfile n)) for n ranked constraints.

Tropical addition (⊕) is min under harmonic inequality. Tropical multiplication (⊗) is componentwise violation addition. The semiring structure is derived, not stipulated: ViolationProfile n = Lex (Fin n → Nat) carries LinearOrder (from Pi.Lex), AddCommMonoid (componentwise), and IsOrderedCancelAddMonoid, and mathlib's Tropical/WithTop wrappers do the rest.

Equations

• Core.Constraint.ViolationSemiring.VS n = Tropical (WithTop (Core.Constraint.Evaluation.ViolationProfile n))

@[implicit_reducible]

noncomputable instance Core.Constraint.ViolationSemiring.instCommSemiringVS (n : ℕ) : CommSemiring (VS n)

The violation semiring is a commutative semiring.

Equations

• Core.Constraint.ViolationSemiring.instCommSemiringVS n = inferInstance

theorem Core.Constraint.ViolationSemiring.ViolationProfile.zero_le (n : ℕ) (a : Evaluation.ViolationProfile n) : 0 ≤ a

The zero-violations profile is the bottom element: no violations is at least as harmonic as any profile.

Proof: a < 0 would require a i < 0 for some i, which is impossible since a i : Nat. So ¬(a < 0), hence 0 ≤ a.

theorem Core.Constraint.ViolationSemiring.merge_monotone (n : ℕ) (a b : Evaluation.ViolationProfile n) : a ≤ a + b

Dijkstra's principle for violation profiles (@cite{riggle-2009} §4, @cite{dijkstra-1959}): merging violations can only make things worse (or keep them equal).

In Riggle's terms: the ⊎ (merge) operator is monotone — A ⊎ B ≥ A for all violation profiles A, B. Equivalently, the ⊗ (min) operator is idempotent — A ⊗ A = A.

This is the structural property that makes shortest-path algorithms applicable to OT optimization: "every piece of an optimal input–output mapping is itself an optimal mapping."

def Core.Constraint.ViolationSemiring.weightMap {n : ℕ} (w : Fin n → ℚ) : Evaluation.ViolationProfile n →+ ℚ

The weight map (@cite{riggle-2009} §4): an additive monoid homomorphism from the violation semiring's underlying monoid (ViolationProfile n, +, 0) to (ℚ, +, 0).

Given weights w : Fin n → ℚ, the weight map sends a violation profile v to the weighted sum Σ wᵢ · vᵢ. This is the function that maps V to T — the violation semiring to the tropical semiring.

Bundling as AddMonoidHom makes the homomorphism property (weight(a ⊎ b) = weight(a) + weight(b)) structural rather than propositional, and unlocks mathlib's homomorphism lemmas (map_sum, map_nsmul, etc.).

Equivalently, this says the weight map preserves tropical multiplication (⊗) from V to T — always true by linearity of the dot product, regardless of weight magnitudes. The interesting condition (exponential separation) is needed for preserving tropical addition (⊕ = min) — see weightMap_strictMono.

Equations

• Core.Constraint.ViolationSemiring.weightMap w = { toFun := fun (v : Core.Constraint.Evaluation.ViolationProfile n) => ∑ i : Fin n, w i * ↑(v i), map_zero' := ⋯, map_add' := ⋯ }

@[reducible, inline]

abbrev Core.Constraint.ViolationSemiring.weightedSum {n : ℕ} (w : Fin n → ℚ) (v : Evaluation.ViolationProfile n) : ℚ

Convenience alias: weightedSum w v = weightMap w v.

Equations

• Core.Constraint.ViolationSemiring.weightedSum w v = (Core.Constraint.ViolationSemiring.weightMap w) v

theorem Core.Constraint.ViolationSemiring.weightMap_eq_weightedViolations {n : ℕ} (w : Fin n → ℚ) (v : Evaluation.ViolationProfile n) : (weightMap w) v = weightedViolations w v

weightMap is definitionally equal to weightedViolations from Core.Constraint.OTLimit.

This bridges the semiring-theoretic framework (violation profiles as algebraic objects) to the existing HG–OT agreement machinery (violation vectors as functions).

theorem Core.Constraint.ViolationSemiring.lt_iff_lexStrictlyBetter {n : ℕ} (a b : Evaluation.ViolationProfile n) : a < b ↔ LexStrictlyBetter a b

LexStrictlyBetter from OTLimit.lean is definitionally equal to < on ViolationProfile n — they are both ∃ k, (∀ j < k, a j = b j) ∧ a k < b k.

This bridges the HG–OT agreement literature's vocabulary (LexStrictlyBetter) to the algebraic ordering on ViolationProfile.

theorem Core.Constraint.ViolationSemiring.weightMap_strictMono {n : ℕ} (w : Fin n → ℚ) (M : ℕ) (hw : ExponentiallySeparated w M) (a b : Evaluation.ViolationProfile n) (hM : ∀ (i : Fin n), a i ≤ M ∧ b i ≤ M) (hab : a < b) : (weightMap w) a < (weightMap w) b

The weight map is strictly order-preserving when weights are exponentially separated (@cite{riggle-2009} §4, @cite{smolensky-legendre-2006} ch. 14):

If a < b lexicographically and all violations are bounded by M, then weight(a) < weight(b).

In tropical semiring terms: the weight map preserves tropical addition (⊕ = min) — it maps the lex-minimum in V to the numerical minimum in T. This is the content that exponential separation buys: the weight map is not just a monoid homomorphism (preserves ⊗ always, § 3) but an order-preserving monoid homomorphism (preserves ⊕ conditionally).

The proof delegates to lex_imp_lower_violations from OTLimit.lean, which we can invoke directly because LexStrictlyBetter is definitionally equal to < on ViolationProfile n.

theorem Core.Constraint.ViolationSemiring.weightMap_mono {n : ℕ} (w : Fin n → ℚ) (M : ℕ) (hw : ExponentiallySeparated w M) (a b : Evaluation.ViolationProfile n) (hM : ∀ (i : Fin n), a i ≤ M ∧ b i ≤ M) (hab : a ≤ b) : (weightMap w) a ≤ (weightMap w) b

Non-strict monotonicity: a ≤ b lexicographically implies weight(a) ≤ weight(b) under exponential separation.

theorem Core.Constraint.ViolationSemiring.weightMap_preserves_minimum {n : ℕ} (w : Fin n → ℚ) (M : ℕ) (hw : ExponentiallySeparated w M) (a : Evaluation.ViolationProfile n) (S : Finset (Evaluation.ViolationProfile n)) (ha : a ∈ S) (hmin : ∀ b ∈ S, a ≤ b) (hM : ∀ b ∈ S, ∀ (i : Fin n), b i ≤ M) (b : Evaluation.ViolationProfile n) : b ∈ S → (weightMap w) a ≤ (weightMap w) b

The lex-minimum of a candidate set maps to the weight-minimum: the OT winner and HG winner coincide under exponential separation.

This is the semiring-theoretic restatement of HG–OT agreement: argmin_V ↦ argmin_T when the weight map preserves both ⊗ and ⊕.