cos_satisfies_continuous_neg
plain-language theorem explainer
Cosine satisfies the continuous regularity hypothesis for the negative-curvature ODE branch of the d'Alembert equation. Researchers assembling uniqueness proofs for angle coupling functions in Recognition Science cite this result when verifying the full regularity package. The argument is a direct one-line appeal to the standard continuity of the real cosine function.
Claim. If a function $H:ℝ→ℝ$ satisfies $H''(t)=-H(t)$ for all real $t$, then $H$ is continuous. This implication holds when $H=cos$.
background
The module develops the cosine branch of d'Alembert uniqueness for angle coupling functions. The governing equation is $H(t+u)+H(t-u)=2H(t)H(u)$, with axioms Aθ1–Aθ4 that include continuity (Aθ2) and the calibration $H''(0)=-1$ (Aθ4) selecting the cosine solution over the hyperbolic branch. The key local definition is the continuous regularity hypothesis: any solution to the ODE $H''=-H$ must be continuous. This construction mirrors the cosh branch in the cost functional equation, where positive curvature instead selects the J-cost functional.
proof idea
The proof is a term-mode one-liner. It introduces the antecedent (the ODE condition $H''=-H$) and then applies the standard theorem that the real cosine function is continuous.
why it matters
This declaration is invoked inside the parent theorem cos_satisfies_regularity to complete the AngleStandardRegularity record for cosine. It supplies the continuous leg of the angle T5 uniqueness result, where the negative curvature calibration forces the cosine solution. The module ties the result to Aczél's functional-equation theory and to the Recognition Science forcing chain for angle coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.