shared_sensitivity
The shared_sensitivity theorem asserts that J-cost is strictly positive for every positive real r distinct from 1. Cross-domain equilibrium analysts cite it to confirm that perturbations away from J=0 carry identical cost signatures in Nash games, market clearing, and homeostatic models. The proof is a direct one-line wrapper that invokes the core positivity lemma for J-cost.
claimFor every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $Jcost(r) > 0$.
background
The J-cost function, introduced in the Cost module, measures deviation from the equilibrium fixed point at unity and satisfies Jcost(1) = 0. Upstream lemmas establish its strict positivity for r > 0 and r ≠ 1 by rewriting the cost as a square divided by a positive term. The CrossDomain module places this positivity inside the C7 universality claim, where the same J-cost=0 condition serves as the equilibrium criterion for Nash, market, and health models.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the supplied hypotheses on r.
why it matters in Recognition Science
This theorem supplies the shared_pert field inside jEquilibriumUniversalityCert, which certifies that the three equilibrium notions reduce to the identical J-cost condition. It completes the C7 structural claim that sensitivity to perturbations is domain-independent and rests on the single J-function of the Recognition framework.
scope and limits
- Does not compute the numerical value of the second derivative of J-cost at r=1.
- Does not address the case r ≤ 0.
- Does not derive the explicit algebraic form of the J-cost function.
Lean usage
theorem apply_shared (r : ℝ) (hr : 0 < r) (hne : r ≠ 1) : Jcost r > 0 := shared_sensitivity r hr hneformal statement (Lean)
49theorem shared_sensitivity (r : ℝ) (hr : 0 < r) (hne : r ≠ 1) :
50 Jcost r > 0 := Jcost_pos_of_ne_one r hr hne
proof body
51