AczelSmoothnessPackage
plain-language theorem explainer
The AczelSmoothnessPackage class encodes the assumption that every continuous solution H to the d'Alembert equation with H(0)=1 is infinitely differentiable. It is cited by classification and uniqueness results that convert the Recognition Composition Law into the J-cost. The declaration is a typeclass definition with no proof body; a concrete instance is supplied separately by dAlembert_contDiff_top.
Claim. Any continuous function $H : ℝ → ℝ$ satisfying $H(0) = 1$ and the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$ is infinitely differentiable.
background
In the cost algebra the shifted function is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$. Under this change of variable the Recognition Composition Law becomes the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The module declares a typeclass interface that packages the smoothness claim for continuous solutions of this equation; the concrete realization lives in AczelProof and is decoupled from the hypothesis carrier as noted in the module documentation.
proof idea
This is a typeclass definition containing no proof. The single field smooth_of_dAlembert is applied directly by the one-line wrapper aczel_dAlembert_smooth. The actual smoothness statement is discharged unconditionally in dAlembert_contDiff_top by case analysis on the three families of solutions furnished by the d'Alembert classification.
why it matters
The package supplies the regularity kernel used by aczelRegularityKernel, aczel_kernel_smooth and primitive_to_uniqueness_aczel to obtain the T5 uniqueness result that any primitive cost equals the J-cost. It thereby closes the regularity step between the functional equation and the phi-ladder mass formula, consistent with the eight-tick octave and the emergence of D=3. The module documentation records that the class was split from the public-release AczelTheorem to keep the unconditional proof independent of the parameterized uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.