Jcost_deriv
plain-language theorem explainer
The J-cost function J(x) = (x + x^{-1})/2 - 1 has derivative (1 - x^{-2})/2 at every nonzero real x. Recognition theorists cite this when linearizing cost increments along multiplicative trajectories or analyzing forcing chains. The proof unfolds the definition, establishes differentiability via standard rules for addition and inversion, then computes the derivative explicitly with HasDerivAt witnesses and algebraic simplification.
Claim. For all real numbers $x$ with $x ≠ 0$, the derivative of $J(x) = (x + x^{-1})/2 - 1$ satisfies $dJ/dx = (1 - x^{-2})/2$.
background
In Recognition Science the J-cost is the explicit cost function induced by multiplicative recognizers on positive ratios, given by the formula J(x) = (x + x^{-1})/2 - 1. This expression coincides with cosh(log x) - 1 and satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The present module collects elementary properties of Jcost, including non-negativity and symmetry under x ↦ 1/x.
proof idea
The proof unfolds Jcost and first verifies DifferentiableAt ℝ (fun y => (y + y^{-1})/2 - 1) x by applying DifferentiableAt.sub and DifferentiableAt.div_const to the sum of the identity and the inverse. It then builds HasDerivAt witnesses step-by-step: hasDerivAt_id for the identity, hasDerivAt_inv for the reciprocal, their sum, division by 2, and subtraction of the constant 1. The final derivative is extracted by rw on the HasDerivAt record and simplified with field_simp and ring.
why it matters
This lemma supplies the local differential analysis required for the J-cost in the T5 J-uniqueness step of the forcing chain. It directly enables the immediate corollary that J-cost is strictly increasing on (1, ∞), which is noted in the module immediately after the declaration. In the broader framework the result underpins cost-increment calculations along the eight-tick octave and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.