pairSystemCost
plain-language theorem explainer
System cost for a pair of agents at positions σ₁ and σ₂ is the sum of their individual J-costs, each expressed as cosh(σ) - 1. Researchers analyzing thermodynamic ethics in Recognition Science cite this when quantifying waste eliminated by the Love operator. The definition is a direct sum, following immediately from the J-cost formula in the multiplicative recognizer.
Claim. For agents at real numbers $σ_1, σ_2$, the pair system cost equals $(cosh σ_1 - 1) + (cosh σ_2 - 1)$.
background
In the module on thermodynamic instability of extraction, this supplies the baseline cost for paired agents in an ethical thermodynamics setting. The J-cost is the recognition cost from the multiplicative recognizer, equal to cosh(σ) - 1, and upstream the cost of any recognition event is this non-negative J-cost. A System is defined as a nonempty collection of energy levels in the Boltzmann distribution. This definition sets the stage for applying the Love operator to average positions and reduce total cost.
proof idea
This is a direct definition that sets the pair system cost to the sum of individual cosh terms minus one for each agent. No lemmas or tactics are used; it is an explicit algebraic expression implementing the J-cost sum.
why it matters
This definition is the starting point for the Love-Jensen inequality and its strict version, as well as the theorem that Love eliminates all waste in balanced extraction pairs. It applies the J-cost from the multiplicative recognizer to show that unequal positions create excess cost that Love removes. In the framework, it links the J-uniqueness in the forcing chain to thermodynamic instability, supporting the claim that Love achieves the ground state with zero waste.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.