love_jensen_strict
plain-language theorem explainer
The theorem shows that for real numbers σ₁ ≠ σ₂ the cost after Love averaging is strictly smaller than the original pair cost expressed via cosh. Researchers modeling interaction costs or thermodynamic ethics would cite it to establish instability of asymmetric extraction states. The tactic proof unfolds the two cost definitions, invokes the d'Alembert cosh-sum identity, and finishes with positivity of cosh together with nlinarith.
Claim. Let σ₁, σ₂ ∈ ℝ satisfy σ₁ ≠ σ₂. Then 2(ℝ.cosh((σ₁ + σ₂)/2) − 1) < (ℝ.cosh σ₁ − 1) + (ℝ.cosh σ₂ − 1).
background
The module defines pairSystemCost(σ₁, σ₂) as the sum of individual costs (cosh σ₁ − 1) + (cosh σ₂ − 1) and pairCostAfterLove as the cost after replacing the pair by their arithmetic mean, 2(cosh((σ₁ + σ₂)/2) − 1). These functionals descend from the cost map induced by a multiplicative recognizer. The supporting identity cosh α + cosh β = 2 cosh((α + β)/2) cosh((α − β)/2) is supplied by the upstream theorem cosh_sum_via_dAlembert.
proof idea
Unfold both cost definitions. Apply cosh_sum_via_dAlembert to rewrite the right-hand side as 2 cosh m ⋅ cosh d with m = (σ₁ + σ₂)/2 and d = (σ₁ − σ₂)/2. Use the hypothesis σ₁ ≠ σ₂ to obtain d ≠ 0, hence cosh d > 1 by one_lt_cosh, while cosh m > 0 by cosh_pos. Conclude the strict inequality by nlinarith.
why it matters
This strict inequality is the central result of the module, showing that Love forces a strict cost reduction precisely when agents differ, thereby rendering selfish extraction thermodynamically unstable. It strengthens the non-strict Love-Jensen inequality proved earlier in the same file and supplies the key step toward extraction_unique_equilibrium and extraction_cost_strict_minimum. In the Recognition framework it illustrates how the J-cost (realized here by cosh) drives convergence to the zero-cost ground state under the Love operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.