cosh_second_deriv_eq
plain-language theorem explainer
The second derivative of the real hyperbolic cosine equals the function itself at every real argument. Recognition Science researchers working on the T5 J-uniqueness step cite this identity to confirm that cosh solves the ODE obtained from the Recognition Composition Law. The term proof substitutes the standard derivative rules for cosh and sinh in two steps.
Claim. For all real numbers $t$, the second derivative of the function $xmapsto cosh x$ at $t$ equals $cosh t$.
background
This lemma sits in the Cost.FunctionalEquation module, which supplies supporting identities for the T5 cost-uniqueness argument in Recognition Science. The J-cost function satisfies J(x) = cosh(log x) - 1, and the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) leads to a d'Alembert-type equation whose smooth solutions obey the ODE H'' = H. The module imports Mathlib calculus results on derivatives, mean-value theorems, and Taylor expansions to handle these reductions.
proof idea
The term proof first rewrites the first derivative of cosh via the library fact Real.deriv_cosh, yielding sinh. It then applies the library fact Real.deriv_sinh to obtain cosh and evaluates the resulting identity at the arbitrary point t.
why it matters
The identity is invoked directly by cosh_dAlembert_to_ODE to discharge the d'Alembert-to-ODE hypothesis for cosh and by ode_cosh_uniqueness_contdiff to establish that cosh is the unique C^2 solution of H'' = H with H(0) = 1 and H'(0) = 0. This step closes a required piece of the T5 J-uniqueness argument in the forcing chain, confirming the differential equation satisfied by the cosh representation of J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.