aczel_kernel_smooth
plain-language theorem explainer
Under the Aczel smoothness package the shifted cost function H satisfies the implication that every continuous solution of the d'Alembert equation is infinitely differentiable. Recognition Science cost theorists cite this projection when they need smoothness for the kernel without invoking the full Aczel classification. The proof extracts the smoothness field directly from the regularity kernel construction.
Claim. Assuming the Aczel smoothness package, for any function $H : ℝ → ℝ$, if $H(0) = 1$, $H$ is continuous, and $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, then $H$ is infinitely differentiable.
background
The module packages the smoothness part of the d'Alembert forcing chain supplied by the Aczel classification theorem. The shifted cost is defined by $H(x) = J(x) + 1$, which converts the Recognition Composition Law into 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 infinitely differentiable, citing Aczel 1966.
proof idea
The proof is a one-line term that constructs the aczelRegularityKernel for the given H and projects its smooth field.
why it matters
This declaration supplies the smoothness projection required by the Aczel classification package in the cost module. It allows downstream code to depend on the calibrated ODE kernel without direct reference to the raw Aczel axiom. It closes the first step of the d'Alembert forcing chain within Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.