remJ
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove any bound on the size of the remainder.
- Does not specify the domain of $x$ or $L$.
- Does not connect to the phi fixed point or eight-tick octave.
Lean usage
lemma remJ_unit (L : ℝ) : remJ 1 L = Jcost (exp L) := by unfold remJ linJ Jcost; simpformal statement (Lean)
105noncomputable def remJ (x L : ℝ) : ℝ :=
proof body
Definition body.
106 Jcost (x * exp L) - Jcost x - linJ x L
107
108-- TODO: Quadratic Remainder Bound
109-- theorem remJ_quadratic_bound (x : ℝ) (hx : 0 < x) :
110-- ∃ C > 0, ∀ L, |L| ≤ 1 → |remJ x L| ≤ C * L ^ 2
111
112/-- At unit multiplier, the remainder equals J(e^L) - J(1) - 0 = J(e^L). -/