J_nonneg
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish non-negativity for $x \leq 0$.
- Does not treat complex or matrix arguments.
- Does not supply an explicit lower bound beyond zero.
formal statement (Lean)
75theorem J_nonneg (x : ℝ) (hx : 0 < x) : 0 ≤ J x :=
proof body
Term-mode proof.
76 Jcost_nonneg hx
77
78/-- **Defect characterization**: J(x) = (x − 1)²/(2x) for x ≠ 0. -/