jcost_nonneg
plain-language theorem explainer
The recognition cost J is nonnegative on every positive real ratio. Cosmology uses it to prove total edge cost is a Lyapunov ground-state functional; entropy-arrow and measure-theory certificates reuse the same bound. The proof splits at ratio one and applies the strict-positivity lemma off the diagonal.
Claim. For every real $x > 0$, the recognition cost $J(x) = \frac{x + x^{-1}}{2} - 1$ satisfies $0 \le J(x)$.
background
In Recognition Science the cost of a positive ratio is the T5 functional $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). It is the unique continuous solution of the Recognition Composition Law that vanishes at identity and is nonnegative. The module RefineTrigger defines this $J$ and proves the strict form: any genuine distinction ($x > 0$, $x \neq 1$) has $J(x) > 0$, via the algebraic identity $J(x) = (x-1)^2/(2x)$.
The present module formalizes Phase-7 forward dynamics on a coupling graph of recognition levels. Each tick resolves one coupled pair to its mean (the $\sigma=0$, $J$-minimal move). Variance is an exact Lyapunov function; the total recognition cost over edges is the global ground-state functional. Nonnegativity of $J$ is the elementary brick under that total cost.
proof idea
Tactic proof by cases on eq_or_ne x 1. If $x = 1$, substitute and evaluate $J(1) = 0$ by norm_num. If $x \neq 1$, apply le_of_lt to the upstream strict bound RefineTrigger.jcost_pos (which already assumes $0 < x$ and $x \neq 1$). No new algebra is introduced here.
why it matters
This lemma is listed in the module doc as one of the central convergence facts discharging the Python forward-dynamics checks. Downstream, totalCost_nonneg is a one-line Finset sum of it, and totalCost_eq_zero_iff uses the nonnegativity hypothesis of sum_eq_zero_iff_of_nonneg to characterize the recognition ground state as graph consensus (constant levels on every edge).
It is also wired into framework certificates: EntropyArrowFromJCost.entropyArrowCert takes nonnegativity as the arrow axiom; MeasureTheoryFromRS.MeasureTheoryCert records $\forall r > 0,, 0 \le J(r)$; information-complexity theorem IC-005.1 and the tachyon-free certificate re-export the same fact. In the forcing chain this is the elementary half of T5 J-uniqueness (nonnegativity plus unique zero at identity).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.