JcostStrictCert
plain-language theorem explainer
Packages strict positivity of the recognition cost: J(x) > 0 whenever x > 0 and x ≠ 1. Anyone citing unique global minimality of J at the identity ratio uses this certificate. The check is a one-line wrapper around the existing Cost lemma Jcost_pos_of_ne_one.
Claim. There is a unit certificate whose verification predicate is the statement: for every real $x > 0$ with $x \neq 1$, the recognition cost $J(x) = \frac{x + x^{-1}}{2} - 1$ satisfies $J(x) > 0$. The certificate always verifies.
background
In Recognition Science the cost of a positive ratio is $J(x) = (x + x^{-1})/2 - 1$, equivalently $(x-1)^2/(2x)$. The module sits in the verification layer that packages analytic facts about $J$ as named certificates for the forcing chain.
Prior certificates already record non-negativity $J(x) \ge 0$ for $x > 0$ and the identity $J(1) = 0$ (JcostAxiomsCert). Strict positivity is the missing half: it forces the zero set of $J$ on $(0,\infty)$ to be exactly ${1}$.
Upstream, Jcost_pos_of_ne_one proves the inequality by rewriting $J$ in squared form and applying positivity of squares and of the denominator $2x$.
proof idea
The structure itself is an empty marker type. Its verified predicate is definitionally the universal statement $\forall x>0,, x\neq 1 \Rightarrow J(x)>0$.
The top-level theorem verified_any is a one-line wrapper: introduce $x$, positivity, and $x\neq 1$, then apply the Cost lemma Jcost_pos_of_ne_one. No new algebra is done at this layer.
why it matters
Strict positivity upgrades the minimum story from "$J\ge 0$ and $J(1)=0$" to "$x=1$ is the unique global minimizer on $(0,\infty)$". That uniqueness is the analytic content behind T5 J-uniqueness in the forcing chain ($J(x)=\cosh(\log x)-1$), and it underwrites the Recognition Composition Law's interpretation of genuine distinctions as strictly costly.
The module doc frames this certificate as the strict companion to JcostAxiomsCert. No downstream consumers are wired yet in the graph; the declaration is a leaf verification node ready for the certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.