harm_linearization_correct
Recognition Science models of harm rely on the first-order expansion of the J-cost along exponential paths. This theorem confirms that the linear term linJ matches the directional derivative of Jcost scaled by x L. It is cited by researchers deriving consent bounds from quadratic remainders in the Ethics module. The argument is a direct invocation of the prior identity relating linJ to the explicit derivative formula.
claimFor $x > 0$ and real $L$, the linearized per-bond delta satisfies $((x - x^{-1})/2) L = J'(x) · x · L$, where $J'$ denotes the derivative of the J-cost function.
background
The J-cost derivative module supplies the calculus for replacing axiomatic harm definitions with derived approximations. It defines the J-cost function whose derivative is $(1 - x^{-2})/2$ for $x > 0$ and introduces the linearization linJ$(x, L) := ((x - x^{-1})/2) L$ as the first-order change under log-strain $L$. This setting rests on the Recognition Composition Law and the uniqueness of J from the forcing chain (T5). Upstream results include the explicit derivative formula deriv_Jcost_eq and the identity linJ_eq_derivative_times_x, which equates the linear term to the scaled derivative via the algebraic step $(1 - x^{-2})x = x - x^{-1}$.
proof idea
The proof is a one-line wrapper that applies the theorem linJ_eq_derivative_times_x x L hx. That prior result substitutes the explicit derivative formula into the definition of linJ and verifies the algebraic cancellation.
why it matters in Recognition Science
This result justifies the use of linBondDelta in the harm decomposition as stated in the module documentation. It closes a key step in replacing axioms with theorems in the Cost and Ethics layers of the Recognition Science framework. The theorem connects directly to J-uniqueness (T5) by ensuring consistent linear approximations across phi-tiers. No open questions are flagged in the supplied dependencies.
scope and limits
- Does not establish bounds on the quadratic remainder term.
- Does not extend to non-positive values of x.
- Does not address multi-variable extensions or higher derivatives.
- Does not provide numerical verification or physical units conversion.
formal statement (Lean)
134theorem harm_linearization_correct (x L : ℝ) (hx : 0 < x) :
135 -- The linearization linJ captures the first-order behavior of J along exp paths
136 linJ x L = deriv Jcost x * x * L :=
proof body
Term-mode proof.
137 linJ_eq_derivative_times_x x L hx
138
139end Cost
140end IndisputableMonolith