JlogStrictConvexCert
plain-language theorem explainer
Audit certificate packaging the fact that the log-domain recognition cost is strictly convex on all of ℝ. Researchers arguing uniqueness of the cost minimum from convexity (together with nonnegativity and a zero at the origin) would cite this package. The verification predicate is discharged by a one-line appeal to the existing strict-convexity theorem for that cost.
Claim. A unit certificate whose verification predicate asserts that the log-domain cost $J_{\log}:\mathbb{R}\to\mathbb{R}$, given by $J_{\log}(t)=\cosh t-1$, is strictly convex on $\mathbb{R}$ (i.e., strictly convex on the universal set).
background
In Recognition Science the base cost on positive reals is the T5 unique $J$, often written $J(x)=(x+x^{-1})/2-1$. The log-domain version pulls this back by $t\mapsto e^{t}$:
$$J_{\log}(t):=J(e^{t})=\cosh t-1.$$
Equivalently, $J_{\log}(t)=((e^{t}+e^{-t})/2)-1$. The present module is a thin verification wrapper around that function: it records, as an audit certificate, that $J_{\log}$ is strictly convex on the whole real line.
Upstream, Jlog_strictConvexOn already states $\mathrm{StrictConvexOn},\mathbb{R},\mathrm{univ},J_{\log}$. Its proof rewrites $J_{\log}$ as $\cosh-1$ and invokes strict convexity of $\cosh$ (second derivative $\cosh>0$) plus preservation under adding a constant. The module doc notes that strict convexity, paired with $J_{\log}(0)=0$ and $J_{\log}\ge 0$, yields an independent route to uniqueness of the cost minimum.
proof idea
The structure itself is an empty token (no fields), used only as a certificate carrier. The verification predicate is definitionally $\mathrm{StrictConvexOn},\mathbb{R},\mathrm{univ},J_{\log}$. The companion theorem that every such certificate is verified is a one-line wrapper: it applies the upstream result that $J_{\log}$ is strictly convex on $\mathbb{R}$, which itself reduces to $\cosh-1$ and uses strict convexity of $\cosh$.
why it matters
This sits in the Verification layer as a machine-checkable audit node for a basic analytic property of the recognition cost. Strict convexity implies a unique global minimizer and a clean gradient characterization ($\nabla J_{\log}(t)=0$ iff $t$ is that minimizer). Together with the zero and nonnegativity certificates named in the module doc, it supplies an optimization-style path to uniqueness of the cost minimum, parallel to the T5 $J$-uniqueness step in the forcing chain (where $J(x)=\cosh(\log x)-1$).
No downstream dependents are recorded in the current graph; the certificate is therefore a leaf meant for external audit and for any later uniqueness or duality arguments that want a named, simp-friendly convexity fact rather than an inline appeal to the Cost.Convexity development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.