force_always_toward_balance
plain-language theorem explainer
The theorem shows that for any nonzero real σ the product σ times the derivative of the extraction system cost C(σ) is strictly positive. This encodes a universal restoring force that always drives the two-agent system back toward balance. Researchers analyzing stability in recognition-based thermodynamic models would cite it when proving that extraction creates its own resistance. The proof rewrites the derivative via the marginal-cost identity then splits into sign cases on σ and applies the strict monotonicity of sinh.
Claim. For every real number $σ ≠ 0$, $σ · C'(σ) > 0$, where $C(σ) = 2(ℝ.cosh σ − 1)$ is the extraction system cost of two agents at $e^σ$ and $e^{−σ}$.
background
The module Ethics.ThermodynamicInstabilityOfExtraction studies how extraction between two agents generates thermodynamic cost using the J-cost function native to Recognition Science. extractionSystemCost(σ) is defined as Jcost(ℝ.exp σ) + Jcost(ℝ.exp(−σ)) and equals 2(cosh σ − 1) by the upstream identity extraction_cost_eq_cosh. Its first derivative is supplied by the sibling theorem deriv_extraction_cost as exactly 2 sinh σ. The local setting therefore reduces questions of instability to the sign behavior of this hyperbolic derivative away from the balanced point σ = 0.
proof idea
The proof begins by rewriting the target product with the explicit marginal-cost formula from deriv_extraction_cost. It then applies lt_or_gt_of_ne to split into the cases σ < 0 and σ > 0. In each case Real.sinh_strictMono together with sinh 0 = 0 shows that sinh σ has the same sign as σ. The inequality is closed by nlinarith in both branches.
why it matters
The result supplies the core restoring-force property that makes extraction thermodynamically unstable, directly supporting the module’s claim that the universe resists imbalance. It rests on the marginal-cost theorem and the cosh representation of the J-cost sum. Within the Recognition framework it confirms that the balanced state is the unique minimum of the cost functional, consistent with J-uniqueness and the composition law that forces the hyperbolic form. No downstream citations are recorded, leaving open its use in larger multi-agent or discrete stability arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.