cosh_sum_via_dAlembert
plain-language theorem explainer
The identity decomposes the sum of coshines evaluated at α and β into a product of coshes at their average and half-difference. Researchers modeling cost minimization under the Love operator in recognition ethics cite it to derive Jensen inequalities for pair system costs. The proof is a direct wrapper that applies the upstream d'Alembert sum identity to the averaged arguments and recovers the originals by ring arithmetic.
Claim. For all real numbers $α, β$, $cosh α + cosh β = 2 cosh((α + β)/2) cosh((α - β)/2)$.
background
This theorem belongs to the module on thermodynamic instability of extraction, which treats agent states σ as positions on the real line whose J-cost is induced by the Recognition Composition Law. The upstream dAlembert_cosh_sum states that cosh(a + b) + cosh(a - b) = 2 cosh a cosh b and is obtained from Jcost_cosh_add_identity after substituting the definition Jcost_G_eq_cosh_sub_one. The Love operator is defined to replace a pair (σ₁, σ₂) by their average m = (σ₁ + σ₂)/2, and the present identity supplies the algebraic step needed to compare total cost before and after averaging.
proof idea
The proof invokes dAlembert_cosh_sum on the arguments ((α + β)/2, (α - β)/2). It then applies the ring tactic twice to establish the two linear identities that recover α and β from those averaged arguments, after which substitution yields the target equality.
why it matters
The result is the immediate prerequisite for love_jensen_inequality and love_jensen_strict, which together establish that the Love operator never increases and strictly decreases pair system cost whenever the agents' states differ. It therefore supplies the analytic content for the claim that selfishness is thermodynamically unstable under the Recognition Composition Law. The identity inherits its validity from the same functional equation that forces the cosh form of the cost function throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.