JlogCoshCert
plain-language theorem explainer
Audit certificate that packages the identity J_log(t) = cosh(t) - 1 for all real t, where J_log is the cost kernel pulled back to log coordinates. Anyone checking the hyperbolic form of the Recognition cost, or the evenness and strict convexity that follow from it, cites this. The verification predicate is discharged by a one-line appeal to the existing Cost lemma that expands J(exp t) into cosh.
Claim. There is a unit certificate whose verification predicate asserts: for every real $t$, $J_{\log}(t) = \cosh(t) - 1$, where $J_{\log}(t) := J(e^{t})$ and $J(x) = (x + x^{-1})/2 - 1$. The predicate holds for every inhabitant of the certificate type.
background
In Recognition Science the cost kernel on the positive reals is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced uniquely by the Recognition Composition Law and the T5 step of the unified forcing chain. The log-domain pullback is defined by $J_{\log}(t) := J(e^{t})$. Working in $t \in \mathbb{R}$ rather than $x > 0$ converts multiplicative structure into additive structure and makes ODE and convexity arguments routine.
The module packages this identity as a verification certificate: a bare structure together with a verified predicate that states $\forall t,, J_{\log}(t) = \cosh(t) - 1$. The module doc records why the form matters: $\cosh$ solves $y'' = y$ with $y(0)=1$, $y'(0)=0$, so $J_{\log}$ satisfies $y'' = y + 1$; evenness of $\cosh$ yields $J(x)=J(1/x)$; and $\cosh'' = \cosh > 0$ yields strict convexity of $J_{\log}$.
Upstream, Jlog_as_cosh in Cost already proves the pointwise identity by unfolding $J$ and the exponential definition of $\cosh$ and simplifying by ring.
proof idea
The structure itself carries no fields. The content is the simp lemma verified_any: introduce an arbitrary real $t$, then apply the upstream lemma Jlog_as_cosh t. That lemma unfolds $J_{\log}$ and $J$, rewrites $\cosh$ via its exponential formula and $e^{-t}$, and closes by ring. No additional arithmetic is done at the certificate layer; it is a one-line wrapper that re-exports the Cost identity under the verification API.
why it matters
The cosh representation is the analytic face of the T5 J-uniqueness landmark: once $J$ is forced, $J_{\log} = \cosh - 1$ is the cleanest closed form and the bridge from the multiplicative RCL domain into ordinary real analysis. It underwrites evenness (reciprocal symmetry of cost), strict convexity (unique minima on the phi-ladder), and the ODE characterization used in later cost and kernel arguments.
This certificate sits in the Verification domain as an audit node: external checkers can demand JlogCoshCert.verified c rather than chase the Cost file. No downstream consumers are wired yet (used_by is empty), so its present role is to freeze the identity in the certificate chain and document the hyperbolic geometry link. It does not itself force phi, the eight-tick octave, or $D=3$; those remain T6–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.