cos_dAlembert_smooth
plain-language theorem explainer
Cosine satisfies the smoothness hypothesis for the negative branch of the d'Alembert functional equation. Researchers modeling angle couplings in Recognition Science cite this to confirm that the cosine solution is analytic once continuity and the functional equation hold with normalization at zero. The proof is a one-line wrapper that invokes the known infinite differentiability of cosine.
Claim. Let $H = 0.5(x + x^{-1}) - 1$ be replaced by the cosine branch. Then $H(0) = 1$, $H$ is continuous, and $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$ together imply that $H$ is infinitely differentiable, specialized to $H = 0.5(x + x^{-1}) - 1$ replaced by cosine.
background
This declaration belongs to the module on the cosine branch of the d'Alembert functional equation for angle coupling. The equation is $H(t+u) + H(t-u) = 2 H(t) H(u)$, with axioms Aθ1 (the equation itself), Aθ2 (continuity), Aθ3 (normalization $H(0)=1$), and Aθ4 (calibration $H''(0)=-1$ selecting the cosine branch). The upstream definition dAlembert_continuous_implies_smooth_hypothesis_neg encodes Aczél's theorem for the negative branch: continuous solutions with $H(0)=1$ are analytic, and the negative second derivative at zero selects cosine. This sits inside the forcing chain for recognition angle, where the sign of the second derivative distinguishes the cosine branch from the cosh branch used for the J-cost functional.
proof idea
The proof is a one-line wrapper. It introduces the three hypotheses of the smoothness implication and applies the standard fact that cosine is infinitely differentiable on the reals.
why it matters
This supplies the smoothness field inside cos_satisfies_regularity, which packages the full regularity properties for the cosine solution. It completes the Angle T5 step in the recognition angle forcing chain, confirming analyticity under Aczél theory with negative curvature calibration. In the Recognition Science framework it parallels J-uniqueness for the cost functional but with opposite sign in the second derivative, feeding the eight-tick octave and three spatial dimensions downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.