pairSystemCost

formal source

 208-/
 209
 210/-- System cost for a pair of agents at positions σ₁ and σ₂. -/
 211def pairSystemCost (σ₁ σ₂ : ℝ) : ℝ :=
 212  (Real.cosh σ₁ - 1) + (Real.cosh σ₂ - 1)
 213
 214/-- System cost after the Love operator averages σ₁ and σ₂. -/
 215def pairCostAfterLove (σ₁ σ₂ : ℝ) : ℝ :=
 216  2 * (Real.cosh ((σ₁ + σ₂) / 2) - 1)
 217
 218/-- **Theorem (Love-Jensen Inequality)**: Love never increases system cost.
 219    Proof uses the d'Alembert identity + cosh ≥ 1. -/
 220theorem love_jensen_inequality (σ₁ σ₂ : ℝ) :
 221    pairCostAfterLove σ₁ σ₂ ≤ pairSystemCost σ₁ σ₂ := by
 222  unfold pairSystemCost pairCostAfterLove
 223  have h := cosh_sum_via_dAlembert σ₁ σ₂
 224  have h_ge_1 : 1 ≤ Real.cosh ((σ₁ - σ₂) / 2) := by
 225    rcases eq_or_ne ((σ₁ - σ₂) / 2) 0 with h0 | h0
 226    · rw [h0, Real.cosh_zero]
 227    · exact le_of_lt (Real.one_lt_cosh.mpr h0)
 228  have h_pos : 0 < Real.cosh ((σ₁ + σ₂) / 2) := Real.cosh_pos _
 229  nlinarith
 230
 231/-- **Theorem (Love-Jensen Strict)**: Love STRICTLY reduces system cost when
 232    agents have different σ. This is the fundamental result: selfishness
 233    (σ₁ ≠ σ₂) is thermodynamically unstable under Love. -/
 234theorem love_jensen_strict (σ₁ σ₂ : ℝ) (h_diff : σ₁ ≠ σ₂) :
 235    pairCostAfterLove σ₁ σ₂ < pairSystemCost σ₁ σ₂ := by
 236  unfold pairSystemCost pairCostAfterLove
 237  have h := cosh_sum_via_dAlembert σ₁ σ₂
 238  have h_ne : (σ₁ - σ₂) / 2 ≠ 0 := by
 239    intro heq; exact h_diff (by linarith)
 240  have h_gt_1 : 1 < Real.cosh ((σ₁ - σ₂) / 2) := Real.one_lt_cosh.mpr h_ne
 241  have h_pos : 0 < Real.cosh ((σ₁ + σ₂) / 2) := Real.cosh_pos _