MaxEnt → OT Limit

@cite{smolensky-legendre-2006} @cite{prince-smolensky-1993}

As the rationality parameter α → ∞, MaxEnt Harmonic Grammar recovers Optimality Theory's categorical optimization. OT is the "infinite-temperature" limit of MaxEnt.

The argument has two components:

1. HG–OT agreement (@cite{smolensky-legendre-2006} ch. 14): with exponentially separated weights, the Harmonic Grammar winner (argmax of harmony score) equals the OT winner (lexicographic comparison of violation profiles). The key: if weight wₖ exceeds M · Σᵢ₍ᵢ>ₖ₎ wᵢ (where M bounds violation counts), then a single violation difference on constraint k outweighs any combination of violations on lower-ranked constraints.

2. MaxEnt concentration (softmax_argmax_limit): as α → ∞, the MaxEnt distribution softmax(α·H) concentrates on the argmax of H — i.e., the HG winner. This is proved in Core.Agent.RationalAction.

Together: MaxEnt(α → ∞) → HG winner = OT winner.

Definitions

• otToWeighted: convert OT ranking + violation bound to weighted constraints
• LexStrictlyBetter: violation vector a lexicographically dominates b
• ExponentiallySeparated: weight separation condition for HG–OT agreement
• lex_imp_harmony: key lemma (lex dominance ⟹ higher harmony)
• maxent_ot_limit: main limit theorem

def Theories.Phonology.HarmonicGrammar.otToWeighted {C : Type} (ranking : List (Core.OT.NamedConstraint C)) (M : ℕ) : List (WeightedConstraint C)

Convert an OT constraint ranking to weighted constraints.

Each constraint at rank position i (0 = highest) receives weight (M+1)^(n−1−i), where n is the number of constraints and M is a violation count bound. This exponential spacing ensures HG–OT agreement.

The eval function is preserved: the weighted constraint evaluates candidates identically to the original named constraint.

Equations

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

theorem Theories.Phonology.HarmonicGrammar.otToWeighted_length {C : Type} (ranking : List (Core.OT.NamedConstraint C)) (M : ℕ) : (otToWeighted ranking M).length = ranking.length

The weighted constraints have the same length as the ranking.

theorem Theories.Phonology.HarmonicGrammar.otToWeighted_eval {C : Type} (ranking : List (Core.OT.NamedConstraint C)) (M : ℕ) (i : Fin ranking.length) (c : C) : ((otToWeighted ranking M).get (Fin.cast ⋯ i)).eval c = (ranking.get i).eval c

Each weighted constraint preserves the original eval function.

def Theories.Phonology.HarmonicGrammar.LexStrictlyBetter {n : ℕ} (va vb : Fin n → ℕ) : Prop

Candidate a (violation vector va) lexicographically beats candidate b (vb): at the first position where they differ, a has strictly fewer violations.

This mirrors Core.ConstraintEvaluation.lexLT but on Fin n → Nat rather than List Nat, enabling Finset-based reasoning.

Equations

• Theories.Phonology.HarmonicGrammar.LexStrictlyBetter va vb = ∃ (k : Fin n), (∀ i < k, va i = vb i) ∧ va k < vb k

def Theories.Phonology.HarmonicGrammar.ExponentiallySeparated {n : ℕ} (w : Fin n → ℚ) (M : ℕ) : Prop

Weights are exponentially separated with violation bound M: each weight exceeds M times the sum of all lower-ranked weights.

This ensures that no combination of lower-constraint violations can override a single higher-constraint violation difference, matching OT's strict ranking semantics.

Equations

• Theories.Phonology.HarmonicGrammar.ExponentiallySeparated w M = ((∀ (i : Fin n), 0 < w i) ∧ ∀ (k : Fin n), ↑M * {x : Fin n | x > k}.sum w < w k)

def Theories.Phonology.HarmonicGrammar.expWeights (n M : ℕ) : Fin n → ℚ

Concrete exponential weights: wᵢ = (M+1)^(n−1−i). Constraint 0 (highest-ranked) gets the largest weight (M+1)^(n−1).

Equations

• Theories.Phonology.HarmonicGrammar.expWeights n M i = (↑M + 1) ^ (n - 1 - ↑i)

theorem Theories.Phonology.HarmonicGrammar.expWeights_pos (n M : ℕ) (i : Fin n) : 0 < expWeights n M i

Exponential weights are positive.

theorem Theories.Phonology.HarmonicGrammar.expWeights_separated (n M : ℕ) (hM : 0 < M) : ExponentiallySeparated (expWeights n M) M

Exponential weights are exponentially separated.

def Theories.Phonology.HarmonicGrammar.Ganging (w₁ w₂ w₃ : ℚ) : Prop

Ganging: two constraints with individual weights w₁, w₂ each weaker than a third weight w₃, but jointly stronger.

This is the hallmark of weighted constraint interaction that distinguishes MaxEnt/HG from OT (@cite{hayes-wilson-2008}). In OT (strict ranking), a lower-ranked constraint can never override a higher-ranked one regardless of how many violations accumulate. In MaxEnt, constraint effects are additive, so multiple weak constraints can "gang up" to outweigh a strong one.

Equations

• Theories.Phonology.HarmonicGrammar.Ganging w₁ w₂ w₃ = (0 < w₁ ∧ 0 < w₂ ∧ 0 < w₃ ∧ w₁ < w₃ ∧ w₂ < w₃ ∧ w₃ < w₁ + w₂)

theorem Theories.Phonology.HarmonicGrammar.ganging_example : Ganging 2 2 3

Ganging is achievable: weights (2, 2, 3) exhibit ganging.

theorem Theories.Phonology.HarmonicGrammar.exponential_separation_precludes_ganging {n : ℕ} (w : Fin n → ℚ) (M : ℕ) (_hw : ExponentiallySeparated w M) (k : Fin n) : ¬Ganging ({x : Fin n | x > k}.sum w) 0 (w k)

Ganging is incompatible with exponential separation: if weights are exponentially separated, no pair of lower constraints can gang up against any higher constraint.

theorem Theories.Phonology.HarmonicGrammar.no_ganging_when_separated {n : ℕ} (w : Fin n → ℚ) (hw : ExponentiallySeparated w 1) (k : Fin n) : {x : Fin n | x > k}.sum w < w k

With exponentially separated weights (M = 1), each constraint outweighs the total of all lower weights.

def Theories.Phonology.HarmonicGrammar.weightedViolations {n : ℕ} (w : Fin n → ℚ) (v : Fin n → ℕ) : ℚ

Weighted violation sum (the positive part of harmony: harmonyScore = -weightedViolations).

Equations

• Theories.Phonology.HarmonicGrammar.weightedViolations w v = ∑ i : Fin n, w i * ↑(v i)

theorem Theories.Phonology.HarmonicGrammar.lex_imp_lower_violations {n : ℕ} (w : Fin n → ℚ) (M : ℕ) (va vb : Fin n → ℕ) (hM : ∀ (i : Fin n), va i ≤ M ∧ vb i ≤ M) (hw : ExponentiallySeparated w M) (hlex : LexStrictlyBetter va vb) : weightedViolations w va < weightedViolations w vb

HG–OT agreement lemma (@cite{smolensky-legendre-2006}): with exponentially separated weights and bounded violations, lexicographic dominance implies strictly lower weighted violations.

Since harmonyScore = -weightedViolations, this means the lexicographically better candidate has strictly higher harmony.

Proof sketch: decompose the violation-difference sum at the first differing position k.

• For i < k: terms cancel (va(i) = vb(i) by hlex)
• At i = k: wₖ · (vb(k) − va(k)) ≥ wₖ (since vb(k) > va(k))
• For i > k: |wᵢ · (vb(i) − va(i))| ≤ wᵢ · M (by hM)
• Net: ≥ wₖ − M · Σᵢ₍ᵢ>ₖ₎ wᵢ > 0 (by hw)

theorem Theories.Phonology.HarmonicGrammar.ot_lex_imp_higher_harmony {C : Type} (ranking : List (Core.OT.NamedConstraint C)) (M : ℕ) (hM : 0 < M) (a b : C) (hbound : ∀ con ∈ ranking, con.eval a ≤ M ∧ con.eval b ≤ M) (hlex : LexStrictlyBetter (fun (i : Fin ranking.length) => (ranking.get i).eval a) fun (i : Fin ranking.length) => (ranking.get i).eval b) : harmonyScoreR (otToWeighted ranking M) a > harmonyScoreR (otToWeighted ranking M) b

HG–OT agreement for a concrete candidate type: if candidate a lexicographically beats b on the violation profile induced by ranking, then a has strictly higher harmony under otToWeighted ranking M, provided M bounds all violation counts.

theorem Theories.Phonology.HarmonicGrammar.maxent_concentrates_on_hg_winner {C : Type} [Fintype C] [Nonempty C] [DecidableEq C] (constraints : List (WeightedConstraint C)) (c_opt : C) (h_opt : ∀ (c : C), c ≠ c_opt → harmonyScoreR constraints c < harmonyScoreR constraints c_opt) (ε : ℝ) : ε > 0 → ∃ (α₀ : ℝ), ∀ α > α₀, |Core.softmax (harmonyScoreR constraints) α c_opt - 1| < ε

MaxEnt concentration on HG winner: as α → ∞, MaxEnt probability concentrates on the candidate with the highest harmony score.

This is softmax_argmax_limit instantiated with harmony scores. The interesting content is in the hypotheses: showing that the HG winner equals the OT winner (§4).

theorem Theories.Phonology.HarmonicGrammar.maxent_ot_limit {C : Type} [Fintype C] [Nonempty C] [DecidableEq C] (ranking : List (Core.OT.NamedConstraint C)) (M : ℕ) (hM : 0 < M) (c_opt : C) (hbound : ∀ (c : C), ∀ con ∈ ranking, con.eval c ≤ M) (hlex : ∀ (c : C), c ≠ c_opt → LexStrictlyBetter (fun (i : Fin ranking.length) => (ranking.get i).eval c_opt) fun (i : Fin ranking.length) => (ranking.get i).eval c) (ε : ℝ) : ε > 0 → ∃ (α₀ : ℝ), ∀ α > α₀, |Core.softmax (harmonyScoreR (otToWeighted ranking M)) α c_opt - 1| < ε

MaxEnt → OT limit (@cite{smolensky-legendre-2006}): as α → ∞, MaxEnt probability concentrates on the OT winner.

Given a constraint ranking with violation bound M and a candidate c_opt that lexicographically beats all competitors, the MaxEnt probability softmax(α · H)(c_opt) → 1 as α → ∞.

The proof combines:

1. ot_lex_imp_higher_harmony: lex-better ⟹ higher harmony (HG–OT agreement)
2. softmax_argmax_limit: MaxEnt concentrates on harmony maximizer