differentiableAt_Jcost
The J-cost function J(x) = (x + x^{-1})/2 - 1 is differentiable at every positive real x. Analysts deriving linear approximations for bond deltas or harm bounds cite this result. The proof is a direct term-mode application of Mathlib's DifferentiableAt rules after unfolding the definition.
claimFor every real number $x > 0$, the function $J(x) = (x + x^{-1})/2 - 1$ is differentiable at $x$.
background
The J-cost function is defined by J(x) = (x + x^{-1})/2 - 1 and satisfies the Recognition Composition Law. This module supplies derivative formulas that replace axioms in the Ethics/Harm module with theorems. Upstream structures from PhiForcingDerived and LedgerFactorization fix the calibration of J on positive reals, while the module doc states that these derivatives enable linBondDelta(x, L) = ((x - x^{-1})/2) · L as the correct linearization with quadratic remainder.
proof idea
The proof unfolds Jcost, applies DifferentiableAt.sub to isolate the constant, then DifferentiableAt.div_const on the scaled sum. Inside the sum it invokes DifferentiableAt.add of the identity map and the reciprocal, with the reciprocal case obtained from ne_of_gt applied to the positivity hypothesis.
why it matters in Recognition Science
This lemma supplies the differentiability step required by deriv_Jcost_eq and linBondDelta_is_derivative in the same module. Those results in turn support consent derivations from harm bounds. It closes the basic calculus prerequisite for the J-uniqueness step in the forcing chain (T5) without introducing new axioms.
scope and limits
- Does not establish differentiability for x ≤ 0.
- Does not compute the explicit derivative formula.
- Does not address higher-order derivatives or Taylor remainders.
formal statement (Lean)
29lemma differentiableAt_Jcost (x : ℝ) (hx : 0 < x) : DifferentiableAt ℝ Jcost x := by
proof body
Term-mode proof.
30 have hxne : x ≠ 0 := ne_of_gt hx
31 unfold Jcost
32 apply DifferentiableAt.sub
33 · apply DifferentiableAt.div_const
34 apply DifferentiableAt.add differentiableAt_id
35 exact differentiableAt_inv hxne
36 · exact differentiableAt_const 1
37
38/-- The derivative of J at x equals (1 - x⁻²)/2.
39
40 Proof: J(x) = (x + x⁻¹)/2 - 1
41 J'(x) = d/dx[(x + x⁻¹)/2 - 1] = (1 + (-x⁻²))/2 = (1 - x⁻²)/2
42
43 **Technical note**: This is standard calculus, using:
44 - d/dx[x] = 1
45 - d/dx[x⁻¹] = -x⁻² -/