restoring_force_positive
plain-language theorem explainer
Positive extraction levels produce strictly positive marginal costs in the extraction system cost function. Analysts of recognition-based thermodynamics cite the result to establish that extraction generates a restoring force that grows with sinh(σ). The proof reduces the derivative via the marginal cost identity to the strict monotonicity of the hyperbolic sine and concludes by linear arithmetic.
Claim. Let $C(σ)$ denote the extraction system cost $J(e^σ) + J(e^{-σ})$. Then for all $σ > 0$, the derivative satisfies $C'(σ) > 0$.
background
The extractionSystemCost combines J-costs of two agents in a multiplicative recognition system, one at scale $e^σ$ and the other at $e^{-σ}$. The upstream theorem deriv_extraction_cost states that this derivative equals exactly $2 sinh(σ)$, the marginal cost of extraction. J-cost itself is the derived cost of a multiplicative recognizer comparator, with the explicit form $J(x) = (x + x^{-1})/2 - 1$ from the foundation cost definitions.
proof idea
The proof rewrites the goal by the marginal cost theorem deriv_extraction_cost. It then applies the strict monotonicity lemma for Real.sinh to obtain sinh(σ) > sinh(0) = 0, and finishes with linear arithmetic to reach positivity.
why it matters
The result anchors the thermodynamic instability argument in the Ethics module by showing extraction always creates a positive marginal cost. It feeds the module's sequence of convexity and equilibrium lemmas that derive from the J-functional equation and observer forcing. No downstream uses are recorded, so the declaration closes a local positivity step rather than feeding a larger chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.