MaxEnt → OT Limit

[SL06] [PS93]

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 ([SL06] 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

• expWeights: exponential weight vector for an OT ranking + violation bound
• ExponentiallySeparated: weight separation condition for HG–OT agreement
• ot_lex_imp_higher_harmony: key lemma (lex dominance ⟹ higher harmony)
• maxent_ot_limit: main limit theorem

OT → HG weights

An OT ranking is a List (Constraint C); as a CON C ranking.length it is just ranking.get. The Harmonic-Grammar reading of that ranking with violation bound M weights coordinate i (0 = highest) by (M+1)^(n−1−i) — the expWeights vector below. So the HG harmony of an OT ranking is harmonyScore ranking.get (expWeights ranking.length M), with no separate weighted-constraint object.

Exponentially separated weights

def 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

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

def 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

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

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

Exponential weights are positive.

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

Exponential weights are exponentially separated.

Ganging (complement of exponential separation)

def 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 ([HW08]). 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

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

theorem HarmonicGrammar.ganging_example : Ganging 2 2 3

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

theorem 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.

theorem HarmonicGrammar.exponential_separation_precludes_ganging {n : ℕ} (w : Fin n → ℝ) (hw : ExponentiallySeparated w 1) (k i j : Fin n) (hi : k < i) (hj : k < j) (hij : i ≠ j) : ¬Ganging (w i) (w j) (w k)

Ganging is precluded by exponential separation: with exponentially separated weights (M = 1), no two distinct lower-ranked constraints i, j can gang up against a higher-ranked k. Their combined weight is at most the total lower weight, which no_ganging_when_separated bounds strictly below w k — contradicting ganging's w k < w i + w j.

HG–OT agreement

theorem 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 : toLex va < toLex vb) : Constraints.weightedViolations w va < Constraints.weightedViolations w vb

HG–OT agreement lemma ([SL06]): 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 HarmonicGrammar.ot_lex_imp_higher_harmony {C : Type u_1} (ranking : List (Constraints.Constraint C)) (M : ℕ) (hM : 0 < M) (a b : C) (hbound : ∀ con ∈ ranking, con a ≤ M ∧ con b ≤ M) (hlex : (toLex fun (i : Fin ranking.length) => ranking.get i a) < toLex fun (i : Fin ranking.length) => ranking.get i b) : Constraints.harmonyScore ranking.get (expWeights ranking.length M) a > Constraints.harmonyScore ranking.get (expWeights ranking.length 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 than b under the ranking's exponential weights expWeights ranking.length M, provided M bounds all violations. With harmonyScore con w c = -weightedViolations w (· c), the bridge to lex_imp_lower_violations is definitional.

MaxEnt → OT limit

theorem HarmonicGrammar.maxent_concentrates_on_hg_winner {C : Type u_1} [Fintype C] [Nonempty C] [DecidableEq C] {n : ℕ} (con : Constraints.CON C n) (w : Fin n → ℝ) (c_opt : C) (h_opt : ∀ (c : C), c ≠ c_opt → Constraints.harmonyScore con w c < Constraints.harmonyScore con w c_opt) : Filter.Tendsto (fun (α : ℝ) => Core.softmax (α • Constraints.harmonyScore con w) c_opt) Filter.atTop (nhds 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 HarmonicGrammar.maxent_ot_limit {C : Type u_1} [Fintype C] [Nonempty C] [DecidableEq C] (ranking : List (Constraints.Constraint C)) (M : ℕ) (hM : 0 < M) (c_opt : C) (hbound : ∀ (c : C), ∀ con ∈ ranking, con c ≤ M) (hlex : ∀ (c : C), c ≠ c_opt → (toLex fun (i : Fin ranking.length) => ranking.get i c_opt) < toLex fun (i : Fin ranking.length) => ranking.get i c) : Filter.Tendsto (fun (α : ℝ) => Core.softmax (α • Constraints.harmonyScore ranking.get (expWeights ranking.length M)) c_opt) Filter.atTop (nhds 1)

MaxEnt → OT limit ([SL06]): 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, Tendsto (softmax (α • H) c_opt) atTop (𝓝 1).

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