Maslov Dequantization: lse α → max as α → ∞

@cite{litvinov-2005} @cite{maslov-1992}

The defining limit of the warped (log-sum-exp) semiring: as the inverse temperature α → ∞, log-sum-exp deforms to max-plus.

  lse α a b  =  (1/α) · log(exp(α·a) + exp(α·b))  ──α → ∞──→  max a b

This is Maslov dequantization (@cite{litvinov-2005}): a one-parameter family of commutative semirings on ℝ — the Maslov / "warped" semirings — that deforms continuously to the max-plus (tropical) semiring as the temperature parameter sweeps to its limit. The name "dequantization" emphasises the analogy with the classical limit of quantum mechanics: the smooth, fluctuation-tolerant semiring becomes a sharp, "winner takes all" semiring.

For us, the linguistic content is the bridge from MaxEnt (soft / gradient) constraint frameworks to HG (deterministic / gradient) — and, composed with the existing exponential-separation bridge V → T from ViolationSemiring.lean, the bridge from MaxEnt all the way to OT (deterministic / categorical). See Constraint/Deformation.lean for the linguistic-theoretic packaging.

Proof outline

WLOG b ≤ a. The factorization

  lse α a b  =  a + (1/α) · log(1 + exp(α · (b - a)))

isolates the "winner score" a from a non-negative correction term. The correction is bounded between 0 (when b ≪ a, the loser contributes nothing) and (log 2) / α (when b = a, the loser contributes a tied share). Both bounds tend to 0 as α → ∞, so the correction tends to 0 by the squeeze theorem, and lse α a b → a = max a b.

theorem Core.Constraint.lse_eq_max_plus_correction (α : ℝ) (hα : 0 < α) (a b : ℝ) : lse α a b = a + 1 / α * Real.log (1 + Real.exp (α * (b - a)))

Factorization of lse. Extracting exp(α·a) from the partition function gives

  lse α a b  =  a  +  (1/α) · log(1 + exp(α · (b - a)))

Holds for arbitrary a, b (the identity is pure algebra), but is most useful when b ≤ a: then a = max a b and the second term is a non-negative "correction" that vanishes as α → ∞.

theorem Core.Constraint.correction_nonneg (α : ℝ) (hα : 0 < α) (a b : ℝ) : 0 ≤ 1 / α * Real.log (1 + Real.exp (α * (b - a)))

The correction term (1/α) · log(1 + exp(α · (b - a))) is non-negative for α > 0.

theorem Core.Constraint.correction_le_log2_div (α : ℝ) (hα : 0 < α) (a b : ℝ) (hab : b ≤ a) : 1 / α * Real.log (1 + Real.exp (α * (b - a))) ≤ Real.log 2 / α

The correction term is bounded above by (log 2) / α when b ≤ a and α > 0. (At b = a the loser contributes a tied share log 2.)

theorem Core.Constraint.correction_tendsto_zero (a b : ℝ) (hab : b ≤ a) : Filter.Tendsto (fun (α : ℝ) => 1 / α * Real.log (1 + Real.exp (α * (b - a)))) Filter.atTop (nhds 0)

The correction term tends to 0 as α → ∞.

Proof: for α > 0, the correction is sandwiched in [0, (log 2)/α] by correction_nonneg and correction_le_log2_div; both bounds tend to 0 (the upper bound by tendsto_inv_atTop_zero scaled by the constant log 2).

theorem Core.Constraint.lse_tendsto_max (a b : ℝ) : Filter.Tendsto (fun (α : ℝ) => lse α a b) Filter.atTop (nhds (max a b))

Maslov dequantization (binary case). As α → ∞, lse α a b → max a b.

Equivalently: the warped semiring (ℝ, lse α, +) deforms to the max-plus (tropical) semiring (ℝ, max, +) as α → ∞.

The Finset analogue of lse_tendsto_max. The strategy is the same sandwich, generalised to n candidates: the partition function is bounded above by card · exp(α · max) and below by exp(α · max), so lseFinset α cands score lies in [max, max + log(card)/α], both bounds collapsing to max as α → ∞.

theorem Core.Constraint.sup'_le_lseFinset {Cand : Type u_1} {cands : Finset Cand} (hne : cands.Nonempty) (α : ℝ) (hα : 0 < α) (score : Cand → ℝ) : cands.sup' hne score ≤ lseFinset α cands score

Lower bound: cands.sup' hne score ≤ lseFinset α cands score for α > 0.

The maximum score is achieved at some c_max ∈ cands (since cands is non-empty), so exp(α · max) ≤ Σ exp(α · score c'), and taking (1/α) · log of both sides preserves the inequality (α > 0).

theorem Core.Constraint.lseFinset_le_sup'_add {Cand : Type u_1} {cands : Finset Cand} (hne : cands.Nonempty) (α : ℝ) (hα : 0 < α) (score : Cand → ℝ) : lseFinset α cands score ≤ cands.sup' hne score + Real.log ↑cands.card / α

Upper bound: lseFinset α cands score ≤ cands.sup' hne score + log(card)/α for α > 0.

Each summand exp(α · score c') ≤ exp(α · max) (since score c' ≤ max and α ≥ 0), so Σ exp(α · score c') ≤ card · exp(α · max). Take (1/α) · log and split the log of a product.

theorem Core.Constraint.lseFinset_tendsto_sup' {Cand : Type u_1} {cands : Finset Cand} (hne : cands.Nonempty) (score : Cand → ℝ) : Filter.Tendsto (fun (α : ℝ) => lseFinset α cands score) Filter.atTop (nhds (cands.sup' hne score))

Maslov dequantization (n-ary case). As α → ∞, lseFinset α cands score → cands.sup' hne score.

Sandwich proof: by sup'_le_lseFinset and lseFinset_le_sup'_add, the value lies in [sup', sup' + log(card)/α] for α > 0; both bounds tend to sup' because log(card)/α → 0.