jcost_symmetric
plain-language theorem explainer
J-cost satisfies J(x) = J(1/x) for every positive real x. Researchers analyzing convexity and local optimization in Recognition Science cite this result to confirm the cost landscape is reflection-symmetric around its minimum. The proof is a one-line term application of the core symmetry lemma from the Cost module.
Claim. For every positive real number $x$, $J(x) = J(x^{-1})$, where $J(y) = (y + y^{-1})/2 - 1$.
background
The module IC-005 treats computational complexity of physics as determined by J-cost minimization. J-cost is defined by $J(x) = (x + x^{-1})/2 - 1$, which is strictly convex with unique global minimum at $x=1$. The local setting states that ground-state verification is linear-time while phi-rung states require exponential work. Upstream lemma Jcost_symm in Cost unfolds the definition to squares, applies field simplification, and concludes the identity by ring normalization.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_symm from Cost, instantiated directly on the hypothesis hx that x is positive.
why it matters
The result occupies the IC-005.5 slot and confirms reflection symmetry of the RS cost landscape, ensuring the optimization problem is well-conditioned. It supports the module's claims that J-cost gradient descent converges monotonically and that local 8-tick dynamics remain O(1) per step. The symmetry aligns with T5 J-uniqueness and the phi-forced fixed point, closing one algebraic precondition for the complexity classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.