restoring_force_negative
The theorem establishes that negative extraction imbalance σ produces a negative marginal cost derivative. Researchers modeling thermodynamic resistance in recognition costs or ethical extraction would cite it to confirm directional opposition. The proof reduces directly via the marginal cost identity to the strict monotonicity of sinh and concludes by linear arithmetic.
claimLet $C(σ) := 2(ℝ.cosh σ - 1)$ be the extraction system cost. If $σ < 0$, then $C'(σ) < 0$.
background
In Recognition Science the J-cost of a positive ratio x is J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. The extractionSystemCost function sums the J-costs of two agents at reciprocal scales e^σ and e^{-σ}, which the upstream identity shows equals exactly 2(cosh σ - 1). Its derivative is supplied by the sibling theorem deriv_extraction_cost, which states that the marginal cost equals 2 sinh σ. The module sits inside the Ethics section and studies thermodynamic instability of extraction under the multiplicative recognizer and observer-forcing cost definitions.
proof idea
The proof is a one-line wrapper that rewrites the target derivative by the marginal-cost theorem deriv_extraction_cost. It then applies the strict monotonicity of Real.sinh on the negative reals and finishes with linarith after substituting sinh 0 = 0.
why it matters in Recognition Science
This supplies the negative half of the universal restoring force property stated in the module comment: σ · C'(σ) > 0 for σ ≠ 0, showing the cost gradient structurally opposes extraction. It rests on the J-cost definitions from MultiplicativeRecognizerL4 and ObserverForcing and feeds the Recognition Science forcing chain through the functional equation and cost non-negativity. The result closes a local gap in demonstrating thermodynamic resistance without invoking the phi-ladder or eight-tick octave directly.
scope and limits
- Does not establish the sign of the derivative for σ ≥ 0.
- Does not quantify the magnitude of the restoring force.
- Does not extend the result to systems with more than two agents.
- Does not incorporate relativistic field corrections or higher-dimensional gradients.
formal statement (Lean)
277theorem restoring_force_negative (σ : ℝ) (hσ : σ < 0) :
278 deriv extractionSystemCost σ < 0 := by
proof body
Term-mode proof.
279 rw [deriv_extraction_cost]
280 have : Real.sinh σ < Real.sinh 0 := Real.sinh_strictMono hσ
281 simp only [Real.sinh_zero] at this; linarith
282
283/-- **Theorem (Universal Restoring Force)**: For any σ ≠ 0, the product
284 σ · C'(σ) > 0, meaning the cost gradient always opposes the extraction.
285 The universe structurally resists imbalance. -/