J_nonneg
plain-language theorem explainer
J_nonneg asserts that the J-cost is non-negative for every positive real argument. Modelers of recognition costs in physics or defect functionals would cite it to bound energies from below. The proof is a one-line wrapper invoking the core Jcost non-negativity lemma.
Claim. For every real number $x > 0$, the J-cost satisfies $J(x) = 0$, where $J(x) := (x + x^{-1})/2 - 1$.
background
The J-cost is the unique function on positive reals satisfying the Recognition Composition Law, given explicitly by $J(x) = (x + x^{-1})/2 - 1$. This module collects algebraic facts about costs, importing the core definition from Cost and its functional-equation companions. Upstream lemmas prove the same non-negativity claim for the equivalent Jcost representation, one via the identity $J(x) = (x-1)^2/(2x)$ together with non-negativity of squares and positivity of the denominator, another via direct AM-GM.
proof idea
The proof is a one-line wrapper that applies the Jcost_nonneg lemma from the Cost module directly to the hypothesis hx.
why it matters
Non-negativity of J supplies the lower bound required for cost interpretations throughout the framework, including coherence-collapse arguments in gravity and cutoff constructions on the phi-ladder. It aligns with the T5 uniqueness of J and the defect characterization used in forcing-chain steps. The result closes a basic positivity requirement before downstream applications to energy processing or Navier-Stokes models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.