aczel_kernel_smooth
plain-language theorem explainer
Under the AczelSmoothnessPackage assumption, aczel_kernel_smooth asserts that any H satisfies the continuous-implies-smooth hypothesis for the d'Alembert equation. Cost theorists cite it to extract the smoothness guarantee for the shifted cost H without invoking the classification axiom directly. The proof is a one-line term projection of the smooth field from aczelRegularityKernel H.
Claim. Assuming the Aczél smoothness package, for every function $H : ℝ → ℝ$, the hypothesis holds that continuity of $H$ together with the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ and $H(0)=1$ implies $H$ is infinitely differentiable.
background
The module packages the d'Alembert segment of the forcing chain supplied by the Aczel classification theorem: continuous solutions are smooth, after which the calibrated ODE kernel $H''=H$ follows. Downstream exclusivity code can depend on this kernel without touching the raw Aczel axiom directly. H is the shifted cost $H(x) = J(x) + 1 = ½(x + x^{-1})$, under which the Recognition Composition Law becomes the standard d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The AczelSmoothnessPackage class encodes the requirement that any continuous solution of $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$ is $C^∞$, citing Aczél 1966 Ch. 3. The upstream aczelRegularityKernel constructs the default kernel carrying both the smooth and ode fields.
proof idea
The proof is the term (aczelRegularityKernel H).smooth. It is a one-line wrapper that projects the smooth field of the AczelRegularityKernel instance built under the AczelSmoothnessPackage.
why it matters
This theorem supplies the smoothness projection inside the Aczel Classification Package, letting the d'Alembert forcing chain advance to the ODE kernel while hiding the Aczel axiom. It closes the continuous-to-smooth step that follows from the Recognition Composition Law and the H definition in CostAlgebra, supporting the T5 J-uniqueness and T6 phi fixed-point stages of the unified forcing chain. No downstream uses are recorded yet, but the module doc states it is intended for exclusivity code.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.