linJ_unit
plain-language theorem explainer
The linearized J-cost delta vanishes at the identity multiplier x=1 for arbitrary strain L. Researchers deriving harm bounds or consent conditions from Taylor expansions in Recognition Science cite this to confirm the minimum at the canonical identity event. The proof is a direct one-line simplification that substitutes the definition of linJ and cancels the zero factor.
Claim. For every real $L$, the linearized per-bond delta satisfies $((1 - 1^{-1})/2) L = 0$.
background
The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ arising from the Recognition Composition Law. This module supplies its first-order approximations so that axioms in the Ethics/Harm module can be replaced by derivative identities. The auxiliary function linJ(x, L) is defined as $((x - x^{-1})/2) L$ and represents the directional change under log-strain L at base multiplier x. Upstream, the identity event is placed at state 1, the unique minimum of J.
proof idea
The proof is a one-line term-mode wrapper that applies the definition of linJ at argument 1 and simplifies the resulting arithmetic expression to zero.
why it matters
The lemma anchors the linearization at the J-minimum required by the ObserverForcing identity definition. It directly supports the module's main claims that linBondDelta equals the directional derivative and that the quadratic remainder is O(L²), enabling derivative-based derivations of consent. Within the Recognition framework it supplies the base case for the Taylor expansions used in harm bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.