cosh_satisfies_differentiable
cosh_satisfies_differentiable shows that the real hyperbolic cosine satisfies the differentiability hypothesis for the ODE f'' = f. Workers on the T5 J-uniqueness argument in the cost functional equation module cite it to clear the regularity step for cosh as the J-cost solution. The proof is a one-line wrapper that assumes the ODE equality and continuity premises then directly invokes the built-in differentiability of cosh.
claimIf $f''(t) = f(t)$ for all $t$ and $f$ is continuous, then $f$ is differentiable, where $f = $ hyperbolic cosine.
background
The module supplies lemmas for the T5 cost uniqueness proof. The central definition is ode_regularity_differentiable_hypothesis, which encodes the regularity claim for solutions of the linear ODE f'' = f: if the second derivative equals the function itself and the function is continuous, then the function is differentiable. Its doc-comment states: For f'' = f with f continuous, f is differentiable. This follows from the ODE: f' exists since f'' = f requires f' to exist first.
proof idea
The term proof introduces the two premises of the hypothesis (the second-derivative identity and continuity) and then applies the Mathlib fact that the hyperbolic cosine is differentiable on the reals.
why it matters in Recognition Science
The result clears the regularity condition for cosh in the T5 J-uniqueness argument, where J(x) = (x + x^{-1})/2 - 1 arises as the self-similar fixed point. It sits inside the forcing chain T0-T8 and supports the Recognition Composition Law by confirming that the candidate solution meets the ODE differentiability requirement before uniqueness is concluded.
scope and limits
- Does not establish the second-derivative identity for cosh.
- Does not apply the hypothesis to any function other than cosh.
- Does not derive differentiability from the ODE premises.
- Does not address continuity or higher regularity beyond the hypothesis statement.
formal statement (Lean)
494theorem cosh_satisfies_differentiable : ode_regularity_differentiable_hypothesis Real.cosh := by
proof body
Term-mode proof.
495 intro _ _
496 exact Real.differentiable_cosh
497