cos_satisfies_differentiable_neg
plain-language theorem explainer
Cosine satisfies the differentiability implication inside the negative ODE regularity hypothesis for the angle functional equation. Analysts proving uniqueness on the cosine branch of d'Alembert's equation cite this to complete the regularity bootstrap. The proof is a one-line term application of the standard result that cosine is differentiable.
Claim. The function $H(t) = cos(t)$ satisfies the property that if $H''(t) = -H(t)$ for all $t$ and $H$ is continuous, then $H$ is differentiable.
background
The module develops the cosine branch of the d'Alembert functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ under the calibration $H''(0) = -1$, which selects the cosine solution for angle coupling. The definition ode_regularity_differentiable_hypothesis_neg states that any continuous solution to the ODE $f'' = -f$ must be differentiable. This is the negative-curvature counterpart to the cosh regularity conditions in the Cost.FunctionalEquation module.
proof idea
The proof is a term-mode one-liner. It introduces the two antecedents of the implication and applies the Mathlib lemma Real.differentiable_cos.
why it matters
This result is invoked by cos_satisfies_regularity to assemble the full AngleStandardRegularity package for the cosine solution. It supports the master uniqueness theorem for angle coupling (Aθ1–Aθ4) and parallels the J-uniqueness step (T5) on the cost side of the forcing chain. The declaration closes one regularity gap in the cosine branch without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.