linJ
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assume or enforce x > 0.
- Does not include or bound the quadratic remainder after linearization.
- Does not derive the form from the Recognition Composition Law.
- Does not address physical constants such as phi or the eight-tick octave.
formal statement (Lean)
72noncomputable def linJ (x L : ℝ) : ℝ := ((x - x⁻¹) / 2) * L
proof body
Definition body.
73
74/-- At unit multiplier (x=1), the linear term vanishes. -/