jcost_nonneg
plain-language theorem explainer
J-cost is non-negative for every positive real argument. Researchers building entropy arrows or tachyon-free certificates cite this to anchor their structures. The proof is a one-line wrapper that invokes the core non-negativity lemma from the Cost module.
Claim. For every real number $x > 0$, the J-cost function satisfies $Jcost(x) ≥ 0$.
background
The IC-005 module frames the computational complexity of physics through J-cost minimization in Recognition Science. J(x) = (x + 1/x)/2 - 1 is strictly convex, with its unique global minimum at x = 1. Upstream lemmas establish the inequality via AM-GM or by rewriting Jcost x = (x-1)^2 / (2x) and applying positivity of the square and denominator.
proof idea
This is a one-line wrapper that applies the lemma Cost.Jcost_nonneg to the hypothesis hx.
why it matters
The theorem supplies the nonnegativity field required by MeasureTheoryCert and EntropyArrowCert. It realizes IC-005.1, confirming J-cost as a valid non-negative cost function that supports the tachyon-free condition and ground-state verification at x = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.