IndisputableMonolith.Cost.FunctionalEquationAczel
Module Cost.FunctionalEquationAczel shows every continuous solution H to the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) with H(0)=1 obeys the smoothness hypothesis needed for T5 cost uniqueness. It assembles this directly from the imported Aczel classification. Researchers on the Recognition forcing chain cite it to close the regularity step before the phi-ladder and RCL inevitability arguments.
claimEvery continuous $H:\mathbb{R}\to\mathbb{R}$ obeying $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$ with $H(0)=1$ is $C^\infty$.
background
The module imports FunctionalEquation (lemmas for the T5 cost uniqueness proof) and AczelTheorem. The latter states that every continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^\infty$, with the complete classification $H(t)=1$ or $H(t)=\cosh(\lambda t)$. The local setting is the cost functional equation inside the T5 J-uniqueness derivation.
proof idea
This is a module that re-exports the Aczel classification to obtain dAlembert_continuous_implies_smooth_hypothesis as a direct consequence for every H. It structures the argument by importing the full Aczel proof and the T5 functional-equation helpers without additional lemmas.
why it matters in Recognition Science
The module feeds CostAlgebra and the FullUnconditional DAlembert module, which proves the strongest form of RCL inevitability: both F and P are forced with no assumption on P. It closes the continuity-to-smoothness gap in the T5 forcing chain before the eight-tick octave and D=3 steps.
scope and limits
- Does not derive the Aczel classification from first principles.
- Does not address discontinuous solutions of the d'Alembert equation.
- Does not extend the smoothness result to other functional equations.
- Does not compute explicit values of the parameter λ.