cosh_dAlembert_smooth
The hyperbolic cosine satisfies the smoothness hypothesis required by Aczél's theorem for continuous solutions of the d'Alembert equation. Workers on the T5 J-uniqueness proof in Recognition Science cite this result to confirm that cosh meets the continuity-to-ContDiff implication. The proof is a one-line wrapper that discharges the three antecedent hypotheses by direct appeal to the known infinite differentiability of cosh.
claim$H = {}$cosh satisfies the implication $H(0)=1 {}$and continuous $H$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$ imply $H$ is $C^infty$ on $mathbb{R}$.
background
The module supplies helper lemmas for the T5 cost uniqueness proof. The upstream definition dAlembert_continuous_implies_smooth_hypothesis encodes the classical implication that any $H:mathbb{R}to mathbb{R}$ obeying $H(0)=1$, continuity, and the d'Alembert relation $H(t+u)+H(t-u)=2H(t)H(u)$ must be infinitely differentiable. Aczél's theorem states that continuous solutions are analytic and of the form cosh(λx) for some real λ.
proof idea
The proof is a one-line wrapper that applies Real.contDiff_cosh after introducing the three antecedent hypotheses.
why it matters in Recognition Science
The declaration supports the T5 J-uniqueness step by verifying that cosh satisfies the smoothness requirement extracted from Aczél's theorem. It contributes to showing that the J-cost function is the unique solution to the Recognition Composition Law in the Recognition framework. No downstream uses are recorded yet.
scope and limits
- Does not prove the full Aczél theorem for arbitrary continuous solutions.
- Does not derive the explicit form cosh(λx) or the value of λ.
- Does not connect to the phi-ladder, mass formulas, or spatial dimension forcing.
formal statement (Lean)
540theorem cosh_dAlembert_smooth : dAlembert_continuous_implies_smooth_hypothesis Real.cosh := by
proof body
Term-mode proof.
541 intro _ _ _
542 exact Real.contDiff_cosh
543
544/-- cosh satisfies the d'Alembert to ODE hypothesis. -/