linJ_matches_harm_def
plain-language theorem explainer
The linearized J-cost delta under log-strain equals the directional derivative term ((x - x^{-1})/2) L. Researchers replacing axioms in harm decomposition with derivative bounds cite this equality to confirm the linear term is exact. The proof is a one-line reflexivity confirming the shared definition with the harm linearization.
Claim. For real numbers $x$ and $L$, the linearized J-cost increment satisfies $((x - x^{-1})/2) L = ((x - x^{-1})/2) L$.
background
The J-cost derivative module supplies linear approximations to the J function for use in harm bounds. linJ denotes the linearized per-bond delta for J under log-strain L at base x, given explicitly by the product of the first-order term ((x - x^{-1})/2) and L. The module setting replaces ad-hoc linearizations in the Ethics/Harm module with derivative-derived expressions, as stated in the module documentation: linBondDelta(x, L) equals ((x - x^{-1})/2) · L is the correct linearization.
proof idea
The proof is a term-mode reflexivity that equates the definition of linJ directly to the harm linear term expression. No lemmas are applied beyond the definitional unfolding of linJ.
why it matters
This equality justifies the use of the harm linear term in decomposition arguments and feeds the Ethics/Harm module by discharging the need for separate linearization axioms. It closes the link between the derivative formulas (deriv_Jcost_eq and remJ_quadratic) and consent bounds derived from harm. The result supports the broader replacement of axioms with computed linearizations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.