aczel_kernel_smooth
plain-language theorem explainer
The declaration projects the smoothness property of continuous d'Alembert solutions from the regularity kernel under the Aczel smoothness package. Researchers tracing the d'Alembert forcing chain in the cost algebra would cite it to obtain the continuous-to-smooth step without direct reference to the Aczel axiom. The proof is a one-line term extraction of the smooth field from aczelRegularityKernel H.
Claim. Under the Aczel smoothness package, for any function $H : ℝ → ℝ$, the hypothesis that every continuous solution of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0) = 1$ is infinitely differentiable holds.
background
The module packages the Aczel classification step of the d'Alembert forcing chain: continuous solutions are smooth, after which the calibrated ODE kernel follows. The shifted cost function is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$, converting the Recognition Composition Law into the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The AczelSmoothnessPackage class asserts that any continuous $H$ satisfying $H(0) = 1$ and the d'Alembert equation is $C^∞$, citing Aczél 1966 Ch. 3 for the classification into constant and cosh forms.
proof idea
The proof is a one-line term that applies aczelRegularityKernel to H and projects its smooth field.
why it matters
This supplies the smoothness component required by the Aczel classification package so that the ODE kernel H'' = H can be derived downstream. It closes the continuous-to-smooth transition in the cost algebra, supporting uniqueness results for the kernel in the forcing chain. It directly implements the first item listed in the module doc-comment and touches the regularity needed for T5 J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.