IndisputableMonolith.Verification.JlogDerivCert
Verification module certifying the derivative of the J-cost in logarithmic coordinates. J composed with exp reduces to cosh minus one, whose t-derivative is sinh. Analysts checking the T5 J-uniqueness chain and Recognition Composition Law identities cite this certificate. The argument is a short Mathlib differentiation of the closed form imported from Cost.
claimLet $J(x)=(x+x^{-1})/2-1$. In log coordinates set $J_{\log}(t):=J(e^{t})=\cosh t-1$. The module certifies $J_{\log}'(t)=\sinh t$ (and the matching algebraic identities needed by downstream cost verification).
background
Recognition Science fixes the cost functional by T5 uniqueness: $J(x)=(x+x^{-1})/2-1$, equivalently $J(e^{t})=\cosh t-1$. The Recognition Composition Law is stated in multiplicative coordinates, but many analytic arguments (convexity, curvature, small-defect expansions) run more cleanly after the change of variables $t=\log x$.
The parent Cost module supplies the definition of $J$ and the closed form on the positive reals. This verification module sits in the Verification domain: it does not redefine $J$; it records a machine-checked derivative identity for the log-chart representative $J_{\log}$, so later certificates can quote $J_{\log}'=\sinh$ without re-running calculus.
Notation: $J_{\log}(t)=\cosh t-1$, with $t\in\mathbb{R}$ corresponding to $x=e^{t}>0$. The eight-tick and dimension forcings (T7, T8) are not used here; only the J-cost calculus is.
proof idea
Definition-plus-certificate module, not a long development. It imports Mathlib analysis and IndisputableMonolith.Cost, exposes the log-chart form of $J$, and discharges the derivative claim by rewriting $J(e^{t})$ as $\cosh t-1$ and applying Mathlib's derivative of $\cosh$. Any companion algebraic lemmas are one-line rewrites from that closed form. No forcing-chain steps beyond T5's formula are required.
why it matters in Recognition Science
Downstream cost and defect arguments need a trusted derivative of $J$ in additive coordinates: curvature of the cost, linearization near $t=0$, and checks that the RCL-compatible $J$ has the expected odd derivative $\sinh$. This module is the verification pin for that calculus fact.
It feeds the broader Verification layer that audits Cost identities used across the monolith. In the forcing chain it is local to T5 (J-uniqueness) and the RCL setup; it does not itself force $\varphi$, the eight-tick octave, or $D=3$. With no further used_by edges recorded, its role is infrastructural: keep the log-chart derivative from being a silent axiom in later certificates.
scope and limits
- Does not prove T5 uniqueness of J; assumes the Cost closed form.
- Does not derive the Recognition Composition Law or any RCL identity.
- Does not force phi, eight-tick period, or spatial dimension D=3.
- Does not address mass ladder, alpha band, or Berry threshold claims.
- Does not supply numerical bounds; only the symbolic derivative certificate.