pairCostAfterLove
plain-language theorem explainer
pairCostAfterLove defines the system cost after the Love operator averages two recognition states σ₁ and σ₂ as twice the hyperbolic cosine of their mean minus one. Ethics researchers in Recognition Science cite it when proving Love reaches the ground state for balanced extraction pairs. The definition substitutes the averaged state directly into the J-cost formula.
Claim. For recognition states σ₁ and σ₂ the cost after the Love operator equals 2( cosh((σ₁ + σ₂)/2) - 1 ).
background
Recognition Science sets the cost of any recognition event to its J-cost, J(σ) = cosh(σ) - 1, which is nonnegative and zero only at the identity state σ = 1. The module examines thermodynamic instability of extraction under the Love operator that averages states. Upstream results establish that cost equals the derived cost from the multiplicative recognizer comparator and that the identity event has zero cost.
proof idea
This is a direct definition that inserts the arithmetic mean of σ₁ and σ₂ into the hyperbolic-cosine expression for J-cost. No lemmas are invoked beyond the standard definition of cosh.
why it matters
It underpins love_achieves_ground_state and love_eliminates_all_waste, which show Love maps balanced pairs to zero cost and removes all thermodynamic waste. The definition supports the Love-Jensen inequality and illustrates J-uniqueness (T5) by making unequal states thermodynamically unstable under averaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.