extraction_cost_strictly_convex
plain-language theorem explainer
The theorem establishes that the second derivative of the extraction system cost is positive for every real σ, proving the cost function is strictly convex. Mechanism designers and researchers analyzing agent extraction in the Recognition Science ethics module would cite it to guarantee a unique stable equilibrium. The proof is a one-line wrapper that rewrites the second derivative via the prior curvature identity and invokes positivity of cosh.
Claim. Let $C(σ) = J(e^σ) + J(e^{-σ})$ denote the extraction system cost. Then $C''(σ) > 0$ for all real $σ$.
background
The extraction system cost is defined as the sum of J-costs evaluated at the pair of agent positions $e^σ$ and $e^{-σ}$, which the module shows equals $2(ℝ.cosh(σ) - 1)$. This construction appears in the Ethics.ThermodynamicInstabilityOfExtraction module, which examines thermodynamic costs arising from the Recognition Composition Law applied to extraction between agents. The immediate upstream result is the curvature theorem establishing that the second derivative equals exactly $2 ℝ.cosh(σ)$.
proof idea
The proof is a one-line wrapper that applies the second_deriv_extraction_cost identity to replace the nested derivatives with $2 ℝ.cosh(σ)$, then closes the inequality with linear arithmetic using the fact that cosh is positive everywhere.
why it matters
This convexity result directly supports the sibling unique-equilibrium theorem by ensuring the critical point at σ = 0 is a strict global minimum. It fills the curvature step in the thermodynamic instability analysis, connecting the J-functional equation to game-theoretic mechanism design. The declaration closes a local gap in the ethics module without touching open questions in the broader T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.