JcostMinimumCert
plain-language theorem explainer
Audit certificate packaging that the RS cost kernel J has a unique global minimum at the identity: J(1)=0 and J(x)>0 for every positive x≠1. Verification and forcing-chain authors cite it to lock the “no free deviation” half of the cost kernel. The accompanying verified_any proof is a two-line constructor that applies Jcost_unit0 and Jcost_pos_of_ne_one.
Claim. There is a certificate type whose verification predicate asserts that the recognition cost $J(x)=(x+x^{-1})/2-1$ satisfies $J(1)=0$ and $J(x)>0$ for all $x>0$ with $x\neq 1$. Every inhabitant of the certificate type satisfies that predicate.
background
Recognition Science measures deviation from perfect match by the cost kernel
$$J(x)=\frac{x+x^{-1}}{2}-1$$
on positive reals (equivalently $J(x)=\cosh(\log x)-1$). The module packages the unique-minimum half of that kernel as an audit certificate: zero cost exactly at the identity, strictly positive cost on every genuine distinction.
Upstream, Jcost_unit0 is the one-line evaluation $J(1)=0$, and Jcost_pos_of_ne_one rewrites $J$ via the squared form $J(x)=(x-1)^2/(2x)$ to get strict positivity for $x>0$, $x\neq 1$. The module doc notes that the same identity already shows non-negativity with equality only at $x=1$. Together with the separate convexity certificate, this pins the identity as the unique optimal state under the Recognition Composition Law.
proof idea
The structure itself is a unit type (no fields). The real content is the simp predicate verified, which is literally the conjunction of the two cost facts, and the theorem verified_any, which discharges it for every certificate inhabitant.
The proof is a two-goal constructor: the first goal is exactly Jcost_unit0; the second introduces $x>0$, $x\neq 1$ and applies Jcost_pos_of_ne_one. No new analysis is done at this layer; the certificate only re-exports those two Cost lemmas under a named verification interface.
why it matters
In the RS forcing chain, T5 forces the cost kernel to be $J(x)=(x+x^{-1})/2-1$. This certificate is the verification-side lock that $J$ has a unique global minimum at the identity with value zero: perfect recognition is free, every genuine distinction is charged. The module doc states the intended pairing with JcostConvexityCert: unique minimum plus strict convexity rules out other local minima and makes the identity the unique optimal state.
No downstream consumers are wired yet (used_by is empty), so the declaration currently sits as a leaf in the Verification domain, ready for higher audit bundles that assemble cost, convexity, and composition-law certificates into a single forcing report. It does not itself prove T5 uniqueness of $J$ among admissible costs; it only certifies the minimum property of the already-chosen kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.