dAlembert_smooth_of_aczel
plain-language theorem explainer
Continuous solutions of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0) = 1 are infinitely differentiable. This lemma is cited in the T5 cost uniqueness argument to secure smoothness of the shifted cost function before passing to the ODE. The proof is a one-line wrapper that forwards the hypotheses to the Aczel smoothness theorem.
Claim. For any function $H : ℝ → ℝ$, the conditions $H(0) = 1$, continuity of $H$, and the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t, u$ imply that $H$ is infinitely differentiable.
background
The module supplies lemmas supporting the T5 uniqueness proof for the cost function J in Recognition Science. Here H is the shifted version H(t) = G(t) + 1, with G the cost function obeying the Recognition Composition Law; this shift converts the law into the d'Alembert equation. The upstream AczelSmoothnessPackage asserts that any continuous solution to this equation with H(0) = 1 is C^∞, citing Aczél (1966, Ch. 3). The definition dAlembert_continuous_implies_smooth_hypothesis packages the corresponding implication as a Prop.
proof idea
The proof is a one-line wrapper applying aczel_dAlembert_smooth from the AczelClass module to the supplied hypotheses on H(0), continuity, and the functional equation.
why it matters
This result supplies the smoothness step needed for the T5 J-uniqueness proof. It is invoked by aczelRegularityKernel to construct the regularity kernel and by the parallel declaration in FunctionalEquationAczel. Within the framework it enables the subsequent derivation of the ODE H''(t) = H(t) from the functional equation, advancing the identification of H with cosh and J with cosh(log x) - 1. It leaves open the classification of discontinuous solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.