dAlembert_contDiff_smooth
If a continuous real-valued function H satisfies H(0) = 1 and the d'Alembert equation H(t + u) + H(t - u) = 2 H(t) H(u) for all real t, u, then H is infinitely differentiable. Analysts working on functional equations or Recognition Science derivations of cost smoothness would cite this result. The proof is a one-line wrapper that invokes the natural-number differentiability theorem and applies the contDiff_infty equivalence.
claimLet $H : ℝ → ℝ$ be continuous with $H(0) = 1$ and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t, u$. Then $H$ is $C^∞$.
background
In the Recognition Science setting the shifted cost is defined by $H(x) = J(x) + 1$, where $J$ satisfies the Recognition Composition Law; under this shift the law becomes the d'Alembert equation. The module proves that every continuous solution with $H(0) = 1$ is $C^∞$, completing the Aczél classification (constant 1, cosh, or cos). This rests on the upstream natural-number bootstrap theorem, which uses the representation formula $H(t) = (Φ(t+δ) − Φ(t−δ)) / (2 Φ(δ))$ and induction to obtain ContDiff for every finite order.
proof idea
The proof is a one-line wrapper that applies the natural-number differentiability theorem (dAlembert_contDiff_nat) and then uses contDiff_infty.mpr to conclude infinite differentiability.
why it matters in Recognition Science
This supplies the smoothness step required by the full Aczél–Kannappan classification theorem and by the top-level dAlembert_contDiff_top result. It eliminates the former H_AczelClassification hypothesis in the IndisputableMonolith codebase and supports the subsequent ODE derivation H'' = c H. The result aligns with the J-uniqueness step (T5) in the forcing chain and the smoothness needed for the phi-ladder mass formulas.
scope and limits
- Does not classify the functional solutions, only their smoothness.
- Does not apply to discontinuous functions.
- Does not derive the explicit forms cosh or cos.
- Does not address complex or higher-dimensional analogues.
formal statement (Lean)
224private theorem dAlembert_contDiff_smooth (H : ℝ → ℝ) (h_one : H 0 = 1) (h_cont : Continuous H)
225 (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
226 ContDiff ℝ smooth H :=
proof body
Term-mode proof.
227 contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
228
229/-! ## §4 General ODE Derivation: C^∞ + d'Alembert → H'' = c·H -/
230