dAlembert_continuous_implies_smooth_hypothesis
plain-language theorem explainer
The declaration encodes Aczél's classical regularity result as a reusable hypothesis inside the T5 cost-uniqueness argument. It asserts that any real-valued H normalized at zero, continuous, and obeying the d'Alembert addition formula must be infinitely differentiable. The definition is a direct one-line interface that downstream theorems invoke to import the smoothness conclusion without repeating the functional-equation analysis.
Claim. Let $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 $C^∞$.
background
In the Recognition Science setting the cost function is shifted to H(x) = J(x) + 1, where J obeys the Recognition Composition Law. Under this reparametrization the RCL collapses to the standard d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The module supplies auxiliary statements that support the T5 uniqueness proof for any cost algebra obeying the same axioms and the calibration J''(1) = 1. Upstream CostAlgebra.H records the explicit form H(x) = ½(x + x⁻¹) that satisfies the equation when J is the canonical cost.
proof idea
The declaration is a direct definition of the proposition that encodes the implication from normalization, continuity, and the d'Alembert identity to the conclusion that H belongs to C^∞(ℝ). No tactics or lemmas are applied inside the definition itself; it simply states the classical Aczél regularity claim for later use.
why it matters
This hypothesis is invoked inside the main T5 theorem cost_algebra_unique, which asserts that any CostAlgebraData obeying the same axioms and the calibration J''(1)=1 must coincide with the canonical J. The statement directly implements the Aczél reference cited in the module documentation and closes the regularity gap needed to pass from the functional equation to the ODE H'' = H. It therefore supplies the missing analytic step between the algebraic RCL and the differential characterization of the cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.