deriv_Jcost_eq
plain-language theorem explainer
The lemma states that the derivative of the J-cost function at positive real x equals (1 minus x to the minus two) over two. Analysts deriving linear bond deltas from harm bounds in the Recognition framework cite this when replacing axioms with calculus. The proof computes the derivative directly from the definition J(x) equals (x plus x inverse) over two minus one, using HasDerivAt on identity and reciprocal followed by algebraic rewriting of the coefficient.
Claim. For every real $x > 0$, the derivative of $J$ at $x$ satisfies $J'(x) = (1 - x^{-2})/2$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost function is defined by the explicit form $J(x) = (x + x^{-1})/2 - 1$, which satisfies the Recognition Composition Law and arises as the unique solution in the forcing chain at step T5. This module supplies the derivative formulas needed to replace axioms in the Ethics and Harm modules with explicit calculus. The local setting notes that these derivatives establish the linearized bond delta as the directional derivative with quadratic remainder, enabling consent derivations from harm bounds.
proof idea
The proof applies hasDerivAt_id to the identity map and hasDerivAt_inv to the reciprocal, adds the resulting derivatives, divides by the constant 2, and subtracts the constant 1. It then rewrites the intermediate coefficient (1 plus negative (x squared) inverse) over 2 into (1 minus x inverse squared) over 2 by substituting (x squared) inverse equals (x inverse) squared and applying ring simplification. The final step extracts the derivative via the .deriv method on the HasDerivAt witness.
why it matters
This supplies the explicit derivative required by the sibling theorem linJ_eq_derivative_times_x, which proves linJ(x, L) equals deriv Jcost x times x times L. It completes the calculus step in the J-cost derivative theory, allowing the per-bond delta to be identified with the directional derivative. In the framework it bridges the J-uniqueness property from the forcing chain to practical linearization bounds used in harm calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.