cosh_dAlembert_to_ODE
plain-language theorem explainer
Cosh satisfies the hypothesis that converts the d'Alembert functional equation into the ODE H'' = H under the listed smoothness and normalization conditions. Researchers tracing the T5 J-uniqueness step in the Recognition Science forcing chain cite this to confirm that cosh solves the derived differential equation. The proof is a direct term application of the second-derivative identity for cosh after the hypotheses are introduced.
Claim. Let $H(x) = {cosh}(x)$. Then $H(0) = 1$, $H$ is continuous, $H(t+u) + H(t-u) = 2 H(t) H(u)$ holds for all real $t,u$, the second derivative satisfies $H''(0) = 1$, and therefore $H''(t) = H(t)$ for all real $t$.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument. The central definition dAlembert_to_ODE_hypothesis states that any function H obeying H(0)=1, continuity, the d'Alembert relation H(t+u)+H(t-u)=2H(t)H(u), and H''(0)=1 must satisfy H''(t)=H(t) everywhere. The upstream lemma cosh_second_deriv_eq records the identity deriv(deriv (fun x => cosh x)) t = cosh t.
proof idea
The term proof introduces the four premises of dAlembert_to_ODE_hypothesis and immediately applies cosh_second_deriv_eq to discharge the conclusion that the second derivative equals the function itself.
why it matters
The result verifies that cosh solves the ODE obtained from the d'Alembert equation, supplying a concrete solution inside the T5 J-uniqueness argument of the forcing chain. It supports the Recognition Composition Law by confirming the functional form that yields the self-similar fixed point phi. No downstream uses are recorded yet; the declaration closes a verification step rather than an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.