jcost_log_symmetric
plain-language theorem explainer
The J-cost function satisfies J(r) = J(1/r) for every positive real r. Equilibrium analyses in Recognition Science cite this symmetry when proving that the minimum at r = 1 is unique and isolated. The proof reduces immediately to the core symmetry lemma for the squared form of J-cost.
Claim. For every real number $r > 0$, the J-cost satisfies $J(r) = J(r^{-1})$.
background
J-cost is defined on positive reals with the explicit form $J(r) = (r-1)^2/(2r)$, which is nonnegative, vanishes only at $r=1$, and yields the leading quadratic approximation $J(r) ≈ (r-1)^2/2$ near equilibrium. The module states that this local Hessian supplies the universal sensitivity coefficient 1/2 for all RS equilibria. The upstream lemma Jcost_symm establishes the same inversion symmetry by unfolding the squared definition, canceling denominators, and applying ring simplification.
proof idea
One-line wrapper that applies the Jcost_symm lemma from the Cost module.
why it matters
The result supplies the log_symmetry field of jConvexityUniversalityCert and the corresponding field of existenceUniquenessCert. It therefore closes the C25 structural claim that J-cost is convex with isolated minimum at r=1, and it supports the T5 J-uniqueness step in the forcing chain by confirming symmetry around the self-similar fixed point. No open scaffolding remains for this identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.