Violation Semiring — OT/HG Unification

[Rig09b]

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 [Rig09b])

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 ([SL06], formalized in HarmonicGrammar.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."

The Violation Semiring V

@[reducible, inline]

abbrev HarmonicGrammar.ViolationSemiring.VS (n : ℕ) : Type

The violation semiring ([Rig09b] 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

• HarmonicGrammar.ViolationSemiring.VS n = Tropical (WithTop (Constraints.ViolationProfile n))

@[implicit_reducible]

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

The violation semiring is a commutative semiring.

Equations

• HarmonicGrammar.ViolationSemiring.instCommSemiringVS n = inferInstance

Monotonicity — Dijkstra's Principle

theorem HarmonicGrammar.ViolationSemiring.merge_monotone (n : ℕ) (a b : Constraints.ViolationProfile n) : a ≤ a + b

Dijkstra's principle for violation profiles ([Rig09b] §4, [Dij59]): 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 (min_self). An idempotent ⊕ together with a monotone ⊗ make the violation semiring an idempotent semiring (dioid) — the structure that makes shortest-path algorithms applicable to OT optimization: "every piece of an optimal input–output mapping is itself an optimal mapping."

Weight Map V → ℝ (AddMonoidHom)

def HarmonicGrammar.ViolationSemiring.weightMap {n : ℕ} (w : Fin n → ℝ) : Constraints.ViolationProfile n →+ ℝ

The weight map ([Rig09b] §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

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

Bridge to Existing HG Code

theorem HarmonicGrammar.ViolationSemiring.weightMap_eq_weightedViolations {n : ℕ} (w : Fin n → ℝ) (v : Constraints.ViolationProfile n) : (weightMap w) v = Constraints.weightedViolations w v

weightMap is definitionally equal to weightedViolations from HarmonicGrammar.OTLimit.

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

Order-Preservation (⊕-compatibility)

theorem HarmonicGrammar.ViolationSemiring.weightMap_strictMono {n : ℕ} (w : Fin n → ℝ) (M : ℕ) (hw : ExponentiallySeparated w M) (a b : Constraints.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 ([Rig09b] §4, [SL06] 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 is stated over < on ViolationProfile directly.

theorem HarmonicGrammar.ViolationSemiring.weightMap_mono {n : ℕ} (w : Fin n → ℝ) (M : ℕ) (hw : ExponentiallySeparated w M) (a b : Constraints.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 HarmonicGrammar.ViolationSemiring.weightMap_preserves_minimum {n : ℕ} (w : Fin n → ℝ) (M : ℕ) (hw : ExponentiallySeparated w M) (a : Constraints.ViolationProfile n) (S : Finset (Constraints.ViolationProfile n)) (ha : a ∈ S) (hmin : ∀ b ∈ S, a ≤ b) (hM : ∀ b ∈ S, ∀ (i : Fin n), b i ≤ M) (b : Constraints.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 ⊕.