aczel_dAlembert_smooth
Continuous solutions to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 are infinitely differentiable under the AczelSmoothnessPackage hypothesis. Researchers establishing uniqueness of the cost algebra or discharging the Aczél axiom in Recognition Science cite this result. The proof is a direct one-line application of the smoothness field inside the AczelSmoothnessPackage typeclass.
claimIf a function $H : ℝ → ℝ$ satisfies $H(0) = 1$, is continuous, and obeys $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, then $H$ is infinitely differentiable.
background
The d'Alembert equation is the reparametrized Recognition Composition Law under the shifted cost H(x) = J(x) + 1, where J satisfies J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y). The AczelSmoothnessPackage typeclass asserts that every continuous solution with H(0)=1 is C^∞, citing Aczél 1966 classification into the constant and cosh(λt) cases. This module isolates the smoothness interface to avoid circularity between the unconditional Aczél theorem and the parameterized uniqueness results.
proof idea
The proof is a one-line wrapper that applies AczelSmoothnessPackage.smooth_of_dAlembert to the supplied H, h_one, h_cont and h_dAlembert.
why it matters in Recognition Science
This supplies the smoothness step required by cost_algebra_unique (T5 J-uniqueness in the forcing chain) and by h_aczel_classification_proved, which eliminates the remaining foundation axiom. It is also invoked by dAlembert_cosh_solution_aczel and dAlembert_smooth_of_aczel to obtain the cosh form without extra regularity hypotheses. The declaration closes the regularity gap between the functional equation and the eight-tick octave structure.
scope and limits
- Does not establish the AczelSmoothnessPackage instance itself.
- Does not classify solutions beyond smoothness.
- Does not apply to discontinuous functions.
- Does not derive the explicit form H(t) = cosh(λ t).
- Does not extend to complex or higher-dimensional domains.
formal statement (Lean)
47theorem aczel_dAlembert_smooth [AczelSmoothnessPackage] (H : ℝ → ℝ)
48 (h_one : H 0 = 1)
49 (h_cont : Continuous H)
50 (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
51 ContDiff ℝ ⊤ H :=
proof body
Term-mode proof.
52 AczelSmoothnessPackage.smooth_of_dAlembert H h_one h_cont h_dAlembert
53
54end FunctionalEquation
55end Cost
56end IndisputableMonolith