linJ
plain-language theorem explainer
linJ defines the first-order change in J-cost for a log-strain L applied to base multiplier x as ((x - x^{-1})/2) * L. Researchers on harm linearization cite it to replace exact J evaluations with directional derivatives in the Recognition framework. The definition is a direct algebraic expression chosen to match the scaled derivative of Jcost.
Claim. The linearized per-bond delta for J-cost under log-strain $L$ at base multiplier $x$ is given by $((x - x^{-1})/2) L$.
background
The J-cost function is J(x) = (x + x^{-1})/2 - 1, the recognition cost per bond. Module Cost.Derivative develops derivative formulas for this function to enable linear approximations under log-strains, replacing axioms in harm calculations. The derivative identity deriv_Jcost_eq states d/dx J(x) = (1 - x^{-2})/2 for x > 0, and the linear term satisfies linJ(x, L) = x * J'(x) * L.
proof idea
Direct definition. The expression is written to coincide with the algebraic rearrangement of the derivative identity (1 - x^{-2})/2 * x = (x - x^{-1})/2.
why it matters
This definition is invoked by harm_linearization_correct to confirm the linear term equals the directional derivative, and by linJ_eq_derivative_times_x to establish the scaling identity. It fills the linearization step in J-cost derivative theory, supporting harm decomposition and the shift from axioms to derivative bounds. It touches the open quadratic remainder question noted in remJ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.