deriv_extraction_cost
plain-language theorem explainer
The marginal cost of extraction in a two-agent recognition system equals twice the hyperbolic sine of the extraction parameter σ. Modelers of thermodynamic stability in recognition frameworks cite this when deriving gradients that oppose imbalance. The proof rewrites the cost function to its closed hyperbolic form via the prior identity lemma then differentiates the cosh expression directly.
Claim. Let $C(σ)$ be the extraction system cost $J(e^σ) + J(e^{-σ})$, where $J$ is the recognition cost function. Then $C'(σ) = 2 sinh(σ)$.
background
The Ethics module examines thermodynamic instability arising from extraction between two agents. The extraction system cost is defined as the sum of J-costs evaluated at reciprocal scales $e^σ$ and $e^{-σ}$. The J-cost is the recognition cost induced by the multiplicative recognizer on positive ratios and satisfies the functional equation that forces the identity $J(x) + J(1/x) = 2(cosh(log x) - 1)$. This derivative result rests on the upstream identity that converts the sum directly into $2(cosh σ - 1)$.
proof idea
The tactic proof first obtains an extensional equality to the function $x ↦ 2(cosh x - 1)$ by pointwise application of the extraction cost identity lemma. It then rewrites the target derivative and applies the standard derivative of cosh scaled by the constant 2, using the hasDerivAt fact for the hyperbolic cosine.
why it matters
This supplies the explicit first derivative required by the unique-equilibrium theorem and the restoring-force theorems that immediately follow in the same module. It translates the foundational J-uniqueness and Recognition Composition Law into a concrete gradient that always points toward balance, confirming the structural resistance to extraction. The result closes one link in the chain from the eight-tick octave and phi-ladder cost formulas to ethical thermodynamic claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.