cos_satisfies_bootstrap_neg
plain-language theorem explainer
Cosine satisfies the ODE regularity bootstrap hypothesis for the negative curvature case. Analysts working on d'Alembert functional equations in the Recognition Science angle branch would cite this when closing the smoothness gap for uniqueness proofs. The proof reduces directly to the established infinite differentiability of the cosine function.
Claim. Let $H = cos$. If $H''(t) = -H(t)$ holds pointwise for all $t$, then the assumptions that $H$ is continuous and differentiable on the reals imply that $H$ is twice continuously 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)$, with calibration $H''(0) = -1$ selecting the cosine solution over the cosh branch used for the cost functional J. The key definition is the regularity bootstrap hypothesis: for a function satisfying the linear ODE $f'' = -f$, continuity and differentiability imply $C^2$ smoothness. This mirrors the positive curvature case in the Cost.FunctionalEquation module but with opposite sign for the angle coupling. Upstream results include the definition of the bootstrap hypothesis itself.
proof idea
The proof is a one-line wrapper that applies the known result Real.contDiff_cos after introducing the three hypotheses of the bootstrap predicate.
why it matters
This result closes the regularity step in the cosine uniqueness chain, feeding directly into cos_satisfies_regularity which packages the full AngleStandardRegularity. It supports the angle T5 theorem by confirming that cosine meets the smoothness required by Aθ2. In the broader framework, it parallels the J-uniqueness for the cost functional but selects the negative curvature branch, consistent with the eight-tick octave and D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.