aczel_dAlembert_smooth
plain-language theorem explainer
Any continuous real function H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is infinitely differentiable under the AczelSmoothnessPackage assumption. Recognition Science cost-algebra proofs cite this to upgrade continuity to C^infty regularity. The argument is a direct one-line application of the package's smoothness axiom.
Claim. Assuming the Aczél smoothness hypothesis, if a function $H : ℝ → ℝ$ satisfies $H(0) = 1$, is continuous, and obeys the d'Alembert relation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, then $H$ is infinitely differentiable.
background
The AczelSmoothnessPackage typeclass encodes the classical Aczél (1966, Ch. 3) result: any continuous solution of the d'Alembert equation with H(0)=1 is C^∞. Its single field asserts precisely that continuous H obeying H(t+u)+H(t-u)=2 H(t) H(u) must be ContDiff ℝ ⊤ H. In the Recognition Science setting the shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into this exact d'Alembert form. The module isolates the smoothness interface so that the unconditional classification theorem can live separately while downstream results parameterize over the package.
proof idea
The proof is a one-line wrapper that applies the smooth_of_dAlembert field of the supplied AczelSmoothnessPackage instance directly to H, h_one, h_cont and h_dAlembert.
why it matters
This supplies the smoothness step required by cost_algebra_unique to conclude that any CostAlgebraData calibrated at J''(1)=1 must equal J (T5 in the forcing chain). It is invoked by dAlembert_cosh_solution_aczel and dAlembert_smooth_of_aczel to obtain the cosh form and the ODE H'' = H without extra regularity parameters. The downstream h_aczel_classification_proved uses it to discharge the last foundation axiom. The result rests on the RCL reducing to d'Alembert under the H reparametrization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.