jcost_unique_minimum
plain-language theorem explainer
The declaration proves that the J-cost function attains its global minimum of zero at argument 1 for every positive real. Researchers classifying Recognition Science complexity would cite it to establish that ground-state balance checks run in constant time. The argument reduces the claim to the unit value lemma followed by direct invocation of non-negativity.
Claim. $J(1) = 0$ and $J(x) = (x + x^{-1})/2 - 1$, so $J(1) ≤ J(x)$ for all $x > 0$.
background
In the IC-005 module the complexity of physics is reduced to properties of J-cost minimization. The function J, introduced via the Cost module as the derived cost of a multiplicative recognizer, is given explicitly by $J(x) = (x + x^{-1})/2 - 1$. Upstream lemmas record that J(1) evaluates to zero by direct substitution and that J(x) is nonnegative for positive x by the AM-GM inequality.
proof idea
The term proof introduces the positive real x, rewrites the left-hand side via the unit lemma Jcost_unit0, and finishes by applying the non-negativity lemma Jcost_nonneg.
why it matters
The result supplies IC-005.2, the unique-minimum step that anchors the complexity summary in ic005_certificate. It confirms that the ground state at x=1 is the only zero-cost configuration and can be verified in O(1) time, consistent with the J-uniqueness landmark in the forcing chain and the claim that local eight-tick dynamics remain tractable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.