cosh_satisfies_continuous
plain-language theorem explainer
cosh_satisfies_continuous shows that the real hyperbolic cosine satisfies the continuity clause of the ODE regularity hypothesis for solutions to f'' = f. Workers on the T5 J-uniqueness argument inside the Recognition Science cost module cite it when confirming that cosh meets the required regularity for the functional equation. The proof is a one-line term application of the standard Mathlib continuity fact for cosh.
Claim. The function $H(t) = {cosh}(t)$ satisfies the regularity hypothesis: if $H''(t) = H(t)$ holds for all real $t$, then $H$ is continuous.
background
This declaration sits in the module of functional-equation helpers for the T5 cost-uniqueness proof. The central definition is ode_regularity_continuous_hypothesis H, the proposition that any pointwise solution of the ODE H'' = H must be continuous. The module supplies supporting lemmas for deriving J-cost uniqueness from the Recognition Composition Law.
proof idea
The proof is a term-mode one-liner: it opens the antecedent of the implication and immediately applies the Mathlib fact Real.continuous_cosh.
why it matters
The result supports the T5 J-uniqueness step by verifying that cosh, the closed-form expression for the J-cost via J(x) = cosh(log x) - 1, obeys the continuity demanded by the ODE regularity hypothesis. It therefore contributes to the forcing chain that isolates the self-similar fixed point phi and the eight-tick octave. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.