ode_regularity_differentiable_hypothesis_neg
plain-language theorem explainer
The definition packages the regularity hypothesis that any continuous real-valued function obeying the ODE H''(t) = -H(t) for all t is differentiable. Researchers proving uniqueness for cosine solutions to the d'Alembert equation in angle coupling cite it when assembling smoothness assumptions. It is realized as a direct implication that takes the ODE and continuity as premises and concludes differentiability over the reals.
Claim. For a map $H : ℝ → ℝ$, if $H$ satisfies $H''(t) = -H(t)$ for every real $t$ and $H$ is continuous, then $H$ is differentiable on $ℝ$.
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 as the unique angle coupling function. This mirrors the cosh branch for the cost functional but with opposite curvature sign. The upstream reparametrization $H(x) = J(x) + 1$ converts the Recognition Composition Law into standard d'Alembert form, and the same $H$ is reused here for the negative-curvature case.
proof idea
The declaration is a direct definition of the implication (ODE holds and continuous) implies differentiable. It applies no lemmas and serves as a named interface for the differentiability step in the regularity bootstrap.
why it matters
This hypothesis is assembled into the AngleStandardRegularity structure that packages the Aczél-type assumptions for angle coupling. It supports the theorems dAlembert_cos_solution and ode_cos_uniqueness, which conclude that the unique solution is the cosine. In the Recognition Science framework it closes the Angle T5 step of the forcing chain, where the negative calibration forces the cosine solution parallel to the positive case for the cost J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.