remJ
plain-language theorem explainer
remJ defines the remainder after subtracting the linear approximation from the change in J-cost under multiplicative strain e^L. Analysts deriving quadratic bounds for consent in the Ethics module cite this definition when controlling error terms in Taylor expansions of J. The definition is a direct algebraic expression using the already-defined Jcost and linJ functions.
Claim. The remainder after linearization is given by $r(x,L) := J(x e^{L}) - J(x) - ((x - x^{-1})/2) L$, where $J$ denotes the J-cost function and the subtracted term is the linearized per-bond delta under log-strain $L$.
background
In the J-Cost Derivative Theory module, the J-cost function measures recognition cost with derivative $(1 - x^{-2})/2$ for $x > 0$. The linearization linJ$(x, L) = ((x - x^{-1})/2) L$ supplies the first-order term under log-strain $L$ at base $x$. This remainder definition supports the quadratic bound needed to replace axioms in harm calculations, building on the upstream linJ definition.
proof idea
The definition is a direct algebraic subtraction of the linearized term linJ from the difference of Jcost values at $x$ and $x e^L$. No tactics are applied; it is an equational definition relying on the prior definitions of Jcost and linJ.
why it matters
This remainder definition feeds the unit-case lemma remJ_unit, which reduces to $J(e^L)$ at $x=1$, and supports the planned quadratic remainder bound in the derivative theory. It advances the chain by enabling precise control of higher-order terms in the linearization of J-cost, consistent with the Recognition Composition Law. The TODO marks an open step toward the full Taylor expansion bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.