aczel_kernel_smooth
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.
claimAssuming 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 in Recognition Science
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.
scope and limits
- Does not establish the existence of non-constant solutions.
- Does not derive the ODE property H'' = H.
- Does not apply to discontinuous solutions.
- Relies on the external Aczel smoothness package as an assumption.
formal statement (Lean)
38theorem aczel_kernel_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ) :
39 dAlembert_continuous_implies_smooth_hypothesis H :=
proof body
Term-mode proof.
40 (aczelRegularityKernel H).smooth
41
42/-- Convenience projection: the ODE kernel exported by the classification step. -/