harm_linearization_correct
plain-language theorem explainer
The result establishes that the linear approximation to J-cost along log-strain paths coincides with its directional derivative scaled by base value and strain. Researchers deriving harm bounds from calculus in Recognition Science cite it to validate first-order terms in decompositions. The proof is a direct one-line reduction to the established algebraic identity between the linearized term and the derivative.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. For real $L$, the linearized term $(x - x^{-1})L/2$ equals $J'(x) · x · L$.
background
The J-Cost Derivative Theory module supplies derivative formulas for the J-cost function to support harm calculations and replace axioms in the Ethics/Harm module. The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, whose derivative is $(1 - x^{-2})/2$ for $x > 0$. The linearized term is defined as $((x - x^{-1})/2) L$ and represents the first-order change under log-strain $L$ at base $x$.
proof idea
The proof is a one-line wrapper that applies the lemma linJ_eq_derivative_times_x, which itself reduces the claim via the derivative formula and algebraic cancellation of $(1 - x^{-2})x = x - x^{-1}$.
why it matters
This identity justifies using the linear harm term in decompositions, as stated in the module doc-comment. It feeds the broader program of grounding Ethics/Harm axioms in J-cost calculus. The result sits inside the Recognition Science treatment of the J-function that appears in forcing chains and cost ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.