cosh_satisfies_differentiable
plain-language theorem explainer
The declaration shows that the hyperbolic cosine satisfies the differentiability conclusion in the ODE regularity hypothesis used for cost functional equations. Workers on the T5 J-uniqueness step in Recognition Science cite it when confirming that candidate solutions to f'' = f remain differentiable once continuous. The proof is a one-line term wrapper that discards the ODE and continuity premises and invokes the built-in differentiability of cosh.
Claim. If $\frac{d^2}{dt^2} \cosh(t) = \cosh(t)$ and $\cosh$ is continuous, then $\cosh$ is differentiable over $\mathbb{R}$.
background
The module supplies supporting lemmas for the T5 cost uniqueness argument. The key imported definition is ode_regularity_differentiable_hypothesis, which states that any function H satisfying the second-order ODE deriv (deriv H) t = H t and the continuity assumption must be differentiable. The upstream result records that this regularity claim follows from the structure of the linear ODE f'' = f.
proof idea
Term-mode proof. The intro tactic binds the two premises of the hypothesis (the ODE equality and continuity). The body applies the library fact Real.differentiable_cosh directly to discharge the Differentiable conclusion, without using the premises.
why it matters
It supplies one concrete instance of the regularity hypothesis required inside the T5 J-uniqueness argument. The parent chain step is the verification that J-cost candidates built from cosh obey the necessary smoothness conditions before the Recognition Composition Law is applied. No open scaffolding remains for this particular check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.