JcostStrictPosCert
plain-language theorem explainer
Audit certificate that the recognition cost J is strictly positive for every positive real ratio other than 1. Researchers characterizing the unique minimizer of J, or packaging variational uniqueness for verification, cite this certificate. The verified predicate is discharged by a one-line appeal to the existing Cost-module strict-positivity lemma.
Claim. A unit verification certificate asserts that for all real $x>0$ with $x\neq 1$, the recognition cost satisfies $J(x)>0$, where $J(x)=(x+x^{-1})/2-1$. Every inhabitant of the certificate type satisfies this predicate.
background
The recognition cost of a positive ratio is $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$. In the forcing chain it is the unique continuous solution of the Recognition Composition Law (T5). It vanishes at unit ratio and is nonnegative everywhere.
This Verification module packages the strict-positivity half of the unique-minimum story as an audit certificate: $J(x)>0$ whenever $x>0$ and $x\neq 1$. Together with nonnegativity and $J(1)=0$, that forces $x=1$ to be the unique global minimizer, with no flat regions.
The upstream Cost lemma already proves the inequality by rewriting $J(x)=(x-1)^2/(2x)$: the numerator is a positive square off $x=1$, and the denominator is positive for $x>0$.
proof idea
The certificate structure carries no data (unit type with Repr). Its verified predicate is exactly the universal statement $\forall x>0,, x\neq 1\Rightarrow J(x)>0$. The accompanying theorem is a one-line wrapper: introduce $x$, positivity, and inequality-to-one, then apply the Cost-module lemma that $J(x)>0$ for $x>0$ and $x\neq 1$. That lemma itself rewrites via the squared representation and uses positivity of a nonzero square in the numerator.
why it matters
Strict positivity is what upgrades a global minimum of $J$ into a unique, strict global minimum. In Recognition Science that is the variational content of T5 J-uniqueness: any deviation from unit ratio incurs strictly positive cost, so the universe is driven to ratio one. The module doc frames the physical reading directly: no flat regions in the cost landscape.
The declaration is an audit surface in the Verification domain rather than a stepping-stone lemma (no recorded downstream dependents). It closes the certificate form of a fact already proved in Cost, making the unique-minimizer package checkable as a single verified predicate alongside companion certificates for nonnegativity and the unit value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.