dAlembert_contDiff_top
plain-language theorem explainer
Continuous solutions of the d'Alembert functional equation with H(0)=1 are infinitely differentiable. Recognition Science researchers deriving properties of the shifted cost function and analysts working on functional equations would cite this result. The proof performs case analysis on the classification lemma, then reduces each explicit form (constant, cosh, cos) to known differentiability facts for elementary functions.
Claim. Any continuous function $H : ℝ → ℝ$ satisfying $H(0) = 1$ and $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$ is infinitely differentiable, i.e., of class $C^∞$.
background
In the Recognition Science cost algebra the shifted cost is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$. Under this change of variable the Recognition Composition Law becomes exactly the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The present theorem therefore supplies the smoothness statement needed for the cost function on the reals.
proof idea
The proof performs case analysis via rcases on the upstream classification theorem dAlembert_classification. The constant case rewrites H to the constant function and applies contDiff_const. The remaining cases rewrite H as cosh(α t) or cos(α t) and compose the known contDiff_cosh or contDiff_cos lemmas with the linear map t ↦ α t.
why it matters
This theorem supplies the smoothness direction of the Aczél classification and is invoked directly by h_aczel_classification_proved, which states that H_AczelClassification holds unconditionally and thereby eliminates the sole remaining foundation axiom. It confirms that the shifted cost H is C^∞, aligning with the analyticity expected from J-uniqueness (T5) and the phi-ladder. The result also populates the AczelSmoothnessPackage instance required by the cost-algebra development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.