dAlembert_continuous_implies_smooth_hypothesis_neg
plain-language theorem explainer
The declaration defines the proposition that any function H from reals to reals with H(0)=1, continuous, and obeying the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) must be infinitely differentiable. Researchers packaging regularity axioms for the cosine branch of angle coupling in Recognition Science cite it when assembling the Aθ1–Aθ4 bundle. It is a direct one-line packaging of the Aczél analyticity result applied to the negative-calibration case.
Claim. If a function $H:ℝ→ℝ$ satisfies $H(0)=1$, is continuous, and obeys the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, then $H$ is infinitely differentiable.
background
The module develops the cosine branch of the angle functional equation, mirroring the cosh branch in Cost.FunctionalEquation. Axiom Aθ1 is the d'Alembert relation; Aθ2 requires continuity, which this definition converts into infinite differentiability. The negative calibration H''(0)=-1 selects the cos solutions, in contrast to the positive calibration that yields the shifted cost H(x)=J(x)+1 from CostAlgebra.
proof idea
One-line definition that packages the implication from continuity plus the d'Alembert equation to ContDiff ℝ ⊤ H, importing the Aczél smoothness result already established for the parallel cosh case in Cost.AczelTheorem and Cost.AczelProof.
why it matters
Supplies the smoothness field inside the AngleStandardRegularity structure that feeds dAlembert_cos_solution, the Angle T5 theorem. It closes the regularity step in the forcing chain for angle coupling, parallel to T5 J-uniqueness on the cost side, and rests on the Aczél reference cited in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.