jcost_pos_away_from_one
plain-language theorem explainer
J-cost is strictly positive for positive reals away from its unique minimum at x=1. Researchers classifying Recognition Science complexity cite this to bound the gap between ground states and imbalanced configurations. The proof rewrites via the squared algebraic form of J-cost then applies positivity of the resulting quotient.
Claim. For every real $x>0$ with $x≠1$, the J-cost satisfies $J(x)>0$, where $J(x)=((x-1)^2)/(2x)$.
background
The IC-005 module examines where physics sits in the complexity zoo by analyzing J-cost minimization. J-cost is the deviation measure $J(x)=(x+x^{-1})/2-1$ on positive ratios, equivalently expressed as $(x-1)^2/(2x)$ by the upstream lemma jcost_squared_form. This squared form makes strict positivity away from the ground state at x=1 immediate from the assumptions.
proof idea
The term proof rewrites the goal using jcost_squared_form, then applies div_pos to the quotient with positivity of numerator and denominator following from x>0 and x≠1.
why it matters
This fills IC-005.4 and feeds jcost_complexity_gap (IC-005.17) plus the rs_complexity_classes certificate. It confirms the strict positivity that separates the zero-cost ground state from all other configurations, consistent with the convex landscape and phi-hierarchy in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.