cos_satisfies_regularity
plain-language theorem explainer
Cosine satisfies the standard regularity bundle for the angle branch of the d'Alembert functional equation. Researchers establishing uniqueness of angle coupling functions in Recognition Science cite this when closing the cos solution path. The proof assembles five pre-established component theorems into the AngleStandardRegularity structure via a direct term construction.
Claim. The function $H=cos$ satisfies the standard regularity bundle: it is smooth, converts the d'Alembert equation into the ODE $H''=-H$, and meets the continuity, differentiability, and bootstrap hypotheses required by Aczél theory under the calibration $H''(0)=-1$.
background
AngleStandardRegularity packages the Aczél theory hypotheses for the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with negative curvature. The structure requires smoothness (continuous implies $C^∞$), conversion to the ODE $H''=-H$, plus continuity, differentiability, and linear regularity bootstrap conditions. This module develops the cosine branch parallel to the cosh branch in the Cost module, with axioms Aθ1–Aθ4 specifying the functional equation, regularity, normalization $H(0)=1$, and calibration $H''(0)=-1$ that selects cosine.
proof idea
The proof is a term-mode construction of the AngleStandardRegularity structure. It directly supplies the five fields: smooth from cos_dAlembert_smooth, ode from cos_dAlembert_to_ODE, cont from cos_satisfies_continuous_neg, diff from cos_satisfies_differentiable_neg, and boot from cos_satisfies_bootstrap_neg.
why it matters
This result closes the regularity verification for the cosine solution, enabling the master theorem THEOREM_angle_coupling_rigidity that packages Aθ1–Aθ4 to conclude $H=cos$. It parallels the cosh uniqueness in the cost functional and supports the angle T5 step in the forcing chain, where negative curvature selects the trigonometric solution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.