cosh_satisfies_differentiable
plain-language theorem explainer
The declaration verifies that the real hyperbolic cosine satisfies the differentiability regularity condition for the linear ODE f'' = f. Researchers proving T5 J-uniqueness in Recognition Science cite it to confirm cosh meets the cost-function hypotheses. The proof is a direct one-line application of the known differentiability of cosh after introducing the ODE and continuity premises.
Claim. The function $H(t) = (e^t + e^{-t})/2$ satisfies: if $H''(t) = H(t)$ for all real $t$, then continuity of $H$ implies differentiability of $H$ over the reals.
background
This theorem sits in the module of functional-equation helpers for the T5 cost-uniqueness proof. The central definition is the ODE regularity differentiable hypothesis, which encodes that any solution to the second-order equation $f'' = f$ that is continuous must in fact be differentiable. The upstream definition states precisely: if the second derivative of $H$ equals $H$ pointwise, then continuity of $H$ yields differentiability of $H$ over the reals. In the Recognition Science setting, T5 forces the J-cost function to be unique and equal to cosh(log x) - 1.
proof idea
The proof is a one-line term-mode wrapper. It introduces the two premises of the hypothesis (the second-derivative identity and continuity) and immediately applies the library fact that the real hyperbolic cosine is differentiable.
why it matters
The result closes a regularity check required by the T5 uniqueness argument in the Recognition Science forcing chain. It ensures the candidate cost function cosh satisfies the differentiability needed before the self-similar fixed point phi and the eight-tick octave are derived. The module as a whole supplies the algebraic identities that convert the Recognition Composition Law into the explicit J-cost form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.