jcost_complexity_gap
plain-language theorem explainer
The theorem shows that the J-cost function exceeds its value at one for every positive real argument different from one. Modelers of physical complexity in recognition frameworks cite it to separate the balanced ground state from any imbalanced configuration. The proof is a one-line wrapper that rewrites the unit value to zero and applies the positivity lemma for deviations from unity.
Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > J(1)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost is defined by $J(x) = (x + x^{-1})/2 - 1$, equivalently written as the squared ratio $(x-1)^2/(2x)$. It is strictly convex on the positive reals with a unique global minimum of zero at $x=1$, as established by the second-derivative test $J''(x) = x^{-3} > 0$. The module IC-005 frames physics complexity through J-cost minimization: ground-state verification is linear-time while higher φ-rung states require exponential work. Upstream, Jcost_unit0 records the minimum value $J(1)=0$ and jcost_pos_away_from_one supplies the strict positivity away from one.
proof idea
The proof is a one-line wrapper. It rewrites the right-hand side via the unit lemma Jcost_unit0 to obtain the target inequality $Jcost x > 0$, then applies the upstream positivity theorem jcost_pos_away_from_one directly to the hypotheses $x>0$ and $x≠1$.
why it matters
The result supplies the complexity-gap statement IC-005.17 inside the RS computational classification. It underpins the module claim that J-cost gradient descent converges monotonically to the ground state while φ-hierarchy computations remain EXPTIME. The gap connects to T5 J-uniqueness and the convex minimization property of the forcing chain, confirming that balanced ledgers are the only zero-cost configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.