jcost_symmetric
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove strict convexity of J-cost.
- Does not compute explicit J values or minima.
- Does not extend the identity beyond positive reals.
- Does not address multi-variable or higher-dimensional costs.
formal statement (Lean)
76theorem jcost_symmetric (x : ℝ) (hx : x > 0) :
77 Jcost x = Jcost x⁻¹ :=
proof body
Term-mode proof.
78 Cost.Jcost_symm hx
79
80/-! ## II. Gradient of J-Cost (Computability of First-Order Optimization) -/
81
82/-- The derivative of J-cost: J'(x) = (1 - 1/x²)/2 = (x² - 1)/(2x²). -/