theorem
proved
tactic proof
love_jensen_strict
show as:
view Lean formalization →
formal statement (Lean)
234theorem love_jensen_strict (σ₁ σ₂ : ℝ) (h_diff : σ₁ ≠ σ₂) :
235 pairCostAfterLove σ₁ σ₂ < pairSystemCost σ₁ σ₂ := by
proof body
Tactic-mode proof.
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 _
242 nlinarith
243
244/-- **Theorem (Love Achieves Ground State)**: For a balanced extraction pair
245 (σ, −σ), Love maps both agents to σ = 0, achieving zero cost. -/