love_jensen_inequality
plain-language theorem explainer
The Love-Jensen inequality shows that replacing two agents' recognition parameters σ₁ and σ₂ by their average via the Love operator produces a pair cost no larger than the original sum of individual costs. Researchers deriving equilibrium conditions or thermodynamic stability in multi-agent recognition models would cite it. The proof unfolds the two cost definitions, invokes the d'Alembert identity for cosh, and closes with the elementary bounds cosh ≥ 1 and cosh > 0 via nlinarith.
Claim. For real numbers σ₁, σ₂ the averaged cost satisfies $2( cosh( (σ₁ + σ₂)/2 ) - 1 ) ≤ ( cosh σ₁ - 1 ) + ( cosh σ₂ - 1 )$.
background
In the Ethics.ThermodynamicInstabilityOfExtraction module, pairSystemCost(σ₁, σ₂) is defined as the sum of individual J-costs (cosh σᵢ - 1). The Love operator produces pairCostAfterLove(σ₁, σ₂) = 2(cosh((σ₁ + σ₂)/2) - 1), which replaces the pair by a single averaged state. These definitions rest on the cost function imported from MultiplicativeRecognizerL4 and ObserverForcing, where cost is the J-cost of a recognition event.
proof idea
The proof unfolds both pair-cost definitions, applies the upstream lemma cosh_sum_via_dAlembert to obtain the product decomposition of cosh σ₁ + cosh σ₂, then proves cosh((σ₁ - σ₂)/2) ≥ 1 by case analysis on the difference and cosh((σ₁ + σ₂)/2) > 0 by the standard positivity fact. The desired inequality follows by algebraic rearrangement and nlinarith.
why it matters
This is the central result of the module: Love never increases system cost, so selfish configurations (σ₁ ≠ σ₂) are thermodynamically unstable. It supplies the key inequality used to establish strict convexity, unique equilibrium, and minimum-at-zero properties for extraction costs in the same module. Within Recognition Science it instantiates J-cost non-increase under the composition law and aligns with the non-negativity of costs derived from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.