jcost_pos_away_from_one
plain-language theorem explainer
The theorem establishes that the J-cost is strictly positive for every positive real not equal to one. Foundation paper F1 authors cite it when they need the complexity gap between the ground state at x=1 and any other configuration. The proof is a one-line wrapper that forwards the hypotheses to the core positivity lemma Jcost_pos_of_ne_one.
Claim. For every real $x>0$ with $x≠1$, $J(x)>0$ where $J(x)=½(x+x^{-1})-1$.
background
Module F1 collects log-domain identities for the canonical reciprocal cost $J(x)=½(x+x^{-1})-1$. The local setting is the geometry of this cost function, its strict convexity, and its minimization at the geometric mean. Upstream lemma Jcost_pos_of_ne_one states: J(x)>0 for x≠1 and x>0. Its proof rewrites Jcost via Jcost_eq_sq as (x-1)²/(2x) and applies div_pos together with sq_pos_of_ne_zero on the numerator.
proof idea
One-line wrapper that applies the lemma Jcost_pos_of_ne_one from JcostCore (and its duplicate in Cost). The lemma itself rewrites Jcost via Jcost_eq_sq, then uses div_pos on the squared numerator after confirming the denominator is positive.
why it matters
The result supplies the strict positivity required by jcost_complexity_gap and ic005_certificate inside PhysicsComplexityStructure. It directly implements F1.1.5, the consequence of J''(x)=x^{-3}>0 that witnesses the unique minimum at x=1. The declaration closes the local convexity argument needed for the RS complexity classification and the eight-tick update rules that follow from the same J-cost geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.