linJ_unit
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim the vanishing result for any multiplier other than 1.
- Does not derive the explicit derivative J'(x) or its closed form.
- Does not bound the quadratic remainder term.
- Does not apply to non-real or discrete strains.
formal statement (Lean)
75lemma linJ_unit (L : ℝ) : linJ 1 L = 0 := by simp [linJ]
proof body
Term-mode proof.
76
77/-- The key identity connecting linJ to the derivative:
78 linJ(x, L) = J'(x) · x · L
79
80 Algebraic identity: (x - x⁻¹)/2 = ((1 - x⁻²)/2) · x -/