IndisputableMonolith.Verification.JlogCoshCert
Certification module equating the Recognition cost J on the positive reals with the closed form cosh(log x) - 1. Auditors of the T5 J-uniqueness step and of any identity that rewrites J via hyperbolic functions cite it. The module packages the algebraic identity and its Lean certificate against the Cost API.
claimFor $x > 0$, the Recognition cost satisfies $J(x) = \cosh(\log x) - 1$, equivalently $J(x) = \frac{x + x^{-1}}{2} - 1$. The module records this identity as a verification certificate over the Cost layer.
background
Recognition Science fixes a unique nonnegative cost $J$ on the positive reals by the Recognition Composition Law and normalization. The forced closed form is $J(x) = (x + x^{-1})/2 - 1$, which is identical to $\cosh(\log x) - 1$. That double expression is the content of forcing step T5 (J-uniqueness).
The Cost module supplies the ambient definition of $J$ and the algebraic lemmas that relate multiplicative arguments to additive logarithms. This verification module sits one layer above Cost: it does not redefine $J$, it certifies the log-cosh presentation so downstream proofs may switch forms without re-deriving the identity.
proof idea
Definition-plus-certificate module, not a long tactic development. It exposes the equality $J(x) = \cosh(\log x) - 1$ by reducing the cosh form to the rational form $(x + x^{-1})/2 - 1$ via the standard identity $\cosh u = (e^u + e^{-u})/2$ with $u = \log x$, then matching the Cost-layer definition of $J$. Mathlib supplies the real-analysis facts; Cost supplies $J$.
why it matters in Recognition Science
T5 in the forcing chain (UnifiedForcingChain) names $J(x) = \cosh(\log x) - 1$ as the unique cost. Any later argument that prefers hyperbolic identities (periodicity, eight-tick octave estimates, or defect bounds written with cosh) needs a single trusted certificate rather than an ad-hoc rewrite. This module is that certificate inside the Verification domain. No downstream used_by edges are recorded yet; the intended consumers are uniqueness corollaries and any proof that switches between the rational and hyperbolic presentations of $J$.
scope and limits
- Does not prove uniqueness of J; only certifies the log-cosh closed form.
- Does not derive the Recognition Composition Law or the forcing chain T0–T8.
- Does not fix units, phi, or dimensional constants; pure real-cost identity.
- Does not supply numerical bounds or interval arithmetic for J.