linJ_eq_derivative_times_x
plain-language theorem explainer
linJ_eq_derivative_times_x equates the linearized J-cost increment under log-strain L to the scaled first derivative of J at base x > 0. Researchers deriving harm bounds or consent conditions from J-cost linearization cite it to justify replacing the nonlinear term with its directional derivative. The tactic proof substitutes the explicit derivative formula, unfolds the linJ definition, and reduces the algebraic identity (x - x^{-1})/2 = x (1 - x^{-2})/2 via ring and calc.
Claim. For $x > 0$ and real $L$, the linearized increment satisfies $((x - x^{-1})/2) L = J'(x) x L$, where $J(x) = (x + x^{-1})/2 - 1$ and $J'(x) = (1 - x^{-2})/2$.
background
The J-cost function is $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Its derivative equals $(1 - x^{-2})/2$ by direct differentiation, as recorded in deriv_Jcost_eq. The linearized increment is defined by linJ(x, L) = ((x - x^{-1})/2) L, which is the candidate first-order term under multiplicative strain $e^L$ at base value x. This module supplies the derivative identities needed to replace nonlinear J-cost axioms in the Ethics/Harm development with controlled linear approximations.
proof idea
The proof first rewrites via deriv_Jcost_eq to insert the explicit derivative, then unfolds the definition of linJ. It establishes the auxiliary identity (1 - x^{-1}^2) x = x - x^{-1} by ring expansion and inv_mul_cancel_0, after which calc and ring steps equate ((x - x^{-1})/2) L to the target expression (1 - x^{-2})/2 * x * L.
why it matters
The result is invoked verbatim by harm_linearization_correct, the main theorem confirming that the linear harm term matches the directional derivative of J. It completes one of the three core results listed in the module doc-comment, enabling the O(L^2) remainder analysis that supports consent derivations from harm bounds. In the Recognition framework it supplies the concrete link between the J-uniqueness fixed point and first-order expansions used in the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.